English
If S and T are well-founded with nonempty minima, then mulAntidiagonal hs ht (min S · min T) equals the singleton of the pair (min S, min T).
Русский
Если S и T хорошо упорядочены, и существуют минимумы, то mulAntidiagonal hs ht (min S · min T) = { (min S, min T) }.
LaTeX
$$mulAntidiagonal hs.isPWO ht.isPWO (hs.min hns * ht.min hnt) = { (hs.min hns, ht.min hnt) }$$
Lean4
@[to_additive]
theorem mulAntidiagonal_min_mul_min {α} [CommMonoid α] [LinearOrder α] [IsOrderedCancelMonoid α] {s t : Set α}
(hs : s.IsWF) (ht : t.IsWF) (hns : s.Nonempty) (hnt : t.Nonempty) :
mulAntidiagonal hs.isPWO ht.isPWO (hs.min hns * ht.min hnt) = {(hs.min hns, ht.min hnt)} :=
by
ext ⟨a, b⟩
simp only [mem_mulAntidiagonal, mem_singleton, Prod.ext_iff]
constructor
· rintro ⟨has, hat, hst⟩
obtain rfl := (hs.min_le hns has).eq_of_not_lt fun hlt => (mul_lt_mul_of_lt_of_le hlt <| ht.min_le hnt hat).ne' hst
exact ⟨rfl, mul_left_cancel hst⟩
· rintro ⟨rfl, rfl⟩
exact ⟨hs.min_mem _, ht.min_mem _, rfl⟩
