fintypeOfFinsetCardLe — Mathlib

English

If every Finset of a type has cardinality bounded by n, then the type is finite.

Русский

Если каждая конечная подмножность типа имеет кардинал не более n, то тип конечен.

LaTeX

$$$\\left(\\exists n\\in \\mathbb{N}. \\forall s:\\mathrm{Finset}(\\iota), |s| \\le n\\right) \\Rightarrow |\\iota| < \\infty$$$

Lean4

/-- If every finset in a type has bounded cardinality, that type is finite. -/
noncomputable def fintypeOfFinsetCardLe {ι : Type*} (n : ℕ) (w : ∀ s : Finset ι, #s ≤ n) : Fintype ι :=
  by
  apply fintypeOfNotInfinite
  intro i
  obtain ⟨s, c⟩ := Infinite.exists_subset_card_eq ι (n + 1)
  specialize w s
  rw [c] at w
  exact Nat.not_succ_le_self n w

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