coe_subtypeA — Mathlib

English

For an affine subspace s with a nonempty witness, the restriction map from s to the ambient space equals the standard projection.

Русский

Для аффинного подпространства s с непустым подвидом ограничение из s в окружающее пространство равно стандартной проекции.

LaTeX

$$coe_subtypeA(s) = Subtype.val$$

Lean4

@[simp]
theorem coe_subtypeA (s : AffineSubspace R P) [Nonempty s] : ⇑s.subtypeA = Subtype.val :=
  rfl

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