card_le_of — Mathlib

English

If every finite subset s of α has card ≤ n, then the cardinality of α is ≤ n.

Русский

Если каждый конечный подмножество s альфа имеет кардинал ≤ n, то кардинал α ≤ n.

LaTeX

$$$\left( \forall s : Finset \alpha, s.\mathrm{card} \le n \right) \Rightarrow \#\alpha \le n$$$

Lean4

theorem card_le_of {α : Type u} {n : ℕ} (H : ∀ s : Finset α, s.card ≤ n) : #α ≤ n :=
  by
  contrapose! H
  apply exists_finset_le_card α (n + 1)
  simpa only [nat_succ, succ_le_iff] using H

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