Loogle!

Result

Found 308 declarations mentioning MonotoneOn. Of these, only the first 200 are shown.

• MonotoneOn 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] (f : α → β) (s : Set α) : Prop
• monotoneOn_id 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} [Preorder α] {s : Set α} : MonotoneOn id s
• monotoneOn_const 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {c : β} {s : Set α} : MonotoneOn (fun x => c) s
• monotoneOn_univ 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} : MonotoneOn f Set.univ ↔ Monotone f
• Monotone.monotoneOn 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : Monotone f) (s : Set α) : MonotoneOn f s
• StrictMonoOn.monotoneOn 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] {f : α → β} {s : Set α} (hf : StrictMonoOn f s) : MonotoneOn f s
• Antitone.comp_antitoneOn 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} (hg : Antitone g) (hf : AntitoneOn f s) : MonotoneOn (g ∘ f) s
• Antitone.comp_monotoneOn 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} (hg : Antitone g) (hf : MonotoneOn f s) : AntitoneOn (g ∘ f) s
• Monotone.comp_monotoneOn 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} (hg : Monotone g) (hf : MonotoneOn f s) : MonotoneOn (g ∘ f) s
• AntitoneOn.comp 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} {t : Set β} (hg : AntitoneOn g t) (hf : AntitoneOn f s) (hs : Set.MapsTo f s t) : MonotoneOn (g ∘ f) s
• AntitoneOn.comp_MonotoneOn 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} {t : Set β} (hg : AntitoneOn g t) (hf : MonotoneOn f s) (hs : Set.MapsTo f s t) : AntitoneOn (g ∘ f) s
• MonotoneOn.comp 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} {t : Set β} (hg : MonotoneOn g t) (hf : MonotoneOn f s) (hs : Set.MapsTo f s t) : MonotoneOn (g ∘ f) s
• MonotoneOn.comp_AntitoneOn 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} {t : Set β} (hg : MonotoneOn g t) (hf : AntitoneOn f s) (hs : Set.MapsTo f s t) : AntitoneOn (g ∘ f) s
• instDecidableMonotoneOnOfForallForallMemSetForallForallForallLe 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} [i : Decidable (∀ a ∈ s, ∀ b ∈ s, a ≤ b → f a ≤ f b)] : Decidable (MonotoneOn f s)
• monotoneOn_iff_forall_lt 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] {f : α → β} {s : Set α} : MonotoneOn f s ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a < b → f a ≤ f b
• MonotoneOn.reflect_lt 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} {s : Set α} (hf : MonotoneOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) (h : f a < f b) : a < b
• MonotoneOn.strictMonoOn_of_injOn 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [PartialOrder β] {f : α → β} {s : Set α} (hmono : MonotoneOn f s) (hinj : Set.InjOn f s) : StrictMonoOn f s
• monotone_add_nat_iff_monotoneOn_nat_Ici 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} [Preorder α] {f : ℕ → α} {k : ℕ} : (Monotone fun n => f (n + k)) ↔ MonotoneOn f {x | k ≤ x}
• MonotoneOn.strictMonoOn_iff_injOn 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [LinearOrder α] [PartialOrder β] {f : α → β} {s : Set α} (hf : MonotoneOn f s) : StrictMonoOn f s ↔ Set.InjOn f s
• monotoneOn_nat_Ici_of_le_succ 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} [Preorder α] {f : ℕ → α} {k : ℕ} (hf : ∀ n ≥ k, f n ≤ f (n + 1)) : MonotoneOn f {x | k ≤ x}
• Nat.pow_monotoneOn 📋 Mathlib.Order.Monotone.Basic
  : MonotoneOn (fun p => p.1 ^ p.2) {p | p.1 ≠ 0}
