[GOAL]
X : Type u_1
t : TopologicalSpace X
⊢ t = ⨅ (u : Opens X), induced (fun x => x ∈ u) sierpinskiSpace
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
X : Type u_1
t : TopologicalSpace X
⊢ t ≤ ⨅ (u : Opens X), induced (fun x => x ∈ u) sierpinskiSpace
[PROOFSTEP]
rw [le_iInf_iff]
[GOAL]
case a
X : Type u_1
t : TopologicalSpace X
⊢ ∀ (i : Opens X), t ≤ induced (fun x => x ∈ i) sierpinskiSpace
[PROOFSTEP]
exact fun u => Continuous.le_induced (isOpen_iff_continuous_mem.mp u.2)
[GOAL]
case a
X : Type u_1
t : TopologicalSpace X
⊢ ⨅ (u : Opens X), induced (fun x => x ∈ u) sierpinskiSpace ≤ t
[PROOFSTEP]
intro u h
[GOAL]
case a
X : Type u_1
t : TopologicalSpace X
u : Set X
h : IsOpen u
⊢ IsOpen u
[PROOFSTEP]
rw [← generateFrom_iUnion_isOpen]
[GOAL]
case a
X : Type u_1
t : TopologicalSpace X
u : Set X
h : IsOpen u
⊢ IsOpen u
[PROOFSTEP]
apply isOpen_generateFrom_of_mem
[GOAL]
case a.hs
X : Type u_1
t : TopologicalSpace X
u : Set X
h : IsOpen u
⊢ u ∈ ⋃ (i : Opens X), {s | IsOpen s}
[PROOFSTEP]
simp only [Set.mem_iUnion, Set.mem_setOf_eq, isOpen_induced_iff]
[GOAL]
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
[PROOFSTEP]
exact ⟨⟨u, h⟩, { True }, isOpen_singleton_true, by simp [Set.preimage]⟩
[GOAL]
X : Type u_1
t : TopologicalSpace X
u : Set X
h : IsOpen u
⊢ (fun x => x ∈ { carrier := u, is_open' := h }) ⁻¹' {True} = u
[PROOFSTEP]
simp [Set.preimage]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
⊢ Inducing ↑(productOfMemOpens X)
[PROOFSTEP]
convert inducing_iInf_to_pi fun (u : Opens X) (x : X) => x ∈ u
[GOAL]
case h.e'_3
X : Type u_1
inst✝ : TopologicalSpace X
⊢ inst✝ = ⨅ (i : Opens X), induced (fun x => x ∈ i) inferInstance
[PROOFSTEP]
apply eq_induced_by_maps_to_sierpinski
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
⊢ Function.Injective ↑(productOfMemOpens X)
[PROOFSTEP]
intro x1 x2 h
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
x1 x2 : X
h : ↑(productOfMemOpens X) x1 = ↑(productOfMemOpens X) x2
⊢ x1 = x2
[PROOFSTEP]
apply Inseparable.eq
[GOAL]
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
x1 x2 : X
h : ↑(productOfMemOpens X) x1 = ↑(productOfMemOpens X) x2
⊢ Inseparable x1 x2
[PROOFSTEP]
rw [← Inducing.inseparable_iff (productOfMemOpens_inducing X), h]
