image_lowerBounds_subset_upperBounds_image

English

If f is antitone on t and s ⊆ t, then f'' (lowerBounds s ∩ t) ⊆ upperBounds (f '' s).

Русский

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

LaTeX

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

Lean4

theorem image_lowerBounds_subset_upperBounds_image (Hf : AntitoneOn f t) (Hst : s ⊆ t) :
    f '' (lowerBounds s ∩ t) ⊆ upperBounds (f '' s) :=
  Hf.dual_right.image_lowerBounds_subset_lowerBounds_image Hst

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