Loogle!

Result

Found 1472 declarations mentioning OrderTopology. Of these, only the first 200 are shown.

• OrderTopology 📋 Mathlib.Topology.Order.Basic
  (α : Type u_1) [t : TopologicalSpace α] [Preorder α] : Prop
• instSecondCountableTopologyOfOrderTopologyOfCountable 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] [Countable α] : SecondCountableTopology α
• OrderTopology.mk 📋 Mathlib.Topology.Order.Basic
  {α : Type u_1} [t : TopologicalSpace α] [Preorder α] (topology_eq_generate_intervals : t = Preorder.topology α) : OrderTopology α
• OrderTopology.topology_eq_generate_intervals 📋 Mathlib.Topology.Order.Basic
  {α : Type u_1} {t : TopologicalSpace α} {inst✝ : Preorder α} [self : OrderTopology α] : t = Preorder.topology α
• isOpen_Iio' 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) : IsOpen (Set.Iio a)
• isOpen_Ioi' 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) : IsOpen (Set.Ioi a)
• instOrderTopologyOrderDual 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [ts : TopologicalSpace α] [Preorder α] [t : OrderTopology α] : OrderTopology αᵒᵈ
• isOpen_Ioo' 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] (a b : α) : IsOpen (Set.Ioo a b)
• isOpen_gt' 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) : IsOpen {b | b < a}
• isOpen_lt' 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) : IsOpen {b | a < b}
• tendstoIccClassNhds 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) : Filter.TendstoIxxClass Set.Icc (nhds a) (nhds a)
• tendstoIcoClassNhds 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) : Filter.TendstoIxxClass Set.Ico (nhds a) (nhds a)
• tendstoIocClassNhds 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) : Filter.TendstoIxxClass Set.Ioc (nhds a) (nhds a)
• tendstoIooClassNhds 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) : Filter.TendstoIxxClass Set.Ioo (nhds a) (nhds a)
• ge_mem_nhds 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] {a b : α} (h : b < a) : ∀ᶠ (x : α) in nhds b, x ≤ a
• gt_mem_nhds 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] {a b : α} (h : b < a) : ∀ᶠ (x : α) in nhds b, x < a
• le_mem_nhds 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] {a b : α} (h : a < b) : ∀ᶠ (x : α) in nhds b, a ≤ x
• lt_mem_nhds 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] {a b : α} (h : a < b) : ∀ᶠ (x : α) in nhds b, a < x
• OrderTopology.to_orderClosedTopology 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] : OrderClosedTopology α
• instIsCountablyGenerated_atBot 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [TopologicalSpace.SeparableSpace α] : Filter.atBot.IsCountablyGenerated
• instIsCountablyGenerated_atTop 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [TopologicalSpace.SeparableSpace α] : Filter.atTop.IsCountablyGenerated
• SecondCountableTopology.of_separableSpace_orderTopology 📋 Mathlib.Topology.Order.Basic
  (α : Type u) [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [TopologicalSpace.SeparableSpace α] : SecondCountableTopology α
• isOpen_iff_generate_intervals 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [ts : TopologicalSpace α] [Preorder α] [t : OrderTopology α] {s : Set α} : IsOpen s ↔ TopologicalSpace.GenerateOpen {s | ∃ a, s = Set.Ioi a ∨ s = Set.Iio a} s
• OrderTopology.continuous_iff 📋 Mathlib.Topology.Order.Basic
  {α : Type u} {β : Type v} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] [TopologicalSpace β] {f : β → α} : Continuous f ↔ ∀ (a : α), IsOpen (f ⁻¹' Set.Ioi a) ∧ IsOpen (f ⁻¹' Set.Iio a)
• countable_setOfPred_covBy_left 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] : {x | ∃ y, y ⋖ x}.Countable
• countable_setOfPred_covBy_right 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] : {x | ∃ y, x ⋖ y}.Countable
• countable_setOf_covBy_left 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] : {x | ∃ y, y ⋖ x}.Countable
• countable_setOf_covBy_right 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] : {x | ∃ y, x ⋖ y}.Countable
• induced_topology_le_preorder 📋 Mathlib.Topology.Order.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : ∀ {x y : α}, f x < f y ↔ x < y) : TopologicalSpace.induced f inst✝ ≤ Preorder.topology α
• tendstoIccClassNhdsPi 📋 Mathlib.Topology.Order.Basic
  {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Preorder (α i)] [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), OrderTopology (α i)] (f : (i : ι) → α i) : Filter.TendstoIxxClass Set.Icc (nhds f) (nhds f)
• IsLowerSet.isClosed 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [WellFoundedGT α] {s : Set α} (h : IsLowerSet s) : IsClosed s
• IsLowerSet.isOpen 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [WellFoundedLT α] {s : Set α} (h : IsLowerSet s) : IsOpen s
• IsUpperSet.isClosed 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [WellFoundedLT α] {s : Set α} (h : IsUpperSet s) : IsClosed s
• IsUpperSet.isOpen 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [WellFoundedGT α] {s : Set α} (h : IsUpperSet s) : IsOpen s
• exists_countable_generateFrom_Ioi_Iio 📋 Mathlib.Topology.Order.Basic
  (α : Type u) [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] [SecondCountableTopology α] : ∃ c, c.Countable ∧ ts = TopologicalSpace.generateFrom {s | ∃ a ∈ c, s = Set.Ioi a ∨ s = Set.Iio a}
• tendsto_nhds_bot_mono 📋 Mathlib.Topology.Order.Basic
  {α : Type u} {β : Type v} [TopologicalSpace β] [Preorder β] [OrderBot β] [OrderTopology β] {l : Filter α} {f g : α → β} (hf : Filter.Tendsto f l (nhds ⊥)) (hg : g ≤ᶠ[l] f) : Filter.Tendsto g l (nhds ⊥)
• tendsto_nhds_top_mono 📋 Mathlib.Topology.Order.Basic
  {α : Type u} {β : Type v} [TopologicalSpace β] [Preorder β] [OrderTop β] [OrderTopology β] {l : Filter α} {f g : α → β} (hf : Filter.Tendsto f l (nhds ⊤)) (hg : f ≤ᶠ[l] g) : Filter.Tendsto g l (nhds ⊤)
