English
The SMulAntidiagonal built from the minima is exactly the singleton of the pair of minima.
Русский
SMulAntidiagonal, построенный из минимальных элементов, равен одиночному множеству пары минимума.
LaTeX
$$SMulAntidiagonal hs isPWO ht isPWO (hs.min hns • ht.min hnt) = { (hs.min hns, ht.min hnt) }$$
Lean4
@[to_additive]
theorem smulAntidiagonal_min_smul_min [LinearOrder G] [LinearOrder P] [SMul G P] [IsOrderedCancelSMul G P] {s : Set G}
{t : Set P} (hs : s.IsWF) (ht : t.IsWF) (hns : s.Nonempty) (hnt : t.Nonempty) :
SMulAntidiagonal hs.isPWO ht.isPWO (hs.min hns • ht.min hnt) = {(hs.min hns, ht.min hnt)} :=
by
ext ⟨a, b⟩
simp only [mem_smulAntidiagonal, mem_singleton, Prod.ext_iff]
constructor
· rintro ⟨has, hat, hst⟩
obtain rfl :=
(hs.min_le hns has).eq_of_not_lt fun hlt => (SMul.smul_lt_smul_of_lt_of_le hlt <| ht.min_le hnt hat).ne' hst
exact ⟨rfl, IsCancelSMul.left_cancel _ _ _ hst⟩
· rintro ⟨rfl, rfl⟩
exact ⟨hs.min_mem _, ht.min_mem _, rfl⟩
