beq_eq_beq — Mathlib

English

For any a1,a2 ∈ α and b1,b2 ∈ β, the boolean tests (a1 == a2) and (b1 == b2) are equal exactly when a1 = a2 iff b1 = b2.

Русский

Для любых a1,a2 ∈ α и b1,b2 ∈ β булевы тесты (a1 == a2) и (b1 == b2) равны тогда и только тогда, когда a1 = a2 ⇔ b1 = b2.

LaTeX

$$$ (a_1 == a_2) = (b_1 == b_2) \;\Longleftrightarrow\; (a_1 = a_2 \;\Leftrightarrow\; b_1 = b_2) $$$

Lean4

@[simp]
theorem beq_eq_beq {α β : Type*} [BEq α] [LawfulBEq α] [BEq β] [LawfulBEq β] {a₁ a₂ : α} {b₁ b₂ : β} :
    (a₁ == a₂) = (b₁ == b₂) ↔ (a₁ = a₂ ↔ b₁ = b₂) := by rw [Bool.eq_iff_iff]; simp

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