ofFinset — Mathlib

English

If p ⊆ α is a set and s is a Finset with the same elements as p, then p is finite.

Русский

Если p — множество, а s — конечноуровневый конечный набор с теми же элементами, то p конечно.

LaTeX

$$$$ (\\forall x, x\\in s \\iff x\\in p) \\Rightarrow p.Finite. $$$$

Lean4

/-- Construct a `Finite` instance for a `Set` from a `Finset` with the same elements. -/
protected theorem ofFinset {p : Set α} (s : Finset α) (H : ∀ x, x ∈ s ↔ x ∈ p) : p.Finite :=
  have := Fintype.ofFinset s H;
  p.toFinite

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