bihimp_assoc

Mathlib.Order.SymmDiff

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

English

bihimp is associative: bihimp(bihimp a b) c = bihimp a bihimp b c.

Русский

Согласование bihimp: bihimp(bihimp a b) c = bihimp a(bihimp b c).

LaTeX

$$$ bihimp(bihimp(a,b), c) = bihimp(a, bihimp(b,c)) $$$

Lean4

theorem bihimp_assoc : a ⇔ b ⇔ c = a ⇔ (b ⇔ c) :=
  @symmDiff_assoc αᵒᵈ _ _ _ _

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

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

Разделы

Аффилиация

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