• nhdsGE_eq_iInf_inf_principal 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) : nhdsWithin a (Set.Ici a) = (⨅ u, ⨅ (_ : a < u), Filter.principal (Set.Iio u)) ⊓ Filter.principal (Set.Ici a)
• nhdsGE_eq_iInf_principal 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] {a : α} (ha : ∃ u, a < u) : nhdsWithin a (Set.Ici a) = ⨅ u, ⨅ (_ : a < u), Filter.principal (Set.Ico a u)
• nhdsLE_eq_iInf_inf_principal 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) : nhdsWithin a (Set.Iic a) = (⨅ u, ⨅ (_ : u < a), Filter.principal (Set.Ioi u)) ⊓ Filter.principal (Set.Iic a)
• nhdsLE_eq_iInf_principal 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTopology α] {a : α} (ha : ∃ u, u < a) : nhdsWithin a (Set.Iic a) = ⨅ u, ⨅ (_ : u < a), Filter.principal (Set.Ioc u a)
• induced_orderTopology 📋 Mathlib.Topology.Order.Basic
  {α : Type u_1} {β : Type u_2} [Preorder α] [ta : TopologicalSpace β] [Preorder β] [OrderTopology β] (f : α → β) (hf : ∀ {x y : α}, f x < f y ↔ x < y) (H : ∀ {x y : β}, x < y → ∃ a, f a ∈ Set.Ioo x y) : OrderTopology α
• tendsto_nhds_bot_mono' 📋 Mathlib.Topology.Order.Basic
  {α : Type u} {β : Type v} [TopologicalSpace β] [Preorder β] [OrderBot β] [OrderTopology β] {l : Filter α} {f g : α → β} (hf : Filter.Tendsto f l (nhds ⊥)) (hg : g ≤ f) : Filter.Tendsto g l (nhds ⊥)
• tendsto_nhds_top_mono' 📋 Mathlib.Topology.Order.Basic
  {α : Type u} {β : Type v} [TopologicalSpace β] [Preorder β] [OrderTop β] [OrderTopology β] {l : Filter α} {f g : α → β} (hf : Filter.Tendsto f l (nhds ⊤)) (hg : f ≤ g) : Filter.Tendsto g l (nhds ⊤)
• tendsto_order 📋 Mathlib.Topology.Order.Basic
  {α : Type u} {β : Type v} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] {f : β → α} {a : α} {x : Filter β} : Filter.Tendsto f x (nhds a) ↔ (∀ a' < a, ∀ᶠ (b : β) in x, a' < f b) ∧ ∀ a' > a, ∀ᶠ (b : β) in x, f b < a'
• countable_of_isolated_left' 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] : {x | ∃ y < x, Set.Ioo y x = ∅}.Countable
• tendsto_of_tendsto_of_tendsto_of_le_of_le 📋 Mathlib.Topology.Order.Basic
  {α : Type u} {β : Type v} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] {f g h : β → α} {b : Filter β} {a : α} (hg : Filter.Tendsto g b (nhds a)) (hh : Filter.Tendsto h b (nhds a)) (hgf : g ≤ f) (hfh : f ≤ h) : Filter.Tendsto f b (nhds a)
• tendsto_of_tendsto_of_tendsto_of_le_of_le' 📋 Mathlib.Topology.Order.Basic
  {α : Type u} {β : Type v} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] {f g h : β → α} {b : Filter β} {a : α} (hg : Filter.Tendsto g b (nhds a)) (hh : Filter.Tendsto h b (nhds a)) (hgf : ∀ᶠ (b : β) in b, g b ≤ f b) (hfh : ∀ᶠ (b : β) in b, f b ≤ h b) : Filter.Tendsto f b (nhds a)
• Filter.Tendsto.squeeze 📋 Mathlib.Topology.Order.Basic
  {α : Type u} {β : Type v} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] {f g h : β → α} {b : Filter β} {a : α} (hg : Filter.Tendsto g b (nhds a)) (hh : Filter.Tendsto h b (nhds a)) (hgf : g ≤ f) (hfh : f ≤ h) : Filter.Tendsto f b (nhds a)
• Filter.Tendsto.squeeze' 📋 Mathlib.Topology.Order.Basic
  {α : Type u} {β : Type v} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] {f g h : β → α} {b : Filter β} {a : α} (hg : Filter.Tendsto g b (nhds a)) (hh : Filter.Tendsto h b (nhds a)) (hgf : ∀ᶠ (b : β) in b, g b ≤ f b) (hfh : ∀ᶠ (b : β) in b, f b ≤ h b) : Filter.Tendsto f b (nhds a)
• orderTopology_of_ordConnected 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {t : Set α} [ht : t.OrdConnected] : OrderTopology ↑t
• nhds_bot_order 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [Preorder α] [OrderBot α] [OrderTopology α] : nhds ⊥ = ⨅ l, ⨅ (_ : ⊥ < l), Filter.principal (Set.Iio l)
• nhds_top_order 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [Preorder α] [OrderTop α] [OrderTopology α] : nhds ⊤ = ⨅ l, ⨅ (_ : l < ⊤), Filter.principal (Set.Ioi l)
• IsOpen.exists_Ioo_subset 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Nontrivial α] {s : Set α} (hs : IsOpen s) (h : s.Nonempty) : ∃ a b, a < b ∧ Set.Ioo a b ⊆ s
• dense_of_exists_between 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Nontrivial α] {s : Set α} (h : ∀ ⦃a b : α⦄, a < b → ∃ c ∈ s, c ∈ Set.Ioo a b) : Dense s
• tendsto_order_unbounded 📋 Mathlib.Topology.Order.Basic
  {α : Type u} {β : Type v} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] {f : β → α} {a : α} {x : Filter β} (hu : ∃ u, a < u) (hl : ∃ l, l < a) (h : ∀ (l u : α), l < a → a < u → ∀ᶠ (b : β) in x, l < f b ∧ f b < u) : Filter.Tendsto f x (nhds a)
