le_symmDiff_iff_right

Mathlib.Order.SymmDiff

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

English

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

Русский

Inf распределяется над симмDiff слева: a ∧ b Δ c = (a ∧ b) Δ (a ∧ c).

LaTeX

$$a ∧ b ∆ c = (a ∧ b) ∆ (a ∧ c)$$

Lean4

@[simp]
theorem le_symmDiff_iff_right : b ≤ a ∆ b ↔ Disjoint a b := by rw [symmDiff_comm, le_symmDiff_iff_left, disjoint_comm]

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

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

Разделы

Аффилиация

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