beq_eq — Mathlib

English

For any a,b, if f is injective, then (f a == f b) = (a == b) for decidable equality types.

Русский

Пусть f инъективна; тогда для любых a,b выполняется (f a == f b) = (a == b).

LaTeX

$$$ (f a == f b) = (a == b) $$$

Lean4

theorem beq_eq {α β : Type*} [BEq α] [LawfulBEq α] [BEq β] [LawfulBEq β] {f : α → β} (I : Injective f) {a b : α} :
    (f a == f b) = (a == b) := by by_cases h : a == b <;> simp [h] <;> simpa [I.eq_iff] using h

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