open_source' — Mathlib

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]

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