Loogle!

Result

Found 185 declarations mentioning StrictMonoOn.

• StrictMonoOn 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] (f : α → β) (s : Set α) : Prop
• strictMonoOn_id 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} [Preorder α] {s : Set α} : StrictMonoOn id s
• strictMonoOn_univ 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} : StrictMonoOn f Set.univ ↔ StrictMono f
• StrictMono.strictMonoOn 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : StrictMono f) (s : Set α) : StrictMonoOn f s
• StrictMonoOn.monotoneOn 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] {f : α → β} {s : Set α} (hf : StrictMonoOn f s) : MonotoneOn f s
• StrictAnti.comp_strictAntiOn 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} (hg : StrictAnti g) (hf : StrictAntiOn f s) : StrictMonoOn (g ∘ f) s
• StrictAnti.comp_strictMonoOn 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} (hg : StrictAnti g) (hf : StrictMonoOn f s) : StrictAntiOn (g ∘ f) s
• StrictMono.comp_strictMonoOn 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} (hg : StrictMono g) (hf : StrictMonoOn f s) : StrictMonoOn (g ∘ f) s
• StrictAntiOn.comp 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} {t : Set β} (hg : StrictAntiOn g t) (hf : StrictAntiOn f s) (hs : Set.MapsTo f s t) : StrictMonoOn (g ∘ f) s
• StrictAntiOn.comp_strictMonoOn 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} {t : Set β} (hg : StrictAntiOn g t) (hf : StrictMonoOn f s) (hs : Set.MapsTo f s t) : StrictAntiOn (g ∘ f) s
• StrictMonoOn.comp 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} {t : Set β} (hg : StrictMonoOn g t) (hf : StrictMonoOn f s) (hs : Set.MapsTo f s t) : StrictMonoOn (g ∘ f) s
• StrictMonoOn.comp_strictAntiOn 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} {t : Set β} (hg : StrictMonoOn g t) (hf : StrictAntiOn f s) (hs : Set.MapsTo f s t) : StrictAntiOn (g ∘ f) s
• instDecidableStrictMonoOnOfForallForallMemSetForallForallForallLt 📋 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 (StrictMonoOn f s)
• StrictMonoOn.injOn 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} {s : Set α} (hf : StrictMonoOn f s) : Set.InjOn f s
• Nat.pow_self_strictMonoOn 📋 Mathlib.Order.Monotone.Basic
  : StrictMonoOn (fun n => n ^ n) {n | n ≠ 0}
• 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
• 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
• StrictMonoOn.eq_iff_eq 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} {s : Set α} (hf : StrictMonoOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) : f a = f b ↔ a = b
• StrictAntiOn.dual_right 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : StrictAntiOn f s → StrictMonoOn (⇑OrderDual.toDual ∘ f) s
• StrictMonoOn.dual_right 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : StrictMonoOn f s → StrictAntiOn (⇑OrderDual.toDual ∘ f) s
• strictAntiOn_toDual_comp_iff 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : StrictAntiOn (⇑OrderDual.toDual ∘ f) s ↔ StrictMonoOn f s
• strictMonoOn_toDual_comp_iff 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : StrictMonoOn (⇑OrderDual.toDual ∘ f) s ↔ StrictAntiOn f s
• StrictAntiOn.dual_left 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : StrictAntiOn f s → StrictMonoOn (f ∘ ⇑OrderDual.ofDual) s
• StrictMonoOn.dual_left 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : StrictMonoOn f s → StrictAntiOn (f ∘ ⇑OrderDual.ofDual) s
• strictAntiOn_comp_ofDual_iff 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : StrictAntiOn (f ∘ ⇑OrderDual.ofDual) s ↔ StrictMonoOn f s
• strictMonoOn_comp_ofDual_iff 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : StrictMonoOn (f ∘ ⇑OrderDual.ofDual) s ↔ StrictAntiOn f s
• StrictMonoOn.le_iff_le 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} {s : Set α} (hf : StrictMonoOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) : f a ≤ f b ↔ a ≤ b
• StrictMonoOn.lt_iff_lt 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} {s : Set α} (hf : StrictMonoOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) : f a < f b ↔ a < b
• StrictMonoOn.compares 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} {s : Set α} (hf : StrictMonoOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) {o : Ordering} : o.Compares (f a) (f b) ↔ o.Compares a b
• StrictMonoOn.cmp_map_eq 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [LinearOrder α] [LinearOrder β] {f : α → β} {s : Set α} {x y : α} (hf : StrictMonoOn f s) (hx : x ∈ s) (hy : y ∈ s) : cmp (f x) (f y) = cmp x y
• StrictMonoOn.dual 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : StrictMonoOn f s → StrictMonoOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s
• strictMonoOn_dual_iff 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : StrictMonoOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s ↔ StrictMonoOn f s
• Set.Subsingleton.strictMonoOn 📋 Mathlib.Data.Set.Subsingleton
  {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] (f : α → β) (h : s.Subsingleton) : StrictMonoOn f s
• Set.strictMonoOn_singleton 📋 Mathlib.Data.Set.Subsingleton
  {α : Type u} {β : Type v} {a : α} [Preorder α] [Preorder β] (f : α → β) : StrictMonoOn f {a}
