mem_lowerBounds_image_self — Mathlib

English

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

Русский

Если f антитонна на t и a ∈ upperBounds t и a ∈ t, то f(a) ∈ lowerBounds (f '' t).

LaTeX

$$$(Hf : AntitoneOn f t) : a \in upperBounds t \\land a \in t \\Rightarrow f(a) \in \mathrm{lowerBounds}(\mathrm{image}(f,t))$$$

Lean4

theorem mem_lowerBounds_image_self (Hf : AntitoneOn f t) : a ∈ upperBounds t → a ∈ t → f a ∈ lowerBounds (f '' t) :=
  Hf.dual_right.mem_upperBounds_image_self

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