inf_symmDiff_distrib_left — Mathlib

English

Inf distributes over symmetric difference on the left: a ∧ b Δ c = (a ∧ b) Δ (a ∧ c).

Русский

Левая дистрибутивность: inf распространяется на симм-дифференциал слева: a ∧ b Δ c = (a ∧ b) Δ (a ∧ c).

LaTeX

$$∀ a b c, a ∧ b Δ c = (a ∧ b) Δ (a ∧ c)$$

Lean4

theorem inf_symmDiff_distrib_left : a ⊓ b ∆ c = (a ⊓ b) ∆ (a ⊓ c) := by
  rw [symmDiff_eq_sup_sdiff_inf, inf_sdiff_distrib_left, inf_sup_left, inf_inf_distrib_left, symmDiff_eq_sup_sdiff_inf]

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