sup_himp_bihimp

Mathlib.Order.SymmDiff

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

English

For any a,b, the implication from a ∨ b to bihimp(a,b) equals bihimp(a,b); i.e., (a ∨ b) → (a ⇔ b) = a ⇔ b.

Русский

Для любых a,b импликация (a ∨ b) → bihimp(a,b) равна bihimp(a,b).

LaTeX

$$$\operatorname{himp}(a \lor b, \operatorname{bihimp}(a,b)) = \operatorname{bihimp}(a,b)$$$

Lean4

@[simp]
theorem sup_himp_bihimp : a ⊔ b ⇨ a ⇔ b = a ⇔ b := by
  rw [himp_bihimp]
  simp [bihimp]

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

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

Разделы

Аффилиация

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