inter_nonempty_of_card_lt_card_add_card

English

If t ⊆ s and u ⊆ s and |s| < |t| + |u|, then t ∩ u ≠ ∅.

Русский

Если t ⊆ s и u ⊆ s и |s| < |t| + |u|, то t ∩ u ненулевое.

LaTeX

$$$t \\subseteq s \\land u \\subseteq s \\land |s| < |t| + |u| \\Rightarrow (t \\cap u) \\neq \\emptyset$$$

Lean4

/-- **Pigeonhole principle** for two finsets inside an ambient finset. -/
theorem inter_nonempty_of_card_lt_card_add_card (hts : t ⊆ s) (hus : u ⊆ s) (hstu : #s < #t + #u) : (t ∩ u).Nonempty :=
  by
  contrapose! hstu
  calc
    _ = #(t ∪ u) := by simp [← card_union_add_card_inter, not_nonempty_iff_eq_empty.1 hstu]
    _ ≤ #s := by gcongr; exact union_subset hts hus

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