Loogle!

Result

Found 465 declarations mentioning OrderClosedTopology. Of these, only the first 200 are shown.

• OrderClosedTopology 📋 Mathlib.Topology.Order.OrderClosed
  (α : Type u_1) [TopologicalSpace α] [Preorder α] : Prop
• instClosedIciTopology 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] : ClosedIciTopology α
• instClosedIicTopology 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] : ClosedIicTopology α
• OrderClosedTopology.to_t2Space 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [PartialOrder α] [t : OrderClosedTopology α] : T2Space α
• instOrderClosedTopologyOrderDual 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] : OrderClosedTopology αᵒᵈ
• isClosed_Icc 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] {a b : α} : IsClosed (Set.Icc a b)
• Subtype.instOrderClosedTopology 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] {p : α → Prop} : OrderClosedTopology (Subtype p)
• Pi.orderClosedTopology' 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [Preorder β] [TopologicalSpace β] [OrderClosedTopology β] : OrderClosedTopology (α → β)
• closure_Icc 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] (a b : α) : closure (Set.Icc a b) = Set.Icc a b
• instOrderClosedTopologyForall 📋 Mathlib.Topology.Order.OrderClosed
  {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Preorder (α i)] [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), OrderClosedTopology (α i)] : OrderClosedTopology ((i : ι) → α i)
