add_biSup — Mathlib

English

Let s be a nonempty set and for any i ∈ s, f i ∈ ENat. Then (a + ⨆ i ∈ s, f i) = ⨆ i ∈ s, (a + f i).

Русский

Пусть s ненулевое множество и для всех i ∈ s верно f(i) ∈ ENat. Тогда a + ⨆_{i∈s} f(i) = ⨆_{i∈s} (a + f(i)).

LaTeX

$$$ (s \neq \varnothing) \rightarrow \left( a + \bigsqcup_{i \in s} f(i) = \bigsqcup_{i \in s} (a + f(i)) \right) $$$

Lean4

theorem add_biSup {ι : Type*} {s : Set ι} (hs : s.Nonempty) (f : ι → ℕ∞) : a + ⨆ i ∈ s, f i = ⨆ i ∈ s, a + f i :=
  add_biSup' hs _

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