Loogle!

Result

Found 192 declarations mentioning frontier.

• frontier 📋 Mathlib.Topology.Defs.Basic
  {X : Type u} [TopologicalSpace X] (s : Set X) : Set X
• isClosed_frontier 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} : IsClosed (frontier s)
• frontier_univ 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] : frontier Set.univ = ∅
• frontier_subset_closure 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} : frontier s ⊆ closure s
• frontier_empty 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] : frontier ∅ = ∅
• IsClosed.frontier_subset 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} : IsClosed s → frontier s ⊆ s
• frontier_subset_iff_isClosed 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} : frontier s ⊆ s ↔ IsClosed s
• frontier_closure_subset 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} : frontier (closure s) ⊆ frontier s
• frontier_compl 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] (s : Set X) : frontier sᶜ = frontier s
• frontier_interior_subset 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} : frontier (interior s) ⊆ frontier s
• closure_eq_self_union_frontier 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] (s : Set X) : closure s = s ∪ frontier s
• self_diff_frontier 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] (s : Set X) : s \ frontier s = interior s
• self_sdiff_frontier 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] (s : Set X) : s \ frontier s = interior s
• interior_frontier 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} (h : IsClosed s) : interior (frontier s) = ∅
• closure_diff_frontier 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] (s : Set X) : closure s \ frontier s = interior s
• closure_diff_interior 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] (s : Set X) : closure s \ interior s = frontier s
• closure_eq_interior_union_frontier 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] (s : Set X) : closure s = interior s ∪ frontier s
• closure_sdiff_frontier 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] (s : Set X) : closure s \ frontier s = interior s
• closure_sdiff_interior 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] (s : Set X) : closure s \ interior s = frontier s
• IsClosed.frontier_eq 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsClosed s) : frontier s = s \ interior s
• IsOpen.frontier_eq 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsOpen s) : frontier s = closure s \ s
• IsOpen.inter_frontier_eq 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsOpen s) : s ∩ frontier s = ∅
• frontier_eq_closure_inter_closure 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} : frontier s = closure s ∩ closure sᶜ
• compl_frontier_eq_union_interior 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} : (frontier s)ᶜ = interior s ∪ interior sᶜ
• mem_frontier_iff_notMem_interior 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} {x : X} (hx : x ∈ s) : x ∈ frontier s ↔ x ∉ interior s
• mem_interior_iff_notMem_frontier 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} {x : X} (hx : x ∈ s) : x ∈ interior s ↔ x ∉ frontier s
• frontier_eq_inter_compl_interior 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} : frontier s = (interior s)ᶜ ∩ (interior sᶜ)ᶜ
• disjoint_interior_frontier 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} : Disjoint (interior s) (frontier s)
• frontier_inter_subset 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] (s t : Set X) : frontier (s ∩ t) ⊆ frontier s ∩ closure t ∪ closure s ∩ frontier t
• disjoint_frontier_iff_isOpen 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} : Disjoint (frontier s) s ↔ IsOpen s
• frontier_union_subset 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] (s t : Set X) : frontier (s ∪ t) ⊆ frontier s ∩ closure tᶜ ∪ closure sᶜ ∩ frontier t
• Disjoint.frontier_left 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s t : Set X} (ht : IsOpen t) (hd : Disjoint s t) : Disjoint (frontier s) t
• Disjoint.frontier_right 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s t : Set X} (hs : IsOpen s) (hd : Disjoint s t) : Disjoint s (frontier t)
• Continuous.frontier_preimage_subset 📋 Mathlib.Topology.Continuous
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) (t : Set Y) : frontier (f ⁻¹' t) ⊆ f ⁻¹' frontier t
• IsOpenMap.preimage_frontier_subset_frontier_preimage 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenMap f) {s : Set Y} : f ⁻¹' frontier s ⊆ frontier (f ⁻¹' s)
• IsOpenMap.preimage_frontier_eq_frontier_preimage 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenMap f) (hfc : Continuous f) (s : Set Y) : f ⁻¹' frontier s = frontier (f ⁻¹' s)
• IsHomeomorph.image_frontier 📋 Mathlib.Topology.Homeomorph.Defs
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsHomeomorph f) (s : Set X) : f '' frontier s = frontier (f '' s)
• image_frontier_preimage_comp 📋 Mathlib.Topology.Homeomorph.Defs
  {X : Type u_4} {Y : Type u_5} {Z : Type u_6} [TopologicalSpace X] [TopologicalSpace Y] (e : X → Y) (he : IsHomeomorph e) (f : Y → Z) (s : Set Z) : f ∘ e '' frontier (f ∘ e ⁻¹' s) = f '' frontier (f ⁻¹' s)
• Homeomorph.image_frontier 📋 Mathlib.Topology.Homeomorph.Defs
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set X) : ⇑h '' frontier s = frontier (⇑h '' s)
• Homeomorph.preimage_frontier 📋 Mathlib.Topology.Homeomorph.Defs
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set Y) : ⇑h ⁻¹' frontier s = frontier (⇑h ⁻¹' s)
• frontier_prod_univ_eq 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (s : Set X) : frontier (s ×ˢ Set.univ) = frontier s ×ˢ Set.univ
• frontier_univ_prod_eq 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (s : Set Y) : frontier (Set.univ ×ˢ s) = Set.univ ×ˢ frontier s
• frontier_prod_eq 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (s : Set X) (t : Set Y) : frontier (s ×ˢ t) = closure s ×ˢ frontier t ∪ frontier s ×ˢ closure t
• frontier_inter_open_inter 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] {s t : Set X} (ht : IsOpen t) : frontier (s ∩ t) ∩ t = frontier s ∩ t
• SeparationQuotient.preimage_mk_frontier 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {t : Set (SeparationQuotient X)} : SeparationQuotient.mk ⁻¹' frontier t = frontier (SeparationQuotient.mk ⁻¹' t)
• IsOpen.ite 📋 Mathlib.Topology.Piecewise
  {α : Type u_1} [TopologicalSpace α] {s s' t : Set α} (hs : IsOpen s) (hs' : IsOpen s') (ht : s ∩ frontier t = s' ∩ frontier t) : IsOpen (t.ite s s')
• IsOpen.ite' 📋 Mathlib.Topology.Piecewise
  {α : Type u_1} [TopologicalSpace α] {s s' t : Set α} (hs : IsOpen s) (hs' : IsOpen s') (ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s') : IsOpen (t.ite s s')
• ite_inter_closure_eq_of_inter_frontier_eq 📋 Mathlib.Topology.Piecewise
  {α : Type u_1} [TopologicalSpace α] {s s' t : Set α} (ht : s ∩ frontier t = s' ∩ frontier t) : t.ite s s' ∩ closure t = s ∩ closure t
• Continuous.piecewise 📋 Mathlib.Topology.Piecewise
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : α → β} {s : Set α} [(a : α) → Decidable (a ∈ s)] (hs : ∀ a ∈ frontier s, f a = g a) (hf : Continuous f) (hg : Continuous g) : Continuous (s.piecewise f g)
• Continuous.if 📋 Mathlib.Topology.Piecewise
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : α → β} {p : α → Prop} [(a : α) → Decidable (p a)] (hp : ∀ a ∈ frontier {x | p x}, f a = g a) (hf : Continuous f) (hg : Continuous g) : Continuous fun a => if p a then f a else g a
• ite_inter_closure_compl_eq_of_inter_frontier_eq 📋 Mathlib.Topology.Piecewise
  {α : Type u_1} [TopologicalSpace α] {s s' t : Set α} (ht : s ∩ frontier t = s' ∩ frontier t) : t.ite s s' ∩ closure tᶜ = s' ∩ closure tᶜ