• StrictMonoOn.add_const 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : β → α} {s : Set β} [AddRightStrictMono α] (hf : StrictMonoOn f s) (c : α) : StrictMonoOn (fun x => f x + c) s
• StrictMonoOn.const_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : β → α} {s : Set β} [AddLeftStrictMono α] (hf : StrictMonoOn f s) (c : α) : StrictMonoOn (fun x => c + f x) s
• StrictMonoOn.const_mul' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : β → α} {s : Set β} [MulLeftStrictMono α] (hf : StrictMonoOn f s) (c : α) : StrictMonoOn (fun x => c * f x) s
• StrictMonoOn.mul_const' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : β → α} {s : Set β} [MulRightStrictMono α] (hf : StrictMonoOn f s) (c : α) : StrictMonoOn (fun x => f x * c) 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_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 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f g : β → α} {s : Set β} [AddLeftStrictMono α] [AddRightStrictMono α] (hf : StrictMonoOn 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' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f g : β → α} {s : Set β} [MulLeftStrictMono α] [MulRightStrictMono α] (hf : StrictMonoOn f s) (hg : StrictMonoOn 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
• StrictAntiOn.inv 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} {β : Type u_1} [Group α] [Preorder α] [MulLeftStrictMono α] [MulRightStrictMono α] [Preorder β] {f : β → α} {s : Set β} (hf : StrictAntiOn f s) : StrictMonoOn (fun x => (f x)⁻¹) s
• StrictAntiOn.neg 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [AddLeftStrictMono α] [AddRightStrictMono α] [Preorder β] {f : β → α} {s : Set β} (hf : StrictAntiOn f s) : StrictMonoOn (fun x => -f x) s
• StrictMonoOn.inv 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} {β : Type u_1} [Group α] [Preorder α] [MulLeftStrictMono α] [MulRightStrictMono α] [Preorder β] {f : β → α} {s : Set β} (hf : StrictMonoOn f s) : StrictAntiOn (fun x => (f x)⁻¹) s
• StrictMonoOn.neg 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [AddLeftStrictMono α] [AddRightStrictMono α] [Preorder β] {f : β → α} {s : Set β} (hf : StrictMonoOn f s) : StrictAntiOn (fun x => -f x) s
• strictMonoOn_mul_self 📋 Mathlib.Algebra.Order.GroupWithZero.Basic
  {M₀ : Type u_2} [MonoidWithZero M₀] [PartialOrder M₀] [PosMulStrictMono M₀] [MulPosMono M₀] : StrictMonoOn (fun x => x * x) {x | 0 ≤ x}
• pow_left_strictMonoOn₀ 📋 Mathlib.Algebra.Order.GroupWithZero.Basic
  {M₀ : Type u_2} [MonoidWithZero M₀] [PartialOrder M₀] {n : ℕ} [PosMulStrictMono M₀] [MulPosMono M₀] (hn : n ≠ 0) : StrictMonoOn (fun x => x ^ n) {a | 0 ≤ a}
• zpow_left_strictMonoOn₀ 📋 Mathlib.Algebra.Order.GroupWithZero.Basic
  {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] [MulPosMono G₀] {n : ℤ} (hn : 0 < n) : StrictMonoOn (fun a => a ^ n) {a | 0 ≤ a}
• StrictMonoOn.congr 📋 Mathlib.Data.Set.Monotone
  {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β} [Preorder α] [Preorder β] (h₁ : StrictMonoOn f₁ s) (h : Set.EqOn f₁ f₂ s) : StrictMonoOn f₂ s
• StrictMonoOn.mono 📋 Mathlib.Data.Set.Monotone
  {α : Type u_1} {β : Type u_2} {s s₂ : Set α} {f : α → β} [Preorder α] [Preorder β] (h : StrictMonoOn f s) (h' : s₂ ⊆ s) : StrictMonoOn f s₂
• Set.EqOn.congr_strictMonoOn 📋 Mathlib.Data.Set.Monotone
  {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β} [Preorder α] [Preorder β] (h : Set.EqOn f₁ f₂ s) : StrictMonoOn f₁ s ↔ StrictMonoOn f₂ s
• StrictMono.of_domRestrict 📋 Mathlib.Data.Set.Monotone
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : StrictMono (s.domRestrict f) → StrictMonoOn f s
• StrictMono.of_restrict 📋 Mathlib.Data.Set.Monotone
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : StrictMono (s.domRestrict f) → StrictMonoOn f s
• StrictMonoOn.domRestrict 📋 Mathlib.Data.Set.Monotone
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : StrictMonoOn f s → StrictMono (s.domRestrict f)
• StrictMonoOn.restrict 📋 Mathlib.Data.Set.Monotone
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : StrictMonoOn f s → StrictMono (s.domRestrict f)
• strictMono_domRestrict 📋 Mathlib.Data.Set.Monotone
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : StrictMono (s.domRestrict f) ↔ StrictMonoOn f s
• strictMono_restrict 📋 Mathlib.Data.Set.Monotone
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : StrictMono (s.domRestrict f) ↔ StrictMonoOn f s
• StrictMonoOn.strictMono 📋 Mathlib.Data.Set.Monotone
  {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} [Preorder α] [Preorder β] (h : StrictMonoOn f s) : StrictMono (f ∘ Subtype.val)
• Function.strictMonoOn_of_rightInvOn_of_mapsTo 📋 Mathlib.Data.Set.Monotone
  {α : Type u_1} {β : Type u_2} [Preorder α] [LinearOrder β] {φ : β → α} {ψ : α → β} {t : Set β} {s : Set α} (hφ : StrictMonoOn φ t) (φψs : Set.RightInvOn ψ φ s) (ψts : Set.MapsTo ψ s t) : StrictMonoOn ψ s
• strictMonoOn_insert_iff_of_forall_ge 📋 Mathlib.Data.Set.Monotone
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} {a : α} (ha : ∀ x ∈ s, a ≤ x) : StrictMonoOn f (insert a s) ↔ (∀ b ∈ s, a < b → f a < f b) ∧ StrictMonoOn f s
• strictMonoOn_insert_iff_of_forall_le 📋 Mathlib.Data.Set.Monotone
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} {a : α} (ha : ∀ x ∈ s, x ≤ a) : StrictMonoOn f (insert a s) ↔ (∀ b ∈ s, b < a → f b < f a) ∧ StrictMonoOn f s
• strictMonoOn_insert_iff 📋 Mathlib.Data.Set.Monotone
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} {a : α} : StrictMonoOn f (insert a s) ↔ (∀ b ∈ s, b < a → f b < f a) ∧ (∀ b ∈ s, a < b → f a < f b) ∧ StrictMonoOn f s
• StrictMonoOn.orderIso 📋 Mathlib.Order.Hom.Set
  {α : Type u_4} {β : Type u_5} [LinearOrder α] [Preorder β] (f : α → β) (s : Set α) (hf : StrictMonoOn f s) : ↑s ≃o ↑(f '' s)
