refl — Mathlib

English

There is an identity continuous affine equivalence on any space P1, serving as the identity for the affine structure.

Русский

Для пространства P1 существует тождественное непрерывное аффинное эквивалентное отображение, выступающее в роли тождества для аффинной структуры.

LaTeX

$$$\text{refl}(k,P_1) : P_1 \simeq_A[k] P_1$$$

Lean4

/-- Identity map as a `ContinuousAffineEquiv`. -/
def refl : P₁ ≃ᴬ[k] P₁ where
  toEquiv := Equiv.refl P₁
  linear := LinearEquiv.refl k V₁
  map_vadd' _ _ := rfl

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