exists_card_eq — Mathlib

English

For any infinite α and any n, there exists a Finset s with card s = n.

Русский

Для бесконечного α и любого n существует конечный набор s с cardinality n.

LaTeX

$$$ [\text{Infinite}(\alpha)] \Rightarrow \forall n:\mathbb{N}, \exists s:\mathrm{Finset}(\alpha), s.card = n $$$

Lean4

theorem exists_card_eq [Infinite α] : ∀ n : ℕ, ∃ s : Finset α, s.card = n
  | 0 => ⟨∅, card_empty⟩
  | n + 1 => by
    classical
    obtain ⟨s, rfl⟩ := exists_card_eq n
    obtain ⟨a, ha⟩ := s.exists_notMem
    exact ⟨insert a s, card_insert_of_notMem ha⟩

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