Loogle!

Result

Found 121 declarations mentioning ClosedIicTopology.

• ClosedIicTopology 📋 Mathlib.Topology.Order.OrderClosed
  (α : Type u_1) [TopologicalSpace α] [Preorder α] : Prop
• instClosedIicTopology 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] : ClosedIicTopology α
• isClosed_Iic 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {a : α} : IsClosed (Set.Iic a)
• ClosedIicTopology.isClosed_Iic 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u_1} {inst✝ : TopologicalSpace α} {inst✝¹ : Preorder α} [self : ClosedIicTopology α] (a : α) : IsClosed (Set.Iic a)
• ClosedIicTopology.mk 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u_1} [TopologicalSpace α] [Preorder α] (isClosed_Iic : ∀ (a : α), IsClosed (Set.Iic a)) : ClosedIicTopology α
• instClosedIciTopologyOrderDual 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] : ClosedIciTopology αᵒᵈ
• instClosedIicTopologyOrderDual 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIciTopology α] : ClosedIicTopology αᵒᵈ
• closure_Iic 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] (a : α) : closure (Set.Iic a) = Set.Iic a
• BddAbove.closure 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {s : Set α} : BddAbove s → BddAbove (closure s)
• bddAbove_closure 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {s : Set α} : BddAbove (closure s) ↔ BddAbove s
• upperBounds_closure 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] (s : Set α) : upperBounds (closure s) = upperBounds s
• inf_nhds_atBot 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [Preorder α] [NoBotOrder α] [TopologicalSpace α] [ClosedIicTopology α] (a : α) : nhds a ⊓ Filter.atBot = ⊥
• nhds_inf_atBot 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [Preorder α] [NoBotOrder α] [TopologicalSpace α] [ClosedIicTopology α] (a : α) : nhds a ⊓ Filter.atBot = ⊥
• isOpen_Ioi 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a : α} : IsOpen (Set.Ioi a)
• not_tendsto_atBot_of_tendsto_nhds 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [Preorder α] [NoBotOrder α] [TopologicalSpace α] [ClosedIicTopology α] {a : α} {l : Filter β} [l.NeBot] {f : β → α} (hf : Filter.Tendsto f l (nhds a)) : ¬Filter.Tendsto f l Filter.atBot
• not_tendsto_nhds_of_tendsto_atBot 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [Preorder α] [NoBotOrder α] [TopologicalSpace α] [ClosedIicTopology α] {l : Filter β} [l.NeBot] {f : β → α} (hf : Filter.Tendsto f l Filter.atBot) (a : α) : ¬Filter.Tendsto f l (nhds a)
• disjoint_nhds_atBot 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [Preorder α] [NoBotOrder α] [TopologicalSpace α] [ClosedIicTopology α] (a : α) : Disjoint (nhds a) Filter.atBot
• le_of_tendsto' 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {f : β → α} {a b : α} {x : Filter β} [hx : x.NeBot] (lim : Filter.Tendsto f x (nhds a)) (h : ∀ (c : β), f c ≤ b) : a ≤ b
• le_of_tendsto_of_frequently 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {f : β → α} {a b : α} {x : Filter β} (lim : Filter.Tendsto f x (nhds a)) (h : ∃ᶠ (c : β) in x, f c ≤ b) : a ≤ b
• disjoint_nhds_atBot_iff 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {a : α} : Disjoint (nhds a) Filter.atBot ↔ ¬IsBot a
• IsLUB.range_of_tendsto 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {f : β → α} {a : α} {F : Filter β} [F.NeBot] (hle : ∀ (i : β), f i ≤ a) (hlim : Filter.Tendsto f F (nhds a)) : IsLUB (Set.range f) a
• le_of_tendsto 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {f : β → α} {a b : α} {x : Filter β} [hx : x.NeBot] (lim : Filter.Tendsto f x (nhds a)) (h : ∀ᶠ (c : β) in x, f c ≤ b) : a ≤ b
• interior_Ioi 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a : α} : interior (Set.Ioi a) = Set.Ioi a
• PredOrder.nhdsGE_eq_nhds 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] [PredOrder α] (a : α) : nhdsWithin a (Set.Ici a) = nhds a
• PredOrder.nhdsLE 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {b : α} [PredOrder α] : nhdsWithin b (Set.Iic b) = pure b
• PredOrder.nhdsLT 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a : α} [PredOrder α] : nhdsWithin a (Set.Iio a) = ⊥
• eventually_ge_nhds 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (hab : b < a) : ∀ᶠ (x : α) in nhds a, b ≤ x
• eventually_gt_nhds 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (hab : b < a) : ∀ᶠ (x : α) in nhds a, b < x
• Ici_mem_nhds 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (h : a < b) : Set.Ici a ∈ nhds b
• Ioi_mem_nhds 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (h : a < b) : Set.Ioi a ∈ nhds b
• CovBy.nhdsLE 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (H : a ⋖ b) : nhdsWithin b (Set.Iic b) = pure b
• CovBy.nhdsLT 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (h : a ⋖ b) : nhdsWithin b (Set.Iio b) = ⊥
• iSup_eq_of_forall_le_of_tendsto 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {ι : Type u_1} {F : Filter ι} [F.NeBot] [ConditionallyCompleteLattice α] [TopologicalSpace α] [ClosedIicTopology α] {a : α} {f : ι → α} (hle : ∀ (i : ι), f i ≤ a) (hlim : Filter.Tendsto f F (nhds a)) : ⨆ i, f i = a
• Dense.exists_ge 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] [NoMaxOrder α] {s : Set α} (hs : Dense s) (x : α) : ∃ y ∈ s, x ≤ y
• Dense.exists_gt 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] [NoMaxOrder α] {s : Set α} (hs : Dense s) (x : α) : ∃ y ∈ s, x < y
• PredOrder.nhdsGT_eq_nhdsNE 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] [PredOrder α] (a : α) : nhdsWithin a (Set.Ioi a) = nhdsWithin a {a}ᶜ
• Filter.Tendsto.eventually_const_le 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {l : Filter γ} {f : γ → α} {u v : α} (hv : u < v) (h : Filter.Tendsto f l (nhds v)) : ∀ᶠ (a : γ) in l, u ≤ f a
• Filter.Tendsto.eventually_const_lt 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {γ : Type w} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {l : Filter γ} {f : γ → α} {u v : α} (hv : u < v) (h : Filter.Tendsto f l (nhds v)) : ∀ᶠ (a : γ) in l, u < f a
• Icc_mem_nhdsLE 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (H : a < b) : Set.Icc a b ∈ nhdsWithin b (Set.Iic b)
• Icc_mem_nhdsLT 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (H : a < b) : Set.Icc a b ∈ nhdsWithin b (Set.Iio b)
• Ico_mem_nhdsLT 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (H : a < b) : Set.Ico a b ∈ nhdsWithin b (Set.Iio b)
• Ioc_mem_nhdsLE 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (H : a < b) : Set.Ioc a b ∈ nhdsWithin b (Set.Iic b)
• Ioc_mem_nhdsLT 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (H : a < b) : Set.Ioc a b ∈ nhdsWithin b (Set.Iio b)
• Ioo_mem_nhdsLT 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (H : a < b) : Set.Ioo a b ∈ nhdsWithin b (Set.Iio b)
• nhdsWithin_Icc_eq_nhdsLE 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (h : a < b) : nhdsWithin b (Set.Icc a b) = nhdsWithin b (Set.Iic b)
• nhdsWithin_Ico_eq_nhdsLT 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (h : a < b) : nhdsWithin b (Set.Ico a b) = nhdsWithin b (Set.Iio b)
• nhdsWithin_Ioc_eq_nhdsLE 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (h : a < b) : nhdsWithin b (Set.Ioc a b) = nhdsWithin b (Set.Iic b)
• nhdsWithin_Ioo_eq_nhdsLT 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b : α} (h : a < b) : nhdsWithin b (Set.Ioo a b) = nhdsWithin b (Set.Iio b)
• Dense.exists_ge' 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {s : Set α} (hs : Dense s) (htop : ∀ (x : α), IsTop x → x ∈ s) (x : α) : ∃ y ∈ s, x ≤ y
• Icc_mem_nhdsLE_of_mem 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b c : α} (H : b ∈ Set.Ioc a c) : Set.Icc a c ∈ nhdsWithin b (Set.Iic b)
• Icc_mem_nhdsLT_of_mem 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b c : α} (H : b ∈ Set.Ioc a c) : Set.Icc a c ∈ nhdsWithin b (Set.Iio b)
• Ico_mem_nhdsLE_of_mem 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b c : α} (H : b ∈ Set.Ioo a c) : Set.Ico a c ∈ nhdsWithin b (Set.Iic b)
• Ico_mem_nhdsLT_of_mem 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b c : α} (H : b ∈ Set.Ioc a c) : Set.Ico a c ∈ nhdsWithin b (Set.Iio b)
• Ioc_mem_nhdsLE_of_mem 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b c : α} (H : b ∈ Set.Ioc a c) : Set.Ioc a c ∈ nhdsWithin b (Set.Iic b)
• Ioc_mem_nhdsLT_of_mem 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b c : α} (H : b ∈ Set.Ioc a c) : Set.Ioc a c ∈ nhdsWithin b (Set.Iio b)
• Ioo_mem_nhdsLE_of_mem 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b c : α} (H : b ∈ Set.Ioo a c) : Set.Ioo a c ∈ nhdsWithin b (Set.Iic b)
• Ioo_mem_nhdsLT_of_mem 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {a b c : α} (H : b ∈ Set.Ioc a c) : Set.Ioo a c ∈ nhdsWithin b (Set.Iio b)
• continuousWithinAt_Icc_iff_Iic 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] [TopologicalSpace β] {a b : α} {f : α → β} (h : a < b) : ContinuousWithinAt f (Set.Icc a b) b ↔ ContinuousWithinAt f (Set.Iic b) b
• continuousWithinAt_Ico_iff_Iio 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] [TopologicalSpace β] {a b : α} {f : α → β} (h : a < b) : ContinuousWithinAt f (Set.Ico a b) b ↔ ContinuousWithinAt f (Set.Iio b) b
• continuousWithinAt_Ioc_iff_Iic 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] [TopologicalSpace β] {a b : α} {f : α → β} (h : a < b) : ContinuousWithinAt f (Set.Ioc a b) b ↔ ContinuousWithinAt f (Set.Iic b) b
• continuousWithinAt_Ioo_iff_Iio 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] [TopologicalSpace β] {a b : α} {f : α → β} (h : a < b) : ContinuousWithinAt f (Set.Ioo a b) b ↔ ContinuousWithinAt f (Set.Iio b) b
• iUnion_Iic_eq_Iio_of_lt_of_tendsto 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {ι : Type u_1} {F : Filter ι} [F.NeBot] [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [ClosedIicTopology α] {a : α} {f : ι → α} (hlt : ∀ (i : ι), f i < a) (hlim : Filter.Tendsto f F (nhds a)) : ⋃ i, Set.Iic (f i) = Set.Iio a
• Set.OrdConnected.mem_nhdsLE 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {S : Set α} {x y : α} (hS : S.OrdConnected) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) : S ∈ nhdsWithin y (Set.Iic y)
• Set.OrdConnected.mem_nhdsLT 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {S : Set α} {x y : α} (hS : S.OrdConnected) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) : S ∈ nhdsWithin y (Set.Iio y)
• Dense.isLUB_inter_iff 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_3} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {s t : Set α} (hs : Dense s) (ht : IsOpen t) {x : α} : IsLUB (t ∩ s) x ↔ IsLUB t x
• isLUB_iff_of_subset_of_subset_closure 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_3} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {s t : Set α} (hst : s ⊆ t) (hts : t ⊆ closure s) {x : α} : IsLUB s x ↔ IsLUB t x
• Dense.upperBounds_image 📋 Mathlib.Topology.Order.IsLUB
  {γ : Type u_2} {α : Type u_3} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {f : γ → α} [TopologicalSpace γ] {S : Set γ} (hS : Dense S) (hf : Continuous f) : upperBounds (f '' S) = upperBounds (Set.range f)
