fintypeOffDiag — Mathlib

English

If α is a finite type and s ⊆ α with a finite domain, then the off-diagonal set s.offDiag is finite (under DecidableEq).

Русский

Если α конечно и s ⊆ α конечна, то s.offDiag конечно (при DecidableEq α).

LaTeX

$$$ [\\text{DecidableEq } \\alpha] (s : Set \\alpha) [\\text{Fintype } s.\\Elem] \\Rightarrow \\text{Finite}(s.\\offDiag.\\Elem) $$$

Lean4

instance fintypeOffDiag [DecidableEq α] (s : Set α) [Fintype s] : Fintype s.offDiag :=
  Fintype.ofFinset s.toFinset.offDiag <| by simp

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