• Set.strictMonoOn_iff_strictMono 📋 Mathlib.Data.Set.Order
  {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] {f : α → β} : StrictMonoOn f s ↔ StrictMono fun a => f ↑a
• StrictMonoOn.mapsTo_Iio 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {b : α} (h : StrictMonoOn f (Set.Iic b)) : Set.MapsTo f (Set.Iio b) (Set.Iio (f b))
• StrictMonoOn.mapsTo_Ioi 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a : α} (h : StrictMonoOn f (Set.Ici a)) : Set.MapsTo f (Set.Ioi a) (Set.Ioi (f a))
• StrictMonoOn.image_Iio_subset 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {b : α} (h : StrictMonoOn f (Set.Iic b)) : f '' Set.Iio b ⊆ Set.Iio (f b)
• StrictMonoOn.image_Ioi_subset 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a : α} (h : StrictMonoOn f (Set.Ici a)) : f '' Set.Ioi a ⊆ Set.Ioi (f a)
• StrictMonoOn.mapsTo_Ioo 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a b : α} (h : StrictMonoOn f (Set.Icc a b)) : Set.MapsTo f (Set.Ioo a b) (Set.Ioo (f a) (f b))
• StrictMonoOn.image_Ioo_subset 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a b : α} (h : StrictMonoOn f (Set.Icc a b)) : f '' Set.Ioo a b ⊆ Set.Ioo (f a) (f b)
• StrictMonoOn.mapsTo_Ico 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [PartialOrder α] [Preorder β] {a b : α} (h : StrictMonoOn f (Set.Icc a b)) : Set.MapsTo f (Set.Ico a b) (Set.Ico (f a) (f b))
• StrictMonoOn.mapsTo_Ioc 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [PartialOrder α] [Preorder β] {a b : α} (h : StrictMonoOn f (Set.Icc a b)) : Set.MapsTo f (Set.Ioc a b) (Set.Ioc (f a) (f b))
• StrictMonoOn.image_Ico_subset 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [PartialOrder α] [Preorder β] {a b : α} (h : StrictMonoOn f (Set.Icc a b)) : f '' Set.Ico a b ⊆ Set.Ico (f a) (f b)
• StrictMonoOn.image_Ioc_subset 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [PartialOrder α] [Preorder β] {a b : α} (h : StrictMonoOn f (Set.Icc a b)) : f '' Set.Ioc a b ⊆ Set.Ioc (f a) (f b)
• IsAntichain.of_strictMonoOn_antitoneOn 📋 Mathlib.Order.Antichain
  {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {f : α → β} {s : Set α} (hf : StrictMonoOn f s) (hf' : AntitoneOn f s) : IsAntichain (fun x1 x2 => x1 ≤ x2) s
• AddConstMapClass.strictMono_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) : StrictMono ⇑f ↔ StrictMonoOn (⇑f) (Set.Icc l (l + a))
• MaximalFor.maximal_of_strictMonoOn 📋 Mathlib.Order.Minimal
  {α : Type u_2} {β : Type u_3} {P : α → Prop} {x : α} [Preorder α] [Preorder β] {g : α → β} (hg : StrictMonoOn g (Set.ofPred P)) (h : MaximalFor P g x) : Maximal P x
• MinimalFor.minimal_of_strictMonoOn 📋 Mathlib.Order.Minimal
  {α : Type u_2} {β : Type u_3} {P : α → Prop} {x : α} [Preorder α] [Preorder β] {g : α → β} (hg : StrictMonoOn g (Set.ofPred P)) (h : MinimalFor P g x) : Minimal P x
• MaximalFor.of_strictMonoOn_comp 📋 Mathlib.Order.Minimal
  {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {Q : ι → Prop} {f : ι → α} {g : α → β} {i : ι} (hg : StrictMonoOn g (f '' Set.ofPred Q)) (h : MaximalFor Q (g ∘ f) i) : MaximalFor Q f i
• MinimalFor.of_strictMonoOn_comp 📋 Mathlib.Order.Minimal
  {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {Q : ι → Prop} {f : ι → α} {g : α → β} {i : ι} (hg : StrictMonoOn g (f '' Set.ofPred Q)) (h : MinimalFor Q (g ∘ f) i) : MinimalFor Q f i
• strictMonoOn_of_lt_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)) : StrictMonoOn f s
• strictMonoOn_of_pred_lt 📋 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) : StrictMonoOn f s
• strictMonoOn_of_lt_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)) → StrictMonoOn f s
• strictMonoOn_of_sub_one_lt 📋 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) → StrictMonoOn f s
• Cardinal.mk_strictMonoOn 📋 Mathlib.SetTheory.Cardinal.Basic
  {α : Type u} : StrictMonoOn (Cardinal.mk ∘ Set.Elem) {s | s.Finite}
