leftLim

Mathlib.Topology.Order.LeftRightLim

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

English

If f is antitone, then the function x ↦ leftLim f x is antitone.

Русский

Если f антимонотонна, то функция x ↦ leftLim f x антимонотна.

LaTeX

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

Lean4

@[mono]
protected theorem leftLim : Antitone (leftLim f) :=
  hf.dual_right.leftLim

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

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

Разделы

Аффилиация

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