apply_le — Mathlib

English

For a strictly monotone f on a type with a well-founded LT, the range of f is not bounded above.

Русский

Для строго монотонной f на типе с хорошо основанным порядком верхняя граница диапазона f отсутствует.

LaTeX

$$$\\text{StrictMono } f \\Rightarrow \\neg \\mathrm{BddAbove}(\\mathrm{Set.range}\\;f)$ under [WellFoundedLT].$$

Lean4

theorem apply_le [WellFoundedGT β] {f : β → β} (hf : StrictMono f) {x} : f x ≤ x :=
  StrictMono.le_apply (β := βᵒᵈ) hf.dual

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