top_coe — Mathlib

English

The top affine subspace, viewed as a set, is the entire set of points.

Русский

Верхнее аффинное подпространство, рассматриваемое как множество, содержит все точки.

LaTeX

$$$((\\top : \\text{AffineSubspace}(k,P)) :\\ Set P) = \\mathrm{Set.univ}$$$

Lean4

/-- `⊤`, coerced to a set, is the whole set of points. -/
@[simp]
theorem top_coe : ((⊤ : AffineSubspace k P) : Set P) = Set.univ :=
  rfl

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