lt_iff_gt — Mathlib

English

Let f: α → β be strictly antitone, with α a linear order and β a preorder. Then for all a,b ∈ α, f(a) < f(b) if and only if b < a.

Русский

Пусть f: α → β является строго антитоничной функцией, т.е. инвертирует порядок на линейном порядке α в предордер β. Тогда для любых a,b ∈ α выполняется f(a) < f(b) тогда и только тогда, когда b < a.

LaTeX

$$$ (StrictAnti\, f) \rightarrow \forall a,b,\ f(a)

Lean4

theorem lt_iff_gt (hf : StrictAnti f) {a b : α} : f a < f b ↔ b < a :=
  (hf.strictAntiOn Set.univ).lt_iff_gt trivial trivial

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