Skip to content

Commit 4c8b20b

Browse files
CoolRmalCoolRmal
committed
move
1 parent e23dee2 commit 4c8b20b

2 files changed

Lines changed: 170 additions & 32 deletions

File tree

‎Mathlib/Order/Filter/Extr.lean‎

Lines changed: 138 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -546,6 +546,144 @@ theorem IsMaxOn.max (hf : IsMaxOn f s a) (hg : IsMaxOn g s a) :
546546
IsMaxOn (fun x => max (f x) (g x)) s a :=
547547
IsMaxFilter.max hf hg
548548

549+
/-! ### Extrema from monotonicity and antitonicity -/
550+
551+
552+
variable {β : Type*} [LinearOrder α] [Preorder β] {a b c : α} {f : α → β}
553+
554+
/-- If `f` is monotone on `(a, b]` and antitone on `[b,c)`, then the maximum of `f` on `(a, c)` is
555+
attained at `b`. -/
556+
lemma isMaxOn_Ioo_of_mono_anti (h₀ : MonotoneOn f (Ioc a b)) (h₁ : AntitoneOn f (Ico b c)) :
557+
IsMaxOn f (Ioo a c) b := by
558+
intro x hx
559+
by_cases! g₀ : x ≤ b
560+
· exact h₀ ⟨hx.1, g₀⟩ (right_mem_Ioc.2 (g₀.trans_lt' hx.1)) g₀
561+
· refine h₁ (left_mem_Ico.2 (g₀.trans hx.2)) ⟨g₀.le, hx.2⟩ g₀.le
562+
563+
/-- If `f` is antitone on `(a, b]` and monotone on `[b,c)`, then the minimum of `f` on `(a, c)` is
564+
attained at `b`. -/
565+
lemma isMinOn_Ioo_of_anti_mono (h₀ : AntitoneOn f (Ioc a b)) (h₁ : MonotoneOn f (Ico b c)) :
566+
IsMinOn f (Ioo a c) b :=
567+
isMaxOn_Ioo_of_mono_anti (β := βᵒᵈ) h₀ h₁
568+
569+
/-- If `f` is monotone on `[a, b]` and antitone on `[b,c)`, then the maximum of `f` on `[a, c)` is
570+
attained at `b`. -/
571+
lemma isMaxOn_Ico_of_mono_anti
572+
(h₀ : MonotoneOn f (Icc a b))
573+
(h₁ : AntitoneOn f (Ico b c)) : IsMaxOn f (Ico a c) b := by
574+
intro x hx
575+
by_cases! g₀ : x ≤ b
576+
· exact h₀ ⟨hx.1, g₀⟩ (right_mem_Icc.2 (hx.1.trans g₀)) g₀
577+
· exact h₁ (left_mem_Ico.2 (g₀.trans hx.2)) ⟨g₀.le, hx.2⟩ g₀.le
578+
579+
/-- If `f` is antitone on `[a, b]` and monotone on `[b,c)`, then the minimum of `f` on `[a, c)` is
580+
attained at `b`. -/
581+
lemma isMinOn_Ico_of_anti_mono (h₀ : AntitoneOn f (Icc a b)) (h₁ : MonotoneOn f (Ico b c)) :
582+
IsMinOn f (Ico a c) b :=
583+
isMaxOn_Ico_of_mono_anti (β := βᵒᵈ) h₀ h₁
584+
585+
/-- If `f` is monotone on `(a, b]` and antitone on `[b,c]`, then the maximum of `f` on `(a, c]` is
586+
attained at `b`. -/
587+
lemma isMaxOn_Ioc_of_mono_anti (h₀ : MonotoneOn f (Ioc a b)) (h₁ : AntitoneOn f (Icc b c)) :
588+
IsMaxOn f (Ioc a c) b := by
589+
intro x hx
590+
by_cases! g₀ : x ≤ b
591+
· exact h₀ ⟨hx.1, g₀⟩ (right_mem_Ioc.2 (g₀.trans_lt' hx.1)) g₀
592+
· exact h₁ (left_mem_Icc.2 (g₀.le.trans hx.2)) ⟨g₀.le, hx.2⟩ g₀.le
593+
594+
/-- If `f` is monotone on `(a, b]` and antitone on `[b,c]`, then the maximum of `f` on `(a, c]` is
595+
attained at `b`. -/
596+
lemma isMinOn_Ioc_of_anti_mono (h₀ : AntitoneOn f (Ioc a b)) (h₁ : MonotoneOn f (Icc b c)) :
597+
IsMinOn f (Ioc a c) b :=
598+
isMaxOn_Ioc_of_mono_anti (β := βᵒᵈ) h₀ h₁
599+
600+
/-- If `f` is monotone on `[a, b]` and antitone on `[b,c]`, then the maximum of `f` on `[a, c]` is
601+
attained at `b`. -/
602+
lemma isMaxOn_Icc_of_mono_anti (h₀ : MonotoneOn f (Icc a b)) (h₁ : AntitoneOn f (Icc b c)) :
603+
IsMaxOn f (Icc a c) b := by
604+
intro x hx
605+
by_cases! g₀ : x ≤ b
606+
· exact h₀ ⟨hx.1, g₀⟩ (right_mem_Icc.2 (hx.1.trans g₀)) g₀
607+
· exact h₁ (left_mem_Icc.2 (g₀.le.trans hx.2)) ⟨g₀.le, hx.2⟩ g₀.le
608+
609+
/-- If `f` is antitone on `[a, b]` and monotone on `[b,c]`, then the minimum of `f` on `(a, c]` is
610+
attained at `b`. -/
611+
lemma isMinOn_Icc_of_anti_mono (h₀ : AntitoneOn f (Icc a b)) (h₁ : MonotoneOn f (Icc b c)) :
612+
IsMinOn f (Icc a c) b :=
613+
isMaxOn_Icc_of_mono_anti (β := βᵒᵈ) h₀ h₁
614+
615+
/-- If `f` is monotone on `(a, b]` and antitone on `[b,∞)`, then the maximum of `f` on `(a, ∞)` is
616+
attained at `b`. -/
617+
lemma isMaxOn_Ioi_of_mono_anti (h₀ : MonotoneOn f (Ioc a b)) (h₁ : AntitoneOn f (Ici b)) :
618+
IsMaxOn f (Ioi a) b := by
619+
intro x hx
620+
by_cases! g₀ : x ≤ b
621+
· exact h₀ ⟨hx, g₀⟩ (right_mem_Ioc.2 (g₀.trans_lt' hx)) g₀
622+
· exact h₁ self_mem_Ici g₀.le g₀.le
623+
624+
/-- If `f` is antitone on `(a, b]` and monotone on `[b,∞)`, then the minimum of `f` on `(a, ∞)` is
625+
attained at `b`. -/
626+
lemma isMinOn_Ioi_of_anti_mono (h₀ : AntitoneOn f (Ioc a b)) (h₁ : MonotoneOn f (Ici b)) :
627+
IsMinOn f (Ioi a) b :=
628+
isMaxOn_Ioi_of_mono_anti (β := βᵒᵈ) h₀ h₁
629+
630+
/-- If `f` is monotone on `[a, b]` and antitone on `[b,∞)`, then the maximum of `f` on `[a, ∞)` is
631+
attained at `b`. -/
632+
lemma isMaxOn_Ici_of_mono_anti (h₀ : MonotoneOn f (Icc a b)) (h₁ : AntitoneOn f (Ici b)) :
633+
IsMaxOn f (Ici a) b := by
634+
intro x hx
635+
by_cases! g₀ : x ≤ b
636+
· exact h₀ ⟨hx, g₀⟩ (right_mem_Icc.2 (hx.trans g₀)) g₀
637+
· exact h₁ self_mem_Ici g₀.le g₀.le
638+
639+
/-- If `f` is antitone on `(a, b]` and monotone on `[b,∞)`, then the minimum of `f` on `[a, ∞)` is
640+
attained at `b`. -/
641+
lemma isMinOn_Ici_of_anti_mono (h₀ : AntitoneOn f (Icc a b)) (h₁ : MonotoneOn f (Ici b)) :
642+
IsMinOn f (Ici a) b :=
643+
isMaxOn_Ici_of_mono_anti (β := βᵒᵈ) h₀ h₁
644+
645+
/-- If `f` is monotone on `(-∞, b]` and antitone on `[b,a)`, then the maximum of `f` on `(-∞, a)` is
646+
attained at `b`. -/
647+
lemma isMaxOn_Iio_of_mono_anti (h₀ : MonotoneOn f (Iic b)) (h₁ : AntitoneOn f (Ico b a)) :
648+
IsMaxOn f (Iio a) b := by
649+
intro x hx
650+
by_cases! g₀ : x ≤ b
651+
· exact h₀ g₀ self_mem_Iic g₀
652+
· exact h₁ (left_mem_Ico.2 (g₀.trans hx)) ⟨g₀.le, hx⟩ g₀.le
653+
654+
/-- If `f` is antitone on `(-∞, b]` and monotone on `[b,a)`, then the minimum of `f` on `(-∞, a)` is
655+
attained at `b`. -/
656+
lemma isMinOn_Iio_of_anti_mono (h₀ : AntitoneOn f (Iic b)) (h₁ : MonotoneOn f (Ico b a)) :
657+
IsMinOn f (Iio a) b :=
658+
isMaxOn_Iio_of_mono_anti (β := βᵒᵈ) h₀ h₁
659+
660+
/-- If `f` is monotone on `(-∞, b]` and antitone on `[b,a]`, then the maximum of
661+
`f` on `(-∞, a]` is attained at `b`. -/
662+
lemma isMaxOn_Iic_of_mono_anti (h₀ : MonotoneOn f (Iic b)) (h₁ : AntitoneOn f (Icc b a)) :
663+
IsMaxOn f (Iic a) b := by
664+
intro x hx
665+
by_cases! g₀ : x ≤ b
666+
· exact h₀ g₀ self_mem_Iic g₀
667+
· exact h₁ (left_mem_Icc.2 (g₀.le.trans hx)) ⟨g₀.le, hx⟩ g₀.le
668+
669+
/-- If `f` is antitone on `(-∞, b]` and monotone on `[b,a]`, then the minimum of `f` on `(-∞, a]` is
670+
attained at `b`. -/
671+
lemma isMinOn_Iic_of_anti_mono (h₀ : AntitoneOn f (Iic b)) (h₁ : MonotoneOn f (Icc b a)) :
672+
IsMinOn f (Iic a) b :=
673+
isMaxOn_Iic_of_mono_anti (β := βᵒᵈ) h₀ h₁
674+
675+
/-- If `f` is monotone on `(-∞, b]` and antitone on `[b,∞)`, then the maximum of `f` is attained
676+
at `b`. -/
677+
lemma isMaxOn_univ_of_mono_anti (h₀ : MonotoneOn f (Iic b)) (h₁ : AntitoneOn f (Ici b)) :
678+
IsMaxOn f univ b :=
679+
fun x _ => by rcases le_total x b <;> aesop
680+
681+
/-- If `f` is antitone on `(-∞, b]` and monotone on `[b,∞)`, then the minimum of `f` is attained
682+
at `b`. -/
683+
lemma isMinOn_univ_of_anti_mono (h₀ : AntitoneOn f (Iic b)) (h₁ : MonotoneOn f (Ici b)) :
684+
IsMinOn f univ b :=
685+
isMaxOn_univ_of_mono_anti (β := βᵒᵈ) h₀ h₁
686+
549687
end LinearOrder
550688

551689
section Eventually

‎Mathlib/Topology/Order/OrderClosedExtr.lean‎

Lines changed: 32 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,15 @@
11
/-
22
Copyright (c) 2024 Bjørn Kjos-Hanssen. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
4-
Authors: Bjørn Kjos-Hanssen, Patrick Massot, Yongxi Lin
4+
Authors: Bjørn Kjos-Hanssen, Patrick Massot
55
-/
66
module
77

88
public import Mathlib.Topology.Order.OrderClosed
99
public import Mathlib.Topology.Order.LocalExtr
1010

1111
/-!
12-
# Extrema from monotonicity and antitonicity
12+
# Local maxima from monotonicity and antitonicity
1313
1414
In this file we prove a lemma that is useful for the First Derivative Test in calculus,
1515
and its dual.
@@ -25,13 +25,13 @@ and its dual.
2525

2626
public section
2727

28-
open Set Topology Filter
28+
open Set
2929

3030
variable {α β : Type*} [LinearOrder α] [Preorder β] {s : Set α} {a b c : α} {f : α → β}
3131

3232
/-- If `f` is monotone on `(a, b]` and antitone on `[b,c)`, then the maximum of `f` on `(a, c)` is
3333
attained at `b`. -/
34-
lemma isMaxOn_of_mono_anti_Ioo (h₀ : MonotoneOn f (Ioc a b)) (h₁ : AntitoneOn f (Ico b c)) :
34+
lemma isMaxOn_Ioo_of_mono_anti (h₀ : MonotoneOn f (Ioc a b)) (h₁ : AntitoneOn f (Ico b c)) :
3535
IsMaxOn f (Ioo a c) b := by
3636
intro x hx
3737
by_cases! g₀ : x ≤ b
@@ -40,13 +40,13 @@ lemma isMaxOn_of_mono_anti_Ioo (h₀ : MonotoneOn f (Ioc a b)) (h₁ : AntitoneO
4040

4141
/-- If `f` is antitone on `(a, b]` and monotone on `[b,c)`, then the minimum of `f` on `(a, c)` is
4242
attained at `b`. -/
43-
lemma isMinOn_of_anti_mono_Ioo (h₀ : AntitoneOn f (Ioc a b)) (h₁ : MonotoneOn f (Ico b c)) :
43+
lemma isMinOn_Ioo_of_anti_mono (h₀ : AntitoneOn f (Ioc a b)) (h₁ : MonotoneOn f (Ico b c)) :
4444
IsMinOn f (Ioo a c) b :=
45-
isMaxOn_of_mono_anti_Ioo (β := βᵒᵈ) h₀ h₁
45+
isMaxOn_Ioo_of_mono_anti (β := βᵒᵈ) h₀ h₁
4646

4747
/-- If `f` is monotone on `[a, b]` and antitone on `[b,c)`, then the maximum of `f` on `[a, c)` is
4848
attained at `b`. -/
49-
lemma isMaxOn_of_mono_anti_Ico
49+
lemma isMaxOn_Ico_of_mono_anti
5050
(h₀ : MonotoneOn f (Icc a b))
5151
(h₁ : AntitoneOn f (Ico b c)) : IsMaxOn f (Ico a c) b := by
5252
intro x hx
@@ -56,13 +56,13 @@ lemma isMaxOn_of_mono_anti_Ico
5656

5757
/-- If `f` is antitone on `[a, b]` and monotone on `[b,c)`, then the minimum of `f` on `[a, c)` is
5858
attained at `b`. -/
59-
lemma isMinOn_of_anti_mono_Ico (h₀ : AntitoneOn f (Icc a b)) (h₁ : MonotoneOn f (Ico b c)) :
59+
lemma isMinOn_Ico_of_anti_mono (h₀ : AntitoneOn f (Icc a b)) (h₁ : MonotoneOn f (Ico b c)) :
6060
IsMinOn f (Ico a c) b :=
61-
isMaxOn_of_mono_anti_Ico (β := βᵒᵈ) h₀ h₁
61+
isMaxOn_Ico_of_mono_anti (β := βᵒᵈ) h₀ h₁
6262

6363
/-- If `f` is monotone on `(a, b]` and antitone on `[b,c]`, then the maximum of `f` on `(a, c]` is
6464
attained at `b`. -/
65-
lemma isMaxOn_of_mono_anti_Ioc (h₀ : MonotoneOn f (Ioc a b)) (h₁ : AntitoneOn f (Icc b c)) :
65+
lemma isMaxOn_Ioc_of_mono_anti (h₀ : MonotoneOn f (Ioc a b)) (h₁ : AntitoneOn f (Icc b c)) :
6666
IsMaxOn f (Ioc a c) b := by
6767
intro x hx
6868
by_cases! g₀ : x ≤ b
@@ -71,13 +71,13 @@ lemma isMaxOn_of_mono_anti_Ioc (h₀ : MonotoneOn f (Ioc a b)) (h₁ : AntitoneO
7171

7272
/-- If `f` is monotone on `(a, b]` and antitone on `[b,c]`, then the maximum of `f` on `(a, c]` is
7373
attained at `b`. -/
74-
lemma isMinOn_of_anti_mono_Ioc (h₀ : AntitoneOn f (Ioc a b)) (h₁ : MonotoneOn f (Icc b c)) :
74+
lemma isMinOn_Ioc_of_anti_mono (h₀ : AntitoneOn f (Ioc a b)) (h₁ : MonotoneOn f (Icc b c)) :
7575
IsMinOn f (Ioc a c) b :=
76-
isMaxOn_of_mono_anti_Ioc (β := βᵒᵈ) h₀ h₁
76+
isMaxOn_Ioc_of_mono_anti (β := βᵒᵈ) h₀ h₁
7777

7878
/-- If `f` is monotone on `[a, b]` and antitone on `[b,c]`, then the maximum of `f` on `[a, c]` is
7979
attained at `b`. -/
80-
lemma isMaxOn_of_mono_anti_Icc (h₀ : MonotoneOn f (Icc a b)) (h₁ : AntitoneOn f (Icc b c)) :
80+
lemma isMaxOn_Icc_of_mono_anti (h₀ : MonotoneOn f (Icc a b)) (h₁ : AntitoneOn f (Icc b c)) :
8181
IsMaxOn f (Icc a c) b := by
8282
intro x hx
8383
by_cases! g₀ : x ≤ b
@@ -86,13 +86,13 @@ lemma isMaxOn_of_mono_anti_Icc (h₀ : MonotoneOn f (Icc a b)) (h₁ : AntitoneO
8686

8787
/-- If `f` is antitone on `[a, b]` and monotone on `[b,c]`, then the minimum of `f` on `(a, c]` is
8888
attained at `b`. -/
89-
lemma isMinOn_of_anti_mono_Icc (h₀ : AntitoneOn f (Icc a b)) (h₁ : MonotoneOn f (Icc b c)) :
89+
lemma isMinOn_Icc_of_anti_mono (h₀ : AntitoneOn f (Icc a b)) (h₁ : MonotoneOn f (Icc b c)) :
9090
IsMinOn f (Icc a c) b :=
91-
isMaxOn_of_mono_anti_Icc (β := βᵒᵈ) h₀ h₁
91+
isMaxOn_Icc_of_mono_anti (β := βᵒᵈ) h₀ h₁
9292

9393
/-- If `f` is monotone on `(a, b]` and antitone on `[b,∞)`, then the maximum of `f` on `(a, ∞)` is
9494
attained at `b`. -/
95-
lemma isMaxOn_of_mono_anti_Ioi (h₀ : MonotoneOn f (Ioc a b)) (h₁ : AntitoneOn f (Ici b)) :
95+
lemma isMaxOn_Ioi_of_mono_anti (h₀ : MonotoneOn f (Ioc a b)) (h₁ : AntitoneOn f (Ici b)) :
9696
IsMaxOn f (Ioi a) b := by
9797
intro x hx
9898
by_cases! g₀ : x ≤ b
@@ -101,13 +101,13 @@ lemma isMaxOn_of_mono_anti_Ioi (h₀ : MonotoneOn f (Ioc a b)) (h₁ : AntitoneO
101101

102102
/-- If `f` is antitone on `(a, b]` and monotone on `[b,∞)`, then the minimum of `f` on `(a, ∞)` is
103103
attained at `b`. -/
104-
lemma isMinOn_of_anti_mono_Ioi (h₀ : AntitoneOn f (Ioc a b)) (h₁ : MonotoneOn f (Ici b)) :
104+
lemma isMinOn_Ioi_of_anti_mono (h₀ : AntitoneOn f (Ioc a b)) (h₁ : MonotoneOn f (Ici b)) :
105105
IsMinOn f (Ioi a) b :=
106-
isMaxOn_of_mono_anti_Ioi (β := βᵒᵈ) h₀ h₁
106+
isMaxOn_Ioi_of_mono_anti (β := βᵒᵈ) h₀ h₁
107107

108108
/-- If `f` is monotone on `[a, b]` and antitone on `[b,∞)`, then the maximum of `f` on `[a, ∞)` is
109109
attained at `b`. -/
110-
lemma isMaxOn_of_mono_anti_Ici (h₀ : MonotoneOn f (Icc a b)) (h₁ : AntitoneOn f (Ici b)) :
110+
lemma isMaxOn_Ici_of_mono_anti (h₀ : MonotoneOn f (Icc a b)) (h₁ : AntitoneOn f (Ici b)) :
111111
IsMaxOn f (Ici a) b := by
112112
intro x hx
113113
by_cases! g₀ : x ≤ b
@@ -116,13 +116,13 @@ lemma isMaxOn_of_mono_anti_Ici (h₀ : MonotoneOn f (Icc a b)) (h₁ : AntitoneO
116116

117117
/-- If `f` is antitone on `(a, b]` and monotone on `[b,∞)`, then the minimum of `f` on `[a, ∞)` is
118118
attained at `b`. -/
119-
lemma isMinOn_of_anti_mono_Ici (h₀ : AntitoneOn f (Icc a b)) (h₁ : MonotoneOn f (Ici b)) :
119+
lemma isMinOn_Ici_of_anti_mono (h₀ : AntitoneOn f (Icc a b)) (h₁ : MonotoneOn f (Ici b)) :
120120
IsMinOn f (Ici a) b :=
121-
isMaxOn_of_mono_anti_Ici (β := βᵒᵈ) h₀ h₁
121+
isMaxOn_Ici_of_mono_anti (β := βᵒᵈ) h₀ h₁
122122

123123
/-- If `f` is monotone on `(-∞, b]` and antitone on `[b,a)`, then the maximum of `f` on `(-∞, a)` is
124124
attained at `b`. -/
125-
lemma isMaxOn_of_mono_anti_Iio (h₀ : MonotoneOn f (Iic b)) (h₁ : AntitoneOn f (Ico b a)) :
125+
lemma isMaxOn_Iio_of_mono_anti (h₀ : MonotoneOn f (Iic b)) (h₁ : AntitoneOn f (Ico b a)) :
126126
IsMaxOn f (Iio a) b := by
127127
intro x hx
128128
by_cases! g₀ : x ≤ b
@@ -131,13 +131,13 @@ lemma isMaxOn_of_mono_anti_Iio (h₀ : MonotoneOn f (Iic b)) (h₁ : AntitoneOn
131131

132132
/-- If `f` is antitone on `(-∞, b]` and monotone on `[b,a)`, then the minimum of `f` on `(-∞, a)` is
133133
attained at `b`. -/
134-
lemma isMinOn_of_anti_mono_Iio (h₀ : AntitoneOn f (Iic b)) (h₁ : MonotoneOn f (Ico b a)) :
134+
lemma isMinOn_Iio_of_anti_mono (h₀ : AntitoneOn f (Iic b)) (h₁ : MonotoneOn f (Ico b a)) :
135135
IsMinOn f (Iio a) b :=
136-
isMaxOn_of_mono_anti_Iio (β := βᵒᵈ) h₀ h₁
136+
isMaxOn_Iio_of_mono_anti (β := βᵒᵈ) h₀ h₁
137137

138138
/-- If `f` is monotone on `(-∞, b]` and antitone on `[b,a]`, then the maximum of
139139
`f` on `(-∞, a]` is attained at `b`. -/
140-
lemma isMaxOn_of_mono_anti_Iic (h₀ : MonotoneOn f (Iic b)) (h₁ : AntitoneOn f (Icc b a)) :
140+
lemma isMaxOn_Iic_of_mono_anti (h₀ : MonotoneOn f (Iic b)) (h₁ : AntitoneOn f (Icc b a)) :
141141
IsMaxOn f (Iic a) b := by
142142
intro x hx
143143
by_cases! g₀ : x ≤ b
@@ -146,21 +146,21 @@ lemma isMaxOn_of_mono_anti_Iic (h₀ : MonotoneOn f (Iic b)) (h₁ : AntitoneOn
146146

147147
/-- If `f` is antitone on `(-∞, b]` and monotone on `[b,a]`, then the minimum of `f` on `(-∞, a]` is
148148
attained at `b`. -/
149-
lemma isMinOn_of_anti_mono_Iic (h₀ : AntitoneOn f (Iic b)) (h₁ : MonotoneOn f (Icc b a)) :
149+
lemma isMinOn_Iic_of_anti_mono (h₀ : AntitoneOn f (Iic b)) (h₁ : MonotoneOn f (Icc b a)) :
150150
IsMinOn f (Iic a) b :=
151-
isMaxOn_of_mono_anti_Iic (β := βᵒᵈ) h₀ h₁
151+
isMaxOn_Iic_of_mono_anti (β := βᵒᵈ) h₀ h₁
152152

153153
/-- If `f` is monotone on `(-∞, b]` and antitone on `[b,∞)`, then the maximum of `f` is attained
154154
at `b`. -/
155-
lemma isMaxOn_of_mono_anti_univ (h₀ : MonotoneOn f (Iic b)) (h₁ : AntitoneOn f (Ici b)) :
155+
lemma isMaxOn_univ_of_mono_anti (h₀ : MonotoneOn f (Iic b)) (h₁ : AntitoneOn f (Ici b)) :
156156
IsMaxOn f univ b :=
157157
fun x _ => by rcases le_total x b <;> aesop
158158

159159
/-- If `f` is antitone on `(-∞, b]` and monotone on `[b,∞)`, then the minimum of `f` is attained
160160
at `b`. -/
161-
lemma isMinOn_of_anti_mono_univ (h₀ : AntitoneOn f (Iic b)) (h₁ : MonotoneOn f (Ici b)) :
161+
lemma isMinOn_univ_of_anti_mono (h₀ : AntitoneOn f (Iic b)) (h₁ : MonotoneOn f (Ici b)) :
162162
IsMinOn f univ b :=
163-
isMaxOn_of_mono_anti_univ (β := βᵒᵈ) h₀ h₁
163+
isMaxOn_univ_of_mono_anti (β := βᵒᵈ) h₀ h₁
164164

165165
/-- If `f` is monotone on `(a,b]` and antitone on `[b,c)` then `f` has
166166
a local maximum at `b`. -/
@@ -170,12 +170,12 @@ lemma isLocalMax_of_mono_anti
170170
{a b c : α} (g₀ : a < b) (g₁ : b < c) {f : α → β}
171171
(h₀ : MonotoneOn f (Ioc a b))
172172
(h₁ : AntitoneOn f (Ico b c)) : IsLocalMax f b :=
173-
isLocalMax_of_mono_anti' (Ioc_mem_nhdsLE g₀) (Ico_mem_nhdsGE g₁) h₀ h₁
173+
(isMaxOn_Ioo_of_mono_anti h₀ h₁).isLocalMax (Ioo_mem_nhds g₀ g₁)
174174

175175
/-- If `f` is antitone on `(a,b]` and monotone on `[b,c)` then `f` has
176176
a local minimum at `b`. -/
177177
lemma isLocalMin_of_anti_mono
178178
{α : Type*} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α]
179179
{β : Type*} [Preorder β] {a b c : α} (g₀ : a < b) (g₁ : b < c) {f : α → β}
180180
(h₀ : AntitoneOn f (Ioc a b)) (h₁ : MonotoneOn f (Ico b c)) : IsLocalMin f b :=
181-
mem_of_superset (Ioo_mem_nhds g₀ g₁) (fun x hx => by rcases le_total x b <;> aesop)
181+
isLocalMax_of_mono_anti (β := βᵒᵈ) g₀ g₁ h₀ h₁

0 commit comments

Comments
 (0)