bihimp_eq

Mathlib.Order.SymmDiff

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

English

The equality bihimp a b equals a ⊔ bᶜ ∧ b ⊔ aᶜ; i.e., a bihimp b = (a ∨ ¬b) ∧ (b ∨ ¬a).

Русский

Равенство bihimp a b равно (a ∨ ¬b) ∧ (b ∨ ¬a).

LaTeX

$$$ a \\Leftrightarrow b = (a \\lor \\neg b) \\land (b \\lor \\neg a) $$$

Lean4

theorem bihimp_eq : a ⇔ b = (a ⊔ bᶜ) ⊓ (b ⊔ aᶜ) := by simp only [(· ⇔ ·), himp_eq]

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

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

Разделы

Аффилиация

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