iInf_sup_iInf — Mathlib

English

For sets s ⊆ ι and t ⊆ ι', and f,g, the supremum over i ∈ s and j ∈ t of f(i) ⊔ g(j) equals the infimum over pairs (i,j) ∈ s × t of f(i) ⊔ g(j).

Русский

Для множеств s ⊆ ι и t ⊆ ι', и функций f,g: верхний предел по i∈s и j∈t от f(i) ⊔ g(j) равен инфимума по парам (i,j) ∈ s×t от f(i) ⊔ g(j).

LaTeX

$$$\bigvee_{i \in s} f(i) \;\sqcup\; \bigvee_{j \in t} g(j) = \inf_{(i,j) \in s \times t} \left( f(i) \lor g(j) \right)$$$

Lean4

theorem iInf_sup_iInf {ι ι' : Type*} {f : ι → α} {g : ι' → α} : ((⨅ i, f i) ⊔ ⨅ i, g i) = ⨅ i : ι × ι', f i.1 ⊔ g i.2 :=
  @iSup_inf_iSup αᵒᵈ _ _ _ _ _

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