mulRothNumber_lt_of_forall_not_threeGPFree

English

If every t in the n-th power set of s fails to be GP-free, then mulRothNumber s < n.

Русский

Если всякие подмножества t в n-ной степени множества s не GP-free, тогда mulRothNumber s < n.

LaTeX

$$$\forall t \in \mathcal{P}_n(s), \neg ThreeGPFree(t) \Rightarrow mulRothNumber(s) < n$$$

Lean4

@[to_additive]
theorem mulRothNumber_lt_of_forall_not_threeGPFree (h : ∀ t ∈ powersetCard n s, ¬ThreeGPFree ((t : Finset α) : Set α)) :
    mulRothNumber s < n := by
  obtain ⟨t, hts, hcard, ht⟩ := mulRothNumber_spec s
  rw [← hcard, ← not_le]
  intro hn
  obtain ⟨u, hut, rfl⟩ := exists_subset_card_eq hn
  exact h _ (mem_powersetCard.2 ⟨hut.trans hts, rfl⟩) (ht.mono hut)

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