subtypeEq' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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