closure_eq

Mathlib.Order.Closure

URI: https://scilib.ai/kg/mathlib#ClosureOperator.IsClosed.closure_eq

← MathLib Explorer

English

If x is closed with respect to c, then c(x) = x.

Русский

Если элемент x замкнут относительно замыкателя c, то c(x) = x.

LaTeX

$$$\\\\forall {\\\\alpha : Type*} [PartialOrder {\\\\alpha}] \\\\forall c : ClosureOperator {\\\\alpha} \\\\forall x : {\\\\alpha}, c.IsClosed x \\\\Rightarrow c x = x$$$

Lean4

theorem closure_eq : c.IsClosed x → c x = x :=
  c.isClosed_iff.1

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

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

Разделы

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

Аффилиация

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