finite_toSet — Mathlib

English

There exists a Finset s with p(s) if and only if 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: \\{ S \\subseteq \\alpha \\mid S \\text{ finite} \\},\\; p(S^{\\text{toFinset}}).$$$

Lean4

/-- Gives a `Set.Finite` for the `Finset` coerced to a `Set`.
This is a wrapper around `Set.toFinite`. -/
@[simp]
theorem finite_toSet (s : Finset α) : (s : Set α).Finite :=
  Set.toFinite _

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