le_rightLim

Mathlib.Topology.Order.LeftRightLim

URI: https://scilib.ai/kg/mathlib#Antitone.le_rightLim

English

The function x ↦ rightLim f x is antitone when f is antitone.

Русский

Функция x ↦ rightLim f x антимонотна, если f антимонотонна.

LaTeX

$$$\text{Antitone}(f) \Rightarrow \text{Antitone}(\operatorname{rightLim} f)$$$

Lean4

theorem le_rightLim (h : x < y) : f y ≤ rightLim f x :=
  hf.dual_right.rightLim_le h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru