English
If s and t are nonempty sets, then the upper bounds of their product equal the product of the upper bounds: upperBounds(s × t) = upperBounds(s) × upperBounds(t).
Русский
Если множества s и t непусты, то верхние границы их произведения равны произведению верхних границ: upperBounds(s × t) = upperBounds(s) × upperBounds(t).
LaTeX
$$$(hs : s.Nonempty) \rightarrow (ht : t.Nonempty) \rightarrow Eq(upperBounds( s ×ˢ t ), upperBounds(s) ×ˢ upperBounds(t))$$$
Lean4
@[simp]
theorem upperBounds_prod (hs : s.Nonempty) (ht : t.Nonempty) : upperBounds (s ×ˢ t) = upperBounds s ×ˢ upperBounds t :=
by ext; rw [← nonempty_coe_sort] at hs ht; aesop (add simp [upperBounds, Prod.le_def, forall_and])
