subtypeEq — Mathlib

English

For any y ∈ α, the subtype { x // x = y } carries a finite type structure.

Русский

Для любого y ∈ α подтип { x // x = y } имеет структуру конечного типа.

LaTeX

$$$$ \\text{For all } y \\in \\alpha, \\ Fintype\\ { x \\mid x = y } . $$$$

Lean4

/-- Short-circuit instance to decrease search for `Unique.fintype`,
since that relies on a subsingleton elimination for `Unique`. -/
instance subtypeEq (y : α) : Fintype { x // x = y } :=
  Fintype.subtype { y } (by simp)

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