English
If f is strictly antitone on a set S, then for all a,b ∈ S and any ordering o, o.Compares (f a) (f b) ↔ o.Compares b a.
Русский
Если f строго антимонотонна на множестве S, то для любых a,b ∈ S и любого упорядочения o выполняется: o.Сравнивает f(a) и f(b) тогда и только тогда, когда b ещё больше a по порядку.
LaTeX
$$$ (hf : StrictAntiOn f s) \rightarrow \forall a \in s, \forall b \in s, \forall o : Ordering, o.Compares (f a) (f b) \leftrightarrow o.Compares b a $$$
Lean4
protected theorem compares (hf : StrictAntiOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) {o : Ordering} :
o.Compares (f a) (f b) ↔ o.Compares b a :=
toDual_compares_toDual.trans <| hf.dual_right.compares hb ha
