image2_lowerBounds_upperBounds_subset_lowerBounds_image2

English

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

Русский

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

LaTeX

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

Lean4

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

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