rightLim_le_leftLim

Mathlib.Topology.Order.LeftRightLim

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

English

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

Русский

Для антимонотонной f и x ≤ y выполнено rightLim f y ≤ leftLim f x.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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