• AntitoneOn.dual_right 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : AntitoneOn f s → MonotoneOn (⇑OrderDual.toDual ∘ f) s
• MonotoneOn.dual_right 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : MonotoneOn f s → AntitoneOn (⇑OrderDual.toDual ∘ f) s
• antitoneOn_toDual_comp_iff 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : AntitoneOn (⇑OrderDual.toDual ∘ f) s ↔ MonotoneOn f s
• monotoneOn_toDual_comp_iff 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : MonotoneOn (⇑OrderDual.toDual ∘ f) s ↔ AntitoneOn f s
• AntitoneOn.dual_left 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : AntitoneOn f s → MonotoneOn (f ∘ ⇑OrderDual.ofDual) s
• MonotoneOn.dual_left 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : MonotoneOn f s → AntitoneOn (f ∘ ⇑OrderDual.ofDual) s
• antitoneOn_comp_ofDual_iff 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : AntitoneOn (f ∘ ⇑OrderDual.ofDual) s ↔ MonotoneOn f s
• monotoneOn_comp_ofDual_iff 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : MonotoneOn (f ∘ ⇑OrderDual.ofDual) s ↔ AntitoneOn f s
• MonotoneOn.dual 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : MonotoneOn f s → MonotoneOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s
• monotoneOn_dual_iff 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : MonotoneOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s ↔ MonotoneOn f s
• MonotoneOn.inf 📋 Mathlib.Order.Lattice
  {α : Type u} {β : Type v} [Preorder α] [SemilatticeInf β] {f g : α → β} {s : Set α} (hf : MonotoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (f ⊓ g) s
• MonotoneOn.sup 📋 Mathlib.Order.Lattice
  {α : Type u} {β : Type v} [Preorder α] [SemilatticeSup β] {f g : α → β} {s : Set α} (hf : MonotoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (f ⊔ g) s
• MonotoneOn.of_map_inf 📋 Mathlib.Order.Lattice
  {α : Type u} {β : Type v} {f : α → β} {s : Set α} [SemilatticeInf α] [SemilatticeInf β] (h : ∀ x ∈ s, ∀ y ∈ s, f (x ⊓ y) = f x ⊓ f y) : MonotoneOn f s
• MonotoneOn.of_map_sup 📋 Mathlib.Order.Lattice
  {α : Type u} {β : Type v} {f : α → β} {s : Set α} [SemilatticeSup α] [SemilatticeSup β] (h : ∀ x ∈ s, ∀ y ∈ s, f (x ⊔ y) = f x ⊔ f y) : MonotoneOn f s
• MonotoneOn.map_inf 📋 Mathlib.Order.Lattice
  {α : Type u} {β : Type v} {f : α → β} {s : Set α} {x y : α} [LinearOrder α] [SemilatticeInf β] (hf : MonotoneOn f s) (hx : x ∈ s) (hy : y ∈ s) : f (min x y) = f x ⊓ f y
• MonotoneOn.map_sup 📋 Mathlib.Order.Lattice
  {α : Type u} {β : Type v} {f : α → β} {s : Set α} {x y : α} [LinearOrder α] [SemilatticeSup β] (hf : MonotoneOn f s) (hx : x ∈ s) (hy : y ∈ s) : f (max x y) = f x ⊔ f y
• MonotoneOn.max 📋 Mathlib.Order.Lattice
  {α : Type u} {β : Type v} [Preorder α] [LinearOrder β] {f g : α → β} {s : Set α} (hf : MonotoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (fun x => max (f x) (g x)) s
• MonotoneOn.min 📋 Mathlib.Order.Lattice
  {α : Type u} {β : Type v} [Preorder α] [LinearOrder β] {f g : α → β} {s : Set α} (hf : MonotoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (fun x => min (f x) (g x)) s
• Set.Subsingleton.monotoneOn 📋 Mathlib.Data.Set.Subsingleton
  {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] (f : α → β) (h : s.Subsingleton) : MonotoneOn f s
• Set.monotoneOn_singleton 📋 Mathlib.Data.Set.Subsingleton
  {α : Type u} {β : Type v} {a : α} [Preorder α] [Preorder β] (f : α → β) : MonotoneOn f {a}
• MonotoneOn.set_prod 📋 Mathlib.Data.Set.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} [Preorder α] {f : α → Set β} {g : α → Set γ} (hf : MonotoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (fun x => f x ×ˢ g x) s
• MonotoneOn.map_max 📋 Mathlib.Order.MinMax
  {α : Type u} {β : Type v} [LinearOrder α] [LinearOrder β] {f : α → β} {s : Set α} {a b : α} (hf : MonotoneOn f s) (ha : a ∈ s) (hb : b ∈ s) : f (max a b) = max (f a) (f b)
• MonotoneOn.map_min 📋 Mathlib.Order.MinMax
  {α : Type u} {β : Type v} [LinearOrder α] [LinearOrder β] {f : α → β} {s : Set α} {a b : α} (hf : MonotoneOn f s) (ha : a ∈ s) (hb : b ∈ s) : f (min a b) = min (f a) (f b)
• MonotoneOn.add_const 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : β → α} {s : Set β} [AddRightMono α] (hf : MonotoneOn f s) (a : α) : MonotoneOn (fun x => f x + a) s
• MonotoneOn.const_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : β → α} {s : Set β} [AddLeftMono α] (hf : MonotoneOn f s) (a : α) : MonotoneOn (fun x => a + f x) s
• MonotoneOn.const_mul' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : β → α} {s : Set β} [MulLeftMono α] (hf : MonotoneOn f s) (a : α) : MonotoneOn (fun x => a * f x) s
• MonotoneOn.mul_const' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : β → α} {s : Set β} [MulRightMono α] (hf : MonotoneOn f s) (a : α) : MonotoneOn (fun x => f x * a) s
• MonotoneOn.add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f g : β → α} {s : Set β} [AddLeftMono α] [AddRightMono α] (hf : MonotoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (fun x => f x + g x) s
• MonotoneOn.add_strictMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {s : Set β} [AddLeftStrictMono α] [AddRightMono α] {f g : β → α} (hf : MonotoneOn f s) (hg : StrictMonoOn g s) : StrictMonoOn (fun x => f x + g x) s
• MonotoneOn.mul' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f g : β → α} {s : Set β} [MulLeftMono α] [MulRightMono α] (hf : MonotoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (fun x => f x * g x) s
• MonotoneOn.mul_strictMono' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {s : Set β} [MulLeftStrictMono α] [MulRightMono α] {f g : β → α} (hf : MonotoneOn f s) (hg : StrictMonoOn g s) : StrictMonoOn (fun x => f x * g x) s
• StrictMonoOn.add_monotone 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f g : β → α} {s : Set β} [AddLeftMono α] [AddRightStrictMono α] (hf : StrictMonoOn f s) (hg : MonotoneOn g s) : StrictMonoOn (fun x => f x + g x) s
• StrictMonoOn.mul_monotone' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f g : β → α} {s : Set β} [MulLeftMono α] [MulRightStrictMono α] (hf : StrictMonoOn f s) (hg : MonotoneOn g s) : StrictMonoOn (fun x => f x * g x) s
• AntitoneOn.inv 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} {β : Type u_1} [Group α] [Preorder α] [MulLeftMono α] [MulRightMono α] [Preorder β] {f : β → α} {s : Set β} (hf : AntitoneOn f s) : MonotoneOn (fun x => (f x)⁻¹) s
• AntitoneOn.neg 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [AddLeftMono α] [AddRightMono α] [Preorder β] {f : β → α} {s : Set β} (hf : AntitoneOn f s) : MonotoneOn (fun x => -f x) s
• MonotoneOn.inv 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} {β : Type u_1} [Group α] [Preorder α] [MulLeftMono α] [MulRightMono α] [Preorder β] {f : β → α} {s : Set β} (hf : MonotoneOn f s) : AntitoneOn (fun x => (f x)⁻¹) s
• MonotoneOn.neg 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [AddLeftMono α] [AddRightMono α] [Preorder β] {f : β → α} {s : Set β} (hf : MonotoneOn f s) : AntitoneOn (fun x => -f x) s
• pow_left_monotoneOn 📋 Mathlib.Algebra.Order.GroupWithZero.Basic
  {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {n : ℕ} [PosMulMono M₀] [MulPosMono M₀] : MonotoneOn (fun a => a ^ n) {x | 0 ≤ x}
• MonotoneOn.mul 📋 Mathlib.Algebra.Order.GroupWithZero.Basic
  {α : Type u_1} {M₀ : Type u_2} [Mul M₀] [Zero M₀] [Preorder M₀] [Preorder α] {f g : α → M₀} [PosMulMono M₀] [MulPosMono M₀] {s : Set α} (hf : MonotoneOn f s) (hg : MonotoneOn g s) (hf₀ : ∀ x ∈ s, 0 ≤ f x) (hg₀ : ∀ x ∈ s, 0 ≤ g x) : MonotoneOn (f * g) s
• zpow_left_monoOn₀ 📋 Mathlib.Algebra.Order.GroupWithZero.Basic
  {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] [MulPosMono G₀] {n : ℤ} (hn : 0 ≤ n) : MonotoneOn (fun a => a ^ n) {a | 0 ≤ a}
• constant_of_monotoneOn_antitoneOn 📋 Mathlib.Order.Directed
  {α : Type u_1} {β : Type u_2} [PartialOrder β] [Preorder α] {f : α → β} {s : Set α} (hf : MonotoneOn f s) (hf' : AntitoneOn f s) (hs : DirectedOn (fun x1 x2 => x1 ≤ x2) s) ⦃a : α⦄ : a ∈ s → ∀ ⦃b : α⦄, b ∈ s → f a = f b
• MonotoneOn.congr 📋 Mathlib.Data.Set.Monotone
  {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β} [Preorder α] [Preorder β] (h₁ : MonotoneOn f₁ s) (h : Set.EqOn f₁ f₂ s) : MonotoneOn f₂ s
• MonotoneOn.mono 📋 Mathlib.Data.Set.Monotone
  {α : Type u_1} {β : Type u_2} {s s₂ : Set α} {f : α → β} [Preorder α] [Preorder β] (h : MonotoneOn f s) (h' : s₂ ⊆ s) : MonotoneOn f s₂
• Set.EqOn.congr_monotoneOn 📋 Mathlib.Data.Set.Monotone
  {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β} [Preorder α] [Preorder β] (h : Set.EqOn f₁ f₂ s) : MonotoneOn f₁ s ↔ MonotoneOn f₂ s
• MonotoneOn.monotone 📋 Mathlib.Data.Set.Monotone
  {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} [Preorder α] [Preorder β] (h : MonotoneOn f s) : Monotone (f ∘ Subtype.val)
• Function.monotoneOn_of_rightInvOn_of_mapsTo 📋 Mathlib.Data.Set.Monotone
  {α : Type u_1} {β : Type u_2} [PartialOrder α] [LinearOrder β] {φ : β → α} {ψ : α → β} {t : Set β} {s : Set α} (hφ : MonotoneOn φ t) (φψs : Set.RightInvOn ψ φ s) (ψts : Set.MapsTo ψ s t) : MonotoneOn ψ s
• Set.monotoneOn_insert_iff 📋 Mathlib.Data.Set.Monotone
  {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} [Preorder α] [Preorder β] {a : α} : MonotoneOn f (insert a s) ↔ (∀ b ∈ s, b ≤ a → f b ≤ f a) ∧ (∀ b ∈ s, a ≤ b → f a ≤ f b) ∧ MonotoneOn f s
• MonotoneOn.map_isGreatest 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {t : Set α} {a : α} (Hf : MonotoneOn f t) (Ha : IsGreatest t a) : IsGreatest (f '' t) (f a)
• MonotoneOn.map_isLeast 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {t : Set α} {a : α} (Hf : MonotoneOn f t) (Ha : IsLeast t a) : IsLeast (f '' t) (f a)
• MonotoneOn.map_bddAbove 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s t : Set α} (Hf : MonotoneOn f t) (Hst : s ⊆ t) : (upperBounds s ∩ t).Nonempty → BddAbove (f '' s)
• MonotoneOn.map_bddBelow 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s t : Set α} (Hf : MonotoneOn f t) (Hst : s ⊆ t) : (lowerBounds s ∩ t).Nonempty → BddBelow (f '' s)
• MonotoneOn.image_lowerBounds_subset_lowerBounds_image 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s t : Set α} (Hf : MonotoneOn f t) (Hst : s ⊆ t) : f '' (lowerBounds s ∩ t) ⊆ lowerBounds (f '' s)
• MonotoneOn.image_upperBounds_subset_upperBounds_image 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s t : Set α} (Hf : MonotoneOn f t) (Hst : s ⊆ t) : f '' (upperBounds s ∩ t) ⊆ upperBounds (f '' s)
• MonotoneOn.mem_lowerBounds_image_self 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {t : Set α} {a : α} (Hf : MonotoneOn f t) : a ∈ lowerBounds t → a ∈ t → f a ∈ lowerBounds (f '' t)
• MonotoneOn.mem_upperBounds_image_self 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {t : Set α} {a : α} (Hf : MonotoneOn f t) : a ∈ upperBounds t → a ∈ t → f a ∈ upperBounds (f '' t)
• MonotoneOn.mem_lowerBounds_image 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s t : Set α} {a : α} (Hf : MonotoneOn f t) (Hst : s ⊆ t) (Has : a ∈ lowerBounds s) (Hat : a ∈ t) : f a ∈ lowerBounds (f '' s)
• MonotoneOn.mem_upperBounds_image 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s t : Set α} {a : α} (Hf : MonotoneOn f t) (Hst : s ⊆ t) (Has : a ∈ upperBounds s) (Hat : a ∈ t) : f a ∈ upperBounds (f '' s)
• MonotoneOn.sInf_image_Icc 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} [Preorder α] [ConditionallyCompleteLattice β] {f : α → β} {a b : α} (hab : a ≤ b) (h' : MonotoneOn f (Set.Icc a b)) : sInf (f '' Set.Icc a b) = f a
• MonotoneOn.sSup_image_Icc 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} [Preorder α] [ConditionallyCompleteLattice β] {f : α → β} {a b : α} (hab : b ≤ a) (h' : MonotoneOn f (Set.Icc b a)) : sSup (f '' Set.Icc b a) = f a
• MonotoneOn.map_csInf 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} [WellFoundedLT α] {β : Type u_5} [ConditionallyCompleteLattice β] {f : α → β} (hf : MonotoneOn f s) (hs : s.Nonempty) : f (sInf s) = sInf (f '' s)
• MonotoneOn.map_csSup 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} [WellFoundedGT α] {β : Type u_5} [ConditionallyCompleteLattice β] {f : α → β} (hf : MonotoneOn f s) (hs : s.Nonempty) : f (sSup s) = sSup (f '' s)
• MonotoneOn.csInf_eq_of_subset_of_forall_exists_le 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} [Preorder α] [ConditionallyCompleteLattice β] {f : α → β} {s t : Set α} (ht : BddBelow (f '' t)) (hf : MonotoneOn f t) (hst : s ⊆ t) (h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y) : sInf (f '' s) = sInf (f '' t)
• MonotoneOn.csSup_eq_of_subset_of_forall_exists_le 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} [Preorder α] [ConditionallyCompleteLattice β] {f : α → β} {s t : Set α} (ht : BddAbove (f '' t)) (hf : MonotoneOn f t) (hst : s ⊆ t) (h : ∀ y ∈ t, ∃ x ∈ s, y ≤ x) : sSup (f '' s) = sSup (f '' t)
• Set.monotoneOn_iff_monotone 📋 Mathlib.Data.Set.Order
  {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] {f : α → β} : MonotoneOn f s ↔ Monotone fun a => f ↑a
