Loogle!

Result

Found 269 declarations mentioning AntitoneOn. Of these, only the first 200 are shown.

• AntitoneOn 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] (f : α → β) (s : Set α) : Prop
• antitoneOn_const 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {c : β} {s : Set α} : AntitoneOn (fun x => c) s
• antitoneOn_univ 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} : AntitoneOn f Set.univ ↔ Antitone f
• Antitone.antitoneOn 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) (s : Set α) : AntitoneOn f s
• StrictAntiOn.antitoneOn 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] {f : α → β} {s : Set α} (hf : StrictAntiOn f s) : AntitoneOn 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_antitoneOn 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} (hg : Monotone g) (hf : AntitoneOn f s) : AntitoneOn (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_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
• instDecidableAntitoneOnOfForallForallMemSetForallForallForallLe 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} [i : Decidable (∀ a ∈ s, ∀ b ∈ s, a ≤ b → f b ≤ f a)] : Decidable (AntitoneOn f s)
• antitoneOn_iff_forall_lt 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] {f : α → β} {s : Set α} : AntitoneOn f s ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a < b → f b ≤ f a
• AntitoneOn.reflect_lt 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} {s : Set α} (hf : AntitoneOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) (h : f a < f b) : b < a
• AntitoneOn.strictAntiOn_of_injOn 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [PartialOrder β] {f : α → β} {s : Set α} (hanti : AntitoneOn f s) (hinj : Set.InjOn f s) : StrictAntiOn f s
• antitone_add_nat_iff_antitoneOn_nat_Ici 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} [Preorder α] {f : ℕ → α} {k : ℕ} : (Antitone fun n => f (n + k)) ↔ AntitoneOn f {x | k ≤ x}
• AntitoneOn.strictAnti_iff_injOn 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [LinearOrder α] [PartialOrder β] {f : α → β} {s : Set α} (hf : AntitoneOn f s) : StrictAntiOn f s ↔ Set.InjOn f s
• antitoneOn_nat_Ici_of_succ_le 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} [Preorder α] {f : ℕ → α} {k : ℕ} (hf : ∀ n ≥ k, f (n + 1) ≤ f n) : AntitoneOn f {x | k ≤ x}
• 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
• AntitoneOn.dual 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : AntitoneOn f s → AntitoneOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s
• antitoneOn_dual_iff 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : AntitoneOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s ↔ AntitoneOn f s
• AntitoneOn.inf 📋 Mathlib.Order.Lattice
  {α : Type u} {β : Type v} [Preorder α] [SemilatticeInf β] {f g : α → β} {s : Set α} (hf : AntitoneOn f s) (hg : AntitoneOn g s) : AntitoneOn (f ⊓ g) s
• AntitoneOn.sup 📋 Mathlib.Order.Lattice
  {α : Type u} {β : Type v} [Preorder α] [SemilatticeSup β] {f g : α → β} {s : Set α} (hf : AntitoneOn f s) (hg : AntitoneOn g s) : AntitoneOn (f ⊔ g) s
• AntitoneOn.of_map_inf 📋 Mathlib.Order.Lattice
  {α : Type u} {β : Type v} {f : α → β} {s : Set α} [SemilatticeInf α] [SemilatticeSup β] (h : ∀ x ∈ s, ∀ y ∈ s, f (x ⊓ y) = f x ⊔ f y) : AntitoneOn f s
• AntitoneOn.of_map_sup 📋 Mathlib.Order.Lattice
  {α : Type u} {β : Type v} {f : α → β} {s : Set α} [SemilatticeSup α] [SemilatticeInf β] (h : ∀ x ∈ s, ∀ y ∈ s, f (x ⊔ y) = f x ⊓ f y) : AntitoneOn f s
• AntitoneOn.map_inf 📋 Mathlib.Order.Lattice
  {α : Type u} {β : Type v} {f : α → β} {s : Set α} {x y : α} [LinearOrder α] [SemilatticeSup β] (hf : AntitoneOn f s) (hx : x ∈ s) (hy : y ∈ s) : f (min x y) = f x ⊔ f y
• AntitoneOn.map_sup 📋 Mathlib.Order.Lattice
  {α : Type u} {β : Type v} {f : α → β} {s : Set α} {x y : α} [LinearOrder α] [SemilatticeInf β] (hf : AntitoneOn f s) (hx : x ∈ s) (hy : y ∈ s) : f (max x y) = f x ⊓ f y
