anti

Mathlib.Order.Filter.EventuallyConst

URI: https://scilib.ai/kg/mathlib#Filter.EventuallyConst.anti

English

If h: EventuallyConst f l and hl' : l' ≤ l, then EventuallyConst f l'.

Русский

Если f является EventuallyConst вдоль l и l'≤l, то f является EventuallyConst вдоль l'.

LaTeX

$$$\mathrm{EventuallyConst}(f,l) \land l' \le l \Rightarrow \mathrm{EventuallyConst}(f,l')$$$

Lean4

nonrec theorem anti {l'} (h : EventuallyConst f l) (hl' : l' ≤ l) : EventuallyConst f l' :=
  h.anti (map_mono hl')

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

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

Разделы

Аффилиация

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