iSup_inf_iSup — Mathlib

English

In a frame structure, the combined operation iSup and iSup over products satisfies distributive property: iSup_inf_iSup_eq: (iSup f i) ∧ (iSup g j) = iSup over product of indices of f i and g j.

Русский

Для структуры с iSup и продуктами индексов выполняется дистрибутивность: iSup_inf_iSup_eq.

LaTeX

$$$\\bigl( \\bigvee_i f(i) \\bigr) \\wedge \\bigl( \\bigvee_j g(j) \\bigr) = \\bigvee_{i,j} \\bigl( f(i) \\wedge g(j) \\bigr)$$$

Lean4

theorem iSup_inf_iSup {ι ι' : Type*} {f : ι → α} {g : ι' → α} : ((⨆ i, f i) ⊓ ⨆ j, g j) = ⨆ i : ι × ι', f i.1 ⊓ g i.2 :=
  by simp_rw [iSup_inf_eq, inf_iSup_eq, iSup_prod]

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