mem_upperBounds_image — Mathlib

English

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

Русский

Если f антитонична на t, s ⊆ t, a ∈ нижних границ s и a ∈ t, то f(a) ⊆ верхних границ образа s.

LaTeX

$$$(Hf : AntitoneOn f t) (Hst : s \subseteq t) (Has : a \in lowerBounds(s)) : a \in t \Rightarrow f(a) \in \mathrm{upperBounds}(\mathrm{image}(f,s))$$$

Lean4

theorem mem_upperBounds_image (Hf : AntitoneOn f t) (Hst : s ⊆ t) (Has : a ∈ lowerBounds s) :
    a ∈ t → f a ∈ upperBounds (f '' s) :=
  Hf.dual_right.mem_lowerBounds_image Hst Has

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