le_symmDiff_sup_symmDiff_left — Mathlib

English

If a and b are disjoint, then for any c we have c ≤ a Δ c ⊔ b Δ c.

Русский

Если a и b несовместны (дополняют друг друга нулю), то для любого c выполняется c ≤ (a Δ c) ⊔ (b Δ c).

LaTeX

$$$ (h : Disjoint a b) ": c \\leq a \\triangle c \\sqcup b \\triangle c $$$

Lean4

theorem le_symmDiff_sup_symmDiff_left (h : Disjoint a b) : c ≤ a ∆ c ⊔ b ∆ c :=
  by
  trans c \ (a ⊓ b)
  · rw [h.eq_bot, sdiff_bot]
  · rw [sdiff_inf]
    exact sup_le_sup le_sup_right le_sup_right

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