union — Mathlib

English

If h absorbs s1 by t1, s1 ⊆ s2, and t2 ⊆ t1, then s2 is absorbed by t2.

Русский

Если s1 поглощается t1 при помощи h, и s1 ⊆ s2, и t2 ⊆ t1, то s2 поглощается t2.

LaTeX

$$$h : Absorbs M s_1 t_1 \rightarrow (s_1 \subseteq s_2) \rightarrow (t_2 \subseteq t_1) \rightarrow Absorbs M s_2 t_2$$$

Lean4

protected theorem union (h₁ : Absorbs M s t₁) (h₂ : Absorbs M s t₂) : Absorbs M s (t₁ ∪ t₂) :=
  absorbs_union.2 ⟨h₁, h₂⟩

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