• AntitoneOn.max 📋 Mathlib.Order.Lattice
  {α : Type u} {β : Type v} [Preorder α] [LinearOrder β] {f g : α → β} {s : Set α} (hf : AntitoneOn f s) (hg : AntitoneOn g s) : AntitoneOn (fun x => max (f x) (g x)) s
• AntitoneOn.min 📋 Mathlib.Order.Lattice
  {α : Type u} {β : Type v} [Preorder α] [LinearOrder β] {f g : α → β} {s : Set α} (hf : AntitoneOn f s) (hg : AntitoneOn g s) : AntitoneOn (fun x => min (f x) (g x)) s
• Set.Subsingleton.antitoneOn 📋 Mathlib.Data.Set.Subsingleton
  {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] (f : α → β) (h : s.Subsingleton) : AntitoneOn f s
• Set.antitoneOn_singleton 📋 Mathlib.Data.Set.Subsingleton
  {α : Type u} {β : Type v} {a : α} [Preorder α] [Preorder β] (f : α → β) : AntitoneOn f {a}
• AntitoneOn.set_prod 📋 Mathlib.Data.Set.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} [Preorder α] {f : α → Set β} {g : α → Set γ} (hf : AntitoneOn f s) (hg : AntitoneOn g s) : AntitoneOn (fun x => f x ×ˢ g x) s
• AntitoneOn.map_max 📋 Mathlib.Order.MinMax
  {α : Type u} {β : Type v} [LinearOrder α] [LinearOrder β] {f : α → β} {s : Set α} {a b : α} (hf : AntitoneOn f s) (ha : a ∈ s) (hb : b ∈ s) : f (max a b) = min (f a) (f b)
• AntitoneOn.map_min 📋 Mathlib.Order.MinMax
  {α : Type u} {β : Type v} [LinearOrder α] [LinearOrder β] {f : α → β} {s : Set α} {a b : α} (hf : AntitoneOn f s) (ha : a ∈ s) (hb : b ∈ s) : f (min a b) = max (f a) (f b)
• AntitoneOn.add_const 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : β → α} {s : Set β} [AddRightMono α] (hf : AntitoneOn f s) (a : α) : AntitoneOn (fun x => f x + a) s
• AntitoneOn.const_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : β → α} {s : Set β} [AddLeftMono α] (hf : AntitoneOn f s) (a : α) : AntitoneOn (fun x => a + f x) s
• AntitoneOn.const_mul' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : β → α} {s : Set β} [MulLeftMono α] (hf : AntitoneOn f s) (a : α) : AntitoneOn (fun x => a * f x) s
• AntitoneOn.mul_const' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : β → α} {s : Set β} [MulRightMono α] (hf : AntitoneOn f s) (a : α) : AntitoneOn (fun x => f x * a) s
• AntitoneOn.add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f g : β → α} {s : Set β} [AddLeftMono α] [AddRightMono α] (hf : AntitoneOn f s) (hg : AntitoneOn g s) : AntitoneOn (fun x => f x + g x) s
• AntitoneOn.add_strictAnti 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {s : Set β} [AddLeftStrictMono α] [AddRightMono α] {f g : β → α} (hf : AntitoneOn f s) (hg : StrictAntiOn g s) : StrictAntiOn (fun x => f x + g x) s
• AntitoneOn.mul' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f g : β → α} {s : Set β} [MulLeftMono α] [MulRightMono α] (hf : AntitoneOn f s) (hg : AntitoneOn g s) : AntitoneOn (fun x => f x * g x) s
• AntitoneOn.mul_strictAnti' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {s : Set β} [MulLeftStrictMono α] [MulRightMono α] {f g : β → α} (hf : AntitoneOn f s) (hg : StrictAntiOn g s) : StrictAntiOn (fun x => f x * g x) s
• StrictAntiOn.add_antitone 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f g : β → α} {s : Set β} [AddLeftMono α] [AddRightStrictMono α] (hf : StrictAntiOn f s) (hg : AntitoneOn g s) : StrictAntiOn (fun x => f x + g x) s
• StrictAntiOn.mul_antitone' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f g : β → α} {s : Set β} [MulLeftMono α] [MulRightStrictMono α] (hf : StrictAntiOn f s) (hg : AntitoneOn g s) : StrictAntiOn (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
• antitoneOn_inv_pos 📋 Mathlib.Algebra.Order.GroupWithZero.Basic
  {G₀ : Type u_3} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀] : AntitoneOn (fun x => x⁻¹) {r | 0 < r}
