toFinset_setOf — Mathlib

English

For a finite α, a predicate p, and h stating that {x | p x} is finite, the Finset of this set equals the Finset of those x with p x, i.e., h.toFinset = Finset.filter (λ x, p x) Finset.univ.

Русский

Пусть α конечно, p — предикат, и множество {x | p x} конечно; тогда соответствующее Finset равно Finset.filter (λ x, p x) Finset.univ.

LaTeX

$$$ h.toFinset = \mathrm{Finset}.filter(\\text{(}\\lambda x. p x\\text{)})(\mathrm{Finset}.univ) $$$

Lean4

@[simp high]
protected theorem toFinset_setOf [Fintype α] (p : α → Prop) [DecidablePred p] (h : {x | p x}.Finite) :
    h.toFinset = ({x | p x} : Finset α) := by simp

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