le_leftLim

Mathlib.Topology.Order.LeftRightLim

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

English

If f is antitone and x ≤ y, then f(y) ≤ leftLim f(x).

Русский

Если f антимонотонна и x ≤ y, то f(y) ≤ leftLim f(x).

LaTeX

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

Lean4

theorem le_leftLim (h : x ≤ y) : f y ≤ leftLim f x :=
  hf.dual_right.leftLim_le h

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

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

Разделы

Аффилиация

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