biSup_add' — Mathlib

English

For Exists p, biSup_add' holds: (⨆ i, ⨆ _ : p i, f i) + a = ⨆ i, ⨆ _ : p i, a + f i.

Русский

Для существования p справедливо: (⨆ i, ⨆ _ : p i, f i) + a = ⨆ i, ⨆ _ : p i, a + f i.

LaTeX

$$$ \exists i, p(i) \rightarrow \forall f, \left( (\bigvee_i \bigvee_{x} f_i) + a = \bigvee_i \bigvee_{x} (a + f_i) \right) $$$

Lean4

theorem biSup_add' {p : ι → Prop} (h : ∃ i, p i) (f : ι → ℕ∞) : (⨆ i, ⨆ _ : p i, f i) + a = ⨆ i, ⨆ _ : p i, f i + a :=
  by simp only [add_comm, add_biSup' h]

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