• 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
• AntitoneOn.congr 📋 Mathlib.Data.Set.Monotone
  {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β} [Preorder α] [Preorder β] (h₁ : AntitoneOn f₁ s) (h : Set.EqOn f₁ f₂ s) : AntitoneOn f₂ s
• AntitoneOn.mono 📋 Mathlib.Data.Set.Monotone
  {α : Type u_1} {β : Type u_2} {s s₂ : Set α} {f : α → β} [Preorder α] [Preorder β] (h : AntitoneOn f s) (h' : s₂ ⊆ s) : AntitoneOn f s₂
• Set.EqOn.congr_antitoneOn 📋 Mathlib.Data.Set.Monotone
  {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β} [Preorder α] [Preorder β] (h : Set.EqOn f₁ f₂ s) : AntitoneOn f₁ s ↔ AntitoneOn f₂ s
• AntitoneOn.monotone 📋 Mathlib.Data.Set.Monotone
  {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} [Preorder α] [Preorder β] (h : AntitoneOn f s) : Antitone (f ∘ Subtype.val)
• Function.antitoneOn_of_rightInvOn_of_mapsTo 📋 Mathlib.Data.Set.Monotone
  {α : Type u_1} {β : Type u_2} [PartialOrder α] [LinearOrder β] {φ : β → α} {ψ : α → β} {t : Set β} {s : Set α} (hφ : AntitoneOn φ t) (φψs : Set.RightInvOn ψ φ s) (ψts : Set.MapsTo ψ s t) : AntitoneOn ψ s
• Set.antitoneOn_insert_iff 📋 Mathlib.Data.Set.Monotone
  {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} [Preorder α] [Preorder β] {a : α} : AntitoneOn f (insert a s) ↔ (∀ b ∈ s, b ≤ a → f a ≤ f b) ∧ (∀ b ∈ s, a ≤ b → f b ≤ f a) ∧ AntitoneOn f s
• AntitoneOn.map_isGreatest 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {t : Set α} {a : α} (Hf : AntitoneOn f t) : IsGreatest t a → IsLeast (f '' t) (f a)
• AntitoneOn.map_isLeast 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {t : Set α} {a : α} (Hf : AntitoneOn f t) : IsLeast t a → IsGreatest (f '' t) (f a)
• AntitoneOn.map_bddAbove 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s t : Set α} (Hf : AntitoneOn f t) (Hst : s ⊆ t) : (upperBounds s ∩ t).Nonempty → BddBelow (f '' s)
• AntitoneOn.map_bddBelow 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s t : Set α} (Hf : AntitoneOn f t) (Hst : s ⊆ t) : (lowerBounds s ∩ t).Nonempty → BddAbove (f '' s)
• AntitoneOn.image_lowerBounds_subset_upperBounds_image 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s t : Set α} (Hf : AntitoneOn f t) (Hst : s ⊆ t) : f '' (lowerBounds s ∩ t) ⊆ upperBounds (f '' s)
• AntitoneOn.image_upperBounds_subset_lowerBounds_image 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s t : Set α} (Hf : AntitoneOn f t) (Hst : s ⊆ t) : f '' (upperBounds s ∩ t) ⊆ lowerBounds (f '' s)
• AntitoneOn.mem_lowerBounds_image_self 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {t : Set α} {a : α} (Hf : AntitoneOn f t) : a ∈ upperBounds t → a ∈ t → f a ∈ lowerBounds (f '' t)
• AntitoneOn.mem_upperBounds_image_self 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {t : Set α} {a : α} (Hf : AntitoneOn f t) : a ∈ lowerBounds t → a ∈ t → f a ∈ upperBounds (f '' t)
• AntitoneOn.mem_lowerBounds_image 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s t : Set α} {a : α} (Hf : AntitoneOn f t) (Hst : s ⊆ t) (Has : a ∈ upperBounds s) : a ∈ t → f a ∈ lowerBounds (f '' s)
• AntitoneOn.mem_upperBounds_image 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s t : Set α} {a : α} (Hf : AntitoneOn f t) (Hst : s ⊆ t) (Has : a ∈ lowerBounds s) : a ∈ t → f a ∈ upperBounds (f '' s)
• inv_antitoneOn_Iio 📋 Mathlib.Algebra.Order.Field.Basic
  {α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] : AntitoneOn (fun x => x⁻¹) (Set.Iio 0)
