From 198ed6bb101dee3c9af9a6b5bfb80fdd8f359978 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Thu, 18 Nov 2021 12:48:11 +0000 Subject: [PATCH] doc(order/monotone): fix 2 typos (#10377) --- src/order/monotone.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/order/monotone.lean b/src/order/monotone.lean index 465ef99e64777..5d45b91789625 100644 --- a/src/order/monotone.lean +++ b/src/order/monotone.lean @@ -70,11 +70,11 @@ def monotone (f : α → β) : Prop := ∀ ⦃a b⦄, a ≤ b → f a ≤ f b /-- A function `f` is antitone if `a ≤ b` implies `f b ≤ f a`. -/ def antitone (f : α → β) : Prop := ∀ ⦃a b⦄, a ≤ b → f b ≤ f a -/-- A function `f` is monotone on `s` if, for all `a, b ∈ s`, `a ≤ b` implies `f b ≤ f a`. -/ +/-- A function `f` is monotone on `s` if, for all `a, b ∈ s`, `a ≤ b` implies `f a ≤ f b`. -/ def monotone_on (f : α → β) (s : set α) : Prop := ∀ ⦃a⦄ (ha : a ∈ s) ⦃b⦄ (hb : b ∈ s), a ≤ b → f a ≤ f b -/-- A function `f` is antitone on `s` if, for all `a, b ∈ s`, `a ≤ b` implies `f a ≤ f b`. -/ +/-- A function `f` is antitone on `s` if, for all `a, b ∈ s`, `a ≤ b` implies `f b ≤ f a`. -/ def antitone_on (f : α → β) (s : set α) : Prop := ∀ ⦃a⦄ (ha : a ∈ s) ⦃b⦄ (hb : b ∈ s), a ≤ b → f b ≤ f a