mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds

English

If a ∈ lowerBounds s and b ∈ upperBounds t, then f(a, b) is in lowerBounds (image2 f s t).

Русский

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

LaTeX

$$$(a \\in \\operatorname{lowerBounds}(s)) \\to (b \\in \\operatorname{upperBounds}(t)) \\to f(a,b) \\in \\operatorname{lowerBounds}(\\operatorname{image2} f\\ s\\ t)$$$

Lean4

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

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