• Dense.ciSup' 📋 Mathlib.Topology.Order.IsLUB
  {γ : Type u_2} {α : Type u_3} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [ClosedIicTopology α] {f : γ → α} [TopologicalSpace γ] {S : Set γ} (hS : Dense S) (hf : Continuous f) : ⨆ s, f ↑s = ⨆ i, f i
• Dense.ciSup 📋 Mathlib.Topology.Order.IsLUB
  {γ : Type u_2} {α : Type u_3} [TopologicalSpace α] [ConditionallyCompleteLattice α] [ClosedIicTopology α] {f : γ → α} [TopologicalSpace γ] {S : Set γ} (hS : Dense S) (hf : Continuous f) (h : BddAbove (Set.range f)) : ⨆ s, f ↑s = ⨆ i, f i
• IsCompact.bddBelow 📋 Mathlib.Topology.Order.Compact
  {α : Type u_2} [LinearOrder α] [TopologicalSpace α] [ClosedIicTopology α] [Nonempty α] {s : Set α} (hs : IsCompact s) : BddBelow s
• IsCompact.sInf_mem 📋 Mathlib.Topology.Order.Compact
  {α : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [ClosedIicTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) : sInf s ∈ s
• IsCompact.exists_isLeast 📋 Mathlib.Topology.Order.Compact
  {α : Type u_2} [LinearOrder α] [TopologicalSpace α] [ClosedIicTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) : ∃ x, IsLeast s x
• IsCompact.isGLB_sInf 📋 Mathlib.Topology.Order.Compact
  {α : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [ClosedIicTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) : IsGLB s (sInf s)
• IsCompact.isLeast_sInf 📋 Mathlib.Topology.Order.Compact
  {α : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [ClosedIicTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) : IsLeast s (sInf s)
• Continuous.bddBelow_range_of_hasCompactMulSupport 📋 Mathlib.Topology.Order.Compact
  {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIicTopology α] [One α] {f : β → α} (hf : Continuous f) (h : HasCompactMulSupport f) : BddBelow (Set.range f)
• Continuous.bddBelow_range_of_hasCompactSupport 📋 Mathlib.Topology.Order.Compact
  {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIicTopology α] [Zero α] {f : β → α} (hf : Continuous f) (h : HasCompactSupport f) : BddBelow (Set.range f)
• IsCompact.exists_isGLB 📋 Mathlib.Topology.Order.Compact
  {α : Type u_2} [LinearOrder α] [TopologicalSpace α] [ClosedIicTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) : ∃ x ∈ s, IsGLB s x
• IsCompact.bddBelow_image 📋 Mathlib.Topology.Order.Compact
  {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIicTopology α] [Nonempty α] {f : β → α} {K : Set β} (hK : IsCompact K) (hf : ContinuousOn f K) : BddBelow (f '' K)
• atBot_le_cocompact 📋 Mathlib.Topology.Order.Compact
  {α : Type u_2} [LinearOrder α] [TopologicalSpace α] [NoMinOrder α] [ClosedIicTopology α] : Filter.atBot ≤ Filter.cocompact α
• Continuous.exists_forall_le_of_hasCompactMulSupport 📋 Mathlib.Topology.Order.Compact
  {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIicTopology α] [Nonempty β] [One α] {f : β → α} (hf : Continuous f) (h : HasCompactMulSupport f) : ∃ x, ∀ (y : β), f x ≤ f y
• Continuous.exists_forall_le_of_hasCompactSupport 📋 Mathlib.Topology.Order.Compact
  {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIicTopology α] [Nonempty β] [Zero α] {f : β → α} (hf : Continuous f) (h : HasCompactSupport f) : ∃ x, ∀ (y : β), f x ≤ f y
• IsCompact.exists_isMinOn 📋 Mathlib.Topology.Order.Compact
  {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIicTopology α] {s : Set β} (hs : IsCompact s) (ne_s : s.Nonempty) {f : β → α} (hf : ContinuousOn f s) : ∃ x ∈ s, IsMinOn f s x
• IsCompact.exists_sInf_image_eq 📋 Mathlib.Topology.Order.Compact
  {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIicTopology α] {s : Set β} (hs : IsCompact s) (ne_s : s.Nonempty) {f : β → α} (hf : ContinuousOn f s) : ∃ x ∈ s, sInf (f '' s) = f x
• Continuous.exists_forall_le 📋 Mathlib.Topology.Order.Compact
  {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIicTopology α] [Nonempty β] {f : β → α} (hf : Continuous f) (hlim : Filter.Tendsto f (Filter.cocompact β) Filter.atTop) : ∃ x, ∀ (y : β), f x ≤ f y
• Continuous.exists_forall_le' 📋 Mathlib.Topology.Order.Compact
  {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIicTopology α] {f : β → α} (hf : Continuous f) (x₀ : β) (h : ∀ᶠ (x : β) in Filter.cocompact β, f x₀ ≤ f x) : ∃ x, ∀ (y : β), f x ≤ f y
• cocompact_eq_atBot 📋 Mathlib.Topology.Order.Compact
  {α : Type u_2} [LinearOrder α] [TopologicalSpace α] [NoMinOrder α] [OrderTop α] [ClosedIicTopology α] [CompactIccSpace α] : Filter.cocompact α = Filter.atBot
• IsCompact.exists_sInf_image_eq_and_le 📋 Mathlib.Topology.Order.Compact
  {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIicTopology α] {s : Set β} (hs : IsCompact s) (ne_s : s.Nonempty) {f : β → α} (hf : ContinuousOn f s) : ∃ x ∈ s, sInf (f '' s) = f x ∧ ∀ y ∈ s, f x ≤ f y
• IsCompact.lt_sInf_iff_of_continuous 📋 Mathlib.Topology.Order.Compact
  {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIicTopology α] {f : β → α} {K : Set β} (hK : IsCompact K) (h0K : K.Nonempty) (hf : ContinuousOn f K) (y : α) : y < sInf (f '' K) ↔ ∀ x ∈ K, y < f x
• ContinuousOn.exists_isMinOn' 📋 Mathlib.Topology.Order.Compact
  {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIicTopology α] {s : Set β} {f : β → α} (hf : ContinuousOn f s) (hsc : IsClosed s) {x₀ : β} (h₀ : x₀ ∈ s) (hc : ∀ᶠ (x : β) in Filter.cocompact β ⊓ Filter.principal s, f x₀ ≤ f x) : ∃ x ∈ s, IsMinOn f s x
• IsCompact.exists_isMinOn_mem_subset 📋 Mathlib.Topology.Order.Compact
  {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIicTopology α] {f : β → α} {s t : Set β} {z : β} (ht : IsCompact t) (hf : ContinuousOn f t) (hz : z ∈ t) (hfz : ∀ z' ∈ t \ s, f z < f z') : ∃ x ∈ s, IsMinOn f t x
• IsCompact.exists_isLocalMin_mem_open 📋 Mathlib.Topology.Order.Compact
  {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIicTopology α] {f : β → α} {s t : Set β} {z : β} (ht : IsCompact t) (hst : s ⊆ t) (hf : ContinuousOn f t) (hz : z ∈ t) (hfz : ∀ z' ∈ t \ s, f z < f z') (hs : IsOpen s) : ∃ x ∈ s, IsLocalMin f x
• IsCompact.exists_forall_le' 📋 Mathlib.Topology.Order.Compact
  {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIicTopology α] [NoMaxOrder α] {f : β → α} {s : Set β} (hs : IsCompact s) (hf : ContinuousOn f s) {a : α} (hf' : ∀ b ∈ s, a < f b) : ∃ a', a < a' ∧ ∀ b ∈ s, a' ≤ f b
• hasProd_le_of_prod_le 📋 Mathlib.Topology.Algebra.InfiniteSum.Order
  {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [Preorder α] [CommMonoid α] [TopologicalSpace α] {a c : α} {f : ι → α} [ClosedIicTopology α] [L.NeBot] (hf : HasProd f a L) (h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ c) : a ≤ c
• hasSum_le_of_sum_le 📋 Mathlib.Topology.Algebra.InfiniteSum.Order
  {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [Preorder α] [AddCommMonoid α] [TopologicalSpace α] {a c : α} {f : ι → α} [ClosedIicTopology α] [L.NeBot] (hf : HasSum f a L) (h : ∀ (s : Finset ι), ∑ i ∈ s, f i ≤ c) : a ≤ c
• Multipliable.tprod_le_of_prod_range_le 📋 Mathlib.Topology.Algebra.InfiniteSum.Order
  {α : Type u_3} [Preorder α] [CommMonoid α] [TopologicalSpace α] {c : α} [ClosedIicTopology α] {f : ℕ → α} (hf : Multipliable f) (h : ∀ (n : ℕ), ∏ i ∈ Finset.range n, f i ≤ c) : ∏' (n : ℕ), f n ≤ c
• Summable.tsum_le_of_sum_range_le 📋 Mathlib.Topology.Algebra.InfiniteSum.Order
  {α : Type u_3} [Preorder α] [AddCommMonoid α] [TopologicalSpace α] {c : α} [ClosedIicTopology α] {f : ℕ → α} (hf : Summable f) (h : ∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c) : ∑' (n : ℕ), f n ≤ c
• BoundedGENhdsClass.of_closedIicTopology 📋 Mathlib.Topology.Order.LiminfLimsup
  {α : Type u_2} [LinearOrder α] [TopologicalSpace α] [ClosedIicTopology α] : BoundedGENhdsClass α
• UpperSemicontinuous.IsClosed_hypograph 📋 Mathlib.Topology.Semicontinuity.Basic
  {α : Type u_1} [TopologicalSpace α] {γ : Type u_4} [LinearOrder γ] [TopologicalSpace γ] [ClosedIicTopology γ] {f : α → γ} : UpperSemicontinuous f → IsClosed {p | p.2 ≤ f p.1}
• upperSemicontinuous_iff_IsClosed_hypograph 📋 Mathlib.Topology.Semicontinuity.Basic
  {α : Type u_1} [TopologicalSpace α] {γ : Type u_4} [LinearOrder γ] [TopologicalSpace γ] [ClosedIicTopology γ] {f : α → γ} : UpperSemicontinuous f ↔ IsClosed {p | p.2 ≤ f p.1}
• upperSemicontinuousOn_iff_isClosed_hypograph 📋 Mathlib.Topology.Semicontinuity.Basic
  {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_4} [LinearOrder γ] [TopologicalSpace γ] [ClosedIicTopology γ] {f : α → γ} (hs : IsClosed s) : UpperSemicontinuousOn f s ↔ IsClosed {p | p.1 ∈ s ∧ p.2 ≤ f p.1}
• atBot_isMeasurablyGenerated 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Order
  {α : Type u_1} [TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [Preorder α] [ClosedIicTopology α] : Filter.atBot.IsMeasurablyGenerated
• measurableSet_Iic 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Order
  {α : Type u_1} [TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [Preorder α] {a : α} [ClosedIicTopology α] : MeasurableSet (Set.Iic a)
• nullMeasurableSet_Iic 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Order
  {α : Type u_1} [TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [Preorder α] {a : α} {μ : MeasureTheory.Measure α} [ClosedIicTopology α] : MeasureTheory.NullMeasurableSet (Set.Iic a) μ
• nhdsWithin_Iic_isMeasurablyGenerated 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Order
  {α : Type u_1} [TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [Preorder α] {a b : α} [ClosedIicTopology α] : (nhdsWithin a (Set.Iic b)).IsMeasurablyGenerated
• measurableSet_uIoc 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Order
  {α : Type u_1} [TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [LinearOrder α] {a b : α} [ClosedIicTopology α] : MeasurableSet (Set.uIoc a b)
• measurableSet_Ioi 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Order
  {α : Type u_1} [TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [LinearOrder α] {a : α} [ClosedIicTopology α] : MeasurableSet (Set.Ioi a)
• measurableSet_Ioc 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Order
  {α : Type u_1} [TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [LinearOrder α] {a b : α} [ClosedIicTopology α] : MeasurableSet (Set.Ioc a b)
• nullMeasurableSet_Ioi 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Order
  {α : Type u_1} [TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [LinearOrder α] {a : α} {μ : MeasureTheory.Measure α} [ClosedIicTopology α] : MeasureTheory.NullMeasurableSet (Set.Ioi a) μ
• nhdsWithin_Ioi_isMeasurablyGenerated 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Order
  {α : Type u_1} [TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [LinearOrder α] {a b : α} [ClosedIicTopology α] : (nhdsWithin a (Set.Ioi b)).IsMeasurablyGenerated
• nullMeasurableSet_Ioc 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Order
  {α : Type u_1} [TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [LinearOrder α] {a b : α} {μ : MeasureTheory.Measure α} [ClosedIicTopology α] : MeasureTheory.NullMeasurableSet (Set.Ioc a b) μ
• Asymptotics.IsEquivalent.eventually_neg 📋 Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
  {α : Type u_1} {β : Type u_2} [NormedField β] [LinearOrder β] [IsStrictOrderedRing β] {u v : α → β} {l : Filter α} [ClosedIicTopology β] (h : Asymptotics.IsEquivalent l u v) (hv : ∀ᶠ (t : α) in l, v t < 0) : ∀ᶠ (x : α) in l, u x < 0
• Asymptotics.IsEquivalent.eventually_nonneg 📋 Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
  {α : Type u_1} {β : Type u_2} [NormedField β] [LinearOrder β] [IsStrictOrderedRing β] {u v : α → β} {l : Filter α} [ClosedIicTopology β] (h : Asymptotics.IsEquivalent l u v) (hv : ∀ᶠ (t : α) in l, 0 ≤ v t) : ∀ᶠ (x : α) in l, 0 ≤ u x
• Asymptotics.IsEquivalent.eventually_nonpos 📋 Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
  {α : Type u_1} {β : Type u_2} [NormedField β] [LinearOrder β] [IsStrictOrderedRing β] {u v : α → β} {l : Filter α} [ClosedIicTopology β] (h : Asymptotics.IsEquivalent l u v) (hv : ∀ᶠ (t : α) in l, v t ≤ 0) : ∀ᶠ (x : α) in l, u x ≤ 0
• Asymptotics.IsEquivalent.eventually_pos 📋 Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
  {α : Type u_1} {β : Type u_2} [NormedField β] [LinearOrder β] [IsStrictOrderedRing β] {u v : α → β} {l : Filter α} [ClosedIicTopology β] (h : Asymptotics.IsEquivalent l u v) (hv : ∀ᶠ (t : α) in l, 0 < v t) : ∀ᶠ (x : α) in l, 0 < u x
• Asymptotics.IsEquivalent.exists_pos_eq_mul 📋 Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
  {α : Type u_1} {β : Type u_2} [NormedField β] [LinearOrder β] [IsStrictOrderedRing β] {u v : α → β} {l : Filter α} [ClosedIicTopology β] (h : Asymptotics.IsEquivalent l u v) : ∃ φ, (∀ᶠ (x : α) in l, 0 < φ x) ∧ u =ᶠ[l] φ * v
• isLocallyClosed_Iic 📋 Mathlib.Topology.Order.IsLocallyClosed
  {X : Type u_1} [TopologicalSpace X] {a : X} [Preorder X] [ClosedIicTopology X] : IsLocallyClosed (Set.Iic a)
• isLocallyClosed_Ioi 📋 Mathlib.Topology.Order.IsLocallyClosed
  {X : Type u_1} [TopologicalSpace X] {a : X} [LinearOrder X] [ClosedIicTopology X] : IsLocallyClosed (Set.Ioi a)
• isLocallyClosed_Ioc 📋 Mathlib.Topology.Order.IsLocallyClosed
  {X : Type u_1} [TopologicalSpace X] {a b : X} [LinearOrder X] [ClosedIicTopology X] : IsLocallyClosed (Set.Ioc a b)
• Topology.IsUpper.instClosedIicTopology 📋 Mathlib.Topology.Order.LowerUpperTopology
  {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsUpper α] : ClosedIicTopology α
• Topology.WithUpper.continuous_toUpper 📋 Mathlib.Topology.Order.LowerUpperTopology
  {α : Type u_1} [Preorder α] [TopologicalSpace α] [ClosedIicTopology α] : Continuous ⇑Topology.WithUpper.toUpper
• Topology.IsScott.instClosedIicTopologyOfUnivSet 📋 Mathlib.Topology.Order.ScottTopology
  {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsScott α Set.univ] : ClosedIicTopology α

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