open_target — Mathlib

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

Похожие утверждения