nonempty_inter_of_le_ncard_add_ncard

English

If α is finite and Nat.card α ≤ s.ncard + t.ncard and s ∪ t ≠ univ, then s ∩ t is nonempty.

Русский

Если α конечно и Nat.card α ≤ s.ncard + t.ncard, и s ∪ t не равно вселюбому, тогда s ∩ t непусто.

LaTeX

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

Lean4

theorem nonempty_inter_of_le_ncard_add_ncard [Finite α] (h' : Nat.card α ≤ s.ncard + t.ncard) (h : s ∪ t ≠ univ) :
    (s ∩ t).Nonempty := by
  rw [← ncard_union_add_ncard_inter s t] at h'
  replace h := (ncard_lt_card h).trans_le h'
  rwa [lt_add_iff_pos_right, ncard_pos] at h

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