nonempty_inter_of_lt_ncard_add_ncard

English

If α is finite and the total number of elements is less than the sum of the ncards of s and t, then s ∩ t is nonempty.

Русский

Если α конечно, и общее число меньше суммы кардинальностей s и t, то s ∩ t непусто.

LaTeX

$$$$ [\mathrm{Finite}(\alpha)], \mathrm{Nat.card}(\alpha) < s.ncard + t.ncard \Rightarrow (s \cap t) \neq \varnothing $$$$

Lean4

theorem nonempty_inter_of_lt_ncard_add_ncard [Finite α] (h : Nat.card α < s.ncard + t.ncard) : (s ∩ t).Nonempty :=
  by
  rw [← ncard_union_add_ncard_inter s t] at h
  replace h := (s ∪ t).ncard_le_card.trans_lt h
  rwa [lt_add_iff_pos_right, ncard_pos] at h

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