• continuous_piecewise 📋 Mathlib.Topology.Piecewise
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : α → β} {s : Set α} [(a : α) → Decidable (a ∈ s)] (hs : ∀ a ∈ frontier s, f a = g a) (hf : ContinuousOn f (closure s)) (hg : ContinuousOn g (closure sᶜ)) : Continuous (s.piecewise f g)
• continuous_if 📋 Mathlib.Topology.Piecewise
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : α → β} {p : α → Prop} [(a : α) → Decidable (p a)] (hp : ∀ a ∈ frontier {x | p x}, f a = g a) (hf : ContinuousOn f (closure {x | p x})) (hg : ContinuousOn g (closure {x | ¬p x})) : Continuous fun a => if p a then f a else g a
• continuousOn_piecewise_ite 📋 Mathlib.Topology.Piecewise
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : α → β} {s s' t : Set α} [(x : α) → Decidable (x ∈ t)] (h : ContinuousOn f s) (h' : ContinuousOn g s') (H : s ∩ frontier t = s' ∩ frontier t) (Heq : Set.EqOn f g (s ∩ frontier t)) : ContinuousOn (t.piecewise f g) (t.ite s s')
• ContinuousOn.piecewise 📋 Mathlib.Topology.Piecewise
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : α → β} {s t : Set α} [(a : α) → Decidable (a ∈ t)] (ht : ∀ a ∈ s ∩ frontier t, f a = g a) (hf : ContinuousOn f (s ∩ closure t)) (hg : ContinuousOn g (s ∩ closure tᶜ)) : ContinuousOn (t.piecewise f g) s
• ContinuousOn.if 📋 Mathlib.Topology.Piecewise
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : α → β} {s : Set α} {p : α → Prop} [(a : α) → Decidable (p a)] (hp : ∀ a ∈ s ∩ frontier {a | p a}, f a = g a) (hf : ContinuousOn f (s ∩ closure {a | p a})) (hg : ContinuousOn g (s ∩ closure {a | ¬p a})) : ContinuousOn (fun a => if p a then f a else g a) s
• continuousOn_piecewise_ite' 📋 Mathlib.Topology.Piecewise
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : α → β} {s s' t : Set α} [(x : α) → Decidable (x ∈ t)] (h : ContinuousOn f (s ∩ closure t)) (h' : ContinuousOn g (s' ∩ closure tᶜ)) (H : s ∩ frontier t = s' ∩ frontier t) (Heq : Set.EqOn f g (s ∩ frontier t)) : ContinuousOn (t.piecewise f g) (t.ite s s')
• continuous_if' 📋 Mathlib.Topology.Piecewise
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : α → β} {p : α → Prop} [(a : α) → Decidable (p a)] (hpf : ∀ a ∈ frontier {x | p x}, Filter.Tendsto f (nhdsWithin a {x | p x}) (nhds (if p a then f a else g a))) (hpg : ∀ a ∈ frontier {x | p x}, Filter.Tendsto g (nhdsWithin a {x | ¬p x}) (nhds (if p a then f a else g a))) (hf : ContinuousOn f {x | p x}) (hg : ContinuousOn g {x | ¬p x}) : Continuous fun a => if p a then f a else g a
• ContinuousOn.piecewise' 📋 Mathlib.Topology.Piecewise
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : α → β} {s t : Set α} [(a : α) → Decidable (a ∈ t)] (hpf : ∀ a ∈ s ∩ frontier t, Filter.Tendsto f (nhdsWithin a (s ∩ t)) (nhds (t.piecewise f g a))) (hpg : ∀ a ∈ s ∩ frontier t, Filter.Tendsto g (nhdsWithin a (s ∩ tᶜ)) (nhds (t.piecewise f g a))) (hf : ContinuousOn f (s ∩ t)) (hg : ContinuousOn g (s ∩ tᶜ)) : ContinuousOn (t.piecewise f g) s
• ContinuousOn.if' 📋 Mathlib.Topology.Piecewise
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {p : α → Prop} {f g : α → β} [(a : α) → Decidable (p a)] (hpf : ∀ a ∈ s ∩ frontier {a | p a}, Filter.Tendsto f (nhdsWithin a (s ∩ {a | p a})) (nhds (if p a then f a else g a))) (hpg : ∀ a ∈ s ∩ frontier {a | p a}, Filter.Tendsto g (nhdsWithin a (s ∩ {a | ¬p a})) (nhds (if p a then f a else g a))) (hf : ContinuousOn f (s ∩ {a | p a})) (hg : ContinuousOn g (s ∩ {a | ¬p a})) : ContinuousOn (fun a => if p a then f a else g a) s
• 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}
• 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}
• IsClopen.frontier_eq 📋 Mathlib.Topology.Clopen
  {X : Type u} [TopologicalSpace X] {s : Set X} : IsClopen s → frontier s = ∅
• isClopen_iff_frontier_eq_empty 📋 Mathlib.Topology.Clopen
  {X : Type u} [TopologicalSpace X] {s : Set X} : IsClopen s ↔ frontier s = ∅
• nonempty_frontier_iff 📋 Mathlib.Topology.Connected.Clopen
  {α : Type u} [TopologicalSpace α] [PreconnectedSpace α] {s : Set α} : (frontier s).Nonempty ↔ s.Nonempty ∧ s ≠ Set.univ
• frontier_eq_empty_iff 📋 Mathlib.Topology.Connected.Clopen
  {α : Type u} [TopologicalSpace α] [PreconnectedSpace α] {s : Set α} : frontier s = ∅ ↔ s = ∅ ∨ s = Set.univ