• inv_antitoneOn_Ioi 📋 Mathlib.Algebra.Order.Field.Basic
  {α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] : AntitoneOn (fun x => x⁻¹) (Set.Ioi 0)
• sub_inv_antitoneOn_Iio 📋 Mathlib.Algebra.Order.Field.Basic
  {α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {c : α} : AntitoneOn (fun x => (x - c)⁻¹) (Set.Iio c)
• sub_inv_antitoneOn_Ioi 📋 Mathlib.Algebra.Order.Field.Basic
  {α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {c : α} : AntitoneOn (fun x => (x - c)⁻¹) (Set.Ioi c)
• inv_antitoneOn_Icc_left 📋 Mathlib.Algebra.Order.Field.Basic
  {α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α} (hb : b < 0) : AntitoneOn (fun x => x⁻¹) (Set.Icc a b)
• inv_antitoneOn_Icc_right 📋 Mathlib.Algebra.Order.Field.Basic
  {α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α} (ha : 0 < a) : AntitoneOn (fun x => x⁻¹) (Set.Icc a b)
• sub_inv_antitoneOn_Icc_left 📋 Mathlib.Algebra.Order.Field.Basic
  {α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b c : α} (ha : b < c) : AntitoneOn (fun x => (x - c)⁻¹) (Set.Icc a b)
• sub_inv_antitoneOn_Icc_right 📋 Mathlib.Algebra.Order.Field.Basic
  {α : Type u_1} [Field α] [PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b c : α} (ha : c < a) : AntitoneOn (fun x => (x - c)⁻¹) (Set.Icc a b)
• AntitoneOn.sInf_image_Icc 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} [Preorder α] [ConditionallyCompleteLattice β] {f : α → β} {a b : α} (hab : a ≤ b) (h' : AntitoneOn f (Set.Icc a b)) : sInf (f '' Set.Icc a b) = f b
• AntitoneOn.sSup_image_Icc 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} [Preorder α] [ConditionallyCompleteLattice β] {f : α → β} {a b : α} (hab : b ≤ a) (h' : AntitoneOn f (Set.Icc b a)) : sSup (f '' Set.Icc b a) = f b
• Set.antitoneOn_iff_antitone 📋 Mathlib.Data.Set.Order
  {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] {f : α → β} : AntitoneOn f s ↔ Antitone fun a => f ↑a
• AntitoneOn.inter 📋 Mathlib.Data.Set.Order
  {α : Type u_1} {β : Type u_2} [Preorder β] {f g : β → Set α} {s : Set β} (hf : AntitoneOn f s) (hg : AntitoneOn g s) : AntitoneOn (fun x => f x ∩ g x) s
• AntitoneOn.union 📋 Mathlib.Data.Set.Order
  {α : Type u_1} {β : Type u_2} [Preorder β] {f g : β → Set α} {s : Set β} (hf : AntitoneOn f s) (hg : AntitoneOn g s) : AntitoneOn (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)
• AntitoneOn.mapsTo_Ici 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a : α} (h : AntitoneOn f (Set.Ici a)) : Set.MapsTo f (Set.Ici a) (Set.Iic (f a))
• AntitoneOn.mapsTo_Iic 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {b : α} (h : AntitoneOn f (Set.Iic b)) : Set.MapsTo f (Set.Iic b) (Set.Ici (f b))
• AntitoneOn.image_Ici_subset 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a : α} (h : AntitoneOn f (Set.Ici a)) : f '' Set.Ici a ⊆ Set.Iic (f a)
• AntitoneOn.image_Iic_subset 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {b : α} (h : AntitoneOn f (Set.Iic b)) : f '' Set.Iic b ⊆ Set.Ici (f b)
• AntitoneOn.mapsTo_Icc 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a b : α} (h : AntitoneOn f (Set.Icc a b)) : Set.MapsTo f (Set.Icc a b) (Set.Icc (f b) (f a))
• AntitoneOn.image_Icc_subset 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a b : α} (h : AntitoneOn f (Set.Icc a b)) : f '' Set.Icc a b ⊆ Set.Icc (f b) (f a)
• AntitoneOn.mapsTo_uIcc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [Lattice β] {f : α → β} {a b : α} (hf : AntitoneOn f (Set.uIcc a b)) : Set.MapsTo f (Set.uIcc a b) (Set.uIcc (f a) (f b))
• AntitoneOn.image_uIcc_subset 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [Lattice β] {f : α → β} {a b : α} (hf : AntitoneOn 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_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
• Set.OrdConnected.preimage_antitoneOn 📋 Mathlib.Order.Interval.Set.OrdConnected
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : β → α} {t : Set β} {s : Set α} (hs : s.OrdConnected) (hf : AntitoneOn f t) : ∃ u, u.OrdConnected ∧ t ∩ f ⁻¹' s = t ∩ u
• AddConstMapClass.antitone_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) : Antitone ⇑f ↔ AntitoneOn (⇑f) (Set.Icc l (l + a))
• antitoneOn_of_le_pred 📋 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 a ≤ f (Order.pred a)) : AntitoneOn f s
• antitoneOn_of_succ_le 📋 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 (Order.succ a) ≤ f a) : AntitoneOn f s
• antitoneOn_of_add_one_le 📋 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 + 1) ≤ f a) → AntitoneOn f s
• antitoneOn_of_le_sub_one 📋 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 ≤ f (a - 1)) → AntitoneOn f s
• AntitoneOn.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, AntitoneOn (f i) u) : AntitoneOn (fun x => ∏ i ∈ s, f i x) u
• AntitoneOn.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, AntitoneOn (f i) u) : AntitoneOn (fun x => ∑ i ∈ s, f i x) u
• AntitoneOn.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, AntitoneOn (f i) u) (hf₀ : ∀ i ∈ s, ∀ x ∈ u, 0 ≤ f i x) : AntitoneOn (fun x => ∏ i ∈ s, f i x) u
• Finite.map_iInf_of_antitoneOn 📋 Mathlib.Data.Fintype.Order
  {α : Type u_1} {β : Type u_2} {ι : Type u_3} [ConditionallyCompleteLinearOrder α] [ConditionallyCompleteLattice β] [Finite ι] [Nonempty ι] {s : Set α} {f : ι → α} {g : α → β} (hg : AntitoneOn g s) (hs : ∀ (i : ι), f i ∈ s) : g (⨅ i, f i) = ⨆ i, g (f i)
