bihimp_fst — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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