nonempty_inter_compl_of_ncard_add_ncard_lt

English

If s and t are subsets of α and s.ncard + t.ncard < Nat.card α, then (sᶜ ∩ tᶜ) is nonempty.

Русский

Если s и t — подмножества α и их суммы кардинальностей меньше Nat.card α, тогда пересечение их дополнений непусто.

LaTeX

$$$$ s.ncard + t.ncard < \mathrm{Nat.card}(\alpha) \Rightarrow (s^{c} \cap t^{c}) \neq \varnothing $$$$

Lean4

theorem nonempty_inter_compl_of_ncard_add_ncard_lt (h : s.ncard + t.ncard < Nat.card α) : (sᶜ ∩ tᶜ).Nonempty :=
  by
  rw [← compl_union, nonempty_compl]
  exact union_ne_univ_of_ncard_add_ncard_lt h

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