iInf_sup_eq — Mathlib

English

Let minAx be a MinimalAxioms structure on α. Then for any family f : ι → α and any a ∈ α, the join distributes over the infimum: (⨅ i, f i) ⊔ a = ⨅ i, f i ⊔ a.

Русский

Пусть на пространстве α задана структура минимальных аксиом. Тогда сумма над infimumом распределяется: (⨅ i, f(i)) ⊔ a = ⨅ i, (f(i) ⊔ a).

LaTeX

$$$\\Bigl(\\bigwedge_{i} f(i)\\Bigr) \\lor a = \\bigwedge_{i} (f(i) \\lor a)$$$$

Lean4

theorem iInf_sup_eq (f : ι → α) (a : α) : (⨅ i, f i) ⊔ a = ⨅ i, f i ⊔ a := by rw [iInf, sInf_sup_eq, iInf_range]

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