toFinset_setOf — Mathlib

English

For any predicate p on α, the Finset representation of the set {x ∈ α : p x} is the universal Finset filtered by p: {x | p x}.toFinset = Finset.univ.filter p.

Русский

Для любого предиката p на α множество {x | p x} в виде конечного множества равно отфильтрованному по p исходному универсальному конечному множеству: {x | p x}.toFinset = Finset.univ.filter p.

LaTeX

$$$\text{Set}.toFinset\{x\; | \; p\,x\} = \mathrm{Finset.univ}.filter\; p$$$

Lean4

@[simp]
theorem toFinset_setOf [Fintype α] (p : α → Prop) [DecidablePred p] [Fintype {x | p x}] :
    Set.toFinset {x | p x} = Finset.univ.filter p := by
  ext
  simp

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