le_mulRothNumber_product — Mathlib

English

The Roth number of a product of finite sets in α and β satisfies mulRothNumber(s)·mulRothNumber(t) ≤ mulRothNumber(s × t).

Русский

Число Рота произведения множеств удовлетворяет неравенству mulRothNumber(s)·mulRothNumber(t) ≤ mulRothNumber(s × t).

LaTeX

$$$mulRothNumber(s) \cdot mulRothNumber(t) \le mulRothNumber(s \times t)$$$

Lean4

@[to_additive]
theorem le_mulRothNumber_product (s : Finset α) (t : Finset β) :
    mulRothNumber s * mulRothNumber t ≤ mulRothNumber (s ×ˢ t) :=
  by
  obtain ⟨u, hus, hucard, hu⟩ := mulRothNumber_spec s
  obtain ⟨v, hvt, hvcard, hv⟩ := mulRothNumber_spec t
  rw [← hucard, ← hvcard, ← card_product]
  refine ThreeGPFree.le_mulRothNumber ?_ (product_subset_product hus hvt)
  rw [coe_product]
  exact hu.prod hv

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