image_upperBounds_subset_lowerBounds_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_upperBounds_subset_lowerBounds_image (Hf : AntitoneOn f t) (Hst : s ⊆ t) :
    f '' (upperBounds s ∩ t) ⊆ lowerBounds (f '' s) :=
  Hf.dual_right.image_upperBounds_subset_upperBounds_image Hst

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