lowerBounds_closure

Mathlib.Topology.Order.OrderClosed

URI: https://scilib.ai/kg/mathlib#lowerBounds_closure

← MathLib Explorer

English

The set of lower bounds does not change when taking closures.

Русский

Множество нижних границ не меняется при взятии замыкания.

LaTeX

$$$ lowerBounds(closure s) = lowerBounds(s) $$$

Lean4

@[simp]
theorem lowerBounds_closure (s : Set α) : lowerBounds (closure s : Set α) = lowerBounds s :=
  ext fun a ↦ by simp_rw [mem_lowerBounds_iff_subset_Ici, isClosed_Ici.closure_subset_iff]

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

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

Разделы

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

Аффилиация

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