monotone

Mathlib.Order.Closure

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

English

Every closure operator is a monotone function on α.

Русский

Каждый оператор замыкания является монотонной функцией на множестве α.

LaTeX

$$Monotone c$$

Lean4

@[mono]
theorem monotone : Monotone c :=
  c.monotone'

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

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

Разделы

Аффилиация

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