image_upperBounds_subset_lowerBounds_image

English

Let f be antitone. The image under f of the upper bounds of s is contained in the lower bounds of the image of s.

Русский

Пусть f является антитонной функцией. Образ верхних границ s под действием f содержится в нижних границах образа s.

LaTeX

$$$ f''(\mathrm{upperBounds}(s)) \subseteq \mathrm{lowerBounds}(f''(s)) $$$

Lean4

theorem image_upperBounds_subset_lowerBounds_image : f '' upperBounds s ⊆ lowerBounds (f '' s) :=
  hf.dual_right.image_upperBounds_subset_upperBounds_image

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