u_ciInf_set

Mathlib.Order.ConditionallyCompleteLattice.Indexed

URI: https://scilib.ai/kg/mathlib#GaloisConnection.u_ciInf_set

← MathLib Explorer

English

If f is bounded above, gc.l(sup f) = sup (gc ∘ f).

Русский

Если f ограничено сверху, то l(верхняя грань f) = верхняя грань от l ∘ f.

LaTeX

$$$ l(\mathrm{iSup} f) = \mathrm{iSup} (\lambda i. l(f(i))) $$$

Lean4

theorem u_ciInf_set (gc : GaloisConnection l u) {s : Set γ} {f : γ → β} (hf : BddBelow (f '' s)) (hne : s.Nonempty) :
    u (⨅ i : s, f i) = ⨅ i : s, u (f i) :=
  gc.dual.l_ciSup_set hf hne

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

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

Разделы

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

Аффилиация

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