image_upperBounds_subset_upperBounds_image

English

If f is monotone, then image of upperBounds s is contained in upperBounds of image s: f '' upperBounds s ⊆ upperBounds (f '' s).

Русский

Если f монотонна, образ upperBounds s содержится в upperBounds образа s.

LaTeX

$$$(Hf : Monotone f) \Rightarrow f''(upperBounds s) \subseteq upperBounds(\mathrm{image}(f,s))$$$

Lean4

theorem image_upperBounds_subset_upperBounds_image : f '' upperBounds s ⊆ upperBounds (f '' s) :=
  by
  rintro _ ⟨a, ha, rfl⟩
  exact Hf.mem_upperBounds_image ha

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