mem_maximalAtlas_iff — Mathlib

English

For any e : OpenPartialHomeomorph M H, membership in the maximal atlas is equivalent to a universal property over atlas elements.

Русский

Для любого e: OpenPartialHomeomorph M H, принадлежность к максимальному атласу эквивалентна универсальному свойству по элементам атласа.

LaTeX

$$$e \in G.maximalAtlas M \iff \forall e' \in atlas H M, \; e.symm ≫ₕ e' \in G \land e'.symm ≫ₕ e \in G$$$

Lean4

theorem mem_maximalAtlas_iff {e : OpenPartialHomeomorph M H} :
    e ∈ G.maximalAtlas M ↔ ∀ e' ∈ atlas H M, e.symm ≫ₕ e' ∈ G ∧ e'.symm ≫ₕ e ∈ G :=
  Iff.rfl

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