inf_iSup₂_eq

Mathlib.Order.CompleteBooleanAlgebra

URI: https://scilib.ai/kg/mathlib#inf_iSup₂_eq

English

Dual of iSup₂_eq: in a Frame, (a ∧ ⨆ (i) (j), f i j) = ⨆ (i) (j), a ∧ f i j.

Русский

Двойное сочетание inf и sup: (a ∧ ⨆ i j f(i,j)) = ⨆ i j (a ∧ f(i,j)).

LaTeX

$$$ a \\wedge \\bigl( \\bigvee_{i,j} f(i,j) \\bigr) = \\bigvee_{i,j} (a \\wedge f(i,j)) $$$

Lean4

theorem inf_iSup₂_eq {f : ∀ i, κ i → α} (a : α) : (a ⊓ ⨆ (i) (j), f i j) = ⨆ (i) (j), a ⊓ f i j := by
  simp only [inf_iSup_eq]

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

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

Разделы

Аффилиация

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