le_of_le — Mathlib

English

If i is MaximalFor P f i, and j satisfies P, and f(i) ≤ f(j), then f(j) ≤ f(i).

Русский

Если i максимально для P f i, и j удовлетворяет P, и f(i) ≤ f(j), тогда f(j) ≤ f(i).

LaTeX

$$$\\\\forall i \\\\forall j \\\\,( \\\\operatorname{MaximalFor}(P,f,i) \\\\land P(j) \\\\land f(i) \\\\le f(j) ) \\\\Rightarrow f(j) \\\\le f(i).$$$

Lean4

theorem le_of_le (h : MaximalFor P f i) (hj : P j) (hij : f i ≤ f j) : f j ≤ f i :=
  h.2 hj hij

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