case h.e'_3
X : Type u_1
inst✝ : TopologicalSpace X
⊢ inst✝ = ⨅ (i : Opens X), induced (fun x => x ∈ i) inferInstance
X : Type u_1
inst✝ : TopologicalSpace X
⊢ Inducing ↑(productOfMemOpens X)
convert inducing_iInf_to_pi fun (u : Opens X) (x : X) => x ∈ u
no goals
case h.e'_3
X : Type u_1
inst✝ : TopologicalSpace X
⊢ inst✝ = ⨅ (i : Opens X), induced (fun x => x ∈ i) inferInstance
apply eq_induced_by_maps_to_sierpinski