lift_self — Mathlib

English

If proj z lies in the base set of T, then lifting z by T at the base point proj z returns z.

Русский

Если proj z лежит в базовом множестве T, то подъем z через T по базовой точке proj z возвращает z.

LaTeX

$$$$\text{If }\, proj(z)\in T.baseSet,\quad T.lift(z,\,proj(z))=z.$$$

Lean4

@[simp]
theorem lift_self (he : proj z ∈ T.baseSet) : T.lift z (proj z) = z :=
  symm_apply_mk_proj _ <| T.mem_source.2 he

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