• Finite.map_iSup_of_antitoneOn 📋 Mathlib.Data.Fintype.Order
  {α : Type u_1} {β : Type u_2} {ι : Type u_3} [ConditionallyCompleteLinearOrder α] [ConditionallyCompleteLattice β] [Finite ι] [Nonempty ι] {s : Set α} {f : ι → α} {g : α → β} (hg : AntitoneOn g s) (hs : ∀ (i : ι), f i ∈ s) : g (⨆ i, f i) = ⨅ i, g (f i)
• Filter.HasBasis.prod_same_index_anti 📋 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 : AntitoneOn sa {i | p i}) (hsb : AntitoneOn sb {i | p i}) : (la ×ˢ lb).HasBasis p fun i => sa i ×ˢ sb i
• Nat.clog_antitone_left 📋 Mathlib.Data.Nat.Log
  {n : ℕ} : AntitoneOn (fun b => Nat.clog b n) (Set.Ioi 1)
• Nat.log_antitone_left 📋 Mathlib.Data.Nat.Log
  {n : ℕ} : AntitoneOn (fun b => Nat.log b n) (Set.Ioi 1)
• 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_antitoneOn 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] [Preorder β] {s : Set β} : IsClosed {f | AntitoneOn f s}
• antitoneOn_of_frequently_antitoneOn_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, AntitoneOn (F i) s) (hlim : ∀ x ∈ s, Filter.Tendsto (fun i => F i x) l (nhds (f x))) : AntitoneOn 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
• IsGLB.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 : AntitoneOn f s) (ha : IsGLB s a) (hs : s.Nonempty) (hb : Filter.Tendsto f (nhdsWithin a s) (nhds b)) : IsLUB (f '' s) b
• IsLUB.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 : AntitoneOn f s) (ha : IsLUB s a) (hs : s.Nonempty) (hb : Filter.Tendsto f (nhdsWithin a s) (nhds b)) : IsGLB (f '' s) b
• IsGLB.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 : AntitoneOn f s) (ha : IsGLB s a) (hb : Filter.Tendsto f (nhdsWithin a s) (nhds b)) : b ∈ upperBounds (f '' s)
• IsLUB.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 : AntitoneOn f s) (ha : IsLUB s a) (hb : Filter.Tendsto f (nhdsWithin a s) (nhds b)) : b ∈ lowerBounds (f '' s)
• AntitoneOn.countable_not_continuousWithinAt 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] {f : α → β} [TopologicalSpace β] [OrderTopology β] [SecondCountableTopology β] {s : Set α} (hf : AntitoneOn f s) : {x | x ∈ s ∧ ¬ContinuousWithinAt f s x}.Countable
• AntitoneOn.countable_setOfPred_two_preimages 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] {s : Set α} {f : α → β} [SecondCountableTopology α] (hf : AntitoneOn f s) : {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}.Countable
• AntitoneOn.countable_setOf_two_preimages 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] {s : Set α} {f : α → β} [SecondCountableTopology α] (hf : AntitoneOn f s) : {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}.Countable
• AntitoneOn.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)) (Af : AntitoneOn f A) (A_nonemp : A.Nonempty) (A_bdd : BddBelow A := by bddDefault) : f (sInf A) = sSup (f '' A)
• AntitoneOn.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)) (Af : AntitoneOn f A) (A_nonemp : A.Nonempty) (A_bdd : BddAbove A := by bddDefault) : f (sSup A) = sInf (f '' A)
• AntitoneOn.tendsto_nhdsGT 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_3} {β : Type u_4} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {x : α} (Af : AntitoneOn f (Set.Ioi x)) (h_bdd : BddAbove (f '' Set.Ioi x)) : Filter.Tendsto f (nhdsWithin x (Set.Ioi x)) (nhds (sSup (f '' Set.Ioi x)))
• AntitoneOn.tendsto_nhdsLT 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_3} {β : Type u_4} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {x : α} (Af : AntitoneOn f (Set.Iio x)) (h_bdd : BddBelow (f '' Set.Iio x)) : Filter.Tendsto f (nhdsWithin x (Set.Iio x)) (nhds (sInf (f '' Set.Iio x)))
• AntitoneOn.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) (Af : AntitoneOn f (Set.Ioo y x)) (h_bdd : BddBelow (f '' Set.Ioo y x)) : Filter.Tendsto f (nhdsWithin x (Set.Iio x)) (nhds (sInf (f '' Set.Ioo y x)))
• AntitoneOn.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) (Af : AntitoneOn f (Set.Ioo x y)) (h_bdd : BddAbove (f '' Set.Ioo x y)) : Filter.Tendsto f (nhdsWithin x (Set.Ioi x)) (nhds (sSup (f '' Set.Ioo x y)))
• AntitoneOn.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)) (Af : AntitoneOn f s) (ftop : f ⊤ = ⊥) : f (sInf s) = sSup (f '' s)
• AntitoneOn.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)) (Af : AntitoneOn f s) (fbot : f ⊥ = ⊤) : f (sSup s) = sInf (f '' s)
• ContinuousOn.image_uIcc_of_antitoneOn 📋 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 : AntitoneOn f (Set.uIcc a b)) : f '' Set.uIcc a b = Set.uIcc (f a) (f b)
• ContinuousOn.image_Icc_of_antitoneOn 📋 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 : AntitoneOn f (Set.Icc a b)) : f '' Set.Icc a b = Set.Icc (f b) (f a)
• ContinuousOn.image_Ici_of_antitoneOn 📋 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 : AntitoneOn f (Set.Ici a)) (htop : Filter.Tendsto f Filter.atTop Filter.atBot) : f '' Set.Ici a = Set.Iic (f a)
• ContinuousOn.image_Iic_of_antitoneOn 📋 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 : AntitoneOn f (Set.Iic a)) (hbot : Filter.Tendsto f Filter.atBot Filter.atTop) : f '' Set.Iic a = Set.Ici (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.Iic 📋 Mathlib.Order.Interval.Set.Monotone
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} (hf : AntitoneOn f s) : AntitoneOn (fun x => Set.Iic (f x)) s
• AntitoneOn.Iio 📋 Mathlib.Order.Interval.Set.Monotone
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} (hf : AntitoneOn f s) : AntitoneOn (fun x => Set.Iio (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.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_antitoneOn 📋 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 : AntitoneOn f s) : AEMeasurable f (μ.restrict s)
• Real.tendsto_atTop_csInf_of_antitoneOn_bddBelow_nat_Ici 📋 Mathlib.Topology.Instances.Real.Lemmas
  {f : ℕ → ℝ} {k : ℕ} (h_ant : AntitoneOn f (Set.Ici k)) (h_bdd : BddBelow (f '' Set.Ici k)) : Filter.Tendsto f Filter.atTop (nhds (sInf (f '' Set.Ici k)))
• Real.isGLB_of_tendsto_antitoneOn_bddBelow_nat_Ici 📋 Mathlib.Topology.Instances.Real.Lemmas
  {f : ℕ → ℝ} {k : ℕ} {x : ℝ} (h_tto : Filter.Tendsto f Filter.atTop (nhds x)) (h_ant : AntitoneOn f (Set.Ici k)) (h_bdd : BddBelow (f '' Set.Ici k)) : IsGLB (f '' Set.Ici k) x
• MeasurableSet.image_of_antitoneOn 📋 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 : AntitoneOn g t) : MeasurableSet (g '' t)
• Real.antitoneOn_cos 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
  : AntitoneOn Real.cos (Set.Icc 0 Real.pi)
