English
For any chart e in the atlas, the target of e is open in the topology generated by the atlas.
Русский
Для любого чартe e из атласа область значения e является открытой в топологии, порождаемой атласом.
LaTeX
$$$\forall e\in c.atlas,\; IsOpen\; e.target$ in $c.toTopologicalSpace$.$$
Lean4
theorem open_target (he : e ∈ c.atlas) : IsOpen e.target :=
by
have E : e.target ∩ e.symm ⁻¹' e.source = e.target :=
Subset.antisymm inter_subset_left fun x hx ↦ ⟨hx, PartialEquiv.target_subset_preimage_source _ hx⟩
simpa [PartialEquiv.trans_source, E] using c.open_source e e he he