• pi_Ici_mem_nhds' 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι] {a' x' : ι → α} (ha : ∀ (i : ι), a' i < x' i) : Set.Ici a' ∈ nhds x'
• pi_Iic_mem_nhds' 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι] {a' x' : ι → α} (ha : ∀ (i : ι), x' i < a' i) : Set.Iic a' ∈ nhds x'
• pi_Iio_mem_nhds' 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι] {a' x' : ι → α} [Nonempty ι] (ha : ∀ (i : ι), x' i < a' i) : Set.Iio a' ∈ nhds x'
• pi_Ioi_mem_nhds' 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι] {a' x' : ι → α} [Nonempty ι] (ha : ∀ (i : ι), a' i < x' i) : Set.Ioi a' ∈ nhds x'
• LeftOrdContinuous.continuousWithinAt_Iic 📋 Mathlib.Topology.Order.Basic
  {X : Type u_1} [ConditionallyCompleteLinearOrder X] [TopologicalSpace X] [OrderTopology X] {Y : Type u_2} [ConditionallyCompleteLinearOrder Y] [TopologicalSpace Y] [OrderTopology Y] {f : X → Y} {x : X} (hf : LeftOrdContinuous f) : ContinuousWithinAt f (Set.Iic x) x
• RightOrdContinuous.continuousWithinAt_Ici 📋 Mathlib.Topology.Order.Basic
  {X : Type u_1} [ConditionallyCompleteLinearOrder X] [TopologicalSpace X] [OrderTopology X] {Y : Type u_2} [ConditionallyCompleteLinearOrder Y] [TopologicalSpace Y] [OrderTopology Y] {f : X → Y} {x : X} (hf : RightOrdContinuous f) : ContinuousWithinAt f (Set.Ici x) x
• StrictMono.induced_topology_eq_preorder 📋 Mathlib.Topology.Order.Basic
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] [t : TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : StrictMono f) (hc : (Set.range f).OrdConnected) : TopologicalSpace.induced f t = Preorder.topology α
• Dense.topology_eq_generateFrom 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {s : Set α} (hs : Dense s) : inst✝ = TopologicalSpace.generateFrom (Set.Ioi '' s ∪ Set.Iio '' s)
• PredOrder.hasBasis_nhds_Ico 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [PredOrder α] {a : α} [NoMaxOrder α] : (nhds a).HasBasis (fun x => a < x) fun x => Set.Ico a x
• PredOrder.hasBasis_nhds_Ioc 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [PredOrder α] {a : α} [NoMaxOrder α] : (nhds a).HasBasis (fun x => a < x) fun x => Set.Ico a x
• StrictMono.isEmbedding_of_ordConnected 📋 Mathlib.Topology.Order.Basic
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] [TopologicalSpace α] [h : OrderTopology α] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : StrictMono f) (hc : (Set.range f).OrdConnected) : Topology.IsEmbedding f
• SuccOrder.hasBasis_nhds_Ioc 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SuccOrder α] {a : α} [NoMinOrder α] : (nhds a).HasBasis (fun x => x < a) fun x => Set.Ioc x a
• countable_image_gt_image_Iio 📋 Mathlib.Topology.Order.Basic
  {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [LinearOrder β] (f : β → α) [SecondCountableTopology α] : {x | ∃ z, f x < z ∧ ∀ y < x, z ≤ f y}.Countable
• countable_image_gt_image_Ioi 📋 Mathlib.Topology.Order.Basic
  {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [LinearOrder β] (f : β → α) [SecondCountableTopology α] : {x | ∃ z < f x, ∀ (y : β), x < y → f y ≤ z}.Countable
• countable_image_lt_image_Iio 📋 Mathlib.Topology.Order.Basic
  {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [LinearOrder β] (f : β → α) [SecondCountableTopology α] : {x | ∃ z < f x, ∀ y < x, f y ≤ z}.Countable
• countable_image_lt_image_Ioi 📋 Mathlib.Topology.Order.Basic
  {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [LinearOrder β] (f : β → α) [SecondCountableTopology α] : {x | ∃ z, f x < z ∧ ∀ (y : β), x < y → z ≤ f y}.Countable
• nhdsGE_basis 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] (a : α) : (nhdsWithin a (Set.Ici a)).HasBasis (fun u => a < u) fun u => Set.Ico a u
• nhdsLE_basis 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMinOrder α] (a : α) : (nhdsWithin a (Set.Iic a)).HasBasis (fun u => u < a) fun u => Set.Ioc u a
• PredOrder.hasBasis_nhds_Ico_of_exists_gt 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [PredOrder α] {a : α} (ha : ∃ l, a < l) : (nhds a).HasBasis (fun x => a < x) fun x => Set.Ico a x
• PredOrder.hasBasis_nhds_Ioc_of_exists_gt 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [PredOrder α] {a : α} (ha : ∃ l, a < l) : (nhds a).HasBasis (fun x => a < x) fun x => Set.Ico a x
• SuccOrder.hasBasis_nhds_Ioc_of_exists_lt 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SuccOrder α] {a : α} (ha : ∃ l, l < a) : (nhds a).HasBasis (fun x => x < a) fun x => Set.Ioc x a
• nhdsGE_basis_of_exists_gt 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} (ha : ∃ u, a < u) : (nhdsWithin a (Set.Ici a)).HasBasis (fun u => a < u) fun u => Set.Ico a u
• nhdsLE_basis_of_exists_lt 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} (ha : ∃ u, u < a) : (nhdsWithin a (Set.Iic a)).HasBasis (fun u => u < a) fun u => Set.Ioc u a
• exists_Ico_subset_of_mem_nhds 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (hs : s ∈ nhds a) (h : ∃ l, a < l) : ∃ l, a < l ∧ Set.Ico a l ⊆ s
• exists_Ioc_subset_of_mem_nhds 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (hs : s ∈ nhds a) (h : ∃ l, l < a) : ∃ l < a, Set.Ioc l a ⊆ s
• nhds_order_unbounded 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] {a : α} (hu : ∃ u, a < u) (hl : ∃ l, l < a) : nhds a = ⨅ l, ⨅ (_ : l < a), ⨅ u, ⨅ (_ : a < u), Filter.principal (Set.Ioo l u)
• Continuous.of_ordContinuous 📋 Mathlib.Topology.Order.Basic
  {X : Type u_1} [ConditionallyCompleteLinearOrder X] [TopologicalSpace X] [OrderTopology X] {Y : Type u_2} [ConditionallyCompleteLinearOrder Y] [TopologicalSpace Y] [OrderTopology Y] {f : X → Y} (hl : LeftOrdContinuous f) (hr : RightOrdContinuous f) : Continuous f
