topEquiv — Mathlib

English

The top affine subspace is affinely equivalent to the ambient space; this is the canonical affine correspondence between the two spaces.

Русский

Проверка: верхнее аффинное подпространство имеет аффинное соответствие с окружающим пространством.

LaTeX

$$$ topEquiv : (\\\\top : AffineSubspace k P) \\\\simeq_a_k P $$$

Lean4

/-- The top affine subspace is linearly equivalent to the affine space.
This is the affine version of `Submodule.topEquiv`. -/
@[simps! linear apply symm_apply_coe]
def topEquiv : (⊤ : AffineSubspace k P) ≃ᵃ[k] P
    where
  toEquiv := Equiv.Set.univ P
  linear := .ofEq _ _ (direction_top _ _ _) ≪≫ₗ Submodule.topEquiv
  map_vadd' _ _ := rfl

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