sub — Mathlib

English

If Absorbs on s1 by t1 and on s2 by t2, then Absorbs on s1−s2 by t1−t2.

Русский

Если Absorbs выполняется для s1,t1 и s2,t2, тогда Absorbs для 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

theorem sub {s₁ s₂ t₁ t₂ : Set E} (h₁ : Absorbs M s₁ t₁) (h₂ : Absorbs M s₂ t₂) : Absorbs M (s₁ - s₂) (t₁ - t₂) := by
  simpa only [sub_eq_add_neg] using h₁.add h₂.neg_neg

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