coe_affineSpan_singleton — Mathlib

English

The top affine subspace is affinely equivalent to the ambient space P; i.e., there exists an affine equivalence between ⊤ and P.

Русский

Верхнее аффинное подпространство аффинно эквивалентно окружению пространства P; существует аффинное эквивалентное отображение между ⊤ и P.

LaTeX

$$$ (\\\\top : AffineSubspace k P) \\\\cong^{affine}_k P $$$

Lean4

/-- The affine span of a single point, coerced to a set, contains just that point. -/
@[simp high] -- This needs to take priority over `coe_affineSpan`

theorem coe_affineSpan_singleton (p : P) : (affineSpan k ({ p } : Set P) : Set P) = { p } :=
  by
  ext x
  rw [mem_coe, ← vsub_right_mem_direction_iff_mem (mem_affineSpan k (Set.mem_singleton p)) _, direction_affineSpan]
  simp

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