iff_left_comm — Mathlib

English

For propositions a, b, c, the left commutativity of ↔ distributes: (a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c)).

Русский

Для высказываний a, b, c выполняется слева коммутативность: (a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c)).

LaTeX

$$$ (a \leftrightarrow (b \leftrightarrow c)) \leftrightarrow (b \leftrightarrow (a \leftrightarrow c)) $$$

Lean4

theorem iff_left_comm {a b c : Prop} : (a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c)) := by tauto

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