lowerBounds_infClosure

Mathlib.Order.SupClosed

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

← MathLib Explorer

English

lowerBounds(infClosure s) = lowerBounds s.

Русский

lowerBounds(infClosure s) = lowerBounds s.

LaTeX

$$lowerBounds(\\operatorname{infClosure}(s)) = lowerBounds(s)$$

Lean4

@[simp]
theorem lowerBounds_infClosure (s : Set α) : lowerBounds (infClosure s) = lowerBounds s :=
  (lowerBounds_mono_set subset_infClosure).antisymm <|
    by
    rintro a ha _ ⟨t, ht, hts, rfl⟩
    exact le_inf' _ _ fun b hb ↦ ha <| hts hb

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

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

Разделы

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

Аффилиация

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