mem_lowerBounds_image — Mathlib

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

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