mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds

English

If f swaps preserve antitone behavior in the second argument and is monotone in the first, then for any a ∈ lowerBounds s and b ∈ upperBounds t, f(a,b) is an upper bound of image2 f s t.

Русский

Если f сохраняет антимонотонность во втором аргументе и монотонна в первом, то для любых a ∈ lowerBounds s и b ∈ upperBounds t, значение f(a,b) является верхней границей image2 f s t.

LaTeX

$$ (∀ b, Antitone (swap f b)) → (∀ a, Monotone (f a)) → ∀ (ha : a ∈ lowerBounds s) (hb : b ∈ upperBounds t), f a b ∈ upperBounds (image2 f s t)$$

Lean4

theorem mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds (ha : a ∈ lowerBounds s) (hb : b ∈ upperBounds t) :
    f a b ∈ upperBounds (image2 f s t) :=
  forall_mem_image2.2 fun _ hx _ hy => (h₀ _ <| ha hx).trans <| h₁ _ <| hb hy

Похожие утверждения