exists_finite_iff_finset — Mathlib

English

Let p be a predicate on subsets of α. There exists a finite subset s ⊆ α with p(s) if and only if there exists a finite Finset t of α such that p(↑t).

Русский

Пусть p — предикат на подмножестве α. Существует конечное множество s ⊆ α такое, что p(s), тогда и только тогда существует конечный Finset t над α такой, что p(↑t).

LaTeX

$$$ (\\exists s : \\Set α, s.Finite \\land p s) \\iff (\\exists s : \\Finset α, p ↑s) $$$

Lean4

theorem exists_finite_iff_finset {p : Set α → Prop} : (∃ s : Set α, s.Finite ∧ p s) ↔ ∃ s : Finset α, p ↑s :=
  ⟨fun ⟨_, hs, hps⟩ => ⟨hs.toFinset, hs.coe_toFinset.symm ▸ hps⟩, fun ⟨s, hs⟩ => ⟨s, s.finite_toSet, hs⟩⟩

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