• exists_Ico_subset_of_mem_nhds' 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (hs : s ∈ nhds a) {l : α} (hl : a < l) : ∃ l' ∈ Set.Ioc a l, Set.Ico a l' ⊆ s
• exists_Ioc_subset_of_mem_nhds' 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (hs : s ∈ nhds a) {l : α} (hl : l < a) : ∃ l' ∈ Set.Ico l a, Set.Ioc l' a ⊆ s
• induced_orderTopology' 📋 Mathlib.Topology.Order.Basic
  {α : Type u_1} {β : Type u_2} [Preorder α] [ta : TopologicalSpace β] [Preorder β] [OrderTopology β] (f : α → β) (hf : ∀ {x y : α}, f x < f y ↔ x < y) (H₁ : ∀ {a : α} {x : β}, x < f a → ∃ b < a, x ≤ f b) (H₂ : ∀ {a : α} {x : β}, f a < x → ∃ b > a, f b ≤ x) : OrderTopology α
• nhds_eq_order 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [ts : TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) : nhds a = (⨅ b ∈ Set.Iio a, Filter.principal (Set.Ioi b)) ⊓ ⨅ b ∈ Set.Ioi a, Filter.principal (Set.Iio b)
• countable_image_gt_image_Iio_within 📋 Mathlib.Topology.Order.Basic
  {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [LinearOrder β] [SecondCountableTopology α] (t : Set β) (f : β → α) : {x | x ∈ t ∧ ∃ z, f x < z ∧ ∀ y ∈ t, y < x → z ≤ f y}.Countable
• countable_image_gt_image_Ioi_within 📋 Mathlib.Topology.Order.Basic
  {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [LinearOrder β] [SecondCountableTopology α] (t : Set β) (f : β → α) : {x | x ∈ t ∧ ∃ z < f x, ∀ y ∈ t, x < y → f y ≤ z}.Countable
• countable_image_lt_image_Iio_within 📋 Mathlib.Topology.Order.Basic
  {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [LinearOrder β] [SecondCountableTopology α] (t : Set β) (f : β → α) : {x | x ∈ t ∧ ∃ z < f x, ∀ y ∈ t, y < x → f y ≤ z}.Countable
• countable_image_lt_image_Ioi_within 📋 Mathlib.Topology.Order.Basic
  {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [LinearOrder β] [SecondCountableTopology α] (t : Set β) (f : β → α) : {x | x ∈ t ∧ ∃ z, f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}.Countable
• dense_iff_exists_between 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [Nontrivial α] {s : Set α} : Dense s ↔ ∀ (a b : α), a < b → ∃ c ∈ s, a < c ∧ c < b
• pi_Icc_mem_nhds' 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι] {a' b' x' : ι → α} (ha : ∀ (i : ι), a' i < x' i) (hb : ∀ (i : ι), x' i < b' i) : Set.Icc a' b' ∈ nhds x'
• nhds_bot_basis 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderBot α] [OrderTopology α] [Nontrivial α] : (nhds ⊥).HasBasis (fun a => ⊥ < a) fun a => Set.Iio a
• nhds_top_basis 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTop α] [OrderTopology α] [Nontrivial α] : (nhds ⊤).HasBasis (fun a => a < ⊤) fun a => Set.Ioi a
• exists_Icc_mem_subset_of_mem_nhds 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (hs : s ∈ nhds a) : ∃ b c, a ∈ Set.Icc b c ∧ Set.Icc b c ∈ nhds a ∧ Set.Icc b c ⊆ s
• order_separated 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a₁ a₂ : α} (h : a₁ < a₂) : ∃ u v, IsOpen u ∧ IsOpen v ∧ a₁ ∈ u ∧ a₂ ∈ v ∧ ∀ b₁ ∈ u, ∀ b₂ ∈ v, b₁ < b₂
• pi_Ico_mem_nhds' 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι] {a' b' x' : ι → α} [Nonempty ι] (ha : ∀ (i : ι), x' i < a' i) (hb : ∀ (i : ι), b' i < x' i) : Set.Ico b' a' ∈ nhds x'
• pi_Ioc_mem_nhds' 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι] {a' b' x' : ι → α} [Nonempty ι] (ha : ∀ (i : ι), a' i < x' i) (hb : ∀ (i : ι), x' i < b' i) : Set.Ioc a' b' ∈ nhds x'
• pi_Ioo_mem_nhds' 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι] {a' b' x' : ι → α} [Nonempty ι] (ha : ∀ (i : ι), a' i < x' i) (hb : ∀ (i : ι), x' i < b' i) : Set.Ioo a' b' ∈ nhds x'
• mem_nhds_iff_exists_Ioo_subset 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] [NoMinOrder α] {a : α} {s : Set α} : s ∈ nhds a ↔ ∃ l u, a ∈ Set.Ioo l u ∧ Set.Ioo l u ⊆ s
• Filter.Eventually.exists_Ioo_subset 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] [NoMinOrder α] {a : α} {p : α → Prop} (hp : ∀ᶠ (x : α) in nhds a, p x) : ∃ l u, a ∈ Set.Ioo l u ∧ Set.Ioo l u ⊆ {x | p x}
• Set.PairwiseDisjoint.countable_of_Ioo 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {y : α → α} {s : Set α} (h : s.PairwiseDisjoint fun x => Set.Ioo x (y x)) (h' : ∀ x ∈ s, x < y x) : s.Countable
• pi_Ici_mem_nhds 📋 Mathlib.Topology.Order.Basic
  {ι : Type u_1} {X : ι → Type u_2} [Finite ι] [(i : ι) → LinearOrder (X i)] [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), OrderTopology (X i)] {a x : (i : ι) → X i} (ha : ∀ (i : ι), a i < x i) : Set.Ici a ∈ nhds x
• pi_Iic_mem_nhds 📋 Mathlib.Topology.Order.Basic
  {ι : Type u_1} {X : ι → Type u_2} [Finite ι] [(i : ι) → LinearOrder (X i)] [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), OrderTopology (X i)] {a x : (i : ι) → X i} (ha : ∀ (i : ι), x i < a i) : Set.Iic a ∈ nhds x
• pi_Iio_mem_nhds 📋 Mathlib.Topology.Order.Basic
  {ι : Type u_1} {X : ι → Type u_2} [Finite ι] [(i : ι) → LinearOrder (X i)] [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), OrderTopology (X i)] {a x : (i : ι) → X i} [Nonempty ι] (ha : ∀ (i : ι), x i < a i) : Set.Iio a ∈ nhds x
