absorbs_union — Mathlib

English

Absorbs M s (t1 ∪ t2) holds if and only if Absorbs M s t1 and Absorbs M s t2.

Русский

Поглощение s относительно t1 ∪ t2 эквивалентно поглощению s относительно t1 и относительно t2.

LaTeX

$$$Absorbs M s (t_1 \cup t_2) \iff Absorbs M s t_1 \land Absorbs M s t_2$$$

Lean4

@[simp]
theorem _root_.absorbs_union : Absorbs M s (t₁ ∪ t₂) ↔ Absorbs M s t₁ ∧ Absorbs M s t₂ := by simp [Absorbs]

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