bihimp_bihimp_bihimp_comm — Mathlib

English

For all a, b, c, d in a Boolean algebra, bihimp(bihimp a b, bihimp c d) = bihimp(bihimp a c, bihimp b d).

Русский

Для всех a, b, c, d в булевой алгебре: bihimp(bihimp(a, b), bihimp(c, d)) = bihimp(bihimp(a, c), bihimp(b, d)).

LaTeX

$$$ \operatorname{bihimp}(\operatorname{bihimp}(a, b), \operatorname{bihimp}(c, d)) = \operatorname{bihimp}(\operatorname{bihimp}(a, c), \operatorname{bihimp}(b, d)) $$$

Lean4

theorem bihimp_bihimp_bihimp_comm : a ⇔ b ⇔ (c ⇔ d) = a ⇔ c ⇔ (b ⇔ d) := by simp_rw [bihimp_assoc, bihimp_left_comm]

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