id_le — Mathlib

English

A strictly monotone function on a well-order satisfies x ≤ f x for all x.

Русский

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

LaTeX

$$$\\forall x,\\; x \\le f(x)$ в рамках WellFoundedLT β и StrictMono f$$

Lean4

/-- A strictly monotone function `f` on a well-order satisfies `x ≤ f x` for all `x`. -/
theorem id_le [WellFoundedLT β] {f : β → β} (hf : StrictMono f) : id ≤ f :=
  by
  rw [Pi.le_def]
  by_contra! H
  obtain ⟨m, hm, hm'⟩ := wellFounded_lt.has_min _ H
  exact hm' _ (hf hm) hm

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