le_apply — Mathlib

English

Under a well-founded LT, a strictly monotone function f satisfies x ≤ f x for all x.

Русский

При хорошо основанном LT справедливо, что строго монотонная функция удовлетворяет x ≤ f(x) для всех x.

LaTeX

$$$[\\text{WellFoundedLT }\\beta] \\Rightarrow \\text{StrictMono } f \\Rightarrow \\forall x,\\; x \\le f(x)$$$

Lean4

theorem le_apply [WellFoundedLT β] {f : β → β} (hf : StrictMono f) {x} : x ≤ f x :=
  hf.id_le x

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