case refine'_1
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : Inducing f
h : IsTopologicalBasis T
⊢ ∀ (u : Set α), u ∈ preimage f '' T → IsOpen u

case refine'_2
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : Inducing f
h : IsTopologicalBasis T
⊢ ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ preimage f '' T ∧ a ∈ v ∧ v ⊆ u
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : Inducing f
h : IsTopologicalBasis T
⊢ IsTopologicalBasis (preimage f '' T)
refine' isTopologicalBasis_of_open_of_nhds _ _
case refine'_1.intro.intro
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : Inducing f
h : IsTopologicalBasis T
V : Set β
hV : V ∈ T
⊢ IsOpen (f ⁻¹' V)
case refine'_1
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : Inducing f
h : IsTopologicalBasis T
⊢ ∀ (u : Set α), u ∈ preimage f '' T → IsOpen u
rintro _ ⟨V, hV, rfl⟩
case refine'_1.intro.intro
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : Inducing f
h : IsTopologicalBasis T
V : Set β
hV : V ∈ T
⊢ ∃ t, IsOpen t ∧ f ⁻¹' t = f ⁻¹' V
case refine'_1.intro.intro
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : Inducing f
h : IsTopologicalBasis T
V : Set β
hV : V ∈ T
⊢ IsOpen (f ⁻¹' V)
rw [hf.isOpen_iff]
no goals
case refine'_1.intro.intro
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : Inducing f
h : IsTopologicalBasis T
V : Set β
hV : V ∈ T
⊢ ∃ t, IsOpen t ∧ f ⁻¹' t = f ⁻¹' V
refine' ⟨V, h.isOpen hV, rfl⟩
case refine'_2
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : Inducing f
h : IsTopologicalBasis T
a : α
U : Set α
ha : a ∈ U
hU : IsOpen U
⊢ ∃ v, v ∈ preimage f '' T ∧ a ∈ v ∧ v ⊆ U
case refine'_2
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : Inducing f
h : IsTopologicalBasis T
⊢ ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ preimage f '' T ∧ a ∈ v ∧ v ⊆ u
intro a U ha hU
case refine'_2
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : Inducing f
h : IsTopologicalBasis T
a : α
U : Set α
ha : a ∈ U
hU : ∃ t, IsOpen t ∧ f ⁻¹' t = U
⊢ ∃ v, v ∈ preimage f '' T ∧ a ∈ v ∧ v ⊆ U
case refine'_2
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : Inducing f
h : IsTopologicalBasis T
a : α
U : Set α
ha : a ∈ U
hU : IsOpen U
⊢ ∃ v, v ∈ preimage f '' T ∧ a ∈ v ∧ v ⊆ U
rw [hf.isOpen_iff] at hU
case refine'_2.intro.intro
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : Inducing f
h : IsTopologicalBasis T
a : α
V : Set β
hV : IsOpen V
ha : a ∈ f ⁻¹' V
⊢ ∃ v, v ∈ preimage f '' T ∧ a ∈ v ∧ v ⊆ f ⁻¹' V
case refine'_2
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : Inducing f
h : IsTopologicalBasis T
a : α
U : Set α
ha : a ∈ U
hU : ∃ t, IsOpen t ∧ f ⁻¹' t = U
⊢ ∃ v, v ∈ preimage f '' T ∧ a ∈ v ∧ v ⊆ U
obtain ⟨V, hV, rfl⟩ := hU
case refine'_2.intro.intro.intro.intro
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : Inducing f
h : IsTopologicalBasis T
a : α
S : Set (Set β)
hS : S ⊆ T
hV : IsOpen (⋃₀ S)
ha : a ∈ f ⁻¹' ⋃₀ S
⊢ ∃ v, v ∈ preimage f '' T ∧ a ∈ v ∧ v ⊆ f ⁻¹' ⋃₀ S
case refine'_2.intro.intro
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : Inducing f
h : IsTopologicalBasis T
a : α
V : Set β
hV : IsOpen V
ha : a ∈ f ⁻¹' V
⊢ ∃ v, v ∈ preimage f '' T ∧ a ∈ v ∧ v ⊆ f ⁻¹' V
obtain ⟨S, hS, rfl⟩ := h.open_eq_sUnion hV
case refine'_2.intro.intro.intro.intro.intro.intro
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : Inducing f
h : IsTopologicalBasis T
a : α
S : Set (Set β)
hS : S ⊆ T
hV : IsOpen (⋃₀ S)
W : Set β
hW : W ∈ S
ha : f a ∈ W
⊢ ∃ v, v ∈ preimage f '' T ∧ a ∈ v ∧ v ⊆ f ⁻¹' ⋃₀ S
case refine'_2.intro.intro.intro.intro
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : Inducing f
h : IsTopologicalBasis T
a : α
S : Set (Set β)
hS : S ⊆ T
hV : IsOpen (⋃₀ S)
ha : a ∈ f ⁻¹' ⋃₀ S
⊢ ∃ v, v ∈ preimage f '' T ∧ a ∈ v ∧ v ⊆ f ⁻¹' ⋃₀ S
obtain ⟨W, hW, ha⟩ := ha
no goals
case refine'_2.intro.intro.intro.intro.intro.intro
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : Inducing f
h : IsTopologicalBasis T
a : α
S : Set (Set β)
hS : S ⊆ T
hV : IsOpen (⋃₀ S)
W : Set β
hW : W ∈ S
ha : f a ∈ W
⊢ ∃ v, v ∈ preimage f '' T ∧ a ∈ v ∧ v ⊆ f ⁻¹' ⋃₀ S
refine' ⟨f ⁻¹' W, ⟨_, hS hW, rfl⟩, ha, Set.preimage_mono <| Set.subset_sUnion_of_mem hW⟩