• instOrderClosedTopologyProd 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [Preorder α] [TopologicalSpace α] [OrderClosedTopology α] [Preorder β] [TopologicalSpace β] [OrderClosedTopology β] : OrderClosedTopology (α × β)
• isClosed_antitone 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] [Preorder β] : IsClosed {f | Antitone f}
• isClosed_monotone 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] [Preorder β] : IsClosed {f | Monotone f}
• isClosed_antitoneOn 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] [Preorder β] {s : Set β} : IsClosed {f | AntitoneOn f s}
• isClosed_monotoneOn 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] [Preorder β] {s : Set β} : IsClosed {f | MonotoneOn f s}
• isClosed_le_prod 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] : IsClosed {p | p.1 ≤ p.2}
• isClosed_le_prod' 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] : IsClosed {p | p.2 ≤ p.1}
• OrderClosedTopology.isClosed_le' 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u_1} {inst✝ : TopologicalSpace α} {inst✝¹ : Preorder α} [self : OrderClosedTopology α] : IsClosed {p | p.1 ≤ p.2}
• OrderClosedTopology.mk 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u_1} [TopologicalSpace α] [Preorder α] (isClosed_le' : IsClosed {p | p.1 ≤ p.2}) : OrderClosedTopology α
• isOpen_Ioo 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a b : α} : IsOpen (Set.Ioo a b)
• isClosed_le 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] [TopologicalSpace β] {f g : β → α} (hf : Continuous f) (hg : Continuous g) : IsClosed {b | f b ≤ g b}
• DiscreteTopology.of_predOrder_succOrder 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] [PredOrder α] [SuccOrder α] : DiscreteTopology α
• frontier_Ici_subset 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] (a : α) : frontier (Set.Ici a) ⊆ {a}
• frontier_Iic_subset 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] (a : α) : frontier (Set.Iic a) ⊆ {a}
• antitone_of_frequently_antitone_of_tendsto 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] {ι : Type u_1} {l : Filter ι} [Preorder β] {F : ι → β → α} {f : β → α} (hF : ∃ᶠ (i : ι) in l, Antitone (F i)) (hlim : ∀ (x : β), Filter.Tendsto (fun i => F i x) l (nhds (f x))) : Antitone f
• monotone_of_frequently_monotone_of_tendsto 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] {ι : Type u_1} {l : Filter ι} [Preorder β] {F : ι → β → α} {f : β → α} (hF : ∃ᶠ (i : ι) in l, Monotone (F i)) (hlim : ∀ (x : β), Filter.Tendsto (fun i => F i x) l (nhds (f x))) : Monotone f
• continuous_max 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] : Continuous fun p => max p.1 p.2
• continuous_min 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] : Continuous fun p => min p.1 p.2
• le_of_tendsto_of_tendsto 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] {f g : β → α} {b : Filter β} {a₁ a₂ : α} [hb : b.NeBot] (hf : Filter.Tendsto f b (nhds a₁)) (hg : Filter.Tendsto g b (nhds a₂)) (h : f ≤ᶠ[b] g) : a₁ ≤ a₂
• tendsto_le_of_eventuallyLE 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] {f g : β → α} {b : Filter β} {a₁ a₂ : α} [hb : b.NeBot] (hf : Filter.Tendsto f b (nhds a₁)) (hg : Filter.Tendsto g b (nhds a₂)) (h : f ≤ᶠ[b] g) : a₁ ≤ a₂
• le_of_tendsto_of_tendsto' 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] {f g : β → α} {b : Filter β} {a₁ a₂ : α} [hb : b.NeBot] (hf : Filter.Tendsto f b (nhds a₁)) (hg : Filter.Tendsto g b (nhds a₂)) (h : ∀ (x : β), f x ≤ g x) : a₁ ≤ a₂
• le_of_tendsto_of_tendsto_of_frequently 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] {f g : β → α} {b : Filter β} {a₁ a₂ : α} (hf : Filter.Tendsto f b (nhds a₁)) (hg : Filter.Tendsto g b (nhds a₂)) (h : ∃ᶠ (x : β) in b, f x ≤ g x) : a₁ ≤ a₂
• interior_Ioo 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a b : α} : interior (Set.Ioo a b) = Set.Ioo a b
• Filter.Tendsto.max_left 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f : β → α} {l : Filter β} {a : α} (h : Filter.Tendsto f l (nhds a)) : Filter.Tendsto (fun i => max (f i) a) l (nhds a)
• Filter.Tendsto.max_right 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f : β → α} {l : Filter β} {a : α} (h : Filter.Tendsto f l (nhds a)) : Filter.Tendsto (fun i => max a (f i)) l (nhds a)
• Filter.Tendsto.min_left 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f : β → α} {l : Filter β} {a : α} (h : Filter.Tendsto f l (nhds a)) : Filter.Tendsto (fun i => min (f i) a) l (nhds a)
• Filter.Tendsto.min_right 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f : β → α} {l : Filter β} {a : α} (h : Filter.Tendsto f l (nhds a)) : Filter.Tendsto (fun i => min a (f i)) l (nhds a)
• closure_le_eq 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] [TopologicalSpace β] {f g : β → α} (hf : Continuous f) (hg : Continuous g) : closure {b | f b ≤ g b} = {b | f b ≤ g b}
• isOpen_lt_prod 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] : IsOpen {p | p.1 < p.2}
• isOpen_lt_prod' 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] : IsOpen {p | p.2 < p.1}
• Continuous.max 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f g : β → α} [TopologicalSpace β] (hf : Continuous f) (hg : Continuous g) : Continuous fun b => max (f b) (g b)
• Continuous.min 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f g : β → α} [TopologicalSpace β] (hf : Continuous f) (hg : Continuous g) : Continuous fun b => min (f b) (g b)
• closure_lt_subset_le 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] [TopologicalSpace β] {f g : β → α} (hf : Continuous f) (hg : Continuous g) : closure {b | f b < g b} ⊆ {b | f b ≤ g b}
• IsClosed.isClosed_le 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] [TopologicalSpace β] {f g : β → α} {s : Set β} (hs : IsClosed s) (hf : ContinuousOn f s) (hg : ContinuousOn g s) : IsClosed {x | x ∈ s ∧ f x ≤ g x}
• Ioo_subset_closure_interior 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a b : α} : Set.Ioo a b ⊆ closure (interior (Set.Ioo a b))
• 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
• isOpen_lt 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] [TopologicalSpace β] {f g : β → α} (hf : Continuous f) (hg : Continuous g) : IsOpen {b | f b < g b}
• monotoneOn_of_frequently_monotoneOn_of_tendsto 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] {ι : Type u_1} {l : Filter ι} [Preorder β] {F : ι → β → α} {f : β → α} {s : Set β} (hF : ∃ᶠ (i : ι) in l, MonotoneOn (F i) s) (hlim : ∀ x ∈ s, Filter.Tendsto (fun i => F i x) l (nhds (f x))) : MonotoneOn f s
• IsClosed.epigraph 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] [TopologicalSpace β] {f : β → α} {s : Set β} (hs : IsClosed s) (hf : ContinuousOn f s) : IsClosed {p | p.1 ∈ s ∧ f p.1 ≤ p.2}
• IsClosed.hypograph 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] [TopologicalSpace β] {f : β → α} {s : Set β} (hs : IsClosed s) (hf : ContinuousOn f s) : IsClosed {p | p.1 ∈ s ∧ p.2 ≤ f p.1}
• ContinuousWithinAt.closure_le 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] [TopologicalSpace β] {f g : β → α} {s : Set β} {x : β} (hx : x ∈ closure s) (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) (h : ∀ y ∈ s, f y ≤ g y) : f x ≤ g x
• frontier_ge_subset_eq 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {g f : β → α} [TopologicalSpace β] (hg : Continuous g) (hf : Continuous f) : frontier {b | g b ≤ f b} ⊆ {b | f b = g b}
• frontier_gt_subset_eq 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {g f : β → α} [TopologicalSpace β] (hg : Continuous g) (hf : Continuous f) : frontier {b | g b < f b} ⊆ {b | f b = g b}
• frontier_le_subset_eq 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f g : β → α} [TopologicalSpace β] (hf : Continuous f) (hg : Continuous g) : frontier {b | f b ≤ g b} ⊆ {b | f b = g b}
• frontier_lt_subset_eq 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f g : β → α} [TopologicalSpace β] (hf : Continuous f) (hg : Continuous g) : frontier {b | f b < g b} ⊆ {b | f b = g b}
• le_on_closure 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] [TopologicalSpace β] {f g : β → α} {s : Set β} (h : ∀ x ∈ s, f x ≤ g x) (hf : ContinuousOn f (closure s)) (hg : ContinuousOn g (closure s)) ⦃x : β⦄ (hx : x ∈ closure s) : f x ≤ g x
• Icc_mem_nhds 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a b x : α} (ha : a < x) (hb : x < b) : Set.Icc a b ∈ nhds x
• Ico_mem_nhds 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a b x : α} (hb : b < x) (ha : x < a) : Set.Ico b a ∈ nhds x
• Ioc_mem_nhds 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a b x : α} (ha : a < x) (hb : x < b) : Set.Ioc a b ∈ nhds x
• Ioo_mem_nhds 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {a b x : α} (ha : a < x) (hb : x < b) : Set.Ioo a b ∈ nhds x
• Filter.Tendsto.max 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f g : β → α} {b : Filter β} {a₁ a₂ : α} (hf : Filter.Tendsto f b (nhds a₁)) (hg : Filter.Tendsto g b (nhds a₂)) : Filter.Tendsto (fun b => max (f b) (g b)) b (nhds (max a₁ a₂))
• Filter.Tendsto.min 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f g : β → α} {b : Filter β} {a₁ a₂ : α} (hf : Filter.Tendsto f b (nhds a₁)) (hg : Filter.Tendsto g b (nhds a₂)) : Filter.Tendsto (fun b => min (f b) (g b)) b (nhds (min a₁ a₂))
• Filter.tendsto_nhds_max_left 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f : β → α} {l : Filter β} {a : α} (h : Filter.Tendsto f l (nhdsWithin a (Set.Ioi a))) : Filter.Tendsto (fun i => max (f i) a) l (nhdsWithin a (Set.Ioi a))
• Filter.tendsto_nhds_max_right 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f : β → α} {l : Filter β} {a : α} (h : Filter.Tendsto f l (nhdsWithin a (Set.Ioi a))) : Filter.Tendsto (fun i => max a (f i)) l (nhdsWithin a (Set.Ioi a))
• Filter.tendsto_nhds_min_left 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f : β → α} {l : Filter β} {a : α} (h : Filter.Tendsto f l (nhdsWithin a (Set.Iio a))) : Filter.Tendsto (fun i => min (f i) a) l (nhdsWithin a (Set.Iio a))
• Filter.tendsto_nhds_min_right 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f : β → α} {l : Filter β} {a : α} (h : Filter.Tendsto f l (nhdsWithin a (Set.Iio a))) : Filter.Tendsto (fun i => min a (f i)) l (nhdsWithin a (Set.Iio a))
• ContinuousAt.eventually_lt 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f g : β → α} [TopologicalSpace β] {x₀ : β} (hf : ContinuousAt f x₀) (hg : ContinuousAt g x₀) (hfg : f x₀ < g x₀) : ∀ᶠ (x : β) in nhds x₀, f x < g x
• Filter.Tendsto.eventually_lt 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {l : Filter γ} {f g : γ → α} {y z : α} (hf : Filter.Tendsto f l (nhds y)) (hg : Filter.Tendsto g l (nhds z)) (hyz : y < z) : ∀ᶠ (x : γ) in l, f x < g x
• lt_subset_interior_le 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f g : β → α} [TopologicalSpace β] (hf : Continuous f) (hg : Continuous g) : {b | f b < g b} ⊆ interior {b | f b ≤ g b}
• Dense.exists_between 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] [DenselyOrdered α] {s : Set α} (hs : Dense s) {x y : α} (h : x < y) : ∃ z ∈ s, z ∈ Set.Ioo x y
• Continuous.if_ge 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f g : β → α} [TopologicalSpace β] [TopologicalSpace γ] [(x : β) → Decidable (g x ≤ f x)] {f' g' : β → γ} (hf' : Continuous f') (hg' : Continuous g') (hf : Continuous f) (hg : Continuous g) (hfg : ∀ (x : β), f x = g x → f' x = g' x) : Continuous fun x => if g x ≤ f x then f' x else g' x
• Continuous.if_le 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f g : β → α} [TopologicalSpace β] [TopologicalSpace γ] [(x : β) → Decidable (f x ≤ g x)] {f' g' : β → γ} (hf' : Continuous f') (hg' : Continuous g') (hf : Continuous f) (hg : Continuous g) (hfg : ∀ (x : β), f x = g x → f' x = g' x) : Continuous fun x => if f x ≤ g x then f' x else g' x
• Dense.Iio_eq_biUnion 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] [DenselyOrdered α] {s : Set α} (hs : Dense s) (x : α) : Set.Iio x = ⋃ y ∈ s ∩ Set.Iio x, Set.Iio y
• Dense.Ioi_eq_biUnion 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] [DenselyOrdered α] {s : Set α} (hs : Dense s) (x : α) : Set.Ioi x = ⋃ y ∈ s ∩ Set.Ioi x, Set.Ioi y
• continuous_if_le 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {f g : β → α} [TopologicalSpace β] [TopologicalSpace γ] [(x : β) → Decidable (f x ≤ g x)] {f' g' : β → γ} (hf : Continuous f) (hg : Continuous g) (hf' : ContinuousOn f' {x | f x ≤ g x}) (hg' : ContinuousOn g' {x | g x ≤ f x}) (hfg : ∀ (x : β), f x = g x → f' x = g' x) : Continuous fun x => if f x ≤ g x then f' x else g' x
• IsPreconnected.mapsTo_Ioi_or_Iio 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} {β : Type v} [TopologicalSpace α] {s : Set α} [LinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {b : β} (hs : IsPreconnected s) (hf : ContinuousOn f s) (hfb : ∀ x ∈ s, f x ≠ b) : Set.MapsTo f s (Set.Ioi b) ∨ Set.MapsTo f s (Set.Iio b)
• IsPreconnected.gt_of_ne 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} {β : Type v} [TopologicalSpace α] {s : Set α} [LinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {b : β} (hs : IsPreconnected s) (hf : ContinuousOn f s) (hfb : ∀ x ∈ s, f x ≠ b) (hfx : ∃ x ∈ s, f x < b) {x : α} (hx : x ∈ s) : f x < b
• IsPreconnected.lt_of_ne 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} {β : Type v} [TopologicalSpace α] {s : Set α} [LinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {b : β} (hs : IsPreconnected s) (hf : ContinuousOn f s) (hfb : ∀ x ∈ s, f x ≠ b) (hfx : ∃ x ∈ s, b < f x) {x : α} (hx : x ∈ s) : b < f x
• OrderTopology.to_orderClosedTopology 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] : OrderClosedTopology α
• IsGLB.isGLB_of_tendsto 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} {s : Set α} {a : α} {b : γ} (hf : MonotoneOn f s) : IsGLB s a → s.Nonempty → Filter.Tendsto f (nhdsWithin a s) (nhds b) → IsGLB (f '' s) b
• 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
• IsLUB.isLUB_of_tendsto 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} {s : Set α} {a : α} {b : γ} (hf : MonotoneOn f s) (ha : IsLUB s a) (hs : s.Nonempty) (hb : Filter.Tendsto f (nhdsWithin a s) (nhds b)) : IsLUB (f '' s) b
• IsGLB.mem_lowerBounds_of_tendsto 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} {s : Set α} {a : α} {b : γ} (hf : MonotoneOn f s) (ha : IsGLB s a) (hb : Filter.Tendsto f (nhdsWithin a s) (nhds b)) : b ∈ lowerBounds (f '' s)
• 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)
• IsLUB.mem_upperBounds_of_tendsto 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} {s : Set α} {a : α} {b : γ} (hf : MonotoneOn f s) (ha : IsLUB s a) (hb : Filter.Tendsto f (nhdsWithin a s) (nhds b)) : b ∈ upperBounds (f '' s)
• MonotoneOn.insert_of_continuousWithinAt 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] {s : Set α} {x : α} {f : α → β} [TopologicalSpace β] [OrderClosedTopology β] (hf : MonotoneOn f s) (hx : ClusterPt x (Filter.principal s)) (h'x : ContinuousWithinAt f s x) : MonotoneOn f (insert x s)
• Antitone.map_csInf_of_continuousAt 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {A : Set α} (Cf : ContinuousAt f (sInf A)) (Af : Antitone f) (A_nonemp : A.Nonempty) (A_bdd : BddBelow A := by bddDefault) : f (sInf A) = sSup (f '' A)
• Antitone.map_csSup_of_continuousAt 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {A : Set α} (Cf : ContinuousAt f (sSup A)) (Af : Antitone f) (A_nonemp : A.Nonempty) (A_bdd : BddAbove A := by bddDefault) : f (sSup A) = sInf (f '' A)
• Monotone.map_csInf_of_continuousAt 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {A : Set α} (Cf : ContinuousAt f (sInf A)) (Mf : Monotone f) (A_nonemp : A.Nonempty) (A_bdd : BddBelow A := by bddDefault) : f (sInf A) = sInf (f '' A)
• Monotone.map_csSup_of_continuousAt 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {A : Set α} (Cf : ContinuousAt f (sSup A)) (Mf : Monotone f) (A_nonemp : A.Nonempty) (A_bdd : BddAbove A := by bddDefault) : f (sSup A) = sSup (f '' A)
• 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)
• MonotoneOn.map_csInf_of_continuousWithinAt 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {A : Set α} (Cf : ContinuousWithinAt f A (sInf A)) (Mf : MonotoneOn f A) (A_nonemp : A.Nonempty) (A_bdd : BddBelow A := by bddDefault) : f (sInf A) = sInf (f '' A)
• MonotoneOn.map_csSup_of_continuousWithinAt 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {A : Set α} (Cf : ContinuousWithinAt f A (sSup A)) (Mf : MonotoneOn f A) (A_nonemp : A.Nonempty) (A_bdd : BddAbove A := by bddDefault) : f (sSup A) = sSup (f '' A)
• Antitone.map_ciInf_of_continuousAt 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {ι : Sort u_3} [Nonempty ι] {f : α → β} {g : ι → α} (Cf : ContinuousAt f (iInf g)) (Af : Antitone f) (bdd : BddBelow (Set.range g) := by bddDefault) : f (⨅ i, g i) = ⨆ i, f (g i)
• Antitone.map_ciSup_of_continuousAt 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {ι : Sort u_3} [Nonempty ι] {f : α → β} {g : ι → α} (Cf : ContinuousAt f (iSup g)) (Af : Antitone f) (bdd : BddAbove (Set.range g) := by bddDefault) : f (⨆ i, g i) = ⨅ i, f (g i)
• Monotone.map_ciInf_of_continuousAt 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {ι : Sort u_3} [Nonempty ι] {f : α → β} {g : ι → α} (Cf : ContinuousAt f (iInf g)) (Mf : Monotone f) (bdd : BddBelow (Set.range g) := by bddDefault) : f (⨅ i, g i) = ⨅ i, f (g i)
• Monotone.map_ciSup_of_continuousAt 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {ι : Sort u_3} [Nonempty ι] {f : α → β} {g : ι → α} (Cf : ContinuousAt f (iSup g)) (Mf : Monotone f) (bdd : BddAbove (Set.range g) := by bddDefault) : f (⨆ i, g i) = ⨆ i, f (g i)
• Antitone.map_sInf_of_continuousAt 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_1} {β : Type u_2} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α} (Cf : ContinuousAt f (sInf s)) (Af : Antitone f) (ftop : f ⊤ = ⊥) : f (sInf s) = sSup (f '' s)
• Antitone.map_sSup_of_continuousAt 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_1} {β : Type u_2} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α} (Cf : ContinuousAt f (sSup s)) (Af : Antitone f) (fbot : f ⊥ = ⊤) : f (sSup s) = sInf (f '' s)
• Monotone.map_sInf_of_continuousAt 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_1} {β : Type u_2} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α} (Cf : ContinuousAt f (sInf s)) (Mf : Monotone f) (ftop : f ⊤ = ⊤) : f (sInf s) = sInf (f '' s)
• Monotone.map_sSup_of_continuousAt 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_1} {β : Type u_2} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α} (Cf : ContinuousAt f (sSup s)) (Mf : Monotone f) (fbot : f ⊥ = ⊥) : f (sSup s) = sSup (f '' s)
• 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)
• MonotoneOn.map_sInf_of_continuousWithinAt 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_1} {β : Type u_2} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α} (Cf : ContinuousWithinAt f s (sInf s)) (Mf : MonotoneOn f s) (ftop : f ⊤ = ⊤) : f (sInf s) = sInf (f '' s)
• MonotoneOn.map_sSup_of_continuousWithinAt 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_1} {β : Type u_2} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α} (Cf : ContinuousWithinAt f s (sSup s)) (Mf : MonotoneOn f s) (fbot : f ⊥ = ⊥) : f (sSup s) = sSup (f '' s)
• Antitone.map_iInf_of_continuousAt 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_1} {β : Type u_2} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {ι : Sort u_3} {f : α → β} {g : ι → α} (Cf : ContinuousAt f (iInf g)) (Af : Antitone f) (ftop : f ⊤ = ⊥) : f (iInf g) = iSup (f ∘ g)
• Antitone.map_iSup_of_continuousAt 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_1} {β : Type u_2} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {ι : Sort u_3} {f : α → β} {g : ι → α} (Cf : ContinuousAt f (iSup g)) (Af : Antitone f) (fbot : f ⊥ = ⊤) : f (⨆ i, g i) = ⨅ i, f (g i)
• Monotone.map_iInf_of_continuousAt 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_1} {β : Type u_2} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {ι : Sort u_3} {f : α → β} {g : ι → α} (Cf : ContinuousAt f (iInf g)) (Mf : Monotone f) (ftop : f ⊤ = ⊤) : f (iInf g) = iInf (f ∘ g)
• Monotone.map_iSup_of_continuousAt 📋 Mathlib.Topology.Order.Monotone
  {α : Type u_1} {β : Type u_2} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderClosedTopology β] {ι : Sort u_3} {f : α → β} {g : ι → α} (Cf : ContinuousAt f (iSup g)) (Mf : Monotone f) (fbot : f ⊥ = ⊥) : f (⨆ i, g i) = ⨆ i, f (g i)
