case a
X : Type u_1
t : TopologicalSpace X
⊢ t ≤ ⨅ (u : Opens X), induced (fun x => x ∈ u) sierpinskiSpace

case a
X : Type u_1
t : TopologicalSpace X
⊢ (⨅ (u : Opens X), induced (fun x => x ∈ u) sierpinskiSpace) ≤ t
X : Type u_1
t : TopologicalSpace X
⊢ t = ⨅ (u : Opens X), induced (fun x => x ∈ u) sierpinskiSpace
apply le_antisymm
case a
X : Type u_1
t : TopologicalSpace X
⊢ ∀ (i : Opens X), t ≤ induced (fun x => x ∈ i) sierpinskiSpace
case a
X : Type u_1
t : TopologicalSpace X
⊢ t ≤ ⨅ (u : Opens X), induced (fun x => x ∈ u) sierpinskiSpace
rw [le_iInf_iff]
no goals
case a
X : Type u_1
t : TopologicalSpace X
⊢ ∀ (i : Opens X), t ≤ induced (fun x => x ∈ i) sierpinskiSpace
exact fun u => Continuous.le_induced (isOpen_iff_continuous_mem.mp u.2)
case a
X : Type u_1
t : TopologicalSpace X
u : Set X
h : IsOpen u
⊢ IsOpen u
case a
X : Type u_1
t : TopologicalSpace X
⊢ (⨅ (u : Opens X), induced (fun x => x ∈ u) sierpinskiSpace) ≤ t
intro u h
case a
X : Type u_1
t : TopologicalSpace X
u : Set X
h : IsOpen u
⊢ IsOpen u
case a
X : Type u_1
t : TopologicalSpace X
u : Set X
h : IsOpen u
⊢ IsOpen u
rw [← generateFrom_iUnion_isOpen]
case a.hs
X : Type u_1
t : TopologicalSpace X
u : Set X
h : IsOpen u
⊢ u ∈ ⋃ (i : Opens X), {s | IsOpen s}
case a
X : Type u_1
t : TopologicalSpace X
u : Set X
h : IsOpen u
⊢ IsOpen u
apply isOpen_generateFrom_of_mem
case a.hs
X : Type u_1
t : TopologicalSpace X
u : Set X
h : IsOpen u
⊢ ∃ i t_1, IsOpen t_1 ∧ (fun x => x ∈ i) ⁻¹' t_1 = u
case a.hs
X : Type u_1
t : TopologicalSpace X
u : Set X
h : IsOpen u
⊢ u ∈ ⋃ (i : Opens X), {s | IsOpen s}
simp only [Set.mem_iUnion, Set.mem_setOf_eq, isOpen_induced_iff]
no goals
case a.hs
X : Type u_1
t : TopologicalSpace X
u : Set X
h : IsOpen u
⊢ ∃ i t_1, IsOpen t_1 ∧ (fun x => x ∈ i) ⁻¹' t_1 = u
exact ⟨⟨u, h⟩, {True}, isOpen_singleton_true, by simp [Set.preimage]⟩
no goals
X : Type u_1
t : TopologicalSpace X
u : Set X
h : IsOpen u
⊢ (fun x => x ∈ { carrier := u, is_open' := h }) ⁻¹' {True} = u
simp [Set.preimage]