symmDiff_eq_top

Mathlib.Order.SymmDiff

URI: https://scilib.ai/kg/mathlib#IsCompl.symmDiff_eq_top

English

IsCompl implies symmetric difference with its second argument is top.

Русский

IsCompl подразумевает, что симметрическая разность с двумя аргументами даёт топ.

LaTeX

$$IsCompl a b \Rightarrow a \Delta b = \top$$

Lean4

theorem symmDiff_eq_top {a b : α} (h : IsCompl a b) : a ∆ b = ⊤ := by rw [h.eq_hnot, hnot_symmDiff_self]

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

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

Разделы

Аффилиация

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