mapsTo_Ici — Mathlib

English

If f is monotone on the entire space, then f preserves the upper intervals: for any a, f maps [a, ∞) into [f(a), ∞).

Русский

Если f монотонна на всей области, то отображение сохраняет верхние интервалы: для любого a геометрически [a, ∞) переходит в [f(a), ∞).

LaTeX

$$$$ \\forall a\\, (\\text{Monotone } f)\\;:\\; \\mathrm{MapsTo}\\, f\\,(\\Ici a)\\,(\\Ici (f a)). $$$$

Lean4

theorem mapsTo_Ici (h : MonotoneOn f (Ici a)) : MapsTo f (Ici a) (Ici (f a)) := fun _ _ ↦ by aesop

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