eq_iff_eq — Mathlib

English

On a set s, a and b are mapped to the same value by f if and only if a = b.

Русский

На множестве s пары a,b имеют одинаковое значение под f тогда и только тогда, когда a = b.

LaTeX

$$$hf : StrictAntiOn f s \\Rightarrow ∀ {a b}, a ∈ s → b ∈ s → f a = f b ↔ a = b$$$

Lean4

theorem eq_iff_eq (hf : StrictAntiOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) : f a = f b ↔ b = a :=
  (hf.dual_right.eq_iff_eq ha hb).trans eq_comm

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