• isClopen_preimage_val 📋 Mathlib.Topology.Connected.Clopen
  {X : Type u_3} [TopologicalSpace X] {u v : Set X} (hu : IsOpen u) (huv : Disjoint (frontier u) v) : IsClopen (Subtype.val ⁻¹' u)
• IsOpen.coborder_eq 📋 Mathlib.Topology.LocallyClosed
  {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsOpen s → coborder s = (frontier s)ᶜ
• coborder_eq_compl_frontier_iff 📋 Mathlib.Topology.LocallyClosed
  {X : Type u_1} [TopologicalSpace X] {s : Set X} : coborder s = (frontier s)ᶜ ↔ IsOpen s
• coborder_eq_union_frontier_compl 📋 Mathlib.Topology.LocallyClosed
  {X : Type u_1} [TopologicalSpace X] {s : Set X} : coborder s = s ∪ (frontier s)ᶜ
• frontier_Ici 📋 Mathlib.Topology.Order.DenselyOrdered
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] {a : α} : frontier (Set.Ici a) = {a}
• frontier_Iic 📋 Mathlib.Topology.Order.DenselyOrdered
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMaxOrder α] {a : α} : frontier (Set.Iic a) = {a}
• frontier_Iio 📋 Mathlib.Topology.Order.DenselyOrdered
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] {a : α} : frontier (Set.Iio a) = {a}
• frontier_Ioi 📋 Mathlib.Topology.Order.DenselyOrdered
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMaxOrder α] {a : α} : frontier (Set.Ioi a) = {a}
• frontier_Ici' 📋 Mathlib.Topology.Order.DenselyOrdered
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} (ha : (Set.Iio a).Nonempty) : frontier (Set.Ici a) = {a}
• frontier_Iic' 📋 Mathlib.Topology.Order.DenselyOrdered
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} (ha : (Set.Ioi a).Nonempty) : frontier (Set.Iic a) = {a}
• frontier_Iio' 📋 Mathlib.Topology.Order.DenselyOrdered
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} (ha : (Set.Iio a).Nonempty) : frontier (Set.Iio a) = {a}
• frontier_Ioi' 📋 Mathlib.Topology.Order.DenselyOrdered
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α} (ha : (Set.Ioi a).Nonempty) : frontier (Set.Ioi a) = {a}
• frontier_Ioo 📋 Mathlib.Topology.Order.DenselyOrdered
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α} (h : a < b) : frontier (Set.Ioo a b) = {a, b}
• frontier_Ico 📋 Mathlib.Topology.Order.DenselyOrdered
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] {a b : α} (h : a < b) : frontier (Set.Ico a b) = {a, b}
• frontier_Ioc 📋 Mathlib.Topology.Order.DenselyOrdered
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMaxOrder α] {a b : α} (h : a < b) : frontier (Set.Ioc a b) = {a, b}
• frontier_Icc 📋 Mathlib.Topology.Order.DenselyOrdered
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] [NoMaxOrder α] {a b : α} (h : a ≤ b) : frontier (Set.Icc a b) = {a, b}
• Metric.frontier_ball_subset_sphere 📋 Mathlib.Topology.MetricSpace.Pseudo.Lemmas
  {α : Type u_2} [PseudoMetricSpace α] {x : α} {ε : ℝ} : frontier (Metric.ball x ε) ⊆ Metric.sphere x ε
• Metric.frontier_closedBall_subset_sphere 📋 Mathlib.Topology.MetricSpace.Pseudo.Lemmas
  {α : Type u_2} [PseudoMetricSpace α] {x : α} {ε : ℝ} : frontier (Metric.closedBall x ε) ⊆ Metric.sphere x ε
• measurableSet_frontier 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
  {α : Type u_1} {s : Set α} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] : MeasurableSet (frontier s)
• nullMeasurableSet_of_null_frontier 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
  {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} (h : μ (frontier s) = 0) : MeasureTheory.NullMeasurableSet s μ
