exists_not_mem_of_card_lt_enatCard

English

For a finite set s, if card(s) < ENat.card α, there exists an element a ∈ α not in s.

Русский

Для конечного множества s, если кардинальность s меньше ENat.card α, существует элемент a ∈ α, которого нет в s.

LaTeX

$$$$ \forall s, \mathrm{card}(s) < \mathrm{ENat.card}(\alpha) \Rightarrow \exists a \in \alpha, a \notin s $$$$

Lean4

theorem _root_.Finset.exists_not_mem_of_card_lt_enatCard {s : Finset α} (hs : s.card < ENat.card α) : ∃ a, a ∉ s := by
  contrapose! hs; simp [← Set.encard_coe_eq_coe_finsetCard, Set.eq_univ_of_forall (s := s.toSet) hs]

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