closure_le_closed_iff_le

Mathlib.Order.Closure

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

← MathLib Explorer

English

If α has a top element and b does as well, then u(l(top)) = top.

Русский

Пусть α имеет верхний элемент; тогда u(l(верх)) = верх.

LaTeX

$$$u(l(\top)) = \top$$$

Lean4

@[simp]
theorem closure_le_closed_iff_le (x : α) {y : α} (hy : l.closed y) : u (l x) ≤ y ↔ x ≤ y :=
  (show l.closureOperator.IsClosed y from hy).closure_le_iff

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

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

Разделы

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

Аффилиация

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