inf_symmDiff_distrib_right

Mathlib.Order.SymmDiff

URI: https://scilib.ai/kg/mathlib#inf_symmDiff_distrib_right

English

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

Русский

Правая дистрибутивность: a Δ b ∧ c = (a ∧ c) Δ (b ∧ c).

LaTeX

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

Lean4

theorem inf_symmDiff_distrib_right : a ∆ b ⊓ c = (a ⊓ c) ∆ (b ⊓ c) := by
  simp_rw [inf_comm _ c, inf_symmDiff_distrib_left]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru