iSup_inf_eq — Mathlib

English

For a directed family f, the meet with a distributes over the supremum: (sup_i f_i) ∧ a = sup_i (f_i ∧ a).

Русский

Для направленной семейства f распределяется операция meet над supremum: (sup_i f_i) ∧ a = sup_i (f_i ∧ a).

LaTeX

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

Lean4

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

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