closed_eq_range_close

Mathlib.Order.Closure

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

← MathLib Explorer

English

The closed set equals the range of u ∘ l: l.closed = range (u ∘ l).

Русский

Замкнутое множество равно образу последовательности u ∘ l: l.closed = range (u ∘ l).

LaTeX

$$$l.closed = \mathrm{range}(u \circ l)$$$

Lean4

/-- The set of closed elements for `l` is the range of `u ∘ l`. -/
theorem closed_eq_range_close : l.closed = Set.range (u ∘ l) :=
  l.closureOperator.setOf_isClosed_eq_range_closure

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

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

Разделы

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

Аффилиация

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