biInf_sup_biInf — Mathlib

English

For f : ι → α and a ∈ α, the infimum of f is related to the infimum of pointwise maxima: (⨅ i, f(i)) ⊔ a = ⨅ i, f(i) ⊔ a.

Русский

Для f: ι → α и a ∈ α справедливо: (⨅ i, f(i)) ⊔ a = ⨅ i, (f(i) ⊔ a).

LaTeX

$$$\left(\inf_i f(i)\right) \lor a = \inf_i \left( f(i) \lor a \right)$$$

Lean4

theorem biInf_sup_biInf {ι ι' : Type*} {f : ι → α} {g : ι' → α} {s : Set ι} {t : Set ι'} :
    ((⨅ i ∈ s, f i) ⊔ ⨅ j ∈ t, g j) = ⨅ p ∈ s ×ˢ t, f (p : ι × ι').1 ⊔ g p.2 :=
  @biSup_inf_biSup αᵒᵈ _ _ _ _ _ _ _

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