• Cardinal.toENat_strictMonoOn 📋 Mathlib.SetTheory.Cardinal.ENat
  : StrictMonoOn (⇑Cardinal.toENat) (Set.Iic Cardinal.aleph0)
• Cardinal.toNat_strictMonoOn 📋 Mathlib.SetTheory.Cardinal.ToNat
  : StrictMonoOn (⇑Cardinal.toNat) (Set.Iio Cardinal.aleph0)
• inf_strictMonoOn_Icc_sup 📋 Mathlib.Order.ModularLattice
  {α : Type u_1} [Lattice α] [IsModularLattice α] {a b : α} : StrictMonoOn (fun c => a ⊓ c) (Set.Icc b (a ⊔ b))
• sup_strictMonoOn_Icc_inf 📋 Mathlib.Order.ModularLattice
  {α : Type u_1} [Lattice α] [IsModularLattice α] {a b : α} : StrictMonoOn (fun c => c ⊔ b) (Set.Icc (a ⊓ b) a)
• Set.Finite.encard_strictMonoOn 📋 Mathlib.Data.Set.Card
  {α : Type u_1} : StrictMonoOn Set.encard (Set.ofPred Set.Finite)
• Set.Finite.ncard_strictMonoOn 📋 Mathlib.Data.Set.Card
  {α : Type u_1} : StrictMonoOn Set.ncard (Set.ofPred Set.Finite)
• Set.Finite.card_strictMonoOn 📋 Mathlib.SetTheory.Cardinal.NatCard
  {α : Type u_1} : StrictMonoOn (Nat.card ∘ Set.Elem) (Set.ofPred Set.Finite)
• Set.Finite.ecard_strictMonoOn 📋 Mathlib.SetTheory.Cardinal.NatCard
  {α : Type u_1} : StrictMonoOn (ENat.card ∘ Set.Elem) (Set.ofPred Set.Finite)
• StrictMonoOn.map_finsetSort 📋 Mathlib.Data.Finset.Sort
  {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Finset α) [LinearOrder α] [LinearOrder β] (hf : StrictMonoOn ⇑f ↑s) : List.map (⇑f) (s.sort fun a b => a ≤ b) = (Finset.map f s).sort fun a b => a ≤ b
• Nat.fib_strictMonoOn 📋 Mathlib.Data.Nat.Fib.Basic
  : StrictMonoOn Nat.fib (Set.Ici 2)
• Continuous.strictMonoOn_of_inj_rigidity 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {f : α → δ} (hf_c : Continuous f) (hf_i : Function.Injective f) {a b : α} (hab : a < b) (hf_mono : StrictMonoOn f (Set.Icc a b)) : StrictMono f
• ContinuousOn.strictMonoOn_of_injOn_Icc 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} {f : α → δ} (hab : a ≤ b) (hfab : f a ≤ f b) (hf_c : ContinuousOn f (Set.Icc a b)) (hf_i : Set.InjOn f (Set.Icc a b)) : StrictMonoOn f (Set.Icc a b)
• ContinuousOn.image_Ico_of_strictMonoOn 📋 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 : StrictMonoOn f (Set.Icc a b)) : f '' Set.Ico a b = Set.Ico (f a) (f b)
• ContinuousOn.image_Ioc_of_strictMonoOn 📋 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 : StrictMonoOn f (Set.Icc a b)) : f '' Set.Ioc a b = Set.Ioc (f a) (f b)
• ContinuousOn.image_Ioo_of_strictMonoOn 📋 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 : StrictMonoOn f (Set.Icc a b)) : f '' Set.Ioo a b = Set.Ioo (f a) (f b)
• ContinuousOn.image_Iio_of_strictMonoOn 📋 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 : StrictMonoOn f (Set.Iic a)) (hbot : Filter.Tendsto f Filter.atBot Filter.atBot) : f '' Set.Iio a = Set.Iio (f a)
• ContinuousOn.image_Ioi_of_strictMonoOn 📋 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 : StrictMonoOn f (Set.Ici a)) (htop : Filter.Tendsto f Filter.atTop Filter.atTop) : f '' Set.Ioi a = Set.Ioi (f a)
• ContinuousOn.strictMonoOn_of_injOn_Icc' 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} {f : α → δ} (hab : a ≤ b) (hf_c : ContinuousOn f (Set.Icc a b)) (hf_i : Set.InjOn f (Set.Icc a b)) : StrictMonoOn f (Set.Icc a b) ∨ StrictAntiOn f (Set.Icc a b)
• ContinuousOn.strictMonoOn_of_injOn_Ioo 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} {f : α → δ} (hab : a < b) (hf_c : ContinuousOn f (Set.Ioo a b)) (hf_i : Set.InjOn f (Set.Ioo a b)) : StrictMonoOn f (Set.Ioo a b) ∨ StrictAntiOn f (Set.Ioo a b)
• StrictMonoOn.continuousAt_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 : StrictMonoOn f s) (hs : s ∈ nhds a) (hfs : f '' s ∈ nhds (f a)) : ContinuousAt f a
• StrictMonoOn.continuousAt_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 : StrictMonoOn f s) (hs : s ∈ nhds a) (hfs : closure (f '' s) ∈ nhds (f a)) : ContinuousAt f a
• StrictMonoOn.continuousWithinAt_left_of_surjOn 📋 Mathlib.Topology.Order.MonotoneContinuity
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s ∈ nhdsWithin a (Set.Iic a)) (hfs : Set.SurjOn f s (Set.Iio (f a))) : ContinuousWithinAt f (Set.Iic a) a
• StrictMonoOn.continuousWithinAt_right_of_surjOn 📋 Mathlib.Topology.Order.MonotoneContinuity
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s ∈ nhdsWithin a (Set.Ici a)) (hfs : Set.SurjOn f s (Set.Ioi (f a))) : ContinuousWithinAt f (Set.Ici a) a
• StrictMonoOn.continuousWithinAt_left_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 : StrictMonoOn 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
• StrictMonoOn.continuousWithinAt_right_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 : StrictMonoOn 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
• StrictMonoOn.continuousWithinAt_left_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 : StrictMonoOn 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
• StrictMonoOn.continuousWithinAt_right_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 : StrictMonoOn 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
• StrictMonoOn.continuousWithinAt_left_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 : StrictMonoOn f s) (hs : s ∈ nhdsWithin a (Set.Iic a)) (hfs : ∀ b < f a, ∃ c ∈ s, f c ∈ Set.Ico b (f a)) : ContinuousWithinAt f (Set.Iic a) a
• StrictMonoOn.continuousWithinAt_right_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 : StrictMonoOn f s) (hs : s ∈ nhdsWithin a (Set.Ici a)) (hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Set.Ioc (f a) b) : ContinuousWithinAt f (Set.Ici a) a
• StrictMonoOn.continuousAt_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 : StrictMonoOn f s) (hs : s ∈ nhds a) (hfs_l : ∀ b < f a, ∃ c ∈ s, f c ∈ Set.Ico b (f a)) (hfs_r : ∀ b > f a, ∃ c ∈ s, f c ∈ Set.Ioc (f a) b) : ContinuousAt f a
• Set.strictMonoOn_projIci 📋 Mathlib.Order.Interval.Set.ProjIcc
  {α : Type u_1} [LinearOrder α] {a : α} : StrictMonoOn (Set.projIci a) (Set.Ici a)