• closure_ae_eq_of_null_frontier 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
  {α' : Type u_6} [TopologicalSpace α'] [MeasurableSpace α'] {μ : MeasureTheory.Measure α'} {s : Set α'} (h : μ (frontier s) = 0) : closure s =ᵐ[μ] s
• interior_ae_eq_of_null_frontier 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
  {α' : Type u_6} [TopologicalSpace α'] [MeasurableSpace α'] {μ : MeasureTheory.Measure α'} {s : Set α'} (h : μ (frontier s) = 0) : interior s =ᵐ[μ] s
• measure_closure_of_null_frontier 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
  {α' : Type u_6} [TopologicalSpace α'] [MeasurableSpace α'] {μ : MeasureTheory.Measure α'} {s : Set α'} (h : μ (frontier s) = 0) : μ (closure s) = μ s
• measure_interior_of_null_frontier 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
  {α' : Type u_6} [TopologicalSpace α'] [MeasurableSpace α'] {μ : MeasureTheory.Measure α'} {s : Set α'} (h : μ (frontier s) = 0) : μ (interior s) = μ s
• null_frontier_inter 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
  {α' : Type u_6} [TopologicalSpace α'] [MeasurableSpace α'] {μ : MeasureTheory.Measure α'} {s s' : Set α'} (h : μ (frontier s) = 0) (h' : μ (frontier s') = 0) : μ (frontier (s ∩ s')) = 0
• Metric.frontier_cthickening_subset 📋 Mathlib.Topology.MetricSpace.Thickening
  {α : Type u} [PseudoEMetricSpace α] (E : Set α) {δ : ℝ} : frontier (Metric.cthickening δ E) ⊆ {x | Metric.infEDist x E = ENNReal.ofReal δ}
• Metric.frontier_thickening_subset 📋 Mathlib.Topology.MetricSpace.Thickening
  {α : Type u} [PseudoEMetricSpace α] (E : Set α) {δ : ℝ} : frontier (Metric.thickening δ E) ⊆ {x | Metric.infEDist x E = ENNReal.ofReal δ}
• Metric.frontier_thickening_disjoint 📋 Mathlib.Topology.MetricSpace.Thickening
  {α : Type u} [PseudoEMetricSpace α] (A : Set α) : Pairwise (Function.onFun Disjoint fun r => frontier (Metric.thickening r A))
• Metric.frontier_cthickening_disjoint 📋 Mathlib.Topology.MetricSpace.Thickening
  {α : Type u} [PseudoEMetricSpace α] (A : Set α) : Pairwise (Function.onFun Disjoint fun r => frontier (Metric.cthickening (↑r) A))
• frontier_ball 📋 Mathlib.Analysis.Normed.Module.RCLike.Real
  {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (x : E) {r : ℝ} (hr : r ≠ 0) : frontier (Metric.ball x r) = Metric.sphere x r
• frontier_closedBall 📋 Mathlib.Analysis.Normed.Module.RCLike.Real
  {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (x : E) {r : ℝ} (hr : r ≠ 0) : frontier (Metric.closedBall x r) = Metric.sphere x r
• frontier_sphere 📋 Mathlib.Analysis.Normed.Module.RCLike.Real
  {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (x : E) {r : ℝ} (hr : r ≠ 0) : frontier (Metric.sphere x r) = Metric.sphere x r
• frontier_closedBall' 📋 Mathlib.Analysis.Normed.Module.RCLike.Real
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] (x : E) (r : ℝ) : frontier (Metric.closedBall x r) = Metric.sphere x r
• frontier_sphere' 📋 Mathlib.Analysis.Normed.Module.RCLike.Real
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] (x : E) (r : ℝ) : frontier (Metric.sphere x r) = Metric.sphere x r
• StrictConvex.eq_of_openSegment_subset_frontier 📋 Mathlib.Analysis.Convex.Strict
  {𝕜 : Type u_1} {E : Type u_3} [Ring 𝕜] [PartialOrder 𝕜] [TopologicalSpace E] [AddCommGroup E] [Module 𝕜 E] {s : Set E} {x y : E} [IsOrderedRing 𝕜] [Nontrivial 𝕜] [DenselyOrdered 𝕜] (hs : StrictConvex 𝕜 s) (hx : x ∈ s) (hy : y ∈ s) (h : openSegment 𝕜 x y ⊆ frontier s) : x = y
• Convex.strictConvex 📋 Mathlib.Analysis.Convex.Topology
  {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (h : (s \ interior s).Pairwise fun x y => (segment 𝕜 x y \ frontier s).Nonempty) : StrictConvex 𝕜 s
• IsCompact.exists_mem_frontier_infDist_compl_eq_dist 📋 Mathlib.Analysis.Normed.Module.FiniteDimension
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] {x : E} {K : Set E} (hK : IsCompact K) (hx : x ∈ K) : ∃ y ∈ frontier K, Metric.infDist x Kᶜ = dist x y
• exists_mem_frontier_infDist_compl_eq_dist 📋 Mathlib.Analysis.Normed.Module.FiniteDimension
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {x : E} {s : Set E} (hx : x ∈ s) (hs : s ≠ Set.univ) : ∃ y ∈ frontier s, Metric.infDist x sᶜ = dist x y
• ContinuousOn.continuousAt_indicator 📋 Mathlib.Topology.Algebra.Indicator
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} [Zero β] (hf : ContinuousOn f (interior s)) {x : α} (hx : x ∉ frontier s) : ContinuousAt (s.indicator f) x
• ContinuousOn.continuousAt_mulIndicator 📋 Mathlib.Topology.Algebra.Indicator
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} [One β] (hf : ContinuousOn f (interior s)) {x : α} (hx : x ∉ frontier s) : ContinuousAt (s.mulIndicator f) x
• Continuous.indicator 📋 Mathlib.Topology.Algebra.Indicator
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} [Zero β] (hs : ∀ a ∈ frontier s, f a = 0) (hf : Continuous f) : Continuous (s.indicator f)
• Continuous.mulIndicator 📋 Mathlib.Topology.Algebra.Indicator
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} [One β] (hs : ∀ a ∈ frontier s, f a = 1) (hf : Continuous f) : Continuous (s.mulIndicator f)
• continuous_indicator 📋 Mathlib.Topology.Algebra.Indicator
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} [Zero β] (hs : ∀ a ∈ frontier s, f a = 0) (hf : ContinuousOn f (closure s)) : Continuous (s.indicator f)
• continuous_mulIndicator 📋 Mathlib.Topology.Algebra.Indicator
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} [One β] (hs : ∀ a ∈ frontier s, f a = 1) (hf : ContinuousOn f (closure s)) : Continuous (s.mulIndicator f)
• ContinuousLinearMap.frontier_preimage 📋 Mathlib.Analysis.Normed.Operator.Banach
  {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜' F] (f : E →SL[σ] F) {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] [CompleteSpace E] (hsurj : Function.Surjective ⇑f) (s : Set F) : frontier (⇑f ⁻¹' s) = ⇑f ⁻¹' frontier s
