union_ne_univ_of_ncard_add_ncard_lt

English

If s.ncard + t.ncard is strictly less than Nat.card α, then s ∪ t ≠ univ.

Русский

Если сумма кардинальностей s и t строго меньше Nat.card α, то s ∪ t ≠ univ.

LaTeX

$$$$ s.ncard + t.ncard < \mathrm{Nat.card}(\alpha) \Rightarrow s \cup t \neq \mathrm{univ} $$$$

Lean4

theorem union_ne_univ_of_ncard_add_ncard_lt (h : s.ncard + t.ncard < Nat.card α) : s ∪ t ≠ univ :=
  by
  contrapose! h
  rw [← ncard_univ, ← h]
  exact ncard_union_le s t

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