monotone

Mathlib.Order.ScottContinuity

URI: https://scilib.ai/kg/mathlib#ScottContinuous.monotone

English

If f is Scott-continuous, then f is monotone.

Русский

Если функция Scott–непрерывна, то она монотонна.

LaTeX

$$$\\mathrm{ScottContinuous}(f) \\Rightarrow \\mathrm{Monotone}(f).$$$

Lean4

protected theorem monotone (h : ScottContinuous f) : Monotone f :=
  h.scottContinuousOn.monotone univ (fun _ _ _ ↦ mem_univ _)

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

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

Разделы

Аффилиация

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