add — Mathlib

English

If h1 absorbs s1 by t1 and h2 absorbs s2 by t2, then s1+s2 is absorbed by t1+t2.

Русский

Если s1 поглощается t1 и s2 поглощается t2, то их сумма s1+s2 поглощается t1+t2.

LaTeX

$$$Absorbs M s_1 t_1 \rightarrow Absorbs M s_2 t_2 \rightarrow Absorbs M (s_1 + s_2) (t_1 + t_2)$$$

Lean4

protected theorem add [AddZeroClass E] [DistribSMul M E] (h₁ : Absorbs M s₁ t₁) (h₂ : Absorbs M s₂ t₂) :
    Absorbs M (s₁ + s₂) (t₁ + t₂) :=
  h₂.mp <| h₁.eventually.mono fun x hx₁ hx₂ ↦ by rw [smul_add]; exact add_subset_add hx₁ hx₂

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