English
An empty type M is compatible with any charted space H -> M, via an empty atlas.
Русский
Пусть M пустое; тогда существует структура ChartedSpace H M с пустым атласом.
LaTeX
$$def empty (H) (M) : ChartedSpace H M$$
Lean4
/-- A charted space over a discrete space is discrete. -/
theorem discreteTopology [DiscreteTopology H] : DiscreteTopology M :=
by
apply discreteTopology_iff_isOpen_singleton.2 (fun x ↦ ?_)
have : IsOpen ((chartAt H x).source ∩ (chartAt H x) ⁻¹' {chartAt H x x}) :=
isOpen_inter_preimage _ (isOpen_discrete _)
convert this
refine Subset.antisymm (by simp) ?_
simp only [subset_singleton_iff, mem_inter_iff, mem_preimage, mem_singleton_iff, and_imp]
intro y hy h'y
exact (chartAt H x).injOn hy (mem_chart_source _ x) h'y