• Set.strictMonoOn_projIic 📋 Mathlib.Order.Interval.Set.ProjIcc
  {α : Type u_1} [LinearOrder α] {b : α} : StrictMonoOn (Set.projIic b) (Set.Iic b)
• Set.strictMonoOn_projIcc 📋 Mathlib.Order.Interval.Set.ProjIcc
  {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) : StrictMonoOn (Set.projIcc a b h) (Set.Icc a b)
• StrictMono.strictMonoOn_IciExtend 📋 Mathlib.Order.Interval.Set.ProjIcc
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {a : α} {f : ↑(Set.Ici a) → β} (hf : StrictMono f) : StrictMonoOn (Set.IciExtend f) (Set.Ici a)
• StrictMono.strictMonoOn_IicExtend 📋 Mathlib.Order.Interval.Set.ProjIcc
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {b : α} {f : ↑(Set.Iic b) → β} (hf : StrictMono f) : StrictMonoOn (Set.IicExtend f) (Set.Iic b)
• StrictMono.strictMonoOn_IccExtend 📋 Mathlib.Order.Interval.Set.ProjIcc
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {a b : α} (h : a ≤ b) {f : ↑(Set.Icc a b) → β} (hf : StrictMono f) : StrictMonoOn (Set.IccExtend h f) (Set.Icc a b)
• strictMonoOn_Ici_of_pred_lt 📋 Mathlib.Order.Interval.Set.Monotone
  {α : Type u_1} {β : Type u_2} [PartialOrder α] [Preorder β] {ψ : α → β} [PredOrder α] [IsPredArchimedean α] {n : α} (hψ : ∀ (m : α), n < m → ψ (Order.pred m) < ψ m) : StrictMonoOn ψ (Set.Ici n)
• strictMonoOn_Iic_of_lt_succ 📋 Mathlib.Order.Interval.Set.Monotone
  {α : Type u_1} {β : Type u_2} [PartialOrder α] [Preorder β] {ψ : α → β} [SuccOrder α] [IsSuccArchimedean α] {n : α} (hψ : ∀ m < n, ψ m < ψ (Order.succ m)) : StrictMonoOn ψ (Set.Iic n)
• StrictMonoOn.Ici_le_id 📋 Mathlib.Order.Interval.Set.Monotone
  {α : Type u_1} [LinearOrder α] [PredOrder α] [IsPredArchimedean α] [OrderTop α] {n : α} {φ : α → α} (hφ : StrictMonoOn φ (Set.Ici n)) (m : α) : n ≤ m → φ m ≤ m
• StrictMonoOn.Iic_id_le 📋 Mathlib.Order.Interval.Set.Monotone
  {α : Type u_1} [LinearOrder α] [SuccOrder α] [IsSuccArchimedean α] [OrderBot α] {n : α} {φ : α → α} (hφ : StrictMonoOn φ (Set.Iic n)) (m : α) : m ≤ n → m ≤ φ m
• Real.strictMonoOn_sqrt 📋 Mathlib.Analysis.Real.Sqrt
  : StrictMonoOn Real.sqrt (Set.Ici 0)
• Real.strictMonoOn_sin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
  : StrictMonoOn Real.sin (Set.Icc (-(Real.pi / 2)) (Real.pi / 2))
