disjoint_symmDiff_inf

Mathlib.Order.SymmDiff

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

English

The symmetric difference of a and b is disjoint from their meet: Disjoint (a Δ b) (a ∧ b).

Русский

Симметрическая разность a и b несоприкасается с их пересечением: Disjoint (a Δ b) (a ∧ b).

LaTeX

$$Disjoint (bihimp) (Inf) (a Δ b) (a ∧ b)$$

Lean4

theorem disjoint_symmDiff_inf : Disjoint (a ∆ b) (a ⊓ b) :=
  by
  rw [symmDiff_eq_sup_sdiff_inf]
  exact disjoint_sdiff_self_left

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

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

Разделы

Аффилиация

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