• pi_Ioi_mem_nhds 📋 Mathlib.Topology.Order.Basic
  {ι : Type u_1} {X : ι → Type u_2} [Finite ι] [(i : ι) → LinearOrder (X i)] [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), OrderTopology (X i)] {a x : (i : ι) → X i} [Nonempty ι] (ha : ∀ (i : ι), a i < x i) : Set.Ioi a ∈ nhds x
• induced_topology_eq_preorder 📋 Mathlib.Topology.Order.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (hf : ∀ {x y : α}, f x < f y ↔ x < y) (H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y) (H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b) : TopologicalSpace.induced f inst✝ = Preorder.topology α
• nhds_bot_basis_Iic 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderBot α] [OrderTopology α] [Nontrivial α] [DenselyOrdered α] : (nhds ⊥).HasBasis (fun a => ⊥ < a) Set.Iic
• nhds_top_basis_Ici 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTop α] [OrderTopology α] [Nontrivial α] [DenselyOrdered α] : (nhds ⊤).HasBasis (fun a => a < ⊤) Set.Ici
• mem_nhds_iff_exists_Ioo_subset' 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (hl : ∃ l, l < a) (hu : ∃ u, a < u) : s ∈ nhds a ↔ ∃ l u, a ∈ Set.Ioo l u ∧ Set.Ioo l u ⊆ s
• nhds_basis_Ioo 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] [NoMinOrder α] (a : α) : (nhds a).HasBasis (fun b => b.1 < a ∧ a < b.2) fun b => Set.Ioo b.1 b.2
• exists_Icc_mem_subset_of_mem_nhdsGE 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (hs : s ∈ nhdsWithin a (Set.Ici a)) : ∃ b, a ≤ b ∧ Set.Icc a b ∈ nhdsWithin a (Set.Ici a) ∧ Set.Icc a b ⊆ s
• exists_Icc_mem_subset_of_mem_nhdsLE 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (hs : s ∈ nhdsWithin a (Set.Iic a)) : ∃ b ≤ a, Set.Icc b a ∈ nhdsWithin a (Set.Iic a) ∧ Set.Icc b a ⊆ s
• nhds_basis_Ioo' 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} (hl : ∃ l, l < a) (hu : ∃ u, a < u) : (nhds a).HasBasis (fun b => b.1 < a ∧ a < b.2) fun b => Set.Ioo b.1 b.2
• pi_Icc_mem_nhds 📋 Mathlib.Topology.Order.Basic
  {ι : Type u_1} {X : ι → Type u_2} [Finite ι] [(i : ι) → LinearOrder (X i)] [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), OrderTopology (X i)] {a b x : (i : ι) → X i} (ha : ∀ (i : ι), a i < x i) (hb : ∀ (i : ι), x i < b i) : Set.Icc a b ∈ nhds x
• pi_Ico_mem_nhds 📋 Mathlib.Topology.Order.Basic
  {ι : Type u_1} {X : ι → Type u_2} [Finite ι] [(i : ι) → LinearOrder (X i)] [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), OrderTopology (X i)] {a b x : (i : ι) → X i} [Nonempty ι] (ha : ∀ (i : ι), x i < a i) (hb : ∀ (i : ι), b i < x i) : Set.Ico b a ∈ nhds x
• pi_Ioc_mem_nhds 📋 Mathlib.Topology.Order.Basic
  {ι : Type u_1} {X : ι → Type u_2} [Finite ι] [(i : ι) → LinearOrder (X i)] [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), OrderTopology (X i)] {a b x : (i : ι) → X i} [Nonempty ι] (ha : ∀ (i : ι), a i < x i) (hb : ∀ (i : ι), x i < b i) : Set.Ioc a b ∈ nhds x
• pi_Ioo_mem_nhds 📋 Mathlib.Topology.Order.Basic
  {ι : Type u_1} {X : ι → Type u_2} [Finite ι] [(i : ι) → LinearOrder (X i)] [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), OrderTopology (X i)] {a b x : (i : ι) → X i} [Nonempty ι] (ha : ∀ (i : ι), a i < x i) (hb : ∀ (i : ι), x i < b i) : Set.Ioo a b ∈ nhds x
