exists_finset — Mathlib

English

A finite set holds that there exists a Finset whose membership is the same as the set.

Русский

Для конечного множества существует Finset с тем же множеством элементов.

LaTeX

$$$$ \\exists s' : Finset \\alpha, \\forall a: \\alpha,\\ a \\in s' \\iff a \\in s. $$$$

Lean4

theorem exists_finset {s : Set α} (h : s.Finite) : ∃ s' : Finset α, ∀ a : α, a ∈ s' ↔ a ∈ s :=
  by
  cases h.nonempty_fintype
  exact ⟨s.toFinset, fun _ => mem_toFinset⟩

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