case h_open
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : QuotientMap π
h : IsOpenMap π
⊢ ∀ (u : Set Y), u ∈ image π '' V → IsOpen u

case h_nhds
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : QuotientMap π
h : IsOpenMap π
⊢ ∀ (a : Y) (u : Set Y), a ∈ u → IsOpen u → ∃ v, v ∈ image π '' V ∧ a ∈ v ∧ v ⊆ u
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : QuotientMap π
h : IsOpenMap π
⊢ IsTopologicalBasis (image π '' V)
apply isTopologicalBasis_of_open_of_nhds
case h_open.intro.intro
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : QuotientMap π
h : IsOpenMap π
U : Set X
U_in_V : U ∈ V
⊢ IsOpen (π '' U)
case h_open
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : QuotientMap π
h : IsOpenMap π
⊢ ∀ (u : Set Y), u ∈ image π '' V → IsOpen u
rintro - ⟨U, U_in_V, rfl⟩
no goals
case h_open.intro.intro
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : QuotientMap π
h : IsOpenMap π
U : Set X
U_in_V : U ∈ V
⊢ IsOpen (π '' U)
apply h U (hV.isOpen U_in_V)
case h_nhds
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : QuotientMap π
h : IsOpenMap π
y : Y
U : Set Y
y_in_U : y ∈ U
U_open : IsOpen U
⊢ ∃ v, v ∈ image π '' V ∧ y ∈ v ∧ v ⊆ U
case h_nhds
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : QuotientMap π
h : IsOpenMap π
⊢ ∀ (a : Y) (u : Set Y), a ∈ u → IsOpen u → ∃ v, v ∈ image π '' V ∧ a ∈ v ∧ v ⊆ u
intro y U y_in_U U_open
case h_nhds.intro
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : QuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen U
x : X
y_in_U : π x ∈ U
⊢ ∃ v, v ∈ image π '' V ∧ π x ∈ v ∧ v ⊆ U
case h_nhds
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : QuotientMap π
h : IsOpenMap π
y : Y
U : Set Y
y_in_U : y ∈ U
U_open : IsOpen U
⊢ ∃ v, v ∈ image π '' V ∧ y ∈ v ∧ v ⊆ U
obtain ⟨x, rfl⟩ := h'.surjective y
case h_nhds.intro
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : QuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
⊢ ∃ v, v ∈ image π '' V ∧ π x ∈ v ∧ v ⊆ U
case h_nhds.intro
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : QuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen U
x : X
y_in_U : π x ∈ U
⊢ ∃ v, v ∈ image π '' V ∧ π x ∈ v ∧ v ⊆ U
let W := π ⁻¹' U
case h_nhds.intro
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : QuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
x_in_W : x ∈ W
⊢ ∃ v, v ∈ image π '' V ∧ π x ∈ v ∧ v ⊆ U
case h_nhds.intro
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : QuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
⊢ ∃ v, v ∈ image π '' V ∧ π x ∈ v ∧ v ⊆ U
have x_in_W : x ∈ W := y_in_U
case h_nhds.intro
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : QuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
x_in_W : x ∈ W
W_open : IsOpen W
⊢ ∃ v, v ∈ image π '' V ∧ π x ∈ v ∧ v ⊆ U
case h_nhds.intro
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : QuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
x_in_W : x ∈ W
⊢ ∃ v, v ∈ image π '' V ∧ π x ∈ v ∧ v ⊆ U
have W_open : IsOpen W := U_open.preimage h'.continuous
case h_nhds.intro.intro.intro.intro
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : QuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
x_in_W : x ∈ W
W_open : IsOpen W
Z : Set X
Z_in_V : Z ∈ V
x_in_Z : x ∈ Z
Z_in_W : Z ⊆ W
⊢ ∃ v, v ∈ image π '' V ∧ π x ∈ v ∧ v ⊆ U
case h_nhds.intro
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : QuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
x_in_W : x ∈ W
W_open : IsOpen W
⊢ ∃ v, v ∈ image π '' V ∧ π x ∈ v ∧ v ⊆ U
obtain ⟨Z, Z_in_V, x_in_Z, Z_in_W⟩ := hV.exists_subset_of_mem_open x_in_W W_open
case h_nhds.intro.intro.intro.intro
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : QuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
x_in_W : x ∈ W
W_open : IsOpen W
Z : Set X
Z_in_V : Z ∈ V
x_in_Z : x ∈ Z
Z_in_W : Z ⊆ W
πZ_in_U : π '' Z ⊆ U
⊢ ∃ v, v ∈ image π '' V ∧ π x ∈ v ∧ v ⊆ U
case h_nhds.intro.intro.intro.intro
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : QuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
x_in_W : x ∈ W
W_open : IsOpen W
Z : Set X
Z_in_V : Z ∈ V
x_in_Z : x ∈ Z
Z_in_W : Z ⊆ W
⊢ ∃ v, v ∈ image π '' V ∧ π x ∈ v ∧ v ⊆ U
have πZ_in_U : π '' Z ⊆ U := (Set.image_subset _ Z_in_W).trans (image_preimage_subset π U)
no goals
case h_nhds.intro.intro.intro.intro
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : QuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
x_in_W : x ∈ W
W_open : IsOpen W
Z : Set X
Z_in_V : Z ∈ V
x_in_Z : x ∈ Z
Z_in_W : Z ⊆ W
πZ_in_U : π '' Z ⊆ U
⊢ ∃ v, v ∈ image π '' V ∧ π x ∈ v ∧ v ⊆ U
exact ⟨π '' Z, ⟨Z, Z_in_V, rfl⟩, ⟨x, x_in_Z, rfl⟩, πZ_in_U⟩