• OrderEmbedding.isEmbedding_of_ordConnected 📋 Mathlib.Topology.Order.Basic
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] [TopologicalSpace α] [OrderTopology α] [TopologicalSpace β] [OrderTopology β] (f : α ↪o β) (hc : (Set.range ⇑f).OrdConnected) : Topology.IsEmbedding ⇑f
• countable_setOfPred_isolated_left 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] : {x | nhdsWithin x (Set.Iio x) = ⊥}.Countable
• countable_setOfPred_isolated_right 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] : {x | nhdsWithin x (Set.Ioi x) = ⊥}.Countable
• countable_setOf_isolated_left 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] : {x | nhdsWithin x (Set.Iio x) = ⊥}.Countable
• countable_setOf_isolated_right 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] : {x | nhdsWithin x (Set.Ioi x) = ⊥}.Countable
• countable_setOfPred_isolated_left_within 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {s : Set α} : {x | x ∈ s ∧ nhdsWithin x (s ∩ Set.Iio x) = ⊥}.Countable
• countable_setOfPred_isolated_right_within 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {s : Set α} : {x | x ∈ s ∧ nhdsWithin x (s ∩ Set.Ioi x) = ⊥}.Countable
• countable_setOf_isolated_left_within 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {s : Set α} : {x | x ∈ s ∧ nhdsWithin x (s ∩ Set.Iio x) = ⊥}.Countable
• countable_setOf_isolated_right_within 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {s : Set α} : {x | x ∈ s ∧ nhdsWithin x (s ∩ Set.Ioi x) = ⊥}.Countable
• nhdsGT_eq_bot_iff 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} : nhdsWithin a (Set.Ioi a) = ⊥ ↔ IsTop a ∨ ∃ b, a ⋖ b
• nhdsLT_eq_bot_iff 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} : nhdsWithin a (Set.Iio a) = ⊥ ↔ IsBot a ∨ ∃ b, b ⋖ a
• nhdsGE_basis_Ico 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] (a : α) : (nhdsWithin a (Set.Ici a)).HasBasis (fun u => a < u) (Set.Ico a)
• nhdsGT_basis 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] (a : α) : (nhdsWithin a (Set.Ioi a)).HasBasis (fun x => a < x) (Set.Ioo a)
• nhdsLT_basis 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMinOrder α] (a : α) : (nhdsWithin a (Set.Iio a)).HasBasis (fun x => x < a) fun x => Set.Ioo x a
• nhdsGT_basis_of_exists_gt 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} (h : ∃ b, a < b) : (nhdsWithin a (Set.Ioi a)).HasBasis (fun x => a < x) (Set.Ioo a)
• nhdsLT_basis_of_exists_lt 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} (h : ∃ b, b < a) : (nhdsWithin a (Set.Iio a)).HasBasis (fun x => x < a) fun x => Set.Ioo x a
• nhdsGE_basis_Icc 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] [DenselyOrdered α] {a : α} : (nhdsWithin a (Set.Ici a)).HasBasis (fun x => a < x) (Set.Icc a)
• nhdsGT_basis_Ioc 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMaxOrder α] (a : α) : (nhdsWithin a (Set.Ioi a)).HasBasis (fun x => a < x) (Set.Ioc a)
• nhdsLE_basis_Icc 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMinOrder α] [DenselyOrdered α] {a : α} : (nhdsWithin a (Set.Iic a)).HasBasis (fun x => x < a) fun x => Set.Icc x a
• nhdsLT_basis_Ico 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] (a : α) : (nhdsWithin a (Set.Iio a)).HasBasis (fun x => x < a) fun x => Set.Ico x a
• nhdsGT_basis_Ioc_of_exists_gt 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} (h : ∃ b, a < b) : (nhdsWithin a (Set.Ioi a)).HasBasis (fun x => a < x) (Set.Ioc a)
• mem_nhdsGE_iff_exists_Ico_subset 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] {a : α} {s : Set α} : s ∈ nhdsWithin a (Set.Ici a) ↔ ∃ u ∈ Set.Ioi a, Set.Ico a u ⊆ s
• mem_nhdsGT_iff_exists_Ioo_subset 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] {a : α} {s : Set α} : s ∈ nhdsWithin a (Set.Ioi a) ↔ ∃ u ∈ Set.Ioi a, Set.Ioo a u ⊆ s
• mem_nhdsLE_iff_exists_Ioc_subset 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMinOrder α] {a : α} {s : Set α} : s ∈ nhdsWithin a (Set.Iic a) ↔ ∃ l ∈ Set.Iio a, Set.Ioc l a ⊆ s
• mem_nhdsLT_iff_exists_Ioo_subset 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMinOrder α] {a : α} {s : Set α} : s ∈ nhdsWithin a (Set.Iio a) ↔ ∃ l ∈ Set.Iio a, Set.Ioo l a ⊆ s
• nhdsLT_basis_Ico_of_exists_lt 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} (h : ∃ b, b < a) : (nhdsWithin a (Set.Iio a)).HasBasis (fun x => x < a) fun x => Set.Ico x a
• mem_nhdsGE_iff_exists_Ico_subset' 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a u' : α} {s : Set α} (hu' : a < u') : s ∈ nhdsWithin a (Set.Ici a) ↔ ∃ u ∈ Set.Ioi a, Set.Ico a u ⊆ s
• mem_nhdsGT_iff_exists_Ioo_subset' 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a u' : α} {s : Set α} (hu' : a < u') : s ∈ nhdsWithin a (Set.Ioi a) ↔ ∃ u ∈ Set.Ioi a, Set.Ioo a u ⊆ s
• mem_nhdsLE_iff_exists_Ioc_subset' 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a l' : α} {s : Set α} (hl' : l' < a) : s ∈ nhdsWithin a (Set.Iic a) ↔ ∃ l ∈ Set.Iio a, Set.Ioc l a ⊆ s
• mem_nhdsLT_iff_exists_Ioo_subset' 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a l' : α} {s : Set α} (hl' : l' < a) : s ∈ nhdsWithin a (Set.Iio a) ↔ ∃ l ∈ Set.Iio a, Set.Ioo l a ⊆ s
• Filter.Tendsto.add_atBot 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [OrderTopology α] {l : Filter β} {f g : β → α} {C : α} (hf : Filter.Tendsto f l (nhds C)) (hg : Filter.Tendsto g l Filter.atBot) : Filter.Tendsto (fun x => f x + g x) l Filter.atBot
• Filter.Tendsto.add_atTop 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [OrderTopology α] {l : Filter β} {f g : β → α} {C : α} (hf : Filter.Tendsto f l (nhds C)) (hg : Filter.Tendsto g l Filter.atTop) : Filter.Tendsto (fun x => f x + g x) l Filter.atTop
• Filter.Tendsto.atBot_add 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [OrderTopology α] {l : Filter β} {f g : β → α} {C : α} (hf : Filter.Tendsto f l Filter.atBot) (hg : Filter.Tendsto g l (nhds C)) : Filter.Tendsto (fun x => f x + g x) l Filter.atBot
• Filter.Tendsto.atBot_mul' 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [OrderTopology α] {l : Filter β} {f g : β → α} {C : α} (hf : Filter.Tendsto f l Filter.atBot) (hg : Filter.Tendsto g l (nhds C)) : Filter.Tendsto (fun x => f x * g x) l Filter.atBot
• Filter.Tendsto.atTop_add 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [OrderTopology α] {l : Filter β} {f g : β → α} {C : α} (hf : Filter.Tendsto f l Filter.atTop) (hg : Filter.Tendsto g l (nhds C)) : Filter.Tendsto (fun x => f x + g x) l Filter.atTop
• Filter.Tendsto.atTop_mul' 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [OrderTopology α] {l : Filter β} {f g : β → α} {C : α} (hf : Filter.Tendsto f l Filter.atTop) (hg : Filter.Tendsto g l (nhds C)) : Filter.Tendsto (fun x => f x * g x) l Filter.atTop
• Filter.Tendsto.mul_atBot' 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [OrderTopology α] {l : Filter β} {f g : β → α} {C : α} (hf : Filter.Tendsto f l (nhds C)) (hg : Filter.Tendsto g l Filter.atBot) : Filter.Tendsto (fun x => f x * g x) l Filter.atBot
• Filter.Tendsto.mul_atTop' 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [OrderTopology α] {l : Filter β} {f g : β → α} {C : α} (hf : Filter.Tendsto f l (nhds C)) (hg : Filter.Tendsto g l Filter.atTop) : Filter.Tendsto (fun x => f x * g x) l Filter.atTop
• mem_nhdsGE_iff_exists_mem_Ioc_Ico_subset 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a u' : α} {s : Set α} (hu' : a < u') : s ∈ nhdsWithin a (Set.Ici a) ↔ ∃ u ∈ Set.Ioc a u', Set.Ico a u ⊆ s
• mem_nhdsGT_iff_exists_mem_Ioc_Ioo_subset 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a u' : α} {s : Set α} (hu' : a < u') : s ∈ nhdsWithin a (Set.Ioi a) ↔ ∃ u ∈ Set.Ioc a u', Set.Ioo a u ⊆ s
• mem_nhdsLE_iff_exists_mem_Ico_Ioc_subset 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a l' : α} {s : Set α} (hl' : l' < a) : s ∈ nhdsWithin a (Set.Iic a) ↔ ∃ l ∈ Set.Ico l' a, Set.Ioc l a ⊆ s
• mem_nhdsLT_iff_exists_mem_Ico_Ioo_subset 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a l' : α} {s : Set α} (hl' : l' < a) : s ∈ nhdsWithin a (Set.Iio a) ↔ ∃ l ∈ Set.Ico l' a, Set.Ioo l a ⊆ s
• eventually_abs_sub_lt 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [OrderTopology α] (a : α) {ε : α} (hε : 0 < ε) : ∀ᶠ (x : α) in nhds a, |x - a| < ε
• eventually_mabs_div_lt 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [OrderTopology α] (a : α) {ε : α} (hε : 1 < ε) : ∀ᶠ (x : α) in nhds a, |x / a|ₘ < ε
• mem_nhdsGE_iff_exists_Icc_subset 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] [DenselyOrdered α] {a : α} {s : Set α} : s ∈ nhdsWithin a (Set.Ici a) ↔ ∃ u, a < u ∧ Set.Icc a u ⊆ s
• mem_nhdsLE_iff_exists_Icc_subset 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMinOrder α] [DenselyOrdered α] {a : α} {s : Set α} : s ∈ nhdsWithin a (Set.Iic a) ↔ ∃ l < a, Set.Icc l a ⊆ s
• mem_nhdsGT_iff_exists_Ioc_subset 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMaxOrder α] [DenselyOrdered α] {a : α} {s : Set α} : s ∈ nhdsWithin a (Set.Ioi a) ↔ ∃ u ∈ Set.Ioi a, Set.Ioc a u ⊆ s
• mem_nhdsLT_iff_exists_Ico_subset 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [NoMinOrder α] [DenselyOrdered α] {a : α} {s : Set α} : s ∈ nhdsWithin a (Set.Iio a) ↔ ∃ l ∈ Set.Iio a, Set.Ico l a ⊆ s
• LinearOrderedAddCommGroup.tendsto_nhds 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [OrderTopology α] {f : β → α} {x : Filter β} {a : α} : Filter.Tendsto f x (nhds a) ↔ ∀ ε > 0, ∀ᶠ (b : β) in x, |f b - a| < ε
• LinearOrderedCommGroup.tendsto_nhds 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [OrderTopology α] {f : β → α} {x : Filter β} {a : α} : Filter.Tendsto f x (nhds a) ↔ ∀ ε > 1, ∀ᶠ (b : β) in x, |f b / a|ₘ < ε
• nhds_basis_abs_sub_lt 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [OrderTopology α] [NoMaxOrder α] (a : α) : (nhds a).HasBasis (fun ε => 0 < ε) fun ε => {b | |b - a| < ε}
• nhds_basis_mabs_div_lt 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [OrderTopology α] [NoMaxOrder α] (a : α) : (nhds a).HasBasis (fun ε => 1 < ε) fun ε => {b | |b / a|ₘ < ε}
• nhds_basis_one_mabs_lt 📋 Mathlib.Topology.Order.LeftRightNhds
  (α : Type u_1) [TopologicalSpace α] [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [OrderTopology α] [NoMaxOrder α] : (nhds 1).HasBasis (fun ε => 1 < ε) fun ε => {b | |b|ₘ < ε}
• nhds_basis_zero_abs_lt 📋 Mathlib.Topology.Order.LeftRightNhds
  (α : Type u_1) [TopologicalSpace α] [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [OrderTopology α] [NoMaxOrder α] : (nhds 0).HasBasis (fun ε => 0 < ε) fun ε => {b | |b| < ε}
• nhds_basis_Ioo_one_lt 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [OrderTopology α] [NoMaxOrder α] (a : α) : (nhds a).HasBasis (fun ε => 1 < ε) fun ε => Set.Ioo (a / ε) (a * ε)
• nhds_basis_Ioo_pos 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [OrderTopology α] [NoMaxOrder α] (a : α) : (nhds a).HasBasis (fun ε => 0 < ε) fun ε => Set.Ioo (a - ε) (a + ε)
• nhds_basis_Icc_one_lt 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [OrderTopology α] [NoMaxOrder α] [DenselyOrdered α] (a : α) : (nhds a).HasBasis (fun x => 1 < x) fun ε => Set.Icc (a / ε) (a * ε)
• nhds_basis_Icc_pos 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [OrderTopology α] [NoMaxOrder α] [DenselyOrdered α] (a : α) : (nhds a).HasBasis (fun x => 0 < x) fun ε => Set.Icc (a - ε) (a + ε)
• nhds_eq_iInf_abs_sub 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [OrderTopology α] (a : α) : nhds a = ⨅ r, ⨅ (_ : r > 0), Filter.principal {b | |a - b| < r}
• nhds_eq_iInf_mabs_div 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [OrderTopology α] (a : α) : nhds a = ⨅ r, ⨅ (_ : r > 1), Filter.principal {b | |a / b|ₘ < r}
• orderTopology_of_nhds_abs 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_3} [TopologicalSpace α] [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] (h_nhds : ∀ (a : α), nhds a = ⨅ r, ⨅ (_ : r > 0), Filter.principal {b | |a - b| < r}) : OrderTopology α
• orderTopology_of_nhds_mabs 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_3} [TopologicalSpace α] [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] (h_nhds : ∀ (a : α), nhds a = ⨅ r, ⨅ (_ : r > 1), Filter.principal {b | |a / b|ₘ < r}) : OrderTopology α
• nhds_basis_Ioo_one_lt_of_one_lt 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [OrderTopology α] [NoMaxOrder α] {a : α} (ha : 1 < a) : (nhds a).HasBasis (fun ε => 1 < ε ∧ ε ≤ a) fun ε => Set.Ioo (a / ε) (a * ε)
• nhds_basis_Ioo_pos_of_pos 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [OrderTopology α] [NoMaxOrder α] {a : α} (ha : 0 < a) : (nhds a).HasBasis (fun ε => 0 < ε ∧ ε ≤ a) fun ε => Set.Ioo (a - ε) (a + ε)
• TFAE_mem_nhdsGE 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a b : α} (hab : a < b) (s : Set α) : [s ∈ nhdsWithin a (Set.Ici a), s ∈ nhdsWithin a (Set.Icc a b), s ∈ nhdsWithin a (Set.Ico a b), ∃ u ∈ Set.Ioc a b, Set.Ico a u ⊆ s, ∃ u ∈ Set.Ioi a, Set.Ico a u ⊆ s].TFAE
• TFAE_mem_nhdsGT 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a b : α} (hab : a < b) (s : Set α) : [s ∈ nhdsWithin a (Set.Ioi a), s ∈ nhdsWithin a (Set.Ioc a b), s ∈ nhdsWithin a (Set.Ioo a b), ∃ u ∈ Set.Ioc a b, Set.Ioo a u ⊆ s, ∃ u ∈ Set.Ioi a, Set.Ioo a u ⊆ s].TFAE
• TFAE_mem_nhdsLE 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a b : α} (h : a < b) (s : Set α) : [s ∈ nhdsWithin b (Set.Iic b), s ∈ nhdsWithin b (Set.Icc a b), s ∈ nhdsWithin b (Set.Ioc a b), ∃ l ∈ Set.Ico a b, Set.Ioc l b ⊆ s, ∃ l ∈ Set.Iio b, Set.Ioc l b ⊆ s].TFAE
• TFAE_mem_nhdsLT 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a b : α} (h : a < b) (s : Set α) : [s ∈ nhdsWithin b (Set.Iio b), s ∈ nhdsWithin b (Set.Ico a b), s ∈ nhdsWithin b (Set.Ioo a b), ∃ l ∈ Set.Ico a b, Set.Ioo l b ⊆ s, ∃ l ∈ Set.Iio b, Set.Ioo l b ⊆ s].TFAE
• LinearOrderedAddCommGroup.toIsTopologicalAddGroup 📋 Mathlib.Topology.Algebra.Order.Group
  {G : Type u_1} [TopologicalSpace G] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [OrderTopology G] : IsTopologicalAddGroup G
