add — Mathlib

English

If a and b are substitutions, then their sum is a substitution: HasSubst a → HasSubst b → HasSubst (a + b).

Русский

Если a и b — подстановки, то их сумма тоже подстановка: HasSubst a → HasSubst b → HasSubst (a + b).

LaTeX

$$HasSubst a → HasSubst b → HasSubst (a + b)$$

Lean4

theorem add {a b : σ → MvPowerSeries τ S} (ha : HasSubst a) (hb : HasSubst b) : HasSubst (a + b) :=
  by
  letI : UniformSpace S := ⊥
  rw [hasSubst_iff_hasEval_of_discreteTopology] at ha hb ⊢
  exact ha.add hb

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