truncLT_add — Mathlib

English

For any c in Γ, truncLT_c is additive: truncLT_c(x+y) = truncLT_c(x) + truncLT_c(y).

Русский

Для любого c выполняется аддитивность truncLT: truncLT_c(x+y) = truncLT_c(x) + truncLT_c(y).

LaTeX

$$$$ \operatorname{truncLT}_c\left( x + y \right) = \operatorname{truncLT}_c(x) + \operatorname{truncLT}_c(y). $$$$

Lean4

theorem truncLT_add [DecidableLT Γ] (c : Γ) (x y : HahnSeries Γ R) : truncLT c (x + y) = truncLT c x + truncLT c y :=
  by
  ext i
  by_cases h : i < c <;> simp [h]

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