biSup_congr — Mathlib

English

Let p : ι → Prop. If for all i, p i implies f i = g i, then the nested supremums agree: ⨆ i, ⨆ (hi : p i), f i hi = ⨆ i, ⨆ (hi : p i), g i hi.

Русский

Пусть p : ι → Prop. Если для каждого i, если p i, то f i hi = g i hi, тогда параллельные наслоённые супремумы равны.

LaTeX

$$$$ (\forall i, p i \to f i = g i) \Rightarrow \Big( \bigvee_i \big( \bigvee_{hi : p i} f i hi \big) \Big) = \Big( \bigvee_i \big( \bigvee_{hi : p i} g i hi \big) \Big) $$$$

Lean4

theorem biSup_congr {p : ι → Prop} (h : ∀ i, p i → f i = g i) : ⨆ (i) (_ : p i), f i = ⨆ (i) (_ : p i), g i :=
  iSup_congr fun i ↦ iSup_congr (h i)

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