add_biSup' — Mathlib

English

For any p, the addition distributes across nested iSup: a + (iSup i, iSup x, f i) = iSup i, iSup x, a + f i.

Русский

Для любой p выражение сложения распределяется над вложенным iSup: a + (⨆ i, ⨆ _ : p i, f i) = ⨆ i, ⨆ _ : p i, a + f i.

LaTeX

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

Lean4

theorem add_biSup' {p : ι → Prop} (h : ∃ i, p i) (f : ι → ℕ∞) : a + ⨆ i, ⨆ _ : p i, f i = ⨆ i, ⨆ _ : p i, a + f i :=
  by
  haveI : Nonempty { i // p i } := nonempty_subtype.2 h
  simp only [iSup_subtype', add_iSup]

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