inf_iSup_eq

Mathlib.Order.CompleteBooleanAlgebra

URI: https://scilib.ai/kg/mathlib#Order.Frame.MinimalAxioms.inf_iSup_eq

English

Distributivity of infimum over supremum in the dual setting, expressing a symmetry with iSup.

Русский

Дистрибутивность инфимума над супремумом в двойственной установке, отражающая симметрию с iSup.

LaTeX

$$$\mathrm{inf\_iSup\_eq}$$$

Lean4

theorem inf_iSup_eq (a : α) (f : ι → α) : (a ⊓ ⨆ i, f i) = ⨆ i, a ⊓ f i := by
  simpa only [inf_comm] using minAx.iSup_inf_eq f a

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

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

Разделы

Аффилиация

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