English
If r is a symmetric relation on α and f: α → β satisfies r(a,b) ⇒ f(a) ≤ f(b) for all a,b, then r(a,b) implies f(a) = f(b) for all a,b.
Русский
Если r — симметричное отношение на α и функция f: α → β удовлетворяет r(a,b) ⇒ f(a) ≤ f(b) для всех a,b, тогда при любых a,b из α выполняется r(a,b) ⇒ f(a) = f(b).
LaTeX
$$$ r(a,b) \to f(a) = f(b) \;\;\text{при условии }\; (\forall a,b\, r(a,b) \rightarrow f(a) \le f(b)) $$$
Lean4
/-- A symmetric relation implies two values are equal, when it implies they're less-equal. -/
theorem rel_imp_eq_of_rel_imp_le [PartialOrder β] (r : α → α → Prop) [IsSymm α r] {f : α → β}
(h : ∀ a b, r a b → f a ≤ f b) {a b : α} : r a b → f a = f b := fun hab ↦
le_antisymm (h a b hab) (h b a <| symm hab)
