exists_subset_or_subset_of_two_mul_lt_card

English

If 2n < |X ∪ Y| for finite X,Y, then there exists C ⊆ X ∪ Y with |C| > n and either C ⊆ X or C ⊆ Y.

Русский

Если для конечных X,Y выполняется 2n < |X ∪ Y|, то существует C ⊆ X ∪ Y с |C| > n и либо C ⊆ X, либо C ⊆ Y.

LaTeX

$$$2 \\cdot n < |X \\cup Y| \\Rightarrow \\exists C: Finset, n < |C| \\land (C \\subseteq X \\lor C \\subseteq Y)$$$

Lean4

theorem exists_subset_or_subset_of_two_mul_lt_card [DecidableEq α] {X Y : Finset α} {n : ℕ} (hXY : 2 * n < #(X ∪ Y)) :
    ∃ C : Finset α, n < #C ∧ (C ⊆ X ∨ C ⊆ Y) :=
  by
  have h₁ : #(X ∩ (Y \ X)) = 0 := Finset.card_eq_zero.mpr (by grind)
  have h₂ : #(X ∪ Y) = #X + #(Y \ X) := by grind
  obtain h | h : n < #X ∨ n < #(Y \ X) := by cutsat
  · exact ⟨X, by grind⟩
  · exact ⟨Y \ X, by grind⟩

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