toCloseds

Mathlib.Order.Closure

URI: https://scilib.ai/kg/mathlib#ClosureOperator.toCloseds

Lean4

/-- Send an element to a closed element (by taking the closure). -/
def toCloseds (x : α) : c.Closeds :=
  ⟨c x, c.isClosed_closure x⟩

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

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

Разделы

Аффилиация

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