English
If h0 and h1 ensure that f is antitone in each argument, then taking the upper bounds of s and t yields that image2 f (upperBounds s) (upperBounds t) is contained in the lower bounds of image2 f s t. In particular, for a ∈ upperBounds s and b ∈ upperBounds t, f(a,b) is a lower bound of image2 f s t.
Русский
Если функция f антимонотно зависит от каждого аргумента, и s и t имеют верхние границы, то множество image2 f (upperBounds s) (upperBounds t) состоит из нижних границ image2 f s t. То есть для подстановок a ∈ upperBounds s и b ∈ upperBounds t имеем f(a,b) ниже всех значений f(x,y) с x ∈ s, y ∈ t.
LaTeX
$$$image2 f (\\upperBounds s) (\\upperBounds t) \\subseteq \\lowerBounds (image2 f s t)$$$
Lean4
theorem image2_lowerBounds_lowerBounds_subset_lowerBounds_image2 :
image2 f (upperBounds s) (upperBounds t) ⊆ lowerBounds (image2 f s t) :=
image2_subset_iff.2 fun _ ha _ hb ↦ mem_lowerBounds_image2_of_mem_upperBounds h₀ h₁ ha hb