• Real.antitoneOn_rpow_Ioi_of_exponent_nonpos 📋 Mathlib.Analysis.SpecialFunctions.Pow.Real
  {r : ℝ} (hr : r ≤ 0) : AntitoneOn (fun x => x ^ r) (Set.Ioi 0)
• AntitoneOn.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 : AntitoneOn f s) (hs : Convex 𝕜 s) (r : β) : Convex 𝕜 {x | x ∈ s ∧ r ≤ f x}
• AntitoneOn.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 : AntitoneOn f s) (hs : Convex 𝕜 s) (r : β) : Convex 𝕜 {x | x ∈ s ∧ r < f x}
• AntitoneOn.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 : AntitoneOn f s) (hs : Convex 𝕜 s) (r : β) : Convex 𝕜 {x | x ∈ s ∧ f x ≤ r}
• AntitoneOn.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 : AntitoneOn f s) (hs : Convex 𝕜 s) (r : β) : Convex 𝕜 {x | x ∈ s ∧ f x < r}
• ConcaveOn.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 : ConcaveOn 𝕜 (f '' s) g) (hf : ConvexOn 𝕜 s f) (hg' : AntitoneOn g (f '' s)) : ConcaveOn 𝕜 s (g ∘ f)
• ConvexOn.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 : ConvexOn 𝕜 (f '' s) g) (hf : ConcaveOn 𝕜 s f) (hg' : AntitoneOn g (f '' s)) : ConvexOn 𝕜 s (g ∘ f)
• StrictConcaveOn.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 : StrictConcaveOn 𝕜 (f '' s) g) (hf : ConvexOn 𝕜 s f) (hg' : AntitoneOn g (f '' s)) (hf' : Set.InjOn f s) : StrictConcaveOn 𝕜 s (g ∘ f)
• StrictConvexOn.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 : StrictConvexOn 𝕜 (f '' s) g) (hf : ConcaveOn 𝕜 s f) (hg' : AntitoneOn g (f '' s)) (hf' : Set.InjOn f s) : StrictConvexOn 𝕜 s (g ∘ f)
• antivaryOn_id_iff 📋 Mathlib.Order.Monotone.Monovary
  {ι : Type u_1} {α : Type u_3} [Preorder α] {f : ι → α} {s : Set ι} [PartialOrder ι] : AntivaryOn f id s ↔ AntitoneOn f s
