instSetLike — Mathlib

English

Affine subspaces form a SetLike structure with the carrier given by their point-set.

Русский

Аффинные подпространства образуют структуру SetLike, чьим носителем является множество точек.

LaTeX

$$$\\text{AffineSubspace}(k,P) \\text{ is a SetLike object with } \\mathrm{coe}(s) = s.\\text{carrier}$$$

Lean4

instance : SetLike (AffineSubspace k P) P where
  coe := carrier
  coe_injective' p q _ := by cases p; cases q; congr

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