homOfElement_eq_iff — Mathlib

English

For any X, and x,y ∈ X, homOfElement x = homOfElement y if and only if x = y.

Русский

Для любого множества X и элементов x,y ∈ X: homOfElement x = homOfElement y тогда и только тогда, когда x = y.

LaTeX

$$$$ homOfElement(x) = homOfElement(y) \iff x = y. $$$$

Lean4

theorem homOfElement_eq_iff {X : Type u} (x y : X) : homOfElement x = homOfElement y ↔ x = y :=
  ⟨fun H => congr_fun H PUnit.unit, by simp_all⟩

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