vadd_absorbs — Mathlib

English

If s1 is absorbent and s2 absorbs t, then the vertical sum s1 + s2 absorbs x + t for any x.

Русский

Если s1 абсорбентно, и s2 поглощает t, то x +ᵥ t поглощается s1 + s2 для любого x.

LaTeX

$$$Absorbent M s_1 \\land Absorbs M s_2 t \\Rightarrow Absorbs M (s_1 + s_2) (x +^\\mathrm{v} t)$$$

Lean4

theorem vadd_absorbs {M E : Type*} [Bornology M] [AddZeroClass E] [DistribSMul M E] {s₁ s₂ t : Set E} {x : E}
    (h₁ : Absorbent M s₁) (h₂ : Absorbs M s₂ t) : Absorbs M (s₁ + s₂) (x +ᵥ t) := by rw [← singleton_vadd];
  exact (h₁ x).add h₂

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