eq_iff_eq_cancel_right — Mathlib

English

For any type α and elements a,b ∈ α, the statement that ∀ c, a = c ↔ b = c holds is equivalent to a = b.

Русский

Для типа α и элементов a,b ∈ α, условие ∀ c, a = c ↔ b = c эквивалентно a = b.

LaTeX

$$$ (\\forall c:\\alpha, a = c \\leftrightarrow b = c) \\;\\iff\\; a = b. $$$

Lean4

@[simp]
theorem eq_iff_eq_cancel_right {a b : α} : (∀ {c}, a = c ↔ b = c) ↔ a = b :=
  ⟨fun h ↦ by rw [h], fun h a ↦ by rw [h]⟩

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