fintype — Mathlib

English

For a predicate p, there is a finite type consisting of the elements i with i < n and p(i).

Русский

Для предиката p существует конечный тип, состоящий из элементов i с i < n и p(i).

LaTeX

$$$$\text{Fintype} \{ i : \mathbb{N} \mid i < n \wedge p(i) \}.$$$$

Lean4

/-- A fintype instance for the set relevant to `Nat.count`. Locally an instance in scope `count` -/
def fintype (n : ℕ) : Fintype { i // i < n ∧ p i } :=
  Fintype.ofFinset ({x ∈ range n | p x}) <| by
    intro x
    rw [mem_filter, mem_range]
    rfl

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