inf_iSup_eq — Mathlib

English

Let a be an element of a complete lattice α and {f_i} a directed family. Then a ∧ (sup_i f_i) = sup_i (a ∧ f_i).

Русский

Пусть a ∈ α и направленная семейство {f_i}. Тогда a ∧ (sup_i f_i) = sup_i (a ∧ f_i).

LaTeX

$$$ a \wedge \left( \bigvee_i f(i) \right) = \bigvee_i (a \wedge f(i)) $$$

Lean4

protected theorem inf_iSup_eq (h : Directed (· ≤ ·) f) : (a ⊓ ⨆ i, f i) = ⨆ i, a ⊓ f i := by
  rw [iSup, h.directedOn_range.inf_sSup_eq, iSup_range]

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