English
In a well-ordered smul setting, the minimal smul of two nonempty WF sets equals the smul of their minima.
Русский
В хорошо упорядоченном контексте умножения по заданным множествам минимальное произведение равно произведению их минимальных элементов.
LaTeX
$$min_smul := (hs.min hns) • (ht.min hnt) equals the minimal element of (s • t)$$
Lean4
@[to_additive]
theorem min_smul [LinearOrder G] [LinearOrder P] [SMul G P] [IsOrderedSMul G P] {s : Set G} {t : Set P} (hs : s.IsWF)
(ht : t.IsWF) (hsn : s.Nonempty) (htn : t.Nonempty) : (hs.smul ht).min (hsn.smul htn) = hs.min hsn • ht.min htn :=
by
refine le_antisymm (IsWF.min_le _ _ (mem_smul.2 ⟨_, hs.min_mem _, _, ht.min_mem _, rfl⟩)) ?_
rw [IsWF.le_min_iff]
rintro _ ⟨x, hx, y, hy, rfl⟩
exact IsOrderedSMul.smul_le_smul (hs.min_le _ hx) (ht.min_le _ hy)
