image2_upperBounds_lowerBounds_subset_upperBounds_image2

English

The image2 of the upper bound of s and lower bound of t is contained in the upper bounds of image2 f s t.

Русский

Образ верхней границы s и нижней границы t содержится в верхних границах image2 f s t.

LaTeX

$$$(\\operatorname{upperBounds}(s),\\operatorname{lowerBounds}(t)) \\mapsto \\operatorname{upperBounds}(\\operatorname{image2} f\\ s\\ t)$$$

Lean4

theorem image2_upperBounds_lowerBounds_subset_upperBounds_image2 :
    image2 f (upperBounds s) (lowerBounds t) ⊆ upperBounds (image2 f s t) :=
  image2_subset_iff.2 fun _ ha _ hb ↦ mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds h₀ h₁ ha hb

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