• IsPreconnected.ordConnected 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type v} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set α} (h : IsPreconnected s) : s.OrdConnected
• intermediate_value_univ 📋 Mathlib.Topology.Order.IntermediateValue
  {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] [PreconnectedSpace X] (a b : X) {f : X → α} (hf : Continuous f) : Set.Icc (f a) (f b) ⊆ Set.range f
• IsConnected.Icc_subset 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type v} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set α} (hs : IsConnected s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) : Set.Icc a b ⊆ s
• IsPreconnected.Icc_subset 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type v} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set α} (hs : IsPreconnected s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) : Set.Icc a b ⊆ s
• IsPreconnected.eq_univ_of_unbounded 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type v} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set α} (hs : IsPreconnected s) (hb : ¬BddBelow s) (ha : ¬BddAbove s) : s = Set.univ
• IsPreconnected.intermediate_value 📋 Mathlib.Topology.Order.IntermediateValue
  {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {a b : X} (ha : a ∈ s) (hb : b ∈ s) {f : X → α} (hf : ContinuousOn f s) : Set.Icc (f a) (f b) ⊆ f '' s
• mem_range_of_exists_le_of_exists_ge 📋 Mathlib.Topology.Order.IntermediateValue
  {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] [PreconnectedSpace X] {c : α} {f : X → α} (hf : Continuous f) (h₁ : ∃ a, f a ≤ c) (h₂ : ∃ b, c ≤ f b) : c ∈ Set.range f
• intermediate_value_univ₂ 📋 Mathlib.Topology.Order.IntermediateValue
  {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] [PreconnectedSpace X] {a b : X} {f g : X → α} (hf : Continuous f) (hg : Continuous g) (ha : f a ≤ g a) (hb : g b ≤ f b) : ∃ x, f x = g x
• intermediate_value_univ₂_eventually₁ 📋 Mathlib.Topology.Order.IntermediateValue
  {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] [PreconnectedSpace X] {a : X} {l : Filter X} [l.NeBot] {f g : X → α} (hf : Continuous f) (hg : Continuous g) (ha : f a ≤ g a) (he : g ≤ᶠ[l] f) : ∃ x, f x = g x
• intermediate_value_univ₂_eventually₂ 📋 Mathlib.Topology.Order.IntermediateValue
  {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] [PreconnectedSpace X] {l₁ l₂ : Filter X} [l₁.NeBot] [l₂.NeBot] {f g : X → α} (hf : Continuous f) (hg : Continuous g) (he₁ : f ≤ᶠ[l₁] g) (he₂ : g ≤ᶠ[l₂] f) : ∃ x, f x = g x
• intermediate_value_uIcc 📋 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)) : Set.uIcc (f a) (f b) ⊆ f '' Set.uIcc a b
• IsPreconnected.intermediate_value_Ico 📋 Mathlib.Topology.Order.IntermediateValue
  {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {a : X} {l : Filter X} (ha : a ∈ s) [l.NeBot] (hl : l ≤ Filter.principal s) {f : X → α} (hf : ContinuousOn f s) {v : α} (ht : Filter.Tendsto f l (nhds v)) : Set.Ico (f a) v ⊆ f '' s
• IsPreconnected.intermediate_value_Ioc 📋 Mathlib.Topology.Order.IntermediateValue
  {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {a : X} {l : Filter X} (ha : a ∈ s) [l.NeBot] (hl : l ≤ Filter.principal s) {f : X → α} (hf : ContinuousOn f s) {v : α} (ht : Filter.Tendsto f l (nhds v)) : Set.Ioc v (f a) ⊆ f '' s
• IsPreconnected.intermediate_value_Ici 📋 Mathlib.Topology.Order.IntermediateValue
  {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {a : X} {l : Filter X} (ha : a ∈ s) [l.NeBot] (hl : l ≤ Filter.principal s) {f : X → α} (hf : ContinuousOn f s) (ht : Filter.Tendsto f l Filter.atTop) : Set.Ici (f a) ⊆ f '' s
• IsPreconnected.intermediate_value_Iic 📋 Mathlib.Topology.Order.IntermediateValue
  {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {a : X} {l : Filter X} (ha : a ∈ s) [l.NeBot] (hl : l ≤ Filter.principal s) {f : X → α} (hf : ContinuousOn f s) (ht : Filter.Tendsto f l Filter.atBot) : Set.Iic (f a) ⊆ f '' s
• ContinuousOn.surjOn_uIcc 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {s : Set α} [hs : s.OrdConnected] {f : α → δ} (hf : ContinuousOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) : Set.SurjOn f s (Set.uIcc (f a) (f b))
• Continuous.strictMono_of_inj 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {f : α → δ} (hf_c : Continuous f) (hf_i : Function.Injective f) : StrictMono f ∨ StrictAnti f
• ContinuousOn.surjOn_Icc 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {s : Set α} [hs : s.OrdConnected] {f : α → δ} (hf : ContinuousOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) : Set.SurjOn f s (Set.Icc (f a) (f b))
• IsPreconnected.intermediate_value₂ 📋 Mathlib.Topology.Order.IntermediateValue
  {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {a b : X} (ha : a ∈ s) (hb : b ∈ s) {f g : X → α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) (ha' : f a ≤ g a) (hb' : g b ≤ f b) : ∃ x ∈ s, f x = g x
• IsPreconnected.intermediate_value_Ioo 📋 Mathlib.Topology.Order.IntermediateValue
  {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {l₁ l₂ : Filter X} [l₁.NeBot] [l₂.NeBot] (hl₁ : l₁ ≤ Filter.principal s) (hl₂ : l₂ ≤ Filter.principal s) {f : X → α} (hf : ContinuousOn f s) {v₁ v₂ : α} (ht₁ : Filter.Tendsto f l₁ (nhds v₁)) (ht₂ : Filter.Tendsto f l₂ (nhds v₂)) : Set.Ioo v₁ v₂ ⊆ f '' s
• Continuous.surjective 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {f : α → δ} (hf : Continuous f) (h_top : Filter.Tendsto f Filter.atTop Filter.atTop) (h_bot : Filter.Tendsto f Filter.atBot Filter.atBot) : Function.Surjective f
• Continuous.surjective' 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {f : α → δ} (hf : Continuous f) (h_top : Filter.Tendsto f Filter.atBot Filter.atTop) (h_bot : Filter.Tendsto f Filter.atTop Filter.atBot) : Function.Surjective f
• IsPreconnected.intermediate_value_Iii 📋 Mathlib.Topology.Order.IntermediateValue
  {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {l₁ l₂ : Filter X} [l₁.NeBot] [l₂.NeBot] (hl₁ : l₁ ≤ Filter.principal s) (hl₂ : l₂ ≤ Filter.principal s) {f : X → α} (hf : ContinuousOn f s) (ht₁ : Filter.Tendsto f l₁ Filter.atBot) (ht₂ : Filter.Tendsto f l₂ Filter.atTop) : Set.univ ⊆ f '' s
• Continuous.image_Icc_of_strictMono 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} {f : α → δ} (hf_c : Continuous f) (hf : StrictMono f) : f '' Set.Icc a b = Set.Icc (f a) (f b)
• Continuous.image_Ico_of_strictMono 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} {f : α → δ} (hf_c : Continuous f) (hf : StrictMono f) : f '' Set.Ico a b = Set.Ico (f a) (f b)
• Continuous.image_Ioc_of_strictMono 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} {f : α → δ} (hf_c : Continuous f) (hf : StrictMono f) : f '' Set.Ioc a b = Set.Ioc (f a) (f b)
• Continuous.image_Ioo_of_strictMono 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} {f : α → δ} (hf_c : Continuous f) (hf : StrictMono f) : f '' Set.Ioo a b = Set.Ioo (f a) (f b)
• IsPreconnected.intermediate_value_Iio 📋 Mathlib.Topology.Order.IntermediateValue
  {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {l₁ l₂ : Filter X} [l₁.NeBot] [l₂.NeBot] (hl₁ : l₁ ≤ Filter.principal s) (hl₂ : l₂ ≤ Filter.principal s) {f : X → α} (hf : ContinuousOn f s) {v : α} (ht₁ : Filter.Tendsto f l₁ Filter.atBot) (ht₂ : Filter.Tendsto f l₂ (nhds v)) : Set.Iio v ⊆ f '' s
• IsPreconnected.intermediate_value_Ioi 📋 Mathlib.Topology.Order.IntermediateValue
  {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {l₁ l₂ : Filter X} [l₁.NeBot] [l₂.NeBot] (hl₁ : l₁ ≤ Filter.principal s) (hl₂ : l₂ ≤ Filter.principal s) {f : X → α} (hf : ContinuousOn f s) {v : α} (ht₁ : Filter.Tendsto f l₁ (nhds v)) (ht₂ : Filter.Tendsto f l₂ Filter.atTop) : Set.Ioi v ⊆ f '' s
• IsPreconnected.intermediate_value₂_eventually₁ 📋 Mathlib.Topology.Order.IntermediateValue
  {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {a : X} {l : Filter X} (ha : a ∈ s) [l.NeBot] (hl : l ≤ Filter.principal s) {f g : X → α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) (ha' : f a ≤ g a) (he : g ≤ᶠ[l] f) : ∃ x ∈ s, f x = g x
• Continuous.strictMono_of_inj_boundedOrder' 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] [BoundedOrder α] {f : α → δ} (hf_c : Continuous f) (hf_i : Function.Injective f) : StrictMono f ∨ StrictAnti f
• 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_uIcc_of_monotoneOn 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} {f : α → δ} (hf : ContinuousOn f (Set.uIcc a b)) (hmono : MonotoneOn f (Set.uIcc a b)) : f '' Set.uIcc a b = Set.uIcc (f a) (f b)
• intermediate_value_Icc 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} (hab : a ≤ b) {f : α → δ} (hf : ContinuousOn f (Set.Icc a b)) : Set.Icc (f a) (f b) ⊆ f '' Set.Icc a b
• intermediate_value_Icc' 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} (hab : a ≤ b) {f : α → δ} (hf : ContinuousOn f (Set.Icc a b)) : Set.Icc (f b) (f a) ⊆ f '' Set.Icc a b
• intermediate_value_Ico 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} (hab : a ≤ b) {f : α → δ} (hf : ContinuousOn f (Set.Icc a b)) : Set.Ico (f a) (f b) ⊆ f '' Set.Ico a b
• intermediate_value_Ico' 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} (hab : a ≤ b) {f : α → δ} (hf : ContinuousOn f (Set.Icc a b)) : Set.Ioc (f b) (f a) ⊆ f '' Set.Ico a b
• intermediate_value_Ioc 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} (hab : a ≤ b) {f : α → δ} (hf : ContinuousOn f (Set.Icc a b)) : Set.Ioc (f a) (f b) ⊆ f '' Set.Ioc a b
• intermediate_value_Ioc' 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} (hab : a ≤ b) {f : α → δ} (hf : ContinuousOn f (Set.Icc a b)) : Set.Ico (f b) (f a) ⊆ f '' Set.Ioc a b
• intermediate_value_Ioo 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} (hab : a ≤ b) {f : α → δ} (hf : ContinuousOn f (Set.Icc a b)) : Set.Ioo (f a) (f b) ⊆ f '' Set.Ioo a b
• intermediate_value_Ioo' 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} (hab : a ≤ b) {f : α → δ} (hf : ContinuousOn f (Set.Icc a b)) : Set.Ioo (f b) (f a) ⊆ f '' Set.Ioo a b
• IsPreconnected.intermediate_value₂_eventually₂ 📋 Mathlib.Topology.Order.IntermediateValue
  {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {l₁ l₂ : Filter X} [l₁.NeBot] [l₂.NeBot] (hl₁ : l₁ ≤ Filter.principal s) (hl₂ : l₂ ≤ Filter.principal s) {f g : X → α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) (he₁ : f ≤ᶠ[l₁] g) (he₂ : g ≤ᶠ[l₂] f) : ∃ x ∈ s, f x = g x
• intermediate_value_Ici 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a : α} {f : α → δ} (hf : ContinuousOn f (Set.Ici a)) (htop : Filter.Tendsto f Filter.atTop Filter.atTop) : Set.Ici (f a) ⊆ f '' Set.Ici a
• intermediate_value_Ici' 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a : α} {f : α → δ} (hf : ContinuousOn f (Set.Ici a)) (htop : Filter.Tendsto f Filter.atTop Filter.atBot) : Set.Iic (f a) ⊆ f '' Set.Ici a
• intermediate_value_Iic 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a : α} {f : α → δ} (hf : ContinuousOn f (Set.Iic a)) (hbot : Filter.Tendsto f Filter.atBot Filter.atBot) : Set.Iic (f a) ⊆ f '' Set.Iic a
• intermediate_value_Iic' 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a : α} {f : α → δ} (hf : ContinuousOn f (Set.Iic a)) (hbot : Filter.Tendsto f Filter.atBot Filter.atTop) : Set.Ici (f a) ⊆ f '' Set.Iic a
• intermediate_value_Iio 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a : α} {f : α → δ} (hf : ContinuousOn f (Set.Iic a)) (hbot : Filter.Tendsto f Filter.atBot Filter.atBot) : Set.Iio (f a) ⊆ f '' Set.Iio a
• intermediate_value_Iio' 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a : α} {f : α → δ} (hf : ContinuousOn f (Set.Iic a)) (hbot : Filter.Tendsto f Filter.atBot Filter.atTop) : Set.Ioi (f a) ⊆ f '' Set.Iio a
• intermediate_value_Ioi 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a : α} {f : α → δ} (hf : ContinuousOn f (Set.Ici a)) (htop : Filter.Tendsto f Filter.atTop Filter.atTop) : Set.Ioi (f a) ⊆ f '' Set.Ioi a
• intermediate_value_Ioi' 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a : α} {f : α → δ} (hf : ContinuousOn f (Set.Ici a)) (htop : Filter.Tendsto f Filter.atTop Filter.atBot) : Set.Iio (f a) ⊆ f '' Set.Ioi a
• Continuous.strictMonoOn_of_inj_rigidity 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {f : α → δ} (hf_c : Continuous f) (hf_i : Function.Injective f) {a b : α} (hab : a < b) (hf_mono : StrictMonoOn f (Set.Icc a b)) : StrictMono f
• ContinuousOn.strictAntiOn_of_injOn_Icc 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} {f : α → δ} (hab : a ≤ b) (hfab : f b ≤ f a) (hf_c : ContinuousOn f (Set.Icc a b)) (hf_i : Set.InjOn f (Set.Icc a b)) : StrictAntiOn f (Set.Icc a b)
• ContinuousOn.strictMonoOn_of_injOn_Icc 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} {f : α → δ} (hab : a ≤ b) (hfab : f a ≤ f b) (hf_c : ContinuousOn f (Set.Icc a b)) (hf_i : Set.InjOn f (Set.Icc a b)) : StrictMonoOn f (Set.Icc a b)
• ContinuousOn.image_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_Icc_of_monotoneOn 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} {f : α → δ} (hab : a ≤ b) (hf : ContinuousOn f (Set.Icc a b)) (hmono : MonotoneOn f (Set.Icc a b)) : f '' Set.Icc a b = Set.Icc (f a) (f b)
• ContinuousOn.image_Ico_of_strictAntiOn 📋 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 : StrictAntiOn f (Set.Icc a b)) : f '' Set.Ico a b = Set.Ioc (f b) (f a)
• ContinuousOn.image_Ico_of_strictMonoOn 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} {f : α → δ} (hab : a ≤ b) (hf : ContinuousOn f (Set.Icc a b)) (hmono : StrictMonoOn f (Set.Icc a b)) : f '' Set.Ico a b = Set.Ico (f a) (f b)
• ContinuousOn.image_Ioc_of_strictAntiOn 📋 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 : StrictAntiOn f (Set.Icc a b)) : f '' Set.Ioc a b = Set.Ico (f b) (f a)
• ContinuousOn.image_Ioc_of_strictMonoOn 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} {f : α → δ} (hab : a ≤ b) (hf : ContinuousOn f (Set.Icc a b)) (hmono : StrictMonoOn f (Set.Icc a b)) : f '' Set.Ioc a b = Set.Ioc (f a) (f b)
• ContinuousOn.image_Ioo_of_strictAntiOn 📋 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 : StrictAntiOn f (Set.Icc a b)) : f '' Set.Ioo a b = Set.Ioo (f b) (f a)
• ContinuousOn.image_Ioo_of_strictMonoOn 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} {f : α → δ} (hab : a ≤ b) (hf : ContinuousOn f (Set.Icc a b)) (hmono : StrictMonoOn f (Set.Icc a b)) : f '' Set.Ioo a b = Set.Ioo (f a) (f b)
• ContinuousOn.image_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_Ici_of_monotoneOn 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a : α} {f : α → δ} (hf : ContinuousOn f (Set.Ici a)) (hmono : MonotoneOn f (Set.Ici a)) (htop : Filter.Tendsto f Filter.atTop Filter.atTop) : f '' Set.Ici a = Set.Ici (f a)
• ContinuousOn.image_Iic_of_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)
• ContinuousOn.image_Iic_of_monotoneOn 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a : α} {f : α → δ} (hf : ContinuousOn f (Set.Iic a)) (hmono : MonotoneOn f (Set.Iic a)) (hbot : Filter.Tendsto f Filter.atBot Filter.atBot) : f '' Set.Iic a = Set.Iic (f a)
• ContinuousOn.image_Iio_of_strictAntiOn 📋 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 : StrictAntiOn f (Set.Iic a)) (hbot : Filter.Tendsto f Filter.atBot Filter.atTop) : f '' Set.Iio a = Set.Ioi (f a)
• ContinuousOn.image_Iio_of_strictMonoOn 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a : α} {f : α → δ} (hf : ContinuousOn f (Set.Iic a)) (hmono : StrictMonoOn f (Set.Iic a)) (hbot : Filter.Tendsto f Filter.atBot Filter.atBot) : f '' Set.Iio a = Set.Iio (f a)
• ContinuousOn.image_Ioi_of_strictAntiOn 📋 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 : StrictAntiOn f (Set.Ici a)) (htop : Filter.Tendsto f Filter.atTop Filter.atBot) : f '' Set.Ioi a = Set.Iio (f a)
• ContinuousOn.image_Ioi_of_strictMonoOn 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a : α} {f : α → δ} (hf : ContinuousOn f (Set.Ici a)) (hmono : StrictMonoOn f (Set.Ici a)) (htop : Filter.Tendsto f Filter.atTop Filter.atTop) : f '' Set.Ioi a = Set.Ioi (f a)
• Continuous.strictAnti_of_inj_boundedOrder 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] [BoundedOrder α] {f : α → δ} (hf_c : Continuous f) (hf : f ⊤ ≤ f ⊥) (hf_i : Function.Injective f) : StrictAnti f
• Continuous.strictMono_of_inj_boundedOrder 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] [BoundedOrder α] {f : α → δ} (hf_c : Continuous f) (hf : f ⊥ ≤ f ⊤) (hf_i : Function.Injective f) : StrictMono f
• ContinuousOn.strictMonoOn_of_injOn_Icc' 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} {f : α → δ} (hab : a ≤ b) (hf_c : ContinuousOn f (Set.Icc a b)) (hf_i : Set.InjOn f (Set.Icc a b)) : StrictMonoOn f (Set.Icc a b) ∨ StrictAntiOn f (Set.Icc a b)
• ContinuousOn.strictMonoOn_of_injOn_Ioo 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} {f : α → δ} (hab : a < b) (hf_c : ContinuousOn f (Set.Ioo a b)) (hf_i : Set.InjOn f (Set.Ioo a b)) : StrictMonoOn f (Set.Ioo a b) ∨ StrictAntiOn f (Set.Ioo a b)
• ContinuousOn.surjOn_of_tendsto 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {f : α → δ} {s : Set α} [s.OrdConnected] (hs : s.Nonempty) (hf : ContinuousOn f s) (hbot : Filter.Tendsto (fun x => f ↑x) Filter.atBot Filter.atBot) (htop : Filter.Tendsto (fun x => f ↑x) Filter.atTop Filter.atTop) : Set.SurjOn f s Set.univ
• ContinuousOn.surjOn_of_tendsto' 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {f : α → δ} {s : Set α} [s.OrdConnected] (hs : s.Nonempty) (hf : ContinuousOn f s) (hbot : Filter.Tendsto (fun x => f ↑x) Filter.atBot Filter.atTop) (htop : Filter.Tendsto (fun x => f ↑x) Filter.atTop Filter.atBot) : Set.SurjOn f s Set.univ
• atBot_atTop_le_cocompact 📋 Mathlib.Topology.Order.Compact
  {α : Type u_2} [LinearOrder α] [TopologicalSpace α] [NoMinOrder α] [NoMaxOrder α] [OrderClosedTopology α] : Filter.atBot ⊔ Filter.atTop ≤ Filter.cocompact α