• tendsto_card_div_pow_atTop_volume 📋 Mathlib.Analysis.BoxIntegral.UnitPartition
  {ι : Type u_1} (s : Set (ι → ℝ)) [Fintype ι] (hs₁ : Bornology.IsBounded s) (hs₂ : MeasurableSet s) (hs₃ : MeasureTheory.volume (frontier s) = 0) : Filter.Tendsto (fun n => ↑(Nat.card ↑(s ∩ (↑n)⁻¹ • ↑(Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / ↑n ^ Fintype.card ι) Filter.atTop (nhds (MeasureTheory.volume.real s))
• tendsto_card_div_pow_atTop_volume' 📋 Mathlib.Analysis.BoxIntegral.UnitPartition
  {ι : Type u_1} (s : Set (ι → ℝ)) [Fintype ι] (hs₁ : Bornology.IsBounded s) (hs₂ : MeasurableSet s) (hs₃ : MeasureTheory.volume (frontier s) = 0) (hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s) : Filter.Tendsto (fun x => ↑(Nat.card ↑(s ∩ x⁻¹ • ↑(Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ Fintype.card ι) Filter.atTop (nhds (MeasureTheory.volume.real s))
• tendsto_tsum_div_pow_atTop_integral 📋 Mathlib.Analysis.BoxIntegral.UnitPartition
  {ι : Type u_1} (s : Set (ι → ℝ)) (F : (ι → ℝ) → ℝ) [Fintype ι] (hF : Continuous F) (hs₁ : Bornology.IsBounded s) (hs₂ : MeasurableSet s) (hs₃ : MeasureTheory.volume (frontier s) = 0) : Filter.Tendsto (fun n => (∑' (x : ↑(s ∩ (↑n)⁻¹ • ↑(Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))), F ↑x) / ↑n ^ Fintype.card ι) Filter.atTop (nhds (∫ (x : ι → ℝ) in s, F x))
• ZLattice.covolume.tendsto_card_div_pow' 📋 Mathlib.Algebra.Module.ZLattice.Covolume
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] {s : Set E} (hs₁ : Bornology.IsBounded s) (hs₂ : MeasurableSet s) (hs₃ : MeasureTheory.volume (frontier s) = 0) : Filter.Tendsto (fun n => ↑(Nat.card ↑(s ∩ (↑n)⁻¹ • ↑L)) / ↑n ^ Module.finrank ℝ E) Filter.atTop (nhds (MeasureTheory.volume.real s / ZLattice.covolume L MeasureTheory.volume))
• ZLattice.covolume.tendsto_card_div_pow 📋 Mathlib.Algebra.Module.ZLattice.Covolume
  {ι : Type u_1} [Fintype ι] (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology ↥L] [IsZLattice ℝ L] (b : Module.Basis ι ℤ ↥L) {s : Set (ι → ℝ)} (hs₁ : Bornology.IsBounded s) (hs₂ : MeasurableSet s) (hs₃ : MeasureTheory.volume (frontier s) = 0) : Filter.Tendsto (fun n => ↑(Nat.card ↑(s ∩ (↑n)⁻¹ • ↑L)) / ↑n ^ Fintype.card ι) Filter.atTop (nhds (MeasureTheory.volume.real s / ZLattice.covolume L MeasureTheory.volume))
• ZLattice.covolume.tendsto_card_le_div 📋 Mathlib.Algebra.Module.ZLattice.Covolume
  {ι : Type u_1} [Fintype ι] (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology ↥L] [IsZLattice ℝ L] {X : Set (ι → ℝ)} (hX : ∀ ⦃x : ι → ℝ⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X) {F : (ι → ℝ) → ℝ} (h₁ : ∀ (x : ι → ℝ) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ Fintype.card ι * F x) (h₂ : Bornology.IsBounded {x | x ∈ X ∧ F x ≤ 1}) (h₃ : MeasurableSet {x | x ∈ X ∧ F x ≤ 1}) (h₄ : MeasureTheory.volume (frontier {x | x ∈ X ∧ F x ≤ 1}) = 0) [Nonempty ι] : Filter.Tendsto (fun c => ↑(Nat.card ↑({x | x ∈ X ∧ F x ≤ c} ∩ ↑L)) / c) Filter.atTop (nhds (MeasureTheory.volume.real {x | x ∈ X ∧ F x ≤ 1} / ZLattice.covolume L MeasureTheory.volume))
• ZLattice.covolume.tendsto_card_le_div' 📋 Mathlib.Algebra.Module.ZLattice.Covolume
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] [Nontrivial E] {X : Set E} {F : E → ℝ} (hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X) (h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ Module.finrank ℝ E * F x) (h₂ : Bornology.IsBounded {x | x ∈ X ∧ F x ≤ 1}) (h₃ : MeasurableSet {x | x ∈ X ∧ F x ≤ 1}) (h₄ : MeasureTheory.volume (frontier {x | x ∈ X ∧ F x ≤ 1}) = 0) : Filter.Tendsto (fun c => ↑(Nat.card ↑({x | x ∈ X ∧ F x ≤ c} ∩ ↑L)) / c) Filter.atTop (nhds (MeasureTheory.volume.real {x | x ∈ X ∧ F x ≤ 1} / ZLattice.covolume L MeasureTheory.volume))
• ZLattice.covolume.tendsto_card_div_pow'' 📋 Mathlib.Algebra.Module.ZLattice.Covolume
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] {ι : Type u_2} [Fintype ι] (b : Module.Basis ι ℤ ↥L) [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {s : Set E} (hs₁ : Bornology.IsBounded s) (hs₂ : MeasurableSet s) (hs₃ : MeasureTheory.volume (frontier (⇑(Module.Basis.ofZLatticeBasis ℝ L b).equivFun '' s)) = 0) : Filter.Tendsto (fun n => ↑(Nat.card ↑(s ∩ (↑n)⁻¹ • ↑L)) / ↑n ^ Fintype.card ι) Filter.atTop (nhds (MeasureTheory.volume.real (⇑(Module.Basis.ofZLatticeBasis ℝ L b).equivFun '' s)))
• ZLattice.covolume.tendsto_card_le_div'' 📋 Mathlib.Algebra.Module.ZLattice.Covolume
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] {ι : Type u_2} [Fintype ι] (b : Module.Basis ι ℤ ↥L) [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [Nonempty ι] {X : Set E} (hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X) {F : E → ℝ} (h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ Fintype.card ι * F x) (h₂ : Bornology.IsBounded {x | x ∈ X ∧ F x ≤ 1}) (h₃ : MeasurableSet {x | x ∈ X ∧ F x ≤ 1}) (h₄ : MeasureTheory.volume (frontier (⇑(Module.Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1})) = 0) : Filter.Tendsto (fun c => ↑(Nat.card ↑({x | x ∈ X ∧ F x ≤ c} ∩ ↑L)) / c) Filter.atTop (nhds (MeasureTheory.volume.real (⇑(Module.Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1})))
• gauge_eq_one_iff_mem_frontier 📋 Mathlib.Analysis.Convex.Gauge
  {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} {x : E} [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] (hc : Convex ℝ s) (hs₀ : s ∈ nhds 0) : gauge s x = 1 ↔ x ∈ frontier s
• mem_frontier_of_gauge_eq_one 📋 Mathlib.Analysis.Convex.Gauge
  {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} {x : E} [TopologicalSpace E] [ContinuousSMul ℝ E] (hc : Convex ℝ s) (hs₀ : 0 ∈ s) (ha : Absorbent ℝ s) (h : gauge s x = 1) : x ∈ frontier s
• Complex.frontier_setOfPred_im_le 📋 Mathlib.Analysis.Complex.ReImTopology
  (a : ℝ) : frontier {z | z.im ≤ a} = {z | z.im = a}
• Complex.frontier_setOfPred_im_lt 📋 Mathlib.Analysis.Complex.ReImTopology
  (a : ℝ) : frontier {z | z.im < a} = {z | z.im = a}
• Complex.frontier_setOfPred_le_im 📋 Mathlib.Analysis.Complex.ReImTopology
  (a : ℝ) : frontier {z | a ≤ z.im} = {z | z.im = a}
• Complex.frontier_setOfPred_le_re 📋 Mathlib.Analysis.Complex.ReImTopology
  (a : ℝ) : frontier {z | a ≤ z.re} = {z | z.re = a}
• Complex.frontier_setOfPred_lt_im 📋 Mathlib.Analysis.Complex.ReImTopology
  (a : ℝ) : frontier {z | a < z.im} = {z | z.im = a}
• Complex.frontier_setOfPred_lt_re 📋 Mathlib.Analysis.Complex.ReImTopology
  (a : ℝ) : frontier {z | a < z.re} = {z | z.re = a}
• Complex.frontier_setOfPred_re_le 📋 Mathlib.Analysis.Complex.ReImTopology
  (a : ℝ) : frontier {z | z.re ≤ a} = {z | z.re = a}
• Complex.frontier_setOfPred_re_lt 📋 Mathlib.Analysis.Complex.ReImTopology
  (a : ℝ) : frontier {z | z.re < a} = {z | z.re = a}
• Complex.frontier_setOf_im_le 📋 Mathlib.Analysis.Complex.ReImTopology
  (a : ℝ) : frontier {z | z.im ≤ a} = {z | z.im = a}
• Complex.frontier_setOf_im_lt 📋 Mathlib.Analysis.Complex.ReImTopology
  (a : ℝ) : frontier {z | z.im < a} = {z | z.im = a}
• Complex.frontier_setOf_le_im 📋 Mathlib.Analysis.Complex.ReImTopology
  (a : ℝ) : frontier {z | a ≤ z.im} = {z | z.im = a}
• Complex.frontier_setOf_le_re 📋 Mathlib.Analysis.Complex.ReImTopology
  (a : ℝ) : frontier {z | a ≤ z.re} = {z | z.re = a}
• Complex.frontier_setOf_lt_im 📋 Mathlib.Analysis.Complex.ReImTopology
  (a : ℝ) : frontier {z | a < z.im} = {z | z.im = a}
• Complex.frontier_setOf_lt_re 📋 Mathlib.Analysis.Complex.ReImTopology
  (a : ℝ) : frontier {z | a < z.re} = {z | z.re = a}
• Complex.frontier_setOf_re_le 📋 Mathlib.Analysis.Complex.ReImTopology
  (a : ℝ) : frontier {z | z.re ≤ a} = {z | z.re = a}
• Complex.frontier_setOf_re_lt 📋 Mathlib.Analysis.Complex.ReImTopology
  (a : ℝ) : frontier {z | z.re < a} = {z | z.re = a}
• Complex.frontier_preimage_im 📋 Mathlib.Analysis.Complex.ReImTopology
  (s : Set ℝ) : frontier (Complex.im ⁻¹' s) = Complex.im ⁻¹' frontier s
• Complex.frontier_preimage_re 📋 Mathlib.Analysis.Complex.ReImTopology
  (s : Set ℝ) : frontier (Complex.re ⁻¹' s) = Complex.re ⁻¹' frontier s
• Complex.frontier_reProdIm 📋 Mathlib.Analysis.Complex.ReImTopology
  (s t : Set ℝ) : frontier (s ×ℂ t) = closure s ×ℂ frontier t ∪ frontier s ×ℂ closure t
• Complex.frontier_setOfPred_le_re_and_im_le 📋 Mathlib.Analysis.Complex.ReImTopology
  (a b : ℝ) : frontier {z | a ≤ z.re ∧ z.im ≤ b} = {z | a ≤ z.re ∧ z.im = b ∨ z.re = a ∧ z.im ≤ b}
• Complex.frontier_setOfPred_le_re_and_le_im 📋 Mathlib.Analysis.Complex.ReImTopology
  (a b : ℝ) : frontier {z | a ≤ z.re ∧ b ≤ z.im} = {z | a ≤ z.re ∧ z.im = b ∨ z.re = a ∧ b ≤ z.im}
• Complex.frontier_setOf_le_re_and_im_le 📋 Mathlib.Analysis.Complex.ReImTopology
  (a b : ℝ) : frontier {z | a ≤ z.re ∧ z.im ≤ b} = {z | a ≤ z.re ∧ z.im = b ∨ z.re = a ∧ z.im ≤ b}
• Complex.frontier_setOf_le_re_and_le_im 📋 Mathlib.Analysis.Complex.ReImTopology
  (a b : ℝ) : frontier {z | a ≤ z.re ∧ b ≤ z.im} = {z | a ≤ z.re ∧ z.im = b ∨ z.re = a ∧ b ≤ z.im}
• OpenPartialHomeomorph.IsImage.frontier 📋 Mathlib.Topology.OpenPartialHomeomorph.IsImage
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) : e.IsImage (frontier s) (frontier t)
• OpenPartialHomeomorph.preimage_frontier 📋 Mathlib.Topology.OpenPartialHomeomorph.IsImage
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set Y) : e.source ∩ ↑e ⁻¹' frontier s = e.source ∩ frontier (↑e ⁻¹' s)
• IsUltrametricDist.frontier_ball_eq_empty 📋 Mathlib.Topology.MetricSpace.Ultra.Basic
  {X : Type u_1} [PseudoMetricSpace X] [IsUltrametricDist X] (x : X) (r : ℝ) : frontier (Metric.ball x r) = ∅
• IsUltrametricDist.frontier_closedBall_eq_empty 📋 Mathlib.Topology.MetricSpace.Ultra.Basic
  {X : Type u_1} [PseudoMetricSpace X] [IsUltrametricDist X] (x : X) {r : ℝ} (hr : r ≠ 0) : frontier (Metric.closedBall x r) = ∅
• Subalgebra.frontier_spectrum 📋 Mathlib.Analysis.Normed.Algebra.Spectrum
  {𝕜 : Type u_3} {A : Type u_4} {SA : Type u_5} [NormedRing A] [CompleteSpace A] [SetLike SA A] [SubringClass SA A] [NormedField 𝕜] [NormedAlgebra 𝕜 A] [instSMulMem : SMulMemClass SA 𝕜 A] (S : SA) [hS : IsClosed ↑S] (x : ↥S) : frontier (spectrum 𝕜 x) ⊆ spectrum 𝕜 ↑x
• Subalgebra.frontier_subset_frontier 📋 Mathlib.Analysis.Normed.Algebra.Spectrum
  {𝕜 : Type u_3} {A : Type u_4} {SA : Type u_5} [NormedRing A] [CompleteSpace A] [SetLike SA A] [SubringClass SA A] [NormedField 𝕜] [NormedAlgebra 𝕜 A] [instSMulMem : SMulMemClass SA 𝕜 A] (S : SA) [hS : IsClosed ↑S] (x : ↥S) : frontier (spectrum 𝕜 x) ⊆ frontier (spectrum 𝕜 ↑x)
• OpenPartialHomeomorph.piecewise 📋 Mathlib.Topology.OpenPartialHomeomorph.Constructions
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e e' : OpenPartialHomeomorph X Y) (s : Set X) (t : Set Y) [(x : X) → Decidable (x ∈ s)] [(y : Y) → Decidable (y ∈ t)] (H : e.IsImage s t) (H' : e'.IsImage s t) (Hs : e.source ∩ frontier s = e'.source ∩ frontier s) (Heq : Set.EqOn (↑e) (↑e') (e.source ∩ frontier s)) : OpenPartialHomeomorph X Y
• OpenPartialHomeomorph.piecewise_apply 📋 Mathlib.Topology.OpenPartialHomeomorph.Constructions
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e e' : OpenPartialHomeomorph X Y) (s : Set X) (t : Set Y) [(x : X) → Decidable (x ∈ s)] [(y : Y) → Decidable (y ∈ t)] (H : e.IsImage s t) (H' : e'.IsImage s t) (Hs : e.source ∩ frontier s = e'.source ∩ frontier s) (Heq : Set.EqOn (↑e) (↑e') (e.source ∩ frontier s)) : ↑(e.piecewise e' s t H H' Hs Heq) = s.piecewise ↑e ↑e'
• OpenPartialHomeomorph.piecewise_toPartialHomeomorph 📋 Mathlib.Topology.OpenPartialHomeomorph.Constructions
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e e' : OpenPartialHomeomorph X Y) (s : Set X) (t : Set Y) [(x : X) → Decidable (x ∈ s)] [(y : Y) → Decidable (y ∈ t)] (H : e.IsImage s t) (H' : e'.IsImage s t) (Hs : e.source ∩ frontier s = e'.source ∩ frontier s) (Heq : Set.EqOn (↑e) (↑e') (e.source ∩ frontier s)) : (e.piecewise e' s t H H' Hs Heq).toPartialHomeomorph = { toPartialEquiv := e.piecewise e'.toPartialEquiv s t H H', continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ }
• OpenPartialHomeomorph.symm_piecewise 📋 Mathlib.Topology.OpenPartialHomeomorph.Constructions
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e e' : OpenPartialHomeomorph X Y) {s : Set X} {t : Set Y} [(x : X) → Decidable (x ∈ s)] [(y : Y) → Decidable (y ∈ t)] (H : e.IsImage s t) (H' : e'.IsImage s t) (Hs : e.source ∩ frontier s = e'.source ∩ frontier s) (Heq : Set.EqOn (↑e) (↑e') (e.source ∩ frontier s)) : (e.piecewise e' s t H H' Hs Heq).symm = e.symm.piecewise e'.symm t s ⋯ ⋯ ⋯ ⋯
• Bundle.Trivialization.frontier_preimage 📋 Mathlib.Topology.FiberBundle.Trivialization
  {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Bundle.Trivialization F proj) (s : Set B) : e.source ∩ frontier (proj ⁻¹' s) = proj ⁻¹' (e.baseSet ∩ frontier s)
• Bundle.Trivialization.piecewise 📋 Mathlib.Topology.FiberBundle.Trivialization
  {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e e' : Bundle.Trivialization F proj) (s : Set B) (Hs : e.baseSet ∩ frontier s = e'.baseSet ∩ frontier s) (Heq : Set.EqOn (↑e) (↑e') (proj ⁻¹' (e.baseSet ∩ frontier s))) : Bundle.Trivialization F proj
• ContMDiff.piecewise 📋 Mathlib.Geometry.Manifold.ContMDiff.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H M] [ChartedSpace H' M'] {n : WithTop ℕ∞} {f g : M → M'} {s : Set M} [DecidablePred fun x => x ∈ s] (hf : ContMDiff I I' n f) (hg : ContMDiff I I' n g) (hfg : ∀ x ∈ frontier s, f =ᶠ[nhds x] g) : ContMDiff I I' n (s.piecewise f g)
• Complex.eqOn_of_eqOn_frontier 📋 Mathlib.Analysis.Complex.AbsMax
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℂ F] [Nontrivial E] {f g : E → F} {U : Set E} (hU : Bornology.IsBounded U) (hf : DiffContOnCl ℂ f U) (hg : DiffContOnCl ℂ g U) (hfg : Set.EqOn f g (frontier U)) : Set.EqOn f g U
• Complex.eqOn_closure_of_eqOn_frontier 📋 Mathlib.Analysis.Complex.AbsMax
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℂ F] [Nontrivial E] {f g : E → F} {U : Set E} (hU : Bornology.IsBounded U) (hf : DiffContOnCl ℂ f U) (hg : DiffContOnCl ℂ g U) (hfg : Set.EqOn f g (frontier U)) : Set.EqOn f g (closure U)
• Complex.norm_le_of_forall_mem_frontier_norm_le 📋 Mathlib.Analysis.Complex.AbsMax
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℂ F] [Nontrivial E] {f : E → F} {U : Set E} (hU : Bornology.IsBounded U) (hd : DiffContOnCl ℂ f U) {C : ℝ} (hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C) {z : E} (hz : z ∈ closure U) : ‖f z‖ ≤ C
• Complex.exists_mem_frontier_isMaxOn_norm 📋 Mathlib.Analysis.Complex.AbsMax
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℂ F] [Nontrivial E] [FiniteDimensional ℂ E] {f : E → F} {U : Set E} (hb : Bornology.IsBounded U) (hne : U.Nonempty) (hd : DiffContOnCl ℂ f U) : ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure U) z
• intrinsicFrontier_subset_frontier 📋 Mathlib.Analysis.Convex.Intrinsic
  {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] {s : Set P} : intrinsicFrontier 𝕜 s ⊆ frontier s
• mem_intrinsicFrontier 📋 Mathlib.Analysis.Convex.Intrinsic
  {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] {s : Set P} {x : P} : x ∈ intrinsicFrontier 𝕜 s ↔ ∃ y ∈ frontier (Subtype.val ⁻¹' s), ↑y = x
• exists_homeomorph_image_eq 📋 Mathlib.Analysis.Convex.GaugeRescale
  {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [T1Space E] {s t : Set E} (hsc : Convex ℝ s) (hsne : (interior s).Nonempty) (hsb : Bornology.IsVonNBounded ℝ s) (hst : Convex ℝ t) (htne : (interior t).Nonempty) (htb : Bornology.IsVonNBounded ℝ t) : ∃ e, ⇑e '' interior s = interior t ∧ ⇑e '' closure s = closure t ∧ ⇑e '' frontier s = frontier t
• exists_homeomorph_image_interior_closure_frontier_eq_unitBall 📋 Mathlib.Analysis.Convex.GaugeRescale
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} (hc : Convex ℝ s) (hne : (interior s).Nonempty) (hb : Bornology.IsBounded s) : ∃ h, ⇑h '' interior s = Metric.ball 0 1 ∧ ⇑h '' closure s = Metric.closedBall 0 1 ∧ ⇑h '' frontier s = Metric.sphere 0 1
• Convex.addHaar_frontier 📋 Mathlib.Analysis.Convex.Measure
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {s : Set E} (hs : Convex ℝ s) : μ (frontier s) = 0
• threeAPFree_frontier 📋 Mathlib.Combinatorics.Additive.AP.Three.Behrend
  {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace E] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (hs₀ : IsClosed s) (hs₁ : StrictConvex 𝕜 s) : ThreeAPFree (frontier s)
• ModelWithCorners.isBoundaryPoint_iff 📋 Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {x : M} : I.IsBoundaryPoint x ↔ ↑(extChartAt I x) x ∈ frontier (Set.range ↑I)
• ModelWithCorners.isBoundaryPoint_iff_of_mem_atlas 📋 Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} [IsManifold I n M] {e : OpenPartialHomeomorph M H} {x : M} (hn : n ≠ 0) (he : e ∈ atlas H M) (hx : x ∈ e.source) : I.IsBoundaryPoint x ↔ ↑(e.extend I) x ∈ frontier (e.extend I).target
• frontier_halfSpace 📋 Mathlib.Geometry.Manifold.Instances.Real
  {n : ℕ} (p : ENNReal) (a : ℝ) (i : Fin n) : frontier {y | a ≤ y.ofLp i} = {y | a = y.ofLp i}
• frontier_range_modelWithCornersEuclideanHalfSpace 📋 Mathlib.Geometry.Manifold.Instances.Real
  (n : ℕ) [NeZero n] : frontier (Set.range ↑(modelWithCornersEuclideanHalfSpace n)) = {y | 0 = y.ofLp 0}
• IccLeftChart_extend_bot_mem_frontier 📋 Mathlib.Geometry.Manifold.Instances.Real
  {x y : ℝ} [hxy : Fact (x < y)] : ↑((IccLeftChart x y).extend (modelWithCornersEuclideanHalfSpace 1)) ⊥ ∈ frontier (Set.range ↑(modelWithCornersEuclideanHalfSpace 1))
• IccRightChart_extend_top_mem_frontier 📋 Mathlib.Geometry.Manifold.Instances.Real
  {x y : ℝ} [hxy : Fact (x < y)] : ↑((IccRightChart x y).extend (modelWithCornersEuclideanHalfSpace 1)) ⊤ ∈ frontier (Set.range ↑(modelWithCornersEuclideanHalfSpace 1))
• MeasureTheory.exists_null_frontier_thickening 📋 Mathlib.MeasureTheory.Measure.Portmanteau
  {Ω : Type u_1} [PseudoMetricSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.SFinite μ] (s : Set Ω) {a b : ℝ} (hab : a < b) : ∃ r ∈ Set.Ioo a b, μ (frontier (Metric.thickening r s)) = 0
• MeasureTheory.exists_null_frontiers_thickening 📋 Mathlib.MeasureTheory.Measure.Portmanteau
  {Ω : Type u_1} [PseudoMetricSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.SFinite μ] (s : Set Ω) : ∃ rs, Filter.Tendsto rs Filter.atTop (nhds 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) s)) = 0
• MeasureTheory.ProbabilityMeasure.tendsto_measure_of_null_frontier_of_tendsto 📋 Mathlib.MeasureTheory.Measure.Portmanteau
  {Ω : Type u_1} {ι : Type u_2} {L : Filter ι} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] [HasOuterApproxClosed Ω] {μ : MeasureTheory.ProbabilityMeasure Ω} {μs : ι → MeasureTheory.ProbabilityMeasure Ω} (μs_lim : Filter.Tendsto μs L (nhds μ)) {E : Set Ω} (E_nullbdry : μ (frontier E) = 0) : Filter.Tendsto (fun i => (μs i) E) L (nhds (μ E))
• MeasureTheory.ProbabilityMeasure.tendsto_measure_of_null_frontier_of_tendsto' 📋 Mathlib.MeasureTheory.Measure.Portmanteau
  {Ω : Type u_1} {ι : Type u_2} {L : Filter ι} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] [HasOuterApproxClosed Ω] {μ : MeasureTheory.ProbabilityMeasure Ω} {μs : ι → MeasureTheory.ProbabilityMeasure Ω} (μs_lim : Filter.Tendsto μs L (nhds μ)) {E : Set Ω} (E_nullbdry : ↑μ (frontier E) = 0) : Filter.Tendsto (fun i => ↑(μs i) E) L (nhds (↑μ E))
• MeasureTheory.tendsto_measure_of_null_frontier 📋 Mathlib.MeasureTheory.Measure.Portmanteau
  {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {ι : Type u_2} {L : Filter ι} {μ : MeasureTheory.Measure Ω} {μs : ι → MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)] (h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ Filter.liminf (fun i => (μs i) G) L) {E : Set Ω} (E_nullbdry : μ (frontier E) = 0) : Filter.Tendsto (fun i => (μs i) E) L (nhds (μ E))
• MeasureTheory.limsup_measure_closed_le_of_forall_tendsto_measure 📋 Mathlib.MeasureTheory.Measure.Portmanteau
  {Ω : Type u_1} {ι : Type u_2} {L : Filter ι} [MeasurableSpace Ω] [TopologicalSpace Ω] [TopologicalSpace.PseudoMetrizableSpace Ω] [OpensMeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {μs : ι → MeasureTheory.Measure Ω} (h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Filter.Tendsto (fun i => (μs i) E) L (nhds (μ E))) (F : Set Ω) (F_closed : IsClosed F) : Filter.limsup (fun i => (μs i) F) L ≤ μ F
• MeasureTheory.le_liminf_measure_open_of_forall_tendsto_measure 📋 Mathlib.MeasureTheory.Measure.Portmanteau
  {Ω : Type u_1} {ι : Type u_2} {L : Filter ι} [MeasurableSpace Ω] [TopologicalSpace Ω] [TopologicalSpace.PseudoMetrizableSpace Ω] [OpensMeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {μs : ι → MeasureTheory.Measure Ω} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)] (h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Filter.Tendsto (fun i => (μs i) E) L (nhds (μ E))) (G : Set Ω) (G_open : IsOpen G) : μ G ≤ Filter.liminf (fun i => (μs i) G) L
• IsLowerSet.null_frontier 📋 Mathlib.MeasureTheory.Order.UpperLower
  {ι : Type u_1} [Fintype ι] {s : Set (ι → ℝ)} (hs : IsLowerSet s) : MeasureTheory.volume (frontier s) = 0
• IsUpperSet.null_frontier 📋 Mathlib.MeasureTheory.Order.UpperLower
  {ι : Type u_1} [Fintype ι] {s : Set (ι → ℝ)} (hs : IsUpperSet s) : MeasureTheory.volume (frontier s) = 0
• Set.OrdConnected.null_frontier 📋 Mathlib.MeasureTheory.Order.UpperLower
  {ι : Type u_1} [Fintype ι] {s : Set (ι → ℝ)} (hs : s.OrdConnected) : MeasureTheory.volume (frontier s) = 0
• NumberField.mixedEmbedding.fundamentalCone.volume_frontier_normLeOne 📋 Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
  (K : Type u_1) [Field K] [NumberField K] : MeasureTheory.volume (frontier (NumberField.mixedEmbedding.fundamentalCone.normLeOne K)) = 0
• PredOrder.isPredLimit_of_mem_frontier 📋 Mathlib.Topology.Order.SuccPred
  {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [PredOrder α] [NoMinOrder α] {a : α} {s : Set α} (ha : a ∈ frontier s) : Order.IsPredLimit a
• SuccOrder.isSuccLimit_of_mem_frontier 📋 Mathlib.Topology.Order.SuccPred
  {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [SuccOrder α] [NoMaxOrder α] {a : α} {s : Set α} (ha : a ∈ frontier s) : Order.IsSuccLimit a
• HasSmallInductiveDimensionLT.succ 📋 Mathlib.Topology.SmallInductiveDimension
  {X : Type u} [TopologicalSpace X] (n : ℕ) (s : Set (Set X)) (hs : TopologicalSpace.IsTopologicalBasis s) (h : ∀ U ∈ s, HasSmallInductiveDimensionLT (↑(frontier U)) n) : HasSmallInductiveDimensionLT X (n + 1)

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 69fae59