le_apply

Mathlib.Order.Nucleus

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

English

For a nucleus n, every x satisfies x ≤ n(x).

Русский

Для нуклеуса n выполняется x ≤ n(x) для всех x.

LaTeX

$$$\forall x\; x \le n(x)$$$

Lean4

theorem le_apply : x ≤ n x :=
  n.toClosureOperator.le_closure x

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

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

Разделы

Аффилиация

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