English
Roth number is preserved under left embedding by a scalar: mulRothNumber(s.map mulLeftEmbedding a) = mulRothNumber(s).
Русский
Число Рота сохраняется при левом отображении через умножение на скаляр: mulRothNumber(множество.map mulLeftEmbedding a) = mulRothNumber(множество).
LaTeX
$$$mulRothNumber(s.map\ (mulLeftEmbedding\ a)) = mulRothNumber(s)$$$
Lean4
@[to_additive (attr := simp)]
theorem mulRothNumber_map_mul_left : mulRothNumber (s.map <| mulLeftEmbedding a) = mulRothNumber s :=
by
refine le_antisymm ?_ ?_
· obtain ⟨u, hus, hcard, hu⟩ := mulRothNumber_spec (s.map <| mulLeftEmbedding a)
rw [subset_map_iff] at hus
obtain ⟨u, hus, rfl⟩ := hus
rw [coe_map] at hu
rw [← hcard, card_map]
exact (threeGPFree_smul_set.1 hu).le_mulRothNumber hus
· obtain ⟨u, hus, hcard, hu⟩ := mulRothNumber_spec s
have h : ThreeGPFree (u.map <| mulLeftEmbedding a : Set α) := by rw [coe_map]; exact hu.smul_set
convert h.le_mulRothNumber (map_subset_map.2 hus) using 1
rw [card_map, hcard]
