exists — Mathlib

English

There exists a Finset s with p(s) iff there exists a finite set S with p(S.toFinset).

Русский

Существует Finset s с p(s) тогда и только тогда, когда существует конечное множество S с p(S.toFinset).

LaTeX

$$$\\exists s:\\mathrm{Finset}(\\alpha),\\; p(s) \\iff \\exists S:\\mathrm{Set}(\\alpha),\\; S\\text{ finite} \\land p(S^{\\text{toFinset}}).$$$

Lean4

theorem «exists» {p : Finset α → Prop} : (∃ s, p s) ↔ ∃ (s : Set α) (hs : s.Finite), p hs.toFinset
    where
  mp := fun ⟨s, hs⟩ ↦ ⟨s, s.finite_toSet, by simpa⟩
  mpr := fun ⟨s, hs, hs'⟩ ↦ ⟨hs.toFinset, hs'⟩

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