mem_maximalAtlas_of_mem_groupoid — Mathlib

English

Every element f of the structure groupoid G lies in its maximal atlas on H.

Русский

Каждый элемент f группоида структуры G принадлежит своему максимальному атласу на H.

LaTeX

$$f \in G.maximalAtlas H$$

Lean4

/-- In the model space, any element of the groupoid is in the maximal atlas. -/
theorem mem_maximalAtlas_of_mem_groupoid {f : OpenPartialHomeomorph H H} (hf : f ∈ G) : f ∈ G.maximalAtlas H :=
  by
  rintro e (rfl : e = OpenPartialHomeomorph.refl H)
  exact ⟨G.trans (G.symm hf) G.id_mem, G.trans (G.symm G.id_mem) hf⟩

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