English
The maximal atlas associated to a charted space and a structure groupoid consists of exactly those charts whose coordinate change with any atlas member lies in the groupoid.
Русский
Максимальный атлас, связанный с чартизованным пространством и группоидом, состоит ровно из карт, чьи переходы с любой картой атласа лежат в группoidе.
LaTeX
$$$\text{maximalAtlas} = \{ e \mid \forall e' \in atlas, e.symm ≫ₕ e' \in G \land e'.symm ≫ₕ e \in G \}$$$
Lean4
/-- Given a charted space admitting a structure groupoid, the maximal atlas associated to this
structure groupoid is the set of all charts that are compatible with the atlas, i.e., such
that changing coordinates with an atlas member gives an element of the groupoid. -/
def maximalAtlas : Set (OpenPartialHomeomorph M H) :=
{e | ∀ e' ∈ atlas H M, e.symm ≫ₕ e' ∈ G ∧ e'.symm ≫ₕ e ∈ G}
