filter_mem_univ_eq_toFinset — Mathlib

English

The finite universal Finset filtered by membership in s equals s.toFinset: Finset.univ.filter (· ∈ s) = s.toFinset.

Русский

Универсальное Finset, отфильтрованное по принадлежности элементам s, равно s.toFinset.

LaTeX

$$$\mathrm{univ}.filter(\cdot \in s) = s.toFinset$$$

Lean4

theorem filter_mem_univ_eq_toFinset [Fintype α] (s : Set α) [Fintype s] [DecidablePred (· ∈ s)] :
    Finset.univ.filter (· ∈ s) = s.toFinset := by
  ext
  rw [mem_filter_univ, mem_toFinset]

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