• Real.strictMonoOn_tan 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
  : StrictMonoOn Real.tan (Set.Ioo (-(Real.pi / 2)) (Real.pi / 2))
• Real.strictMonoOn_arcsin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
  : StrictMonoOn Real.arcsin (Set.Icc (-1) 1)
• Real.strictMonoOn_log 📋 Mathlib.Analysis.SpecialFunctions.Log.Basic
  : StrictMonoOn Real.log (Set.Ioi 0)
• Real.strictMonoOn_rpow_Ici_of_exponent_pos 📋 Mathlib.Analysis.SpecialFunctions.Pow.Real
  {r : ℝ} (hr : 0 < r) : StrictMonoOn (fun x => x ^ r) (Set.Ici 0)
• ConcaveOn.comp_strictConcaveOn 📋 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 : StrictConcaveOn 𝕜 s f) (hg' : StrictMonoOn g (f '' s)) : StrictConcaveOn 𝕜 s (g ∘ f)
• ConvexOn.comp_strictConvexOn 📋 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 : StrictConvexOn 𝕜 s f) (hg' : StrictMonoOn g (f '' s)) : StrictConvexOn 𝕜 s (g ∘ f)
• StrictConcaveOn.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 : StrictConcaveOn 𝕜 (f '' s) g) (hf : StrictConcaveOn 𝕜 s f) (hg' : StrictMonoOn g (f '' s)) (hf' : Set.InjOn f s) : StrictConcaveOn 𝕜 s (g ∘ f)
• StrictConvexOn.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 : StrictConvexOn 𝕜 (f '' s) g) (hf : StrictConvexOn 𝕜 s f) (hg' : StrictMonoOn g (f '' s)) (hf' : Set.InjOn f s) : StrictConvexOn 𝕜 s (g ∘ f)
• ConcaveOn.strictMonoOn 📋 Mathlib.Analysis.Convex.Slope
  {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜} (hf : ConcaveOn 𝕜 s f) {x y : 𝕜} (hy : y ∈ s) (hxy : x < y) (hxy' : f x < f y) : StrictMonoOn f (s ∩ Set.Iic x)
• ConvexOn.strictMonoOn 📋 Mathlib.Analysis.Convex.Slope
  {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜} (hf : ConvexOn 𝕜 s f) {x y : 𝕜} (hx : x ∈ s) (hxy : x < y) (hxy' : f x < f y) : StrictMonoOn f (s ∩ Set.Ici y)
• StrictMonoOn.trans_antivaryOn 📋 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 : AntivaryOn g f s) : AntitoneOn 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
• ArchimedeanClass.mk_sum 📋 Mathlib.Algebra.Order.Archimedean.Class
  {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {ι : Type u_2} [LinearOrder ι] {s : Finset ι} (hnonempty : s.Nonempty) {a : ι → M} : StrictMonoOn (ArchimedeanClass.mk ∘ a) ↑s → ArchimedeanClass.mk (∑ i ∈ s, a i) = ArchimedeanClass.mk (a (s.min' hnonempty))
• MulArchimedeanClass.mk_prod 📋 Mathlib.Algebra.Order.Archimedean.Class
  {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {ι : Type u_2} [LinearOrder ι] {s : Finset ι} (hnonempty : s.Nonempty) {a : ι → M} : StrictMonoOn (MulArchimedeanClass.mk ∘ a) ↑s → MulArchimedeanClass.mk (∏ i ∈ s, a i) = MulArchimedeanClass.mk (a (s.min' hnonempty))
• StrictMonoOn.slope_pos 📋 Mathlib.LinearAlgebra.AffineSpace.Slope
  {k : Type u_1} {E : Type u_2} [Field k] [AddCommGroup E] [Module k E] [LinearOrder k] [IsStrictOrderedRing k] [PartialOrder E] [IsOrderedAddMonoid E] [PosSMulMono k E] {f : k → E} {x y : k} {s : Set k} (hf : StrictMonoOn f s) (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y) : 0 < slope f x y
• strictMonoOn_of_deriv_pos 📋 Mathlib.Analysis.Calculus.Deriv.MeanValue
  {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (hf' : ∀ x ∈ interior D, 0 < deriv f x) : StrictMonoOn f D
• strictMonoOn_of_hasDerivWithinAt_pos 📋 Mathlib.Analysis.Calculus.Deriv.MeanValue
  {D : Set ℝ} (hD : Convex ℝ D) {f f' : ℝ → ℝ} (hf : ContinuousOn f D) (hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x) (hf'₀ : ∀ x ∈ interior D, 0 < f' x) : StrictMonoOn f D
• eVariationOn.eVariationOn_eq_strictMonoOn 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] (f : α → E) (s : Set α) : eVariationOn f s = ⨆ p, ∑ i ∈ Finset.range p.fst, edist (f (↑p.snd (i + 1))) (f (↑p.snd i))
• StrictMonoOn.strictConvexOn_of_deriv 📋 Mathlib.Analysis.Convex.Deriv
  {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D) (hf' : StrictMonoOn (deriv f) (interior D)) : StrictConvexOn ℝ D f
• StrictConvexOn.strictMonoOn_derivWithin 📋 Mathlib.Analysis.Convex.Deriv
  {S : Set ℝ} {f : ℝ → ℝ} (hfc : StrictConvexOn ℝ S f) (hfd : DifferentiableOn ℝ f S) : StrictMonoOn (derivWithin f S) S
• StrictConvexOn.strictMonoOn_deriv 📋 Mathlib.Analysis.Convex.Deriv
  {S : Set ℝ} {f : ℝ → ℝ} (hfc : StrictConvexOn ℝ S f) (hfd : ∀ x ∈ S, DifferentiableAt ℝ f x) : StrictMonoOn (deriv f) S
• StrictMonoOn.exists_deriv_lt_slope 📋 Mathlib.Analysis.Convex.Deriv
  {x y : ℝ} {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc x y)) (hxy : x < y) (hf'_mono : StrictMonoOn (deriv f) (Set.Ioo x y)) : ∃ a ∈ Set.Ioo x y, deriv f a < (f y - f x) / (y - x)
• StrictMonoOn.exists_slope_lt_deriv 📋 Mathlib.Analysis.Convex.Deriv
  {x y : ℝ} {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc x y)) (hxy : x < y) (hf'_mono : StrictMonoOn (deriv f) (Set.Ioo x y)) : ∃ a ∈ Set.Ioo x y, (f y - f x) / (y - x) < deriv f a
• StrictMonoOn.exists_deriv_lt_slope_aux 📋 Mathlib.Analysis.Convex.Deriv
  {x y : ℝ} {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc x y)) (hxy : x < y) (hf'_mono : StrictMonoOn (deriv f) (Set.Ioo x y)) (h : ∀ w ∈ Set.Ioo x y, deriv f w ≠ 0) : ∃ a ∈ Set.Ioo x y, deriv f a < (f y - f x) / (y - x)
• StrictMonoOn.exists_slope_lt_deriv_aux 📋 Mathlib.Analysis.Convex.Deriv
  {x y : ℝ} {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc x y)) (hxy : x < y) (hf'_mono : StrictMonoOn (deriv f) (Set.Ioo x y)) (h : ∀ w ∈ Set.Ioo x y, deriv f w ≠ 0) : ∃ a ∈ Set.Ioo x y, (f y - f x) / (y - x) < deriv f a
• StrictMonoOn.Iic_union_Ici 📋 Mathlib.Order.Monotone.Union
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {a : α} {f : α → β} (h₁ : StrictMonoOn f (Set.Iic a)) (h₂ : StrictMonoOn f (Set.Ici a)) : StrictMono f
• StrictMonoOn.union 📋 Mathlib.Order.Monotone.Union
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {f : α → β} {s t : Set α} {c : α} (h₁ : StrictMonoOn f s) (h₂ : StrictMonoOn f t) (hs : IsGreatest s c) (ht : IsLeast t c) : StrictMonoOn f (s ∪ t)
• strictMono_of_odd_strictMonoOn_nonneg 📋 Mathlib.Order.Monotone.Odd
  {G : Type u_1} {H : Type u_2} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H] {f : G → H} (h₁ : ∀ (x : G), f (-x) = -f x) (h₂ : StrictMonoOn f (Set.Ici 0)) : StrictMono f
• Real.cosh_strictMonoOn 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
  : StrictMonoOn Real.cosh (Set.Ici 0)
• Function.locallyFinsuppWithin.logCounting_strictMono 📋 Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
  {E : Type u_1} [NormedAddCommGroup E] [DecidableEq E] [ProperSpace E] {D : Function.locallyFinsupp E ℤ} {e : E} (hD : Function.locallyFinsuppWithin.single e 1 ≤ D) : StrictMonoOn (Function.locallyFinsuppWithin.logCounting D) (Set.Ioi ‖e‖)
• Real.Gamma_strictMonoOn_Ici 📋 Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
  : StrictMonoOn Real.Gamma (Set.Ici 2)
• Real.strictMonoOn_arcosh 📋 Mathlib.Analysis.SpecialFunctions.Arcosh
  : StrictMonoOn Real.arcosh (Set.Ioi 0)
• Real.strictMonoOn_artanh 📋 Mathlib.Analysis.SpecialFunctions.Artanh
  : StrictMonoOn Real.artanh (Set.Ioo (-1) 1)
• Real.strictMonoOn_one_add_div_one_sub 📋 Mathlib.Analysis.SpecialFunctions.Artanh
  : StrictMonoOn (fun x => (1 + x) / (1 - x)) (Set.Ioo (-1) 1)
• Real.binEntropy_strictMonoOn 📋 Mathlib.Analysis.SpecialFunctions.BinaryEntropy
  : StrictMonoOn Real.binEntropy (Set.Icc 0 2⁻¹)
• Real.qaryEntropy_strictMonoOn 📋 Mathlib.Analysis.SpecialFunctions.BinaryEntropy
  {q : ℕ} (qLe2 : 2 ≤ q) : StrictMonoOn (Real.qaryEntropy q) (Set.Icc 0 (1 - 1 / ↑q))
• Real.strictMonoOn_logb 📋 Mathlib.Analysis.SpecialFunctions.Log.Base
  {b : ℝ} (hb : 1 < b) : StrictMonoOn (Real.logb b) (Set.Ioi 0)
• Real.strictMonoOn_logb_of_base_lt_one 📋 Mathlib.Analysis.SpecialFunctions.Log.Base
  {b : ℝ} (b_pos : 0 < b) (b_lt_one : b < 1) : StrictMonoOn (Real.logb b) (Set.Iio 0)
• Real.mul_log_strictMonoOn 📋 Mathlib.Analysis.SpecialFunctions.Log.Monotone
  : StrictMonoOn (fun x => x * Real.log x) (Set.Ici (Real.exp (-1)))
• pentagonal_strictMonoOn 📋 Mathlib.Combinatorics.Enumerative.Pentagonal.Basic
  : StrictMonoOn pentagonal (Set.Ici 0)
• SimpleGraph.strictMonoOn_turanNumber 📋 Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
  {n : ℕ} : StrictMonoOn (SimpleGraph.turanNumber n) (Set.Icc 1 n)
• SimpleGraph.Subgraph.IsMatching.strictMonoOn_edgeSet 📋 Mathlib.Combinatorics.SimpleGraph.Matching
  {V : Type u_1} {G : SimpleGraph V} : StrictMonoOn SimpleGraph.Subgraph.edgeSet (Set.ofPred SimpleGraph.Subgraph.IsMatching)
• AkraBazziRecurrence.strictMonoOn_one_sub_smoothingFn 📋 Mathlib.Computability.AkraBazzi.SumTransform
  : StrictMonoOn (fun x => 1 - AkraBazziRecurrence.smoothingFn x) (Set.Ioi 1)
• Int.strictMonoOn_natAbs 📋 Mathlib.Data.Int.Lemmas
  : StrictMonoOn Int.natAbs (Set.Ici 0)
• Nat.nth_strictMonoOn 📋 Mathlib.Data.Nat.Nth
  {p : ℕ → Prop} (hf : (Set.ofPred p).Finite) : StrictMonoOn (Nat.nth p) (Set.Iio hf.toFinset.card)
• Nat.nth_le_of_strictMonoOn_of_mapsTo 📋 Mathlib.Data.Nat.Nth
  {p : ℕ → Prop} (f : ℕ → ℕ) (hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < hf.toFinset.card} (Set.ofPred p)) (hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < hf.toFinset.card}) {n : ℕ} : Nat.nth p n ≤ f n
• Nat.eq_nth_of_strictMonoOn_of_mapsTo_of_surjOn 📋 Mathlib.Data.Nat.Nth
  {p : ℕ → Prop} (f : ℕ → ℕ) (hsurj : Set.SurjOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < hf.toFinset.card} (Set.ofPred p)) (hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < hf.toFinset.card} (Set.ofPred p)) (hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < hf.toFinset.card}) : Set.EqOn f (Nat.nth p) {n | ∀ (hf : (Set.ofPred p).Finite), n < hf.toFinset.card}
• Finset.nsmul_right_strictMonoOn 📋 Mathlib.Geometry.Group.Growth.LinearLowerBound
  {G : Type u_1} [AddGroup G] [DecidableEq G] {X : Finset G} (hX₁ : 0 ∈ X) (hX : X.Nontrivial) : StrictMonoOn (fun n => n • X) {n | (n - 1) • ↑X ≠ ↑(AddSubgroup.closure ↑X)}
• Finset.pow_right_strictMonoOn 📋 Mathlib.Geometry.Group.Growth.LinearLowerBound
  {G : Type u_1} [Group G] [DecidableEq G] {X : Finset G} (hX₁ : 1 ∈ X) (hX : X.Nontrivial) : StrictMonoOn (fun n => X ^ n) {n | ↑X ^ (n - 1) ≠ ↑(Subgroup.closure ↑X)}
• upperCentralSeries.StrictMonoOn 📋 Mathlib.GroupTheory.Nilpotent
  (G : Type u_1) [Group G] : StrictMonoOn (Subgroup.upperCentralSeries G) (Set.Iic (Group.nilpotencyClass G))
• AddSubgroup.upperCentralSeries.StrictMonoOn 📋 Mathlib.GroupTheory.Nilpotent
  (G : Type u_1) [AddGroup G] : StrictMonoOn (AddSubgroup.upperCentralSeries G) (Set.Iic (AddGroup.nilpotencyClass G))
• Subgroup.upperCentralSeries.StrictMonoOn 📋 Mathlib.GroupTheory.Nilpotent
  (G : Type u_1) [Group G] : StrictMonoOn (Subgroup.upperCentralSeries G) (Set.Iic (Group.nilpotencyClass G))
• Matrix.IsPivotedBy.strictMonoOn 📋 Mathlib.LinearAlgebra.Matrix.Echelon.Pivot
  {m : Type u_1} {n : Type u_2} {R : Type u_3} [Zero R] {A : Matrix m n R} {l : m → WithTop n} [LinearOrder n] [Preorder m] (hA : A.IsPivotedBy l) : StrictMonoOn l {i | l i ≠ ⊤}
• Matrix.isPivotedBy_iff 📋 Mathlib.LinearAlgebra.Matrix.Echelon.Pivot
  {m : Type u_1} {n : Type u_2} {R : Type u_3} [Zero R] {A : Matrix m n R} {l : m → WithTop n} [PartialOrder m] [LinearOrder n] : A.IsPivotedBy l ↔ Monotone l ∧ StrictMonoOn l {i | l i ≠ ⊤} ∧ ∀ (i : m), (∀ (j : n), ↑j < l i → A i j = 0) ∧ ∀ (c : n), l i = ↑c → A i c ≠ 0
• Matrix.isPivotedBy_iff' 📋 Mathlib.LinearAlgebra.Matrix.Echelon.Pivot
  {m : Type u_1} {n : Type u_2} {R : Type u_3} [Zero R] {A : Matrix m n R} {l : m → WithTop n} [PartialOrder m] [LinearOrder n] : A.IsPivotedBy l ↔ Monotone l ∧ StrictMonoOn l {i | l i ≠ ⊤} ∧ ∀ (i : m), l i = ⊤ ∧ A i = 0 ∨ ∃ c, l i = ↑c ∧ A.IsLeadingEntry i c

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