biSup_congr' — Mathlib

English

For a predicate p and f,g with f i hi = g i hi for all i and hi, the double supremum over i and hi are equal.

Русский

Для предиката p и функций f,g, если для всех i и hi выполняется f i hi = g i hi, то равны двойные верхние пределы.

LaTeX

$$$$ (\forall i (hi : p i), f i hi = g i hi) \Rightarrow \operatorname{iSup} i (\operatorname{iSup} hi (f i hi)) = \operatorname{iSup} i (\operatorname{ iSup} hi (g i hi)) $$$$

Lean4

theorem biSup_congr' {p : ι → Prop} {f g : (i : ι) → p i → α} (h : ∀ i (hi : p i), f i hi = g i hi) :
    ⨆ i, ⨆ (hi : p i), f i hi = ⨆ i, ⨆ (hi : p i), g i hi := by grind

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