• StrictAntiOn.trans_monovaryOn 📋 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 : MonovaryOn g f s) : AntitoneOn g s
• 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
• 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
• AntitoneOn.monovaryOn 📋 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 : AntitoneOn g s) : MonovaryOn f g s
• MonotoneOn.antivaryOn 📋 Mathlib.Order.Monotone.Monovary
  {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} {s : Set ι} [LinearOrder ι] (hf : MonotoneOn f s) (hg : AntitoneOn g s) : AntivaryOn f g s
• AntivaryOn.comp_antitoneOn_right 📋 Mathlib.Order.Monotone.Monovary
  {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder α] [LinearOrder β] [Preorder γ] {f : ι → α} {g : ι → β} {g' : β → γ} {s : Set ι} (h : AntivaryOn f g s) (hg : AntitoneOn g' (g '' s)) : MonovaryOn f (g' ∘ g) s
• MonovaryOn.comp_antitoneOn_right 📋 Mathlib.Order.Monotone.Monovary
  {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder α] [LinearOrder β] [Preorder γ] {f : ι → α} {g : ι → β} {g' : β → γ} {s : Set ι} (h : MonovaryOn f g s) (hg : AntitoneOn g' (g '' s)) : AntivaryOn f (g' ∘ g) s
• AntitoneOn.integrableOn_isCompact 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} {s : Set X} [BorelSpace X] [ConditionallyCompleteLinearOrder X] [ConditionallyCompleteLinearOrder E] [OrderTopology X] [OrderTopology E] [SecondCountableTopology E] {f : X → E} [MeasureTheory.IsFiniteMeasureOnCompacts μ] (hs : IsCompact s) (hanti : AntitoneOn f s) : MeasureTheory.IntegrableOn f s μ
• AntitoneOn.memLp_isCompact 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} {s : Set X} [BorelSpace X] [ConditionallyCompleteLinearOrder X] [ConditionallyCompleteLinearOrder E] [OrderTopology X] [OrderTopology E] [SecondCountableTopology E] {p : ENNReal} {f : X → E} [MeasureTheory.IsFiniteMeasureOnCompacts μ] (hs : IsCompact s) (hanti : AntitoneOn f s) : MeasureTheory.MemLp f p (μ.restrict s)
• AntitoneOn.integrableOn_of_measure_ne_top 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} {s : Set X} [BorelSpace X] [ConditionallyCompleteLinearOrder X] [ConditionallyCompleteLinearOrder E] [OrderTopology X] [OrderTopology E] [SecondCountableTopology E] {f : X → E} (hanti : AntitoneOn f s) {a b : X} (ha : IsLeast s a) (hb : IsGreatest s b) (hs : μ s ≠ ⊤) (h's : MeasurableSet s) : MeasureTheory.IntegrableOn f s μ
• AntitoneOn.memLp_top 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} {s : Set X} [BorelSpace X] [ConditionallyCompleteLinearOrder X] [ConditionallyCompleteLinearOrder E] [OrderTopology X] [OrderTopology E] [SecondCountableTopology E] {f : X → E} (hanti : AntitoneOn f s) {a b : X} (ha : IsLeast s a) (hb : IsGreatest s b) (h's : MeasurableSet s) : MeasureTheory.MemLp f ⊤ (μ.restrict s)
• AntitoneOn.memLp_of_measure_ne_top 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} {s : Set X} [BorelSpace X] [ConditionallyCompleteLinearOrder X] [ConditionallyCompleteLinearOrder E] [OrderTopology X] [OrderTopology E] [SecondCountableTopology E] {p : ENNReal} {f : X → E} (hanti : AntitoneOn f s) {a b : X} (ha : IsLeast s a) (hb : IsGreatest s b) (hs : μ s ≠ ⊤) (h's : MeasurableSet s) : MeasureTheory.MemLp f p (μ.restrict s)
• MeasureTheory.integral_antitoneOn_of_integrand_ae 📋 Mathlib.MeasureTheory.Integral.Bochner.Basic
  {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] [ClosedIciTopology E] {β : Type u_6} [Preorder β] {f : α → β → E} {s : Set β} (hf_anti : ∀ᵐ (x : α) ∂μ, AntitoneOn (f x) s) (hf_int : ∀ a ∈ s, MeasureTheory.Integrable (fun x => f x a) μ) : AntitoneOn (fun b => ∫ (x : α), f x b ∂μ) s
• ArchimedeanClass.mk_antitoneOn 📋 Mathlib.Algebra.Order.Archimedean.Class
  {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : AntitoneOn ArchimedeanClass.mk (Set.Ici 0)
• MulArchimedeanClass.mk_antitoneOn 📋 Mathlib.Algebra.Order.Archimedean.Class
  {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] : AntitoneOn MulArchimedeanClass.mk (Set.Ici 1)
• AntitoneOn.slope_nonpos 📋 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 : AntitoneOn f s) (hx : x ∈ s) (hy : y ∈ s) : slope f x y ≤ 0
• AntitoneOn.derivWithin_nonpos 📋 Mathlib.Analysis.Calculus.Deriv.Slope
  {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [OrderTopology 𝕜] {g : 𝕜 → 𝕜} (hg : AntitoneOn g s) : derivWithin g s x ≤ 0
• HasDerivWithinAt.nonpos_of_antitoneOn 📋 Mathlib.Analysis.Calculus.Deriv.Slope
  {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [OrderTopology 𝕜] {g : 𝕜 → 𝕜} {g' : 𝕜} (hx : AccPt x (Filter.principal s)) (hd : HasDerivWithinAt g g' s x) (hg : AntitoneOn g s) : g' ≤ 0

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