eq_top_of_card_le_of_finite — Mathlib

English

Let α be finite and s ⊆ α. If |α| ≤ |s|, then s = α.

Русский

Пусть α конечна и s ⊆ α. Если |α| ≤ |s|, то s = α.

LaTeX

$$$[\\Finite(\\alpha)] \\Rightarrow \\Big(\\operatorname{card}(\\alpha) \\le \\operatorname{card}(s) \\Rightarrow s = \mathrm{univ}\\).$$$

Lean4

theorem eq_top_of_card_le_of_finite [Finite α] {s : Set α} (h : Nat.card α ≤ Nat.card s) : s = ⊤ :=
  Set.Finite.eq_of_subset_of_card_le univ.toFinite (subset_univ s) <| Nat.card_congr (Equiv.Set.univ α) ▸ h

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