English
A charted space over a T1 space is itself a T1 space.
Русский
Пространство с атласом над T1-пространством само является T1.
LaTeX
$$[T1Space H] => [T1Space M]$$
Lean4
/-- A charted space over a T1 space is T1. Note that this is *not* true for T2 (for instance for
the real line with a double origin). -/
theorem t1Space [T1Space H] : T1Space M :=
by
apply t1Space_iff_exists_open.2 (fun x y hxy ↦ ?_)
by_cases hy : y ∈ (chartAt H x).source
· refine ⟨(chartAt H x).source ∩ (chartAt H x) ⁻¹' ({chartAt H x y}ᶜ), ?_, ?_, by simp⟩
· exact OpenPartialHomeomorph.isOpen_inter_preimage _ isOpen_compl_singleton
· simp only [preimage_compl, mem_inter_iff, mem_chart_source, mem_compl_iff, mem_preimage, mem_singleton_iff,
true_and]
exact (chartAt H x).injOn.ne (ChartedSpace.mem_chart_source x) hy hxy
· exact ⟨(chartAt H x).source, (chartAt H x).open_source, ChartedSpace.mem_chart_source x, hy⟩
