liftProp_id — Mathlib

English

Let G be a structure groupoid with a local invariant property Q. If Q holds for the identity transformation on the model space (with universes taken as unbounded), then the lift property holds for the identity map on M.

Русский

Пусть G — структура-группоида с локальной инвариантной свойством Q. Если для всех y выполняется Q(id_H, univ, y), то свойство подстановки (lift) выполняется для тождественного отображения на M.

LaTeX

$$$ \text{If } G \text{ has LocalInvariantProp } G \; Q \text{ and } \forall y,\ Q(\mathrm{id}, \mathrm{univ}, y), \text{ then } \ LiftProp(Q, \mathrm{id}_M). $$$

Lean4

theorem liftProp_id (hG : G.LocalInvariantProp G Q) (hQ : ∀ y, Q id univ y) : LiftProp Q (id : M → M) :=
  by
  simp_rw [liftProp_iff, continuous_id, true_and]
  exact fun x ↦ hG.congr' ((chartAt H x).eventually_right_inverse <| mem_chart_target H x) (hQ _)

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