English
If f is antitone on t and s ⊆ t, a ∈ upperBounds s, then a ∈ t and f(a) ∈ lowerBounds (f '' s).
Русский
Если f антитонна на t и s ⊆ t, а ∈ upperBounds s, то a ∈ t и f(a) ∈ lowerBounds( f'' s ).
LaTeX
$$$(Hf : AntitoneOn f t) (Hst : s \subseteq t) : a \in upperBounds s \rightarrow a \in t \rightarrow f(a) \in \mathrm{lowerBounds}(\mathrm{image}(f,s))$$$
Lean4
theorem mem_lowerBounds_image (Hf : AntitoneOn f t) (Hst : s ⊆ t) :
a ∈ upperBounds s → a ∈ t → f a ∈ lowerBounds (f '' s) :=
Hf.dual_right.mem_upperBounds_image Hst