• LinearOrderedCommGroup.toIsTopologicalGroup 📋 Mathlib.Topology.Algebra.Order.Group
  {G : Type u_1} [TopologicalSpace G] [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [OrderTopology G] : IsTopologicalGroup G
• continuous_abs 📋 Mathlib.Topology.Algebra.Order.Group
  {G : Type u_1} [TopologicalSpace G] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [OrderTopology G] : Continuous abs
• continuous_mabs 📋 Mathlib.Topology.Algebra.Order.Group
  {G : Type u_1} [TopologicalSpace G] [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [OrderTopology G] : Continuous mabs
• Continuous.abs 📋 Mathlib.Topology.Algebra.Order.Group
  {G : Type u_1} [TopologicalSpace G] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [OrderTopology G] {X : Type u_2} [TopologicalSpace X] {f : X → G} (h : Continuous f) : Continuous fun x => |f x|
• Continuous.mabs 📋 Mathlib.Topology.Algebra.Order.Group
  {G : Type u_1} [TopologicalSpace G] [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [OrderTopology G] {X : Type u_2} [TopologicalSpace X] {f : X → G} (h : Continuous f) : Continuous fun x => |f x|ₘ
• ContinuousAt.abs 📋 Mathlib.Topology.Algebra.Order.Group
  {G : Type u_1} [TopologicalSpace G] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [OrderTopology G] {X : Type u_2} [TopologicalSpace X] {f : X → G} {x : X} (h : ContinuousAt f x) : ContinuousAt (fun x => |f x|) x
• ContinuousAt.mabs 📋 Mathlib.Topology.Algebra.Order.Group
  {G : Type u_1} [TopologicalSpace G] [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [OrderTopology G] {X : Type u_2} [TopologicalSpace X] {f : X → G} {x : X} (h : ContinuousAt f x) : ContinuousAt (fun x => |f x|ₘ) x
• ContinuousOn.abs 📋 Mathlib.Topology.Algebra.Order.Group
  {G : Type u_1} [TopologicalSpace G] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [OrderTopology G] {X : Type u_2} [TopologicalSpace X] {f : X → G} {s : Set X} (h : ContinuousOn f s) : ContinuousOn (fun x => |f x|) s
• ContinuousOn.mabs 📋 Mathlib.Topology.Algebra.Order.Group
  {G : Type u_1} [TopologicalSpace G] [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [OrderTopology G] {X : Type u_2} [TopologicalSpace X] {f : X → G} {s : Set X} (h : ContinuousOn f s) : ContinuousOn (fun x => |f x|ₘ) s
• ContinuousWithinAt.abs 📋 Mathlib.Topology.Algebra.Order.Group
  {G : Type u_1} [TopologicalSpace G] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [OrderTopology G] {X : Type u_2} [TopologicalSpace X] {f : X → G} {s : Set X} {x : X} (h : ContinuousWithinAt f s x) : ContinuousWithinAt (fun x => |f x|) s x
• ContinuousWithinAt.mabs 📋 Mathlib.Topology.Algebra.Order.Group
  {G : Type u_1} [TopologicalSpace G] [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [OrderTopology G] {X : Type u_2} [TopologicalSpace X] {f : X → G} {s : Set X} {x : X} (h : ContinuousWithinAt f s x) : ContinuousWithinAt (fun x => |f x|ₘ) s x
• not_denseRange_zpow 📋 Mathlib.Topology.Algebra.Order.Group
  {G : Type u_1} [TopologicalSpace G] [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [OrderTopology G] [Nontrivial G] [DenselyOrdered G] {a : G} : ¬DenseRange fun x => a ^ x

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