biInf_congr' — Mathlib

English

If for all i and hi with p i, f i hi = g i hi, then the nested infima are equal: ⨅ i, ⨅ (hi : p i), f i hi = ⨅ i, ⨅ (hi : p i), g i hi.

Русский

Если для всех i и hi с p i выполняется f i hi = g i hi, то вложенные инфимумы равны.

LaTeX

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

Lean4

theorem biInf_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

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