English
Let S and T be well-founded subsets with nonempty subsets achieving their minima. Then the minimum of the product set S·T equals the product of the minima: min(S) · min(T).
Русский
Пусть S и T — хорошо упорядоченные множества с не пустыми подмножествами, достигающими минимума. Тогда минимальный элемент множества S·T равен произведению минимумов: min(S) · min(T).
LaTeX
$$(hs : S.IsWF) (ht : T.IsWF) (hsn : S.Nonempty) (htn : T.Nonempty) → (hs.mul ht).min (hs.min hsn * ht.min htn) = hs.min hsn * ht.min htn$$
Lean4
@[to_additive]
theorem min_mul (hs : s.IsWF) (ht : t.IsWF) (hsn : s.Nonempty) (htn : t.Nonempty) :
(hs.mul ht).min (hsn.mul htn) = hs.min hsn * ht.min htn :=
by
refine le_antisymm (IsWF.min_le _ _ (mem_mul.2 ⟨_, hs.min_mem _, _, ht.min_mem _, rfl⟩)) ?_
rw [IsWF.le_min_iff]
rintro _ ⟨x, hx, y, hy, rfl⟩
exact mul_le_mul' (hs.min_le _ hx) (ht.min_le _ hy)