• cocompact_eq_atBot_atTop 📋 Mathlib.Topology.Order.Compact
  {α : Type u_2} [LinearOrder α] [TopologicalSpace α] [NoMaxOrder α] [NoMinOrder α] [OrderClosedTopology α] [CompactIccSpace α] : Filter.cocompact α = Filter.atBot ⊔ Filter.atTop
• Continuous.exists_forall_ge_of_isBounded 📋 Mathlib.Topology.MetricSpace.Bounded
  {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] [PseudoMetricSpace β] [ProperSpace β] {f : β → α} (hf : Continuous f) (x₀ : β) (h : Bornology.IsBounded {x | f x₀ ≤ f x}) : ∃ x, ∀ (y : β), f y ≤ f x
• Continuous.exists_forall_le_of_isBounded 📋 Mathlib.Topology.MetricSpace.Bounded
  {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] [PseudoMetricSpace β] [ProperSpace β] {f : β → α} (hf : Continuous f) (x₀ : β) (h : Bornology.IsBounded {x | f x ≤ f x₀}) : ∃ x, ∀ (y : β), f x ≤ f y
• Antitone.ge_of_tendsto 📋 Mathlib.Topology.Order.MonotoneConvergence
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder α] [OrderClosedTopology α] [Preorder β] [IsCodirectedOrder β] {f : β → α} {a : α} (hf : Antitone f) (ha : Filter.Tendsto f Filter.atBot (nhds a)) (b : β) : f b ≤ a
• Antitone.le_of_tendsto 📋 Mathlib.Topology.Order.MonotoneConvergence
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder α] [OrderClosedTopology α] [Preorder β] [IsDirectedOrder β] {f : β → α} {a : α} (hf : Antitone f) (ha : Filter.Tendsto f Filter.atTop (nhds a)) (b : β) : a ≤ f b
• Monotone.ge_of_tendsto 📋 Mathlib.Topology.Order.MonotoneConvergence
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder α] [OrderClosedTopology α] [Preorder β] [IsDirectedOrder β] {f : β → α} {a : α} (hf : Monotone f) (ha : Filter.Tendsto f Filter.atTop (nhds a)) (b : β) : f b ≤ a
• Monotone.le_of_tendsto 📋 Mathlib.Topology.Order.MonotoneConvergence
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder α] [OrderClosedTopology α] [Preorder β] [IsCodirectedOrder β] {f : β → α} {a : α} (hf : Monotone f) (ha : Filter.Tendsto f Filter.atBot (nhds a)) (b : β) : a ≤ f b
• isGLB_of_tendsto_atBot 📋 Mathlib.Topology.Order.MonotoneConvergence
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder α] [OrderClosedTopology α] [Preorder β] [IsCodirectedOrder β] [Nonempty β] {f : β → α} {a : α} (hf : Monotone f) (ha : Filter.Tendsto f Filter.atBot (nhds a)) : IsGLB (Set.range f) a
• isGLB_of_tendsto_atTop 📋 Mathlib.Topology.Order.MonotoneConvergence
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder α] [OrderClosedTopology α] [Preorder β] [IsDirectedOrder β] [Nonempty β] {f : β → α} {a : α} (hf : Antitone f) (ha : Filter.Tendsto f Filter.atTop (nhds a)) : IsGLB (Set.range f) a
• isLUB_of_tendsto_atBot 📋 Mathlib.Topology.Order.MonotoneConvergence
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder α] [OrderClosedTopology α] [Preorder β] [IsCodirectedOrder β] [Nonempty β] {f : β → α} {a : α} (hf : Antitone f) (ha : Filter.Tendsto f Filter.atBot (nhds a)) : IsLUB (Set.range f) a
• isLUB_of_tendsto_atTop 📋 Mathlib.Topology.Order.MonotoneConvergence
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder α] [OrderClosedTopology α] [Preorder β] [IsDirectedOrder β] [Nonempty β] {f : β → α} {a : α} (hf : Monotone f) (ha : Filter.Tendsto f Filter.atTop (nhds a)) : IsLUB (Set.range f) a
• Multipliable.tprod_le_of_prod_le 📋 Mathlib.Topology.Algebra.InfiniteSum.Order
  {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [CommMonoid α] [Preorder α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a₂ : α} [L.NeBot] (hf : Multipliable f L) (h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂) : ∏'[L] (i : ι), f i ≤ a₂

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