mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds

English

If the first argument is a lower bound and the second argument is a lower bound, then f a b is a lower bound of the image2 f s t for all a ∈ upperBounds s and b ∈ upperBounds t, under antitone/monotone conditions on f.

Русский

Если a ∈ upperBounds s и b ∈ upperBounds t, то f(a,b) — нижняя граница image2 f s t, при заданных антимонотонности/монотонности f.

LaTeX

$$ (∀ (b : β), Antitone (swap f b)) → (∀ a, Monotone (f a)) → BddBelow s → BddBelow t → image2 f (upperBounds s) (upperBounds t) ⊆ lowerBounds (image2 f s t)$$

Lean4

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

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