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₂