We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 555c501 commit d83ff13Copy full SHA for d83ff13
1 file changed
Mathlib/Order/WellFounded.lean
@@ -236,7 +236,7 @@ alias StrictAnti.range_inj := StrictAnti.range_inj_of_wellFoundedGT
236
237
/-- A strictly monotone function `f` on a well-order satisfies `x ≤ f x` for all `x`. -/
238
@[to_dual le_id
239
-/-- A strictly monotone function `f` on a cowell-order satisfies `f x ≤ x` for all `x`. -/]
+/-- A strictly monotone function `f` on a co-well-order satisfies `f x ≤ x` for all `x`. -/]
240
theorem StrictMono.id_le [WellFoundedLT β] {f : β → β} (hf : StrictMono f) : id ≤ f := by
241
rw [Pi.le_def]
242
by_contra! H
0 commit comments