image_lowerBounds_subset_lowerBounds_image

English

Let f be monotone on t and s ⊆ t. Then f''(lowerBounds s ∩ t) ⊆ lowerBounds (f'' s).

Русский

Пусть f монотонна на t и s ⊆ t. Тогда образ нижних границ s ∩ t под действием f лежит в нижних границах образа s.

LaTeX

$$$(Hf : MonotoneOn f t) \land (Hst : s \subseteq t) : f''(\mathrm{lowerBounds}(s) \cap t) \subseteq \mathrm{lowerBounds}(f''s)$$$

Lean4

theorem image_lowerBounds_subset_lowerBounds_image (Hf : MonotoneOn f t) (Hst : s ⊆ t) :
    f '' (lowerBounds s ∩ t) ⊆ lowerBounds (f '' s) :=
  Hf.dual.image_upperBounds_subset_upperBounds_image Hst

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