sInf_sup_eq — Mathlib

English

In a coframe, for any subset s of α and any element b, the infimum of s joined with b equals the infimum over s of the joins with b: sInf s ⊔ b = ⨅ a∈s, a ⊔ b.

Русский

В кофрейме для любого подмножества s ⊆ α и элемента b верно: sInf s ⊔ b = ⨅_{a∈s}} (a ⊔ b).

LaTeX

$$$ \\inf s \\lor b = \\inf_{a \\in s} (a \\lor b) $$$

Lean4

theorem sInf_sup_eq : sInf s ⊔ b = ⨅ a ∈ s, a ⊔ b := by simpa only [sup_comm] using @sup_sInf_eq α _ s b

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