leftLim_le_rightLim

Mathlib.Topology.Order.LeftRightLim

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

English

For antitone f and x < y, leftLim f y ≤ rightLim f x.

Русский

Для антимонотонной f и x < y, leftLim f y ≤ rightLim f x.

LaTeX

$$$\text{Antitone}(f) \Rightarrow \forall x,y\ (x < y \rightarrow \operatorname{leftLim} f y \le \operatorname{rightLim} f x)$$$

Lean4

theorem leftLim_le_rightLim (h : x < y) : leftLim f y ≤ rightLim f x :=
  hf.dual_right.rightLim_le_leftLim h

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

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

Разделы

Аффилиация

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