exists_subset_or_subset_of_two_mul_lt_ncard

English

If 2n < |s ∪ t|, then there exists r with either r ⊆ s or r ⊆ t and n < |r|.

Русский

Если 2n < |s ∪ t|, то существует r, такое что r ⊆ s или r ⊆ t и n < |r|.

LaTeX

$$$$ \forall n, \bigl( 2n < (s \cup t).ncard \bigr) \Rightarrow \exists r, (r \subseteq s \lor r \subseteq t) \land n < r.ncard $$$$

Lean4

theorem exists_subset_or_subset_of_two_mul_lt_ncard {n : ℕ} (hst : 2 * n < (s ∪ t).ncard) :
    ∃ r : Set α, n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t) := by
  classical
  have hu := finite_of_ncard_ne_zero ((Nat.zero_le _).trans_lt hst).ne.symm
  rw [ncard_eq_toFinset_card _ hu,
    Finite.toFinset_union (hu.subset subset_union_left) (hu.subset subset_union_right)] at hst
  obtain ⟨r', hnr', hr'⟩ := Finset.exists_subset_or_subset_of_two_mul_lt_card hst
  exact ⟨r', by simpa, by simpa using hr'⟩

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