le_closure

Mathlib.Order.Closure

URI: https://scilib.ai/kg/mathlib#LowerAdjoint.le_closure

← MathLib Explorer

English

The closure operation is extensive: for every x ∈ α, x ≤ u(l(x)).

Русский

Замыкание расширяет элемент: для каждого x ∈ α выполняется x ≤ u(l(x)).

LaTeX

$$$x \\le u(l(x))$$$

Lean4

/-- Every element is less than its closure. This property is sometimes referred to as extensivity or
inflationarity. -/
theorem le_closure (x : α) : x ≤ u (l x) :=
  l.gc.le_u_l _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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