• MonotoneOn.inter 📋 Mathlib.Data.Set.Order
  {α : Type u_1} {β : Type u_2} [Preorder β] {f g : β → Set α} {s : Set β} (hf : MonotoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (fun x => f x ∩ g x) s
• MonotoneOn.union 📋 Mathlib.Data.Set.Order
  {α : Type u_1} {β : Type u_2} [Preorder β] {f g : β → Set α} {s : Set β} (hf : MonotoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (fun x => f x ∪ g x) s
• Set.not_monotoneOn_not_antitoneOn_iff_exists_le_le 📋 Mathlib.Data.Set.Order
  {α : Type u} {β : Type v} {s : Set α} [LinearOrder α] [LinearOrder β] {f : α → β} : ¬MonotoneOn f s ∧ ¬AntitoneOn f s ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
• Set.not_monotoneOn_not_antitoneOn_iff_exists_lt_lt 📋 Mathlib.Data.Set.Order
  {α : Type u} {β : Type v} {s : Set α} [LinearOrder α] [LinearOrder β] {f : α → β} : ¬MonotoneOn f s ∧ ¬AntitoneOn f s ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a < b ∧ b < c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
• MonotoneOn.mapsTo_Ici 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a : α} (h : MonotoneOn f (Set.Ici a)) : Set.MapsTo f (Set.Ici a) (Set.Ici (f a))
• MonotoneOn.mapsTo_Iic 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {b : α} (h : MonotoneOn f (Set.Iic b)) : Set.MapsTo f (Set.Iic b) (Set.Iic (f b))
• MonotoneOn.image_Ici_subset 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a : α} (h : MonotoneOn f (Set.Ici a)) : f '' Set.Ici a ⊆ Set.Ici (f a)
• MonotoneOn.image_Iic_subset 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {b : α} (h : MonotoneOn f (Set.Iic b)) : f '' Set.Iic b ⊆ Set.Iic (f b)
• MonotoneOn.mapsTo_Icc 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a b : α} (h : MonotoneOn f (Set.Icc a b)) : Set.MapsTo f (Set.Icc a b) (Set.Icc (f a) (f b))
• MonotoneOn.image_Icc_subset 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a b : α} (h : MonotoneOn f (Set.Icc a b)) : f '' Set.Icc a b ⊆ Set.Icc (f a) (f b)
• MonotoneOn.mapsTo_uIcc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [Lattice β] {f : α → β} {a b : α} (hf : MonotoneOn f (Set.uIcc a b)) : Set.MapsTo f (Set.uIcc a b) (Set.uIcc (f a) (f b))
• MonotoneOn.image_uIcc_subset 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [Lattice β] {f : α → β} {a b : α} (hf : MonotoneOn f (Set.uIcc a b)) : f '' Set.uIcc a b ⊆ Set.uIcc (f a) (f b)
• Set.monotoneOn_or_antitoneOn_iff_uIcc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {f : α → β} {s : Set α} : MonotoneOn f s ∨ AntitoneOn f s ↔ ∀ a ∈ s, ∀ b ∈ s, ∀ c ∈ s, c ∈ Set.uIcc a b → f c ∈ Set.uIcc (f a) (f b)
• IsAntichain.of_monotoneOn_strictAntiOn 📋 Mathlib.Order.Antichain
  {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {f : α → β} {s : Set α} (hf : MonotoneOn f s) (hf' : StrictAntiOn f s) : IsAntichain (fun x1 x2 => x1 ≤ x2) s
• Set.OrdConnected.preimage_monotoneOn 📋 Mathlib.Order.Interval.Set.OrdConnected
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : β → α} {t : Set β} {s : Set α} (hs : s.OrdConnected) (hf : MonotoneOn f t) : ∃ u, u.OrdConnected ∧ t ∩ f ⁻¹' s = t ∩ u
• AddConstMapClass.monotone_iff_Icc 📋 Mathlib.Algebra.AddConstMap.Basic
  {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H] [AddConstMapClass F G H a b] {f : F} (ha : 0 < a) (l : G) : Monotone ⇑f ↔ MonotoneOn (⇑f) (Set.Icc l (l + a))
• Set.IsPWO.image_of_monotoneOn 📋 Mathlib.Order.WellFoundedSet
  {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {s : Set α} (hs : s.IsPWO) {f : α → β} (hf : MonotoneOn f s) : (f '' s).IsPWO
• monotoneOn_of_le_succ 📋 Mathlib.Order.SuccPred.Archimedean
  {α : Type u_3} {β : Type u_4} [PartialOrder α] [Preorder β] [SuccOrder α] [IsSuccArchimedean α] {s : Set α} {f : α → β} (hs : s.OrdConnected) (hf : ∀ (a : α), ¬IsMax a → a ∈ s → Order.succ a ∈ s → f a ≤ f (Order.succ a)) : MonotoneOn f s
• monotoneOn_of_pred_le 📋 Mathlib.Order.SuccPred.Archimedean
  {α : Type u_3} {β : Type u_4} [PartialOrder α] [Preorder β] [PredOrder α] [IsPredArchimedean α] {s : Set α} {f : α → β} (hs : s.OrdConnected) (hf : ∀ (a : α), ¬IsMin a → a ∈ s → Order.pred a ∈ s → f (Order.pred a) ≤ f a) : MonotoneOn f s
• monotoneOn_of_le_add_one 📋 Mathlib.Algebra.Order.SuccPred
  {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] [Add α] [One α] [SuccAddOrder α] [IsSuccArchimedean α] {s : Set α} {f : α → β} (hs : s.OrdConnected) : (∀ (a : α), ¬IsMax a → a ∈ s → a + 1 ∈ s → f a ≤ f (a + 1)) → MonotoneOn f s
• monotoneOn_of_sub_one_le 📋 Mathlib.Algebra.Order.SuccPred
  {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] [Sub α] [One α] [PredSubOrder α] [IsPredArchimedean α] {s : Set α} {f : α → β} (hs : s.OrdConnected) : (∀ (a : α), ¬IsMin a → a ∈ s → a - 1 ∈ s → f (a - 1) ≤ f a) → MonotoneOn f s
• Cardinal.toNat_monotoneOn 📋 Mathlib.SetTheory.Cardinal.ToNat
  : MonotoneOn (⇑Cardinal.toNat) (Set.Iio Cardinal.aleph0)
• MonotoneOn.finsetProd' 📋 Mathlib.Algebra.Order.BigOperators.Group.Finset
  {ι : Type u_1} {N : Type u_5} [CommMonoid N] [Preorder N] {s : Finset ι} [MulLeftMono N] {γ : Type u_8} [Preorder γ] {u : Set γ} {f : ι → γ → N} (hf : ∀ i ∈ s, MonotoneOn (f i) u) : MonotoneOn (fun x => ∏ i ∈ s, f i x) u
• MonotoneOn.finsetSum 📋 Mathlib.Algebra.Order.BigOperators.Group.Finset
  {ι : Type u_1} {N : Type u_5} [AddCommMonoid N] [Preorder N] {s : Finset ι} [AddLeftMono N] {γ : Type u_8} [Preorder γ] {u : Set γ} {f : ι → γ → N} (hf : ∀ i ∈ s, MonotoneOn (f i) u) : MonotoneOn (fun x => ∑ i ∈ s, f i x) u
• MonotoneOn.finsetProd 📋 Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
  {ι : Type u_1} {R : Type u_2} [CommMonoidWithZero R] [Preorder R] [ZeroLEOneClass R] [PosMulMono R] {s : Finset ι} {γ : Type u_3} [Preorder γ] {u : Set γ} {f : ι → γ → R} (hf : ∀ i ∈ s, MonotoneOn (f i) u) (hf₀ : ∀ i ∈ s, ∀ x ∈ u, 0 ≤ f i x) : MonotoneOn (fun x => ∏ i ∈ s, f i x) u
• Finite.map_iInf_of_monotoneOn 📋 Mathlib.Data.Fintype.Order
  {α : Type u_1} {β : Type u_2} {ι : Type u_3} [ConditionallyCompleteLinearOrder α] [ConditionallyCompleteLattice β] [Finite ι] [Nonempty ι] {s : Set α} {f : ι → α} {g : α → β} (hg : MonotoneOn g s) (hs : ∀ (i : ι), f i ∈ s) : g (⨅ i, f i) = ⨅ i, g (f i)
• Finite.map_iSup_of_monotoneOn 📋 Mathlib.Data.Fintype.Order
  {α : Type u_1} {β : Type u_2} {ι : Type u_3} [ConditionallyCompleteLinearOrder α] [ConditionallyCompleteLattice β] [Finite ι] [Nonempty ι] {s : Set α} {f : ι → α} {g : α → β} (hg : MonotoneOn g s) (hs : ∀ (i : ι), f i ∈ s) : g (⨆ i, f i) = ⨆ i, g (f i)
• Filter.HasBasis.prod_same_index_mono 📋 Mathlib.Order.Filter.Bases.Basic
  {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {ι : Type u_5} [LinearOrder ι] {p : ι → Prop} {sa : ι → Set α} {sb : ι → Set β} (hla : la.HasBasis p sa) (hlb : lb.HasBasis p sb) (hsa : MonotoneOn sa {i | p i}) (hsb : MonotoneOn sb {i | p i}) : (la ×ˢ lb).HasBasis p fun i => sa i ×ˢ sb i
• isMaxOn_univ_of_mono_anti 📋 Mathlib.Order.Filter.Extr
  {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {b : α} {f : α → β} (h₀ : MonotoneOn f (Set.Iic b)) (h₁ : AntitoneOn f (Set.Ici b)) : IsMaxOn f Set.univ b
• isMinOn_univ_of_anti_mono 📋 Mathlib.Order.Filter.Extr
  {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {b : α} {f : α → β} (h₀ : AntitoneOn f (Set.Iic b)) (h₁ : MonotoneOn f (Set.Ici b)) : IsMinOn f Set.univ b
• isMaxOn_Ici_of_mono_anti 📋 Mathlib.Order.Filter.Extr
  {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {a b : α} {f : α → β} (h₀ : MonotoneOn f (Set.Icc a b)) (h₁ : AntitoneOn f (Set.Ici b)) : IsMaxOn f (Set.Ici a) b
• isMaxOn_Iic_of_mono_anti 📋 Mathlib.Order.Filter.Extr
  {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {a b : α} {f : α → β} (h₀ : MonotoneOn f (Set.Iic b)) (h₁ : AntitoneOn f (Set.Icc b a)) : IsMaxOn f (Set.Iic a) b
• isMaxOn_Iio_of_mono_anti 📋 Mathlib.Order.Filter.Extr
  {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {a b : α} {f : α → β} (h₀ : MonotoneOn f (Set.Iic b)) (h₁ : AntitoneOn f (Set.Ico b a)) : IsMaxOn f (Set.Iio a) b
• isMaxOn_Ioi_of_mono_anti 📋 Mathlib.Order.Filter.Extr
  {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {a b : α} {f : α → β} (h₀ : MonotoneOn f (Set.Ioc a b)) (h₁ : AntitoneOn f (Set.Ici b)) : IsMaxOn f (Set.Ioi a) b
• isMinOn_Ici_of_anti_mono 📋 Mathlib.Order.Filter.Extr
  {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {a b : α} {f : α → β} (h₀ : AntitoneOn f (Set.Icc a b)) (h₁ : MonotoneOn f (Set.Ici b)) : IsMinOn f (Set.Ici a) b
• isMinOn_Iic_of_anti_mono 📋 Mathlib.Order.Filter.Extr
  {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {a b : α} {f : α → β} (h₀ : AntitoneOn f (Set.Iic b)) (h₁ : MonotoneOn f (Set.Icc b a)) : IsMinOn f (Set.Iic a) b
• isMinOn_Iio_of_anti_mono 📋 Mathlib.Order.Filter.Extr
  {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {a b : α} {f : α → β} (h₀ : AntitoneOn f (Set.Iic b)) (h₁ : MonotoneOn f (Set.Ico b a)) : IsMinOn f (Set.Iio a) b
• isMinOn_Ioi_of_anti_mono 📋 Mathlib.Order.Filter.Extr
  {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {a b : α} {f : α → β} (h₀ : AntitoneOn f (Set.Ioc a b)) (h₁ : MonotoneOn f (Set.Ici b)) : IsMinOn f (Set.Ioi a) b
• isMaxOn_Icc_of_mono_anti 📋 Mathlib.Order.Filter.Extr
  {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {a b c : α} {f : α → β} (h₀ : MonotoneOn f (Set.Icc a b)) (h₁ : AntitoneOn f (Set.Icc b c)) : IsMaxOn f (Set.Icc a c) b
• isMaxOn_Ico_of_mono_anti 📋 Mathlib.Order.Filter.Extr
  {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {a b c : α} {f : α → β} (h₀ : MonotoneOn f (Set.Icc a b)) (h₁ : AntitoneOn f (Set.Ico b c)) : IsMaxOn f (Set.Ico a c) b
• isMaxOn_Ioc_of_mono_anti 📋 Mathlib.Order.Filter.Extr
  {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {a b c : α} {f : α → β} (h₀ : MonotoneOn f (Set.Ioc a b)) (h₁ : AntitoneOn f (Set.Icc b c)) : IsMaxOn f (Set.Ioc a c) b
• isMaxOn_Ioo_of_mono_anti 📋 Mathlib.Order.Filter.Extr
  {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {a b c : α} {f : α → β} (h₀ : MonotoneOn f (Set.Ioc a b)) (h₁ : AntitoneOn f (Set.Ico b c)) : IsMaxOn f (Set.Ioo a c) b
• isMinOn_Icc_of_anti_mono 📋 Mathlib.Order.Filter.Extr
  {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {a b c : α} {f : α → β} (h₀ : AntitoneOn f (Set.Icc a b)) (h₁ : MonotoneOn f (Set.Icc b c)) : IsMinOn f (Set.Icc a c) b
• isMinOn_Ico_of_anti_mono 📋 Mathlib.Order.Filter.Extr
  {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {a b c : α} {f : α → β} (h₀ : AntitoneOn f (Set.Icc a b)) (h₁ : MonotoneOn f (Set.Ico b c)) : IsMinOn f (Set.Ico a c) b
• isMinOn_Ioc_of_anti_mono 📋 Mathlib.Order.Filter.Extr
  {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {a b c : α} {f : α → β} (h₀ : AntitoneOn f (Set.Ioc a b)) (h₁ : MonotoneOn f (Set.Icc b c)) : IsMinOn f (Set.Ioc a c) b
• isMinOn_Ioo_of_anti_mono 📋 Mathlib.Order.Filter.Extr
  {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {a b c : α} {f : α → β} (h₀ : AntitoneOn f (Set.Ioc a b)) (h₁ : MonotoneOn f (Set.Ico b c)) : IsMinOn f (Set.Ioo a c) b
• isClosed_monotoneOn 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] [Preorder β] {s : Set β} : IsClosed {f | MonotoneOn f s}
• monotoneOn_of_frequently_monotoneOn_of_tendsto 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] {ι : Type u_1} {l : Filter ι} [Preorder β] {F : ι → β → α} {f : β → α} {s : Set β} (hF : ∃ᶠ (i : ι) in l, MonotoneOn (F i) s) (hlim : ∀ x ∈ s, Filter.Tendsto (fun i => F i x) l (nhds (f x))) : MonotoneOn f s
• isLocalMax_of_mono_anti' 📋 Mathlib.Topology.Order.LocalExtr
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] {β : Type u_2} [Preorder β] {b : α} {f : α → β} {a : Set α} (ha : a ∈ nhdsWithin b (Set.Iic b)) {c : Set α} (hc : c ∈ nhdsWithin b (Set.Ici b)) (h₀ : MonotoneOn f a) (h₁ : AntitoneOn f c) : IsLocalMax f b
• isLocalMin_of_anti_mono' 📋 Mathlib.Topology.Order.LocalExtr
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] {β : Type u_2} [Preorder β] {b : α} {f : α → β} {a : Set α} (ha : a ∈ nhdsWithin b (Set.Iic b)) {c : Set α} (hc : c ∈ nhdsWithin b (Set.Ici b)) (h₀ : AntitoneOn f a) (h₁ : MonotoneOn f c) : IsLocalMin f b
• monotoneOn_descPochhammer_eval 📋 Mathlib.RingTheory.Polynomial.Pochhammer
  {S : Type u_1} [Ring S] [PartialOrder S] [IsStrictOrderedRing S] (n : ℕ) : MonotoneOn (fun x => Polynomial.eval x (descPochhammer S n)) (Set.Ici (↑n - 1))
• IsGLB.isGLB_of_tendsto 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} {s : Set α} {a : α} {b : γ} (hf : MonotoneOn f s) : IsGLB s a → s.Nonempty → Filter.Tendsto f (nhdsWithin a s) (nhds b) → IsGLB (f '' s) b
• IsLUB.isLUB_of_tendsto 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} {s : Set α} {a : α} {b : γ} (hf : MonotoneOn f s) (ha : IsLUB s a) (hs : s.Nonempty) (hb : Filter.Tendsto f (nhdsWithin a s) (nhds b)) : IsLUB (f '' s) b
• IsGLB.mem_lowerBounds_of_tendsto 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} {s : Set α} {a : α} {b : γ} (hf : MonotoneOn f s) (ha : IsGLB s a) (hb : Filter.Tendsto f (nhdsWithin a s) (nhds b)) : b ∈ lowerBounds (f '' s)
• IsLUB.mem_upperBounds_of_tendsto 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} {s : Set α} {a : α} {b : γ} (hf : MonotoneOn f s) (ha : IsLUB s a) (hb : Filter.Tendsto f (nhdsWithin a s) (nhds b)) : b ∈ upperBounds (f '' s)
• MonotoneOn.countable_not_continuousWithinAt 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] {s : Set α} {f : α → β} [TopologicalSpace β] [OrderTopology β] [SecondCountableTopology β] (hf : MonotoneOn f s) : {x | x ∈ s ∧ ¬ContinuousWithinAt f s x}.Countable
• MonotoneOn.countable_not_continuousWithinAt_Iio 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] {s : Set α} {f : α → β} [TopologicalSpace β] [OrderTopology β] [SecondCountableTopology β] (hf : MonotoneOn f s) : {x | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Set.Iio x) x}.Countable
• MonotoneOn.countable_not_continuousWithinAt_Ioi 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] {s : Set α} {f : α → β} [TopologicalSpace β] [OrderTopology β] [SecondCountableTopology β] (hf : MonotoneOn f s) : {x | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Set.Ioi x) x}.Countable
• MonotoneOn.countable_setOfPred_two_preimages 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] {s : Set α} {f : α → β} [SecondCountableTopology α] (hf : MonotoneOn f s) : {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}.Countable
• MonotoneOn.countable_setOf_two_preimages 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] {s : Set α} {f : α → β} [SecondCountableTopology α] (hf : MonotoneOn f s) : {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}.Countable
• MonotoneOn.insert_of_continuousWithinAt 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] {s : Set α} {x : α} {f : α → β} [TopologicalSpace β] [OrderClosedTopology β] (hf : MonotoneOn f s) (hx : ClusterPt x (Filter.principal s)) (h'x : ContinuousWithinAt f s x) : MonotoneOn f (insert x s)
• MonotoneOn.map_csInf_of_continuousWithinAt 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {A : Set α} (Cf : ContinuousWithinAt f A (sInf A)) (Mf : MonotoneOn f A) (A_nonemp : A.Nonempty) (A_bdd : BddBelow A := by bddDefault) : f (sInf A) = sInf (f '' A)
• MonotoneOn.map_csSup_of_continuousWithinAt 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {A : Set α} (Cf : ContinuousWithinAt f A (sSup A)) (Mf : MonotoneOn f A) (A_nonemp : A.Nonempty) (A_bdd : BddAbove A := by bddDefault) : f (sSup A) = sSup (f '' A)
• MonotoneOn.tendsto_nhdsGT 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_3} {β : Type u_4} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {x : α} (Mf : MonotoneOn f (Set.Ioi x)) (h_bdd : BddBelow (f '' Set.Ioi x)) : Filter.Tendsto f (nhdsWithin x (Set.Ioi x)) (nhds (sInf (f '' Set.Ioi x)))
• MonotoneOn.tendsto_nhdsLT 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_3} {β : Type u_4} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {x : α} (Mf : MonotoneOn f (Set.Iio x)) (h_bdd : BddAbove (f '' Set.Iio x)) : Filter.Tendsto f (nhdsWithin x (Set.Iio x)) (nhds (sSup (f '' Set.Iio x)))
• MonotoneOn.tendsto_nhdsWithin_Ioo_left 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_3} {β : Type u_4} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {x y : α} (h_nonempty : (Set.Ioo y x).Nonempty) (Mf : MonotoneOn f (Set.Ioo y x)) (h_bdd : BddAbove (f '' Set.Ioo y x)) : Filter.Tendsto f (nhdsWithin x (Set.Iio x)) (nhds (sSup (f '' Set.Ioo y x)))
• MonotoneOn.tendsto_nhdsWithin_Ioo_right 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_3} {β : Type u_4} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {x y : α} (h_nonempty : (Set.Ioo x y).Nonempty) (Mf : MonotoneOn f (Set.Ioo x y)) (h_bdd : BddBelow (f '' Set.Ioo x y)) : Filter.Tendsto f (nhdsWithin x (Set.Ioi x)) (nhds (sInf (f '' Set.Ioo x y)))
• MonotoneOn.map_sInf_of_continuousWithinAt 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_1} {β : Type u_2} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α} (Cf : ContinuousWithinAt f s (sInf s)) (Mf : MonotoneOn f s) (ftop : f ⊤ = ⊤) : f (sInf s) = sInf (f '' s)
• MonotoneOn.map_sSup_of_continuousWithinAt 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_1} {β : Type u_2} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α} (Cf : ContinuousWithinAt f s (sSup s)) (Mf : MonotoneOn f s) (fbot : f ⊥ = ⊥) : f (sSup s) = sSup (f '' s)
• ContinuousOn.image_uIcc_of_monotoneOn 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} {f : α → δ} (hf : ContinuousOn f (Set.uIcc a b)) (hmono : MonotoneOn f (Set.uIcc a b)) : f '' Set.uIcc a b = Set.uIcc (f a) (f b)
• ContinuousOn.image_Icc_of_monotoneOn 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} {f : α → δ} (hab : a ≤ b) (hf : ContinuousOn f (Set.Icc a b)) (hmono : MonotoneOn f (Set.Icc a b)) : f '' Set.Icc a b = Set.Icc (f a) (f b)
• ContinuousOn.image_Ici_of_monotoneOn 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a : α} {f : α → δ} (hf : ContinuousOn f (Set.Ici a)) (hmono : MonotoneOn f (Set.Ici a)) (htop : Filter.Tendsto f Filter.atTop Filter.atTop) : f '' Set.Ici a = Set.Ici (f a)
• ContinuousOn.image_Iic_of_monotoneOn 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a : α} {f : α → δ} (hf : ContinuousOn f (Set.Iic a)) (hmono : MonotoneOn f (Set.Iic a)) (hbot : Filter.Tendsto f Filter.atBot Filter.atBot) : f '' Set.Iic a = Set.Iic (f a)
• continuousAt_of_monotoneOn_of_image_mem_nhds 📋 Mathlib.Topology.Order.MonotoneContinuity
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : α → β} {s : Set α} {a : α} (h_mono : MonotoneOn f s) (hs : s ∈ nhds a) (hfs : f '' s ∈ nhds (f a)) : ContinuousAt f a
• continuousAt_of_monotoneOn_of_closure_image_mem_nhds 📋 Mathlib.Topology.Order.MonotoneContinuity
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : α → β} {s : Set α} {a : α} (h_mono : MonotoneOn f s) (hs : s ∈ nhds a) (hfs : closure (f '' s) ∈ nhds (f a)) : ContinuousAt f a
• continuousWithinAt_left_of_monotoneOn_of_image_mem_nhdsWithin 📋 Mathlib.Topology.Order.MonotoneContinuity
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : α → β} {s : Set α} {a : α} (h_mono : MonotoneOn f s) (hs : s ∈ nhdsWithin a (Set.Iic a)) (hfs : f '' s ∈ nhdsWithin (f a) (Set.Iic (f a))) : ContinuousWithinAt f (Set.Iic a) a
• continuousWithinAt_right_of_monotoneOn_of_image_mem_nhdsWithin 📋 Mathlib.Topology.Order.MonotoneContinuity
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : α → β} {s : Set α} {a : α} (h_mono : MonotoneOn f s) (hs : s ∈ nhdsWithin a (Set.Ici a)) (hfs : f '' s ∈ nhdsWithin (f a) (Set.Ici (f a))) : ContinuousWithinAt f (Set.Ici a) a
• continuousWithinAt_left_of_monotoneOn_of_closure_image_mem_nhdsWithin 📋 Mathlib.Topology.Order.MonotoneContinuity
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : α → β} {s : Set α} {a : α} (hf : MonotoneOn f s) (hs : s ∈ nhdsWithin a (Set.Iic a)) (hfs : closure (f '' s) ∈ nhdsWithin (f a) (Set.Iic (f a))) : ContinuousWithinAt f (Set.Iic a) a
• continuousWithinAt_right_of_monotoneOn_of_closure_image_mem_nhdsWithin 📋 Mathlib.Topology.Order.MonotoneContinuity
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : α → β} {s : Set α} {a : α} (h_mono : MonotoneOn f s) (hs : s ∈ nhdsWithin a (Set.Ici a)) (hfs : closure (f '' s) ∈ nhdsWithin (f a) (Set.Ici (f a))) : ContinuousWithinAt f (Set.Ici a) a
• continuousWithinAt_left_of_monotoneOn_of_exists_between 📋 Mathlib.Topology.Order.MonotoneContinuity
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {s : Set α} {a : α} (hf : MonotoneOn f s) (hs : s ∈ nhdsWithin a (Set.Iic a)) (hfs : ∀ b < f a, ∃ c ∈ s, f c ∈ Set.Ioo b (f a)) : ContinuousWithinAt f (Set.Iic a) a
• continuousWithinAt_right_of_monotoneOn_of_exists_between 📋 Mathlib.Topology.Order.MonotoneContinuity
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {s : Set α} {a : α} (h_mono : MonotoneOn f s) (hs : s ∈ nhdsWithin a (Set.Ici a)) (hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Set.Ioo (f a) b) : ContinuousWithinAt f (Set.Ici a) a
• continuousAt_of_monotoneOn_of_exists_between 📋 Mathlib.Topology.Order.MonotoneContinuity
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {s : Set α} {a : α} (h_mono : MonotoneOn f s) (hs : s ∈ nhds a) (hfs_l : ∀ b < f a, ∃ c ∈ s, f c ∈ Set.Ioo b (f a)) (hfs_r : ∀ b > f a, ∃ c ∈ s, f c ∈ Set.Ioo (f a) b) : ContinuousAt f a
• AntitoneOn.Ici 📋 Mathlib.Order.Interval.Set.Monotone
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} (hf : AntitoneOn f s) : MonotoneOn (fun x => Set.Ici (f x)) s
• AntitoneOn.Ioi 📋 Mathlib.Order.Interval.Set.Monotone
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} (hf : AntitoneOn f s) : MonotoneOn (fun x => Set.Ioi (f x)) s
• MonotoneOn.Ici 📋 Mathlib.Order.Interval.Set.Monotone
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} (hf : MonotoneOn f s) : AntitoneOn (fun x => Set.Ici (f x)) s
• MonotoneOn.Iic 📋 Mathlib.Order.Interval.Set.Monotone
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} (hf : MonotoneOn f s) : MonotoneOn (fun x => Set.Iic (f x)) s
• MonotoneOn.Iio 📋 Mathlib.Order.Interval.Set.Monotone
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} (hf : MonotoneOn f s) : MonotoneOn (fun x => Set.Iio (f x)) s
• MonotoneOn.Ioi 📋 Mathlib.Order.Interval.Set.Monotone
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} (hf : MonotoneOn f s) : AntitoneOn (fun x => Set.Ioi (f x)) s
• AntitoneOn.Icc 📋 Mathlib.Order.Interval.Set.Monotone
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f g : α → β} {s : Set α} (hf : AntitoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (fun x => Set.Icc (f x) (g x)) s
• AntitoneOn.Ico 📋 Mathlib.Order.Interval.Set.Monotone
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f g : α → β} {s : Set α} (hf : AntitoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (fun x => Set.Ico (f x) (g x)) s
• AntitoneOn.Ioc 📋 Mathlib.Order.Interval.Set.Monotone
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f g : α → β} {s : Set α} (hf : AntitoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (fun x => Set.Ioc (f x) (g x)) s
• AntitoneOn.Ioo 📋 Mathlib.Order.Interval.Set.Monotone
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f g : α → β} {s : Set α} (hf : AntitoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (fun x => Set.Ioo (f x) (g x)) s
• MonotoneOn.Icc 📋 Mathlib.Order.Interval.Set.Monotone
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f g : α → β} {s : Set α} (hf : MonotoneOn f s) (hg : AntitoneOn g s) : AntitoneOn (fun x => Set.Icc (f x) (g x)) s
• MonotoneOn.Ico 📋 Mathlib.Order.Interval.Set.Monotone
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f g : α → β} {s : Set α} (hf : MonotoneOn f s) (hg : AntitoneOn g s) : AntitoneOn (fun x => Set.Ico (f x) (g x)) s
• MonotoneOn.Ioc 📋 Mathlib.Order.Interval.Set.Monotone
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f g : α → β} {s : Set α} (hf : MonotoneOn f s) (hg : AntitoneOn g s) : AntitoneOn (fun x => Set.Ioc (f x) (g x)) s
• MonotoneOn.Ioo 📋 Mathlib.Order.Interval.Set.Monotone
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f g : α → β} {s : Set α} (hf : MonotoneOn f s) (hg : AntitoneOn g s) : AntitoneOn (fun x => Set.Ioo (f x) (g x)) s
• aemeasurable_restrict_of_monotoneOn 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Order
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α] [TopologicalSpace β] {mβ : MeasurableSpace β} [BorelSpace β] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] [LinearOrder β] [OrderClosedTopology β] {μ : MeasureTheory.Measure β} {s : Set β} (hs : MeasurableSet s) {f : β → α} (hf : MonotoneOn f s) : AEMeasurable f (μ.restrict s)
• Real.tendsto_atTop_csSup_of_monotoneOn_bddAbove_nat_Ici 📋 Mathlib.Topology.Instances.Real.Lemmas
  {f : ℕ → ℝ} {k : ℕ} (h_mon : MonotoneOn f (Set.Ici k)) (h_bdd : BddAbove (f '' Set.Ici k)) : Filter.Tendsto f Filter.atTop (nhds (sSup (f '' Set.Ici k)))
