iSup_inf_eq — Mathlib

English

Distributivity of iSup over inf, i.e., the supremum of infimum over a family equals the infimum of the supremum after applying Min.

Русский

Дистрибутивность iSup над inf, т.е. максимум от минимума равен минимуму от максимумов после применения Min.

LaTeX

$$$\mathrm{iSup\_inf\_eq}: \ \min(a, \big\vee_i f(i)) = \big\vee_i \min(a, f(i))$$$

Lean4

theorem iSup_inf_eq (f : ι → α) (a : α) : (⨆ i, f i) ⊓ a = ⨆ i, f i ⊓ a := by rw [iSup, sSup_inf_eq, iSup_range]

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