English
For any chart e in the atlas, the source of e is open in the topology generated from the atlas.
Русский
Для любого чартe e из атласа область определения e является открытой в топологии, порождаемой атласом.
LaTeX
$$$\forall e\in c.atlas,\; IsOpen\; e.source$ in $c.toTopologicalSpace$.$$
Lean4
theorem open_source' (he : e ∈ c.atlas) : IsOpen[c.toTopologicalSpace] e.source :=
by
apply TopologicalSpace.GenerateOpen.basic
simp only [exists_prop, mem_iUnion, mem_singleton_iff]
refine ⟨e, he, univ, isOpen_univ, ?_⟩
simp only [Set.univ_inter, Set.preimage_univ]