le_mulRothNumber

Mathlib.Combinatorics.Additive.AP.Three.Defs

URI: https://scilib.ai/kg/mathlib#ThreeGPFree.le_mulRothNumber

← MathLib Explorer

English

If s ⊆ t and s is GP-free, then #s ≤ mulRothNumber t.

Русский

Если s ⊆ t и s GP-free, то кардинал s не превосходит mulRothNumber t.

LaTeX

$$$ThreeGPFree(s) \Rightarrow (s \subseteq t \Rightarrow |s| \le mulRothNumber(t))$$$

Lean4

@[to_additive]
theorem le_mulRothNumber (hs : ThreeGPFree (s : Set α)) (h : s ⊆ t) : #s ≤ mulRothNumber t :=
  Nat.le_findGreatest (card_le_card h) ⟨s, h, rfl, hs⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru