monotone

Mathlib.Order.Nucleus

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

English

The function underlying a nucleus is monotone.

Русский

Функция, лежащая в основе нуклеуса, монотонна.

LaTeX

$$$\text{Monotone}(n)$$$

Lean4

theorem monotone : Monotone n :=
  n.toClosureOperator.monotone

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

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

Разделы

Аффилиация

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