English
The infimum of a family of R1 topologies on X is again an R1 space.
Русский
На множестве X наименьшее верхнеуровневое (inf) множество топологий, каждое из которых является R1-пространством, образует R1-пространство.
LaTeX
$$R1Space(sInf T)$$
Lean4
protected theorem sInf {X : Type*} {T : Set (TopologicalSpace X)} (hT : ∀ t ∈ T, @R1Space X t) : @R1Space X (sInf T) :=
by
let _ := sInf T
refine ⟨fun x y ↦ ?_⟩
simp only [Specializes, nhds_sInf]
rcases em (∃ t ∈ T, Disjoint (@nhds X t x) (@nhds X t y)) with ⟨t, htT, htd⟩ | hTd
· exact .inr <| htd.mono (iInf₂_le t htT) (iInf₂_le t htT)
· push_neg at hTd
exact .inl <| iInf₂_mono fun t ht ↦ ((hT t ht).1 x y).resolve_right (hTd t ht)
