inf_iSup_eq

Mathlib.Order.CompleteBooleanAlgebra

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

English

In a Frame α, the distributive interaction between infimum and supremum yields: (a ∧ ⨆ i f i) = ⨆ i (a ∧ f i).

Русский

В рамках α применимо: (a ∧ ⨆ i f i) = ⨆ i (a ∧ f i).

LaTeX

$$$ a \\wedge \\bigl(\\bigvee_i f(i)\\bigr) = \\bigvee_i (a \\wedge f(i)) $$$

Lean4

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

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

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

Разделы

Аффилиация

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