• Real.isLUB_of_tendsto_monotoneOn_bddAbove_nat_Ici 📋 Mathlib.Topology.Instances.Real.Lemmas
  {f : ℕ → ℝ} {k : ℕ} {x : ℝ} (h_tto : Filter.Tendsto f Filter.atTop (nhds x)) (h_mon : MonotoneOn f (Set.Ici k)) (h_bdd : BddAbove (f '' Set.Ici k)) : IsLUB (f '' Set.Ici k) x
• MeasurableSet.image_of_monotoneOn 📋 Mathlib.MeasureTheory.Constructions.Polish.Basic
  {α : Type u_6} {β : Type u_7} {t : Set α} {g : α → β} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [LinearOrder α] [OrderTopology α] [PolishSpace α] [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] [LinearOrder β] [OrderTopology β] [SecondCountableTopology β] (ht : MeasurableSet t) (hg : MonotoneOn g t) : MeasurableSet (g '' t)
• MeasurableSet.image_of_monotoneOn_of_continuousOn 📋 Mathlib.MeasureTheory.Constructions.Polish.Basic
  {α : Type u_6} {β : Type u_7} {t : Set α} {g : α → β} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [LinearOrder α] [OrderTopology α] [PolishSpace α] [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] [LinearOrder β] [OrderTopology β] (ht : MeasurableSet t) (hg : MonotoneOn g t) (h'g : ContinuousOn g t) : MeasurableSet (g '' t)
• Real.monotoneOn_sin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
  : MonotoneOn Real.sin (Set.Icc (-(Real.pi / 2)) (Real.pi / 2))
• Real.monotoneOn_rpow_Ici_of_exponent_nonneg 📋 Mathlib.Analysis.SpecialFunctions.Pow.Real
  {r : ℝ} (hr : 0 ≤ r) : MonotoneOn (fun x => x ^ r) (Set.Ici 0)
• MonotoneOn.convex_ge 📋 Mathlib.Analysis.Convex.Basic
  {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {s : Set E} {f : E → β} (hf : MonotoneOn f s) (hs : Convex 𝕜 s) (r : β) : Convex 𝕜 {x | x ∈ s ∧ r ≤ f x}
• MonotoneOn.convex_gt 📋 Mathlib.Analysis.Convex.Basic
  {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {s : Set E} {f : E → β} (hf : MonotoneOn f s) (hs : Convex 𝕜 s) (r : β) : Convex 𝕜 {x | x ∈ s ∧ r < f x}
• MonotoneOn.convex_le 📋 Mathlib.Analysis.Convex.Basic
  {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {s : Set E} {f : E → β} (hf : MonotoneOn f s) (hs : Convex 𝕜 s) (r : β) : Convex 𝕜 {x | x ∈ s ∧ f x ≤ r}
• MonotoneOn.convex_lt 📋 Mathlib.Analysis.Convex.Basic
  {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [PartialOrder β] [Module 𝕜 E] [PosSMulMono 𝕜 E] {s : Set E} {f : E → β} (hf : MonotoneOn f s) (hs : Convex 𝕜 s) (r : β) : Convex 𝕜 {x | x ∈ s ∧ f x < r}
• ConcaveOn.comp 📋 Mathlib.Analysis.Convex.Function
  {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [AddCommMonoid α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [SMul 𝕜 E] [SMul 𝕜 α] [SMul 𝕜 β] {s : Set E} {f : E → β} {g : β → α} (hg : ConcaveOn 𝕜 (f '' s) g) (hf : ConcaveOn 𝕜 s f) (hg' : MonotoneOn g (f '' s)) : ConcaveOn 𝕜 s (g ∘ f)
• ConvexOn.comp 📋 Mathlib.Analysis.Convex.Function
  {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [AddCommMonoid α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [SMul 𝕜 E] [SMul 𝕜 α] [SMul 𝕜 β] {s : Set E} {f : E → β} {g : β → α} (hg : ConvexOn 𝕜 (f '' s) g) (hf : ConvexOn 𝕜 s f) (hg' : MonotoneOn g (f '' s)) : ConvexOn 𝕜 s (g ∘ f)
• StrictConcaveOn.comp_concaveOn 📋 Mathlib.Analysis.Convex.Function
  {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [AddCommMonoid α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [SMul 𝕜 E] [SMul 𝕜 α] [SMul 𝕜 β] {s : Set E} {f : E → β} {g : β → α} (hg : StrictConcaveOn 𝕜 (f '' s) g) (hf : ConcaveOn 𝕜 s f) (hg' : MonotoneOn g (f '' s)) (hf' : Set.InjOn f s) : StrictConcaveOn 𝕜 s (g ∘ f)
• StrictConvexOn.comp_convexOn 📋 Mathlib.Analysis.Convex.Function
  {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [AddCommMonoid α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [SMul 𝕜 E] [SMul 𝕜 α] [SMul 𝕜 β] {s : Set E} {f : E → β} {g : β → α} (hg : StrictConvexOn 𝕜 (f '' s) g) (hf : ConvexOn 𝕜 s f) (hg' : MonotoneOn g (f '' s)) (hf' : Set.InjOn f s) : StrictConvexOn 𝕜 s (g ∘ f)
• monovaryOn_id_iff 📋 Mathlib.Order.Monotone.Monovary
  {ι : Type u_1} {α : Type u_3} [Preorder α] {f : ι → α} {s : Set ι} [PartialOrder ι] : MonovaryOn f id s ↔ MonotoneOn f s
• StrictAntiOn.trans_antivaryOn 📋 Mathlib.Order.Monotone.Monovary
  {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} {s : Set ι} [PartialOrder ι] (hf : StrictAntiOn f s) (h : AntivaryOn g f s) : MonotoneOn g s
• StrictMonoOn.trans_monovaryOn 📋 Mathlib.Order.Monotone.Monovary
  {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} {s : Set ι} [PartialOrder ι] (hf : StrictMonoOn f s) (h : MonovaryOn g f s) : MonotoneOn g s
• AntitoneOn.antivaryOn 📋 Mathlib.Order.Monotone.Monovary
  {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} {s : Set ι} [LinearOrder ι] (hf : AntitoneOn f s) (hg : MonotoneOn g s) : AntivaryOn f g s

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c