le_of_le — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem le_of_le (h : MinimalFor P f i) (hj : P j) (hji : f j ≤ f i) : f i ≤ f j :=
  h.2 hj hji

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