bihimp_snd — Mathlib

English

The second projection of bihimp on a pair equals the biconditional of the second projections: (a ⇔ b).2 = a.2 ⇔ b.2.

Русский

Вторая проекция bihimp равна биэквиваленции вторых проекций: (a ⇔ b).2 = a.2 ⇔ b.2.

LaTeX

$$$ (a \Leftrightarrow b).2 = a.2 \Leftrightarrow b.2 $$$

Lean4

@[simp]
theorem bihimp_snd [GeneralizedHeytingAlgebra α] [GeneralizedHeytingAlgebra β] (a b : α × β) : (a ⇔ b).2 = a.2 ⇔ b.2 :=
  rfl

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