le_id — Mathlib

English

A strictly monotone function on a cowell-order satisfies f ≤ id; i.e., f reversely bounded by identity.

Русский

Строго монотонная функция на обратном порядке удовлетворяет f ≤ id.

LaTeX

$$$\\text{StrictMono } f \\Rightarrow f \\leq \\mathrm{id}$ на cowell-order β$$

Lean4

/-- A strictly monotone function `f` on a cowell-order satisfies `f x ≤ x` for all `x`. -/
theorem le_id [WellFoundedGT β] {f : β → β} (hf : StrictMono f) : f ≤ id :=
  StrictMono.id_le (β := βᵒᵈ) hf.dual

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