l_iSup₂

Mathlib.Order.GaloisConnection.Basic

URI: https://scilib.ai/kg/mathlib#GaloisConnection.l_iSup₂

English

For a Galois connection, the dual of l_sup gives that u preserves inf via duality: u(b1 ⊓ b2) = u b1 ⊓ u b2.

Русский

Через дуальность u сохраняет инфимум: u(b1 ⊓ b2) = u(b1) ⊓ u(b2).

LaTeX

$$$$ u\\left(b_1 \\land b_2\\right) = u(b_1) \\land u(b_2) $$$$

Lean4

theorem l_iSup₂ (gc : GaloisConnection l u) {f : ∀ i, κ i → α} : l (⨆ (i) (j), f i j) = ⨆ (i) (j), l (f i j) := by
  simp_rw [gc.l_iSup]

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

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

Разделы

Аффилиация

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