mem_upperBounds_image_self — Mathlib

English

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

Русский

Пусть f монотонна на t и a принадлежит верхним границам t и самому t. Тогда f(a) является верхней гранью образа t под f.

LaTeX

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

Lean4

theorem mem_upperBounds_image_self (Hf : MonotoneOn f t) : a ∈ upperBounds t → a ∈ t → f a ∈ upperBounds (f '' t) :=
  Hf.mem_upperBounds_image subset_rfl

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