Loogle!

Result

Found 102 declarations mentioning NormalSpace.

NormalSpace 📋 Mathlib.Topology.Separation.Regular
(X : Type u) [TopologicalSpace X] : Prop
CompletelyNormalSpace.toNormalSpace 📋 Mathlib.Topology.Separation.Regular
{X : Type u_1} [TopologicalSpace X] [CompletelyNormalSpace X] : NormalSpace X
T4Space.toNormalSpace 📋 Mathlib.Topology.Separation.Regular
{X : Type u} {inst✝ : TopologicalSpace X} [self : T4Space X] : NormalSpace X
instT4SpaceOfT1SpaceOfNormalSpace 📋 Mathlib.Topology.Separation.Regular
{X : Type u_1} [TopologicalSpace X] [T1Space X] [NormalSpace X] : T4Space X
NormalSpace.of_compactSpace_r1Space 📋 Mathlib.Topology.Separation.Regular
{X : Type u_1} [TopologicalSpace X] [CompactSpace X] [R1Space X] : NormalSpace X
NormalSpace.of_regularSpace_lindelofSpace 📋 Mathlib.Topology.Separation.Regular
{X : Type u_1} [TopologicalSpace X] [RegularSpace X] [LindelofSpace X] : NormalSpace X
NormalSpace.of_regularSpace_secondCountableTopology 📋 Mathlib.Topology.Separation.Regular
{X : Type u_1} [TopologicalSpace X] [RegularSpace X] [SecondCountableTopology X] : NormalSpace X
T4Space.mk 📋 Mathlib.Topology.Separation.Regular
{X : Type u} [TopologicalSpace X] [toT1Space : T1Space X] [toNormalSpace : NormalSpace X] : T4Space X
SeparationQuotient.instNormalSpace 📋 Mathlib.Topology.Separation.Regular
{X : Type u_1} [TopologicalSpace X] [NormalSpace X] : NormalSpace (SeparationQuotient X)
Homeomorph.normalSpace 📋 Mathlib.Topology.Separation.Regular
{X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [NormalSpace X] (h : X ≃ₜ Y) : NormalSpace Y
Topology.IsClosedEmbedding.normalSpace 📋 Mathlib.Topology.Separation.Regular
{X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [NormalSpace Y] {f : X → Y} (hf : Topology.IsClosedEmbedding f) : NormalSpace X
CompletelyNormalSpace.of_forall_normalSpace 📋 Mathlib.Topology.Separation.Regular
{X : Type u_1} [TopologicalSpace X] : (∀ (s : Set X), NormalSpace ↑s) → CompletelyNormalSpace X
completelyNormalSpace_iff_forall_normalSpace 📋 Mathlib.Topology.Separation.Regular
{X : Type u_1} [TopologicalSpace X] : CompletelyNormalSpace X ↔ ∀ (s : Set X), NormalSpace ↑s
CompletelyNormalSpace.of_forall_isOpen_normalSpace 📋 Mathlib.Topology.Separation.Regular
{X : Type u_1} [TopologicalSpace X] : (∀ (s : Set X), IsOpen s → NormalSpace ↑s) → CompletelyNormalSpace X
completelyNormalSpace_iff_forall_isOpen_normalSpace 📋 Mathlib.Topology.Separation.Regular
{X : Type u_1} [TopologicalSpace X] : CompletelyNormalSpace X ↔ ∀ (s : Set X), IsOpen s → NormalSpace ↑s
lift'_nhdsSet_closure 📋 Mathlib.Topology.Separation.Regular
{X : Type u_1} [TopologicalSpace X] [NormalSpace X] (u : Set X) (hu : IsClosed u) : (nhdsSet u).lift' closure = nhdsSet u
hasBasis_nhdsSet_closure 📋 Mathlib.Topology.Separation.Regular
{X : Type u_1} [TopologicalSpace X] [NormalSpace X] (u : Set X) (hu : IsClosed u) : (nhdsSet u).HasBasis (fun s => s ∈ nhdsSet u) closure
Filter.HasBasis.nhdsSet_closure 📋 Mathlib.Topology.Separation.Regular
{X : Type u_1} [TopologicalSpace X] [NormalSpace X] {ι : Sort u_3} {u : Set X} {p : ι → Prop} {s : ι → Set X} (hu : IsClosed u) (h : (nhdsSet u).HasBasis p s) : (nhdsSet u).HasBasis p fun i => closure (s i)
closed_nhdsSet_basis 📋 Mathlib.Topology.Separation.Regular
{X : Type u_1} [TopologicalSpace X] [NormalSpace X] (u : Set X) (hu : IsClosed u) : (nhdsSet u).HasBasis (fun s => s ∈ nhdsSet u ∧ IsClosed s) id
normal_exists_closure_subset 📋 Mathlib.Topology.Separation.Regular
{X : Type u_1} [TopologicalSpace X] [NormalSpace X] {s t : Set X} (hs : IsClosed s) (ht : IsOpen t) (hst : s ⊆ t) : ∃ u, IsOpen u ∧ s ⊆ u ∧ closure u ⊆ t
exists_mem_nhdsSet_isClosed_subset 📋 Mathlib.Topology.Separation.Regular
{X : Type u_1} [TopologicalSpace X] [NormalSpace X] {u s : Set X} (h : s ∈ nhdsSet u) (hu : IsClosed u) : ∃ t ∈ nhdsSet u, IsClosed t ∧ t ⊆ s
normal_separation 📋 Mathlib.Topology.Separation.Regular
{X : Type u_1} [TopologicalSpace X] [NormalSpace X] {s t : Set X} (H1 : IsClosed s) (H2 : IsClosed t) (H3 : Disjoint s t) : SeparatedNhds s t
NormalSpace.mk 📋 Mathlib.Topology.Separation.Regular
{X : Type u} [TopologicalSpace X] (normal : ∀ (s t : Set X), IsClosed s → IsClosed t → Disjoint s t → SeparatedNhds s t) : NormalSpace X
NormalSpace.normal 📋 Mathlib.Topology.Separation.Regular
{X : Type u} {inst✝ : TopologicalSpace X} [self : NormalSpace X] (s t : Set X) : IsClosed s → IsClosed t → Disjoint s t → SeparatedNhds s t
disjoint_nhdsSet_nhdsSet 📋 Mathlib.Topology.Separation.Regular
{X : Type u_1} [TopologicalSpace X] [NormalSpace X] {s t : Set X} (hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) : Disjoint (nhdsSet s) (nhdsSet t)
PerfectlyNormalSpace.toNormalSpace 📋 Mathlib.Topology.Separation.GDelta
{X : Type u} {inst✝ : TopologicalSpace X} [self : PerfectlyNormalSpace X] : NormalSpace X
PerfectlyNormalSpace.mk 📋 Mathlib.Topology.Separation.GDelta
{X : Type u} [TopologicalSpace X] [toNormalSpace : NormalSpace X] (closed_gdelta : ∀ ⦃h : Set X⦄, IsClosed h → IsGδ h) : PerfectlyNormalSpace X
Disjoint.hasSeparatingCover_closed_gdelta_right 📋 Mathlib.Topology.Separation.GDelta
{X : Type u_1} [TopologicalSpace X] {s t : Set X} [NormalSpace X] (st_dis : Disjoint s t) (t_cl : IsClosed t) (t_gd : IsGδ t) : HasSeparatingCover s t
instNormalSpaceOfPseudoMetrizableSpace 📋 Mathlib.Topology.GDelta.MetrizableSpace
{X : Type u_1} [TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X] : NormalSpace X
exists_continuous_zero_one_of_isClosed 📋 Mathlib.Topology.UrysohnsLemma
{X : Type u_1} [TopologicalSpace X] [NormalSpace X] {s t : Set X} (hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) : ∃ f, Set.EqOn (⇑f) 0 s ∧ Set.EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Set.Icc 0 1
NormalSpace.of_paracompactSpace_r1Space 📋 Mathlib.Topology.Compactness.Paracompact
{X : Type v} [TopologicalSpace X] [R1Space X] [ParacompactSpace X] : NormalSpace X
exists_iUnion_eq_closed_subset 📋 Mathlib.Topology.ShrinkingLemma
{ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {u : ι → Set X} [NormalSpace X] (uo : ∀ (i : ι), IsOpen (u i)) (uf : ∀ (x : X), {i | x ∈ u i}.Finite) (uU : ⋃ i, u i = Set.univ) : ∃ v, Set.iUnion v = Set.univ ∧ (∀ (i : ι), IsClosed (v i)) ∧ ∀ (i : ι), v i ⊆ u i
exists_iUnion_eq_closure_subset 📋 Mathlib.Topology.ShrinkingLemma
{ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {u : ι → Set X} [NormalSpace X] (uo : ∀ (i : ι), IsOpen (u i)) (uf : ∀ (x : X), {i | x ∈ u i}.Finite) (uU : ⋃ i, u i = Set.univ) : ∃ v, Set.iUnion v = Set.univ ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i
exists_subset_iUnion_closed_subset 📋 Mathlib.Topology.ShrinkingLemma
{ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {u : ι → Set X} {s : Set X} [NormalSpace X] (hs : IsClosed s) (uo : ∀ (i : ι), IsOpen (u i)) (uf : ∀ x ∈ s, {i | x ∈ u i}.Finite) (us : s ⊆ ⋃ i, u i) : ∃ v, s ⊆ Set.iUnion v ∧ (∀ (i : ι), IsClosed (v i)) ∧ ∀ (i : ι), v i ⊆ u i
exists_subset_iUnion_closure_subset 📋 Mathlib.Topology.ShrinkingLemma
{ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {u : ι → Set X} {s : Set X} [NormalSpace X] (hs : IsClosed s) (uo : ∀ (i : ι), IsOpen (u i)) (uf : ∀ x ∈ s, {i | x ∈ u i}.Finite) (us : s ⊆ ⋃ i, u i) : ∃ v, s ⊆ Set.iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i
ShrinkingLemma.PartialRefinement.exists_gt 📋 Mathlib.Topology.ShrinkingLemma
{ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {u : ι → Set X} {s : Set X} [NormalSpace X] (v : ShrinkingLemma.PartialRefinement u s ⊤) (hs : IsClosed s) (i : ι) (hi : i ∉ v.carrier) : ∃ v', v < v'
BumpCovering.exists_isSubordinate 📋 Mathlib.Topology.PartitionOfUnity
{ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} [NormalSpace X] [ParacompactSpace X] (hs : IsClosed s) (U : ι → Set X) (ho : ∀ (i : ι), IsOpen (U i)) (hU : s ⊆ ⋃ i, U i) : ∃ f, f.IsSubordinate U
PartitionOfUnity.exists_isSubordinate 📋 Mathlib.Topology.PartitionOfUnity
{ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} [NormalSpace X] [ParacompactSpace X] (hs : IsClosed s) (U : ι → Set X) (ho : ∀ (i : ι), IsOpen (U i)) (hU : s ⊆ ⋃ i, U i) : ∃ f, f.IsSubordinate U
BumpCovering.exists_isSubordinate_of_locallyFinite 📋 Mathlib.Topology.PartitionOfUnity
{ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} [NormalSpace X] (hs : IsClosed s) (U : ι → Set X) (ho : ∀ (i : ι), IsOpen (U i)) (hf : LocallyFinite U) (hU : s ⊆ ⋃ i, U i) : ∃ f, f.IsSubordinate U
PartitionOfUnity.exists_isSubordinate_of_locallyFinite 📋 Mathlib.Topology.PartitionOfUnity
{ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} [NormalSpace X] (hs : IsClosed s) (U : ι → Set X) (ho : ∀ (i : ι), IsOpen (U i)) (hf : LocallyFinite U) (hU : s ⊆ ⋃ i, U i) : ∃ f, f.IsSubordinate U
BumpCovering.exists_isSubordinate_of_prop 📋 Mathlib.Topology.PartitionOfUnity
{ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} [NormalSpace X] [ParacompactSpace X] (p : (X → ℝ) → Prop) (h01 : ∀ (s t : Set X), IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ⇑f ∧ Set.EqOn (⇑f) 0 s ∧ Set.EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Set.Icc 0 1) (hs : IsClosed s) (U : ι → Set X) (ho : ∀ (i : ι), IsOpen (U i)) (hU : s ⊆ ⋃ i, U i) : ∃ f, (∀ (i : ι), p ⇑(f i)) ∧ f.IsSubordinate U
BumpCovering.exists_isSubordinate_of_locallyFinite_of_prop 📋 Mathlib.Topology.PartitionOfUnity
{ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} [NormalSpace X] (p : (X → ℝ) → Prop) (h01 : ∀ (s t : Set X), IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ⇑f ∧ Set.EqOn (⇑f) 0 s ∧ Set.EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Set.Icc 0 1) (hs : IsClosed s) (U : ι → Set X) (ho : ∀ (i : ι), IsOpen (U i)) (hf : LocallyFinite U) (hU : s ⊆ ⋃ i, U i) : ∃ f, (∀ (i : ι), p ⇑(f i)) ∧ f.IsSubordinate U
exists_continuous_forall_mem_convex_of_local_const 📋 Mathlib.Analysis.Convex.PartitionOfUnity
{X : Type u_2} {E : Type u_3} [TopologicalSpace X] [AddCommGroup E] [Module ℝ E] [NormalSpace X] [ParacompactSpace X] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] {t : X → Set E} (ht : ∀ (x : X), Convex ℝ (t x)) (H : ∀ (x : X), ∃ c, ∀ᶠ (y : X) in nhds x, c ∈ t y) : ∃ g, ∀ (x : X), g x ∈ t x
exists_continuous_forall_mem_convex_of_local 📋 Mathlib.Analysis.Convex.PartitionOfUnity
{X : Type u_2} {E : Type u_3} [TopologicalSpace X] [AddCommGroup E] [Module ℝ E] [NormalSpace X] [ParacompactSpace X] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] {t : X → Set E} (ht : ∀ (x : X), Convex ℝ (t x)) (H : ∀ (x : X), ∃ U ∈ nhds x, ∃ g, ContinuousOn g U ∧ ∀ y ∈ U, g y ∈ t y) : ∃ g, ∀ (x : X), g x ∈ t x
exists_contMDiffMap_one_nhds_of_subset_interior 📋 Mathlib.Geometry.Manifold.PartitionOfUnity
{E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [IsManifold I (↑⊤) M] {n : ℕ∞} [T2Space M] [NormalSpace M] [SigmaCompactSpace M] {s t : Set M} (hs : IsClosed s) (hd : s ⊆ interior t) : ∃ f, (∀ᶠ (x : M) in nhdsSet s, f x = 1) ∧ (∀ x ∉ t, f x = 0) ∧ ∀ (x : M), f x ∈ Set.Icc 0 1
exists_contMDiffMap_zero_one_nhds_of_isClosed 📋 Mathlib.Geometry.Manifold.PartitionOfUnity
{E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [IsManifold I (↑⊤) M] {n : ℕ∞} [T2Space M] [NormalSpace M] [SigmaCompactSpace M] {s t : Set M} (hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) : ∃ f, (∀ᶠ (x : M) in nhdsSet s, f x = 0) ∧ (∀ᶠ (x : M) in nhdsSet t, f x = 1) ∧ ∀ (x : M), f x ∈ Set.Icc 0 1
exists_bounded_mem_Icc_of_closed_of_le 📋 Mathlib.Topology.UrysohnsBounded
{X : Type u_1} [TopologicalSpace X] [NormalSpace X] {s t : Set X} (hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) {a b : ℝ} (hle : a ≤ b) : ∃ f, Set.EqOn (⇑f) (Function.const X a) s ∧ Set.EqOn (⇑f) (Function.const X b) t ∧ ∀ (x : X), f x ∈ Set.Icc a b
exists_bounded_zero_one_of_closed 📋 Mathlib.Topology.UrysohnsBounded
{X : Type u_1} [TopologicalSpace X] [NormalSpace X] {s t : Set X} (hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) : ∃ f, Set.EqOn (⇑f) 0 s ∧ Set.EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Set.Icc 0 1
ContinuousMap.exists_extension 📋 Mathlib.Topology.TietzeExtension
{X₁ : Type u₁} [TopologicalSpace X₁] {X : Type u} [TopologicalSpace X] [NormalSpace X] {e : X₁ → X} {Y : Type v} [TopologicalSpace Y] [TietzeExtension Y] (he : Topology.IsClosedEmbedding e) (f : C(X₁, Y)) : ∃ g, g.comp { toFun := e, continuous_toFun := ⋯ } = f
ContinuousMap.exists_restrict_eq 📋 Mathlib.Topology.TietzeExtension
{X : Type u} [TopologicalSpace X] [NormalSpace X] {s : Set X} {Y : Type v} [TopologicalSpace Y] [TietzeExtension Y] (hs : IsClosed s) (f : C(↑s, Y)) : ∃ g, ContinuousMap.restrict s g = f
TietzeExtension.exists_restrict_eq' 📋 Mathlib.Topology.TietzeExtension
{Y : Type v} {inst✝ : TopologicalSpace Y} [self : TietzeExtension Y] {X : Type u} [TopologicalSpace X] [NormalSpace X] (s : Set X) (hs : IsClosed s) (f : C(↑s, Y)) : ∃ g, ContinuousMap.restrict s g = f
TietzeExtension.mk 📋 Mathlib.Topology.TietzeExtension
{Y : Type v} [TopologicalSpace Y] (exists_restrict_eq' : ∀ {X : Type u} [inst : TopologicalSpace X] [NormalSpace X] (s : Set X), IsClosed s → ∀ (f : C(↑s, Y)), ∃ g, ContinuousMap.restrict s g = f) : TietzeExtension Y
ContinuousMap.exists_extension' 📋 Mathlib.Topology.TietzeExtension
{X₁ : Type u₁} [TopologicalSpace X₁] {X : Type u} [TopologicalSpace X] [NormalSpace X] {e : X₁ → X} {Y : Type v} [TopologicalSpace Y] [TietzeExtension Y] (he : Topology.IsClosedEmbedding e) (f : C(X₁, Y)) : ∃ g, ⇑g ∘ e = ⇑f
BoundedContinuousFunction.exists_extension_norm_eq_of_isClosedEmbedding' 📋 Mathlib.Topology.TietzeExtension
{X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [NormalSpace Y] (f : BoundedContinuousFunction X ℝ) (e : C(X, Y)) (he : Topology.IsClosedEmbedding ⇑e) : ∃ g, ‖g‖ = ‖f‖ ∧ g.compContinuous e = f
BoundedContinuousFunction.exists_extension_norm_eq_of_isClosedEmbedding 📋 Mathlib.Topology.TietzeExtension
{X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [NormalSpace Y] (f : BoundedContinuousFunction X ℝ) {e : X → Y} (he : Topology.IsClosedEmbedding e) : ∃ g, ‖g‖ = ‖f‖ ∧ ⇑g ∘ e = ⇑f
BoundedContinuousFunction.exists_extension_forall_mem_of_isClosedEmbedding 📋 Mathlib.Topology.TietzeExtension
{X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [NormalSpace Y] (f : BoundedContinuousFunction X ℝ) {t : Set ℝ} {e : X → Y} [hs : t.OrdConnected] (hf : ∀ (x : X), f x ∈ t) (hne : t.Nonempty) (he : Topology.IsClosedEmbedding e) : ∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f
ContinuousMap.exists_extension_forall_mem 📋 Mathlib.Topology.TietzeExtension
{X₁ : Type u₁} [TopologicalSpace X₁] {X : Type u} [TopologicalSpace X] [NormalSpace X] {e : X₁ → X} (he : Topology.IsClosedEmbedding e) {Y : Type v} [TopologicalSpace Y] (f : C(X₁, Y)) {t : Set Y} (hf : ∀ (x : X₁), f x ∈ t) [ht : TietzeExtension ↑t] : ∃ g, (∀ (x : X), g x ∈ t) ∧ g.comp { toFun := e, continuous_toFun := ⋯ } = f
BoundedContinuousFunction.exists_extension_forall_mem_Icc_of_isClosedEmbedding 📋 Mathlib.Topology.TietzeExtension
{X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [NormalSpace Y] (f : BoundedContinuousFunction X ℝ) {a b : ℝ} {e : X → Y} (hf : ∀ (x : X), f x ∈ Set.Icc a b) (hle : a ≤ b) (he : Topology.IsClosedEmbedding e) : ∃ g, (∀ (y : Y), g y ∈ Set.Icc a b) ∧ ⇑g ∘ e = ⇑f
BoundedContinuousFunction.exists_norm_eq_domRestrict_eq_of_closed 📋 Mathlib.Topology.TietzeExtension
{Y : Type u_2} [TopologicalSpace Y] [NormalSpace Y] {s : Set Y} (f : BoundedContinuousFunction ↑s ℝ) (hs : IsClosed s) : ∃ g, ‖g‖ = ‖f‖ ∧ g.domRestrict s = f
BoundedContinuousFunction.exists_norm_eq_restrict_eq_of_closed 📋 Mathlib.Topology.TietzeExtension
{Y : Type u_2} [TopologicalSpace Y] [NormalSpace Y] {s : Set Y} (f : BoundedContinuousFunction ↑s ℝ) (hs : IsClosed s) : ∃ g, ‖g‖ = ‖f‖ ∧ g.domRestrict s = f
BoundedContinuousFunction.exists_extension_forall_exists_le_ge_of_isClosedEmbedding 📋 Mathlib.Topology.TietzeExtension
{X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [NormalSpace Y] [Nonempty X] (f : BoundedContinuousFunction X ℝ) {e : X → Y} (he : Topology.IsClosedEmbedding e) : ∃ g, (∀ (y : Y), ∃ x₁ x₂, g y ∈ Set.Icc (f x₁) (f x₂)) ∧ ⇑g ∘ e = ⇑f
BoundedContinuousFunction.exists_forall_mem_domRestrict_eq_of_closed 📋 Mathlib.Topology.TietzeExtension
{Y : Type u_2} [TopologicalSpace Y] [NormalSpace Y] {s : Set Y} (f : BoundedContinuousFunction ↑s ℝ) (hs : IsClosed s) {t : Set ℝ} [t.OrdConnected] (hf : ∀ (x : ↑s), f x ∈ t) (hne : t.Nonempty) : ∃ g, (∀ (y : Y), g y ∈ t) ∧ g.domRestrict s = f
BoundedContinuousFunction.exists_forall_mem_restrict_eq_of_closed 📋 Mathlib.Topology.TietzeExtension
{Y : Type u_2} [TopologicalSpace Y] [NormalSpace Y] {s : Set Y} (f : BoundedContinuousFunction ↑s ℝ) (hs : IsClosed s) {t : Set ℝ} [t.OrdConnected] (hf : ∀ (x : ↑s), f x ∈ t) (hne : t.Nonempty) : ∃ g, (∀ (y : Y), g y ∈ t) ∧ g.domRestrict s = f
ContinuousMap.exists_forall_mem_restrict_eq 📋 Mathlib.Topology.TietzeExtension
{X : Type u} [TopologicalSpace X] [NormalSpace X] {s : Set X} (hs : IsClosed s) {Y : Type v} [TopologicalSpace Y] (f : C(↑s, Y)) {t : Set Y} (hf : ∀ (x : ↑s), f x ∈ t) [ht : TietzeExtension ↑t] : ∃ g, (∀ (x : X), g x ∈ t) ∧ ContinuousMap.restrict s g = f
ContinuousMap.exists_extension_forall_mem_of_isClosedEmbedding 📋 Mathlib.Topology.TietzeExtension
{X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [NormalSpace Y] (f : C(X, ℝ)) {t : Set ℝ} {e : X → Y} [hs : t.OrdConnected] (hf : ∀ (x : X), f x ∈ t) (hne : t.Nonempty) (he : Topology.IsClosedEmbedding e) : ∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f
ContinuousMap.exists_restrict_eq_forall_mem_of_closed 📋 Mathlib.Topology.TietzeExtension
{Y : Type u_2} [TopologicalSpace Y] [NormalSpace Y] {s : Set Y} (f : C(↑s, ℝ)) {t : Set ℝ} [t.OrdConnected] (ht : ∀ (x : ↑s), f x ∈ t) (hne : t.Nonempty) (hs : IsClosed s) : ∃ g, (∀ (y : Y), g y ∈ t) ∧ ContinuousMap.restrict s g = f
BoundedContinuousFunction.tietze_extension_step 📋 Mathlib.Topology.TietzeExtension
{X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [NormalSpace Y] (f : BoundedContinuousFunction X ℝ) (e : C(X, Y)) (he : Topology.IsClosedEmbedding ⇑e) : ∃ g, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖
BoundedContinuousFunction.exists_norm_eq_domRestrict_eq 📋 Mathlib.Analysis.Complex.Tietze
{X : Type u} [TopologicalSpace X] [NormalSpace X] {s : Set X} (hs : IsClosed s) (𝕜 : Type v) [RCLike 𝕜] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] (f : BoundedContinuousFunction (↑s) E) : ∃ g, ‖g‖ = ‖f‖ ∧ g.domRestrict s = f
BoundedContinuousFunction.exists_norm_eq_restrict_eq 📋 Mathlib.Analysis.Complex.Tietze
{X : Type u} [TopologicalSpace X] [NormalSpace X] {s : Set X} (hs : IsClosed s) (𝕜 : Type v) [RCLike 𝕜] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] (f : BoundedContinuousFunction (↑s) E) : ∃ g, ‖g‖ = ‖f‖ ∧ g.domRestrict s = f
OnePoint.instNormalSpaceOfWeaklyLocallyCompactSpaceOfR1Space 📋 Mathlib.Topology.Compactification.OnePoint.Basic
{X : Type u_1} [TopologicalSpace X] [WeaklyLocallyCompactSpace X] [R1Space X] : NormalSpace (OnePoint X)
MeasureTheory.Integrable.exists_hasCompactSupport_integral_sub_le 📋 Mathlib.MeasureTheory.Function.ContinuousMapDense
{α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] {E : Type u_2} [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} [NormedSpace ℝ E] [R1Space α] [WeaklyLocallyCompactSpace α] [μ.Regular] {f : α → E} (hf : MeasureTheory.Integrable f μ) {ε : ℝ} (hε : 0 < ε) : ∃ g, HasCompactSupport g ∧ ∫ (x : α), ‖f x - g x‖ ∂μ ≤ ε ∧ Continuous g ∧ MeasureTheory.Integrable g μ
MeasureTheory.Integrable.exists_hasCompactSupport_lintegral_sub_le 📋 Mathlib.MeasureTheory.Function.ContinuousMapDense
{α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] {E : Type u_2} [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} [NormedSpace ℝ E] [R1Space α] [WeaklyLocallyCompactSpace α] [μ.Regular] {f : α → E} (hf : MeasureTheory.Integrable f μ) {ε : ENNReal} (hε : ε ≠ 0) : ∃ g, HasCompactSupport g ∧ ∫⁻ (x : α), ‖f x - g x‖ₑ ∂μ ≤ ε ∧ Continuous g ∧ MeasureTheory.Integrable g μ
MeasureTheory.Integrable.exists_boundedContinuous_integral_sub_le 📋 Mathlib.MeasureTheory.Function.ContinuousMapDense
{α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] {E : Type u_2} [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} [NormedSpace ℝ E] [μ.WeaklyRegular] {f : α → E} (hf : MeasureTheory.Integrable f μ) {ε : ℝ} (hε : 0 < ε) : ∃ g, ∫ (x : α), ‖f x - g x‖ ∂μ ≤ ε ∧ MeasureTheory.Integrable (⇑g) μ
MeasureTheory.Integrable.exists_boundedContinuous_lintegral_sub_le 📋 Mathlib.MeasureTheory.Function.ContinuousMapDense
{α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] {E : Type u_2} [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} [NormedSpace ℝ E] [μ.WeaklyRegular] {f : α → E} (hf : MeasureTheory.Integrable f μ) {ε : ENNReal} (hε : ε ≠ 0) : ∃ g, ∫⁻ (x : α), ‖f x - g x‖ₑ ∂μ ≤ ε ∧ MeasureTheory.Integrable (⇑g) μ
MeasureTheory.MemLp.exists_hasCompactSupport_integral_rpow_sub_le 📋 Mathlib.MeasureTheory.Function.ContinuousMapDense
{α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] {E : Type u_2} [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} [NormedSpace ℝ E] [R1Space α] [WeaklyLocallyCompactSpace α] [μ.Regular] {p : ℝ} (hp : 0 < p) {f : α → E} (hf : MeasureTheory.MemLp f (ENNReal.ofReal p) μ) {ε : ℝ} (hε : 0 < ε) : ∃ g, HasCompactSupport g ∧ ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε ∧ Continuous g ∧ MeasureTheory.MemLp g (ENNReal.ofReal p) μ
MeasureTheory.MemLp.exists_hasCompactSupport_eLpNorm_sub_le 📋 Mathlib.MeasureTheory.Function.ContinuousMapDense
{α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] {E : Type u_2} [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [NormedSpace ℝ E] [R1Space α] [WeaklyLocallyCompactSpace α] [μ.Regular] (hp : p ≠ ⊤) {f : α → E} (hf : MeasureTheory.MemLp f p μ) {ε : ENNReal} (hε : ε ≠ 0) : ∃ g, HasCompactSupport g ∧ MeasureTheory.eLpNorm (f - g) p μ ≤ ε ∧ Continuous g ∧ MeasureTheory.MemLp g p μ
MeasureTheory.MemLp.exists_boundedContinuous_integral_rpow_sub_le 📋 Mathlib.MeasureTheory.Function.ContinuousMapDense
{α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] {E : Type u_2} [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} [NormedSpace ℝ E] [μ.WeaklyRegular] {p : ℝ} (hp : 0 < p) {f : α → E} (hf : MeasureTheory.MemLp f (ENNReal.ofReal p) μ) {ε : ℝ} (hε : 0 < ε) : ∃ g, ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε ∧ MeasureTheory.MemLp (⇑g) (ENNReal.ofReal p) μ
MeasureTheory.MemLp.exists_boundedContinuous_eLpNorm_sub_le 📋 Mathlib.MeasureTheory.Function.ContinuousMapDense
{α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] {E : Type u_2} [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [NormedSpace ℝ E] [μ.WeaklyRegular] (hp : p ≠ ⊤) {f : α → E} (hf : MeasureTheory.MemLp f p μ) {ε : ENNReal} (hε : ε ≠ 0) : ∃ g, MeasureTheory.eLpNorm (f - ⇑g) p μ ≤ ε ∧ MeasureTheory.MemLp (⇑g) p μ
MeasureTheory.exists_continuous_eLpNorm_sub_le_of_closed 📋 Mathlib.MeasureTheory.Function.ContinuousMapDense
{α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] {E : Type u_2} [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [NormedSpace ℝ E] [μ.OuterRegular] (hp : p ≠ ⊤) {s u : Set α} (s_closed : IsClosed s) (u_open : IsOpen u) (hsu : s ⊆ u) (hs : μ s ≠ ⊤) (c : E) {ε : ENNReal} (hε : ε ≠ 0) : ∃ f, Continuous f ∧ MeasureTheory.eLpNorm (fun x => f x - s.indicator (fun _y => c) x) p μ ≤ ε ∧ (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ MeasureTheory.MemLp f p μ
MeasureTheory.Lp.boundedContinuousFunction_dense 📋 Mathlib.MeasureTheory.Function.ContinuousMapDense
{α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] (E : Type u_2) [NormedAddCommGroup E] (μ : MeasureTheory.Measure α) {p : ENNReal} [NormedSpace ℝ E] [SecondCountableTopologyEither α E] [Fact (1 ≤ p)] (hp : p ≠ ⊤) [μ.WeaklyRegular] : Dense ↑(MeasureTheory.Lp.boundedContinuousFunction E p μ)
MeasureTheory.Lp.boundedContinuousFunction_topologicalClosure 📋 Mathlib.MeasureTheory.Function.ContinuousMapDense
{α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] (E : Type u_2) [NormedAddCommGroup E] (μ : MeasureTheory.Measure α) {p : ENNReal} [NormedSpace ℝ E] [SecondCountableTopologyEither α E] [Fact (1 ≤ p)] (hp : p ≠ ⊤) [μ.WeaklyRegular] : (MeasureTheory.Lp.boundedContinuousFunction E p μ).topologicalClosure = ⊤
BoundedContinuousFunction.toLp_denseRange 📋 Mathlib.MeasureTheory.Function.ContinuousMapDense
{α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] (E : Type u_2) [NormedAddCommGroup E] (μ : MeasureTheory.Measure α) {p : ENNReal} [SecondCountableTopologyEither α E] [_i : Fact (1 ≤ p)] (𝕜 : Type u_3) [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [NormedSpace ℝ E] [μ.WeaklyRegular] [MeasureTheory.IsFiniteMeasure μ] (hp : p ≠ ⊤) : DenseRange ⇑(BoundedContinuousFunction.toLp p μ 𝕜)
ContinuousMap.toLp_denseRange 📋 Mathlib.MeasureTheory.Function.ContinuousMapDense
{α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] (E : Type u_2) [NormedAddCommGroup E] (μ : MeasureTheory.Measure α) {p : ENNReal} [SecondCountableTopologyEither α E] [_i : Fact (1 ≤ p)] (𝕜 : Type u_3) [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [NormedSpace ℝ E] [CompactSpace α] [μ.WeaklyRegular] [MeasureTheory.IsFiniteMeasure μ] (hp : p ≠ ⊤) : DenseRange ⇑(ContinuousMap.toLp p μ 𝕜)
NormalSpace.instCompletelyRegularSpace 📋 Mathlib.Topology.Separation.CompletelyRegular
{X : Type u} [TopologicalSpace X] [NormalSpace X] [R0Space X] : CompletelyRegularSpace X
MeasureTheory.FiniteMeasure.Topology.IsClosedEmbedding.isEmbedding_map_finiteMeasure 📋 Mathlib.MeasureTheory.Measure.FiniteMeasure
{Ω' : Type u_2} [MeasurableSpace Ω'] [TopologicalSpace Ω'] [BorelSpace Ω'] {Ω : Type u_3} [MeasurableSpace Ω] [TopologicalSpace Ω] [BorelSpace Ω] [NormalSpace Ω'] (f : Ω → Ω') (hf : Topology.IsClosedEmbedding f) : Topology.IsEmbedding fun μ => μ.map f
Topology.IsClosedEmbedding.continuousOn_comap_finiteMeasure 📋 Mathlib.MeasureTheory.Measure.FiniteMeasure
{Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] [TopologicalSpace Ω] [TopologicalSpace Ω'] [BorelSpace Ω] [BorelSpace Ω'] [NormalSpace Ω'] {f : Ω → Ω'} (hf : Topology.IsClosedEmbedding f) : ContinuousOn (fun μ => MeasureTheory.FiniteMeasure.comap f μ) {μ | μ (Set.range f)ᶜ = 0}
DomAddAct.instNormalSpace 📋 Mathlib.Topology.Algebra.Constructions.DomMulAct
{M : Type u_1} [TopologicalSpace M] [NormalSpace M] : NormalSpace Mᵈᵃᵃ
DomMulAct.instNormalSpace 📋 Mathlib.Topology.Algebra.Constructions.DomMulAct
{M : Type u_1} [TopologicalSpace M] [NormalSpace M] : NormalSpace Mᵈᵐᵃ
IsOpen.measure_eq_biSup_integral_continuous 📋 Mathlib.MeasureTheory.Integral.Regular
{X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [T2Space X] {U : Set X} (hU : IsOpen U) (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegularCompactLTTop] [NormalSpace X] : μ U = ⨆ f, ⨆ (_ : Continuous f), ⨆ (_ : Set.EqOn f 0 Uᶜ), ⨆ (_ : 0 ≤ f), ⨆ (_ : f ≤ 1), ENNReal.ofReal (∫ (x : X), f x ∂μ)
isCompact_setOfPred_probabilityMeasure_mass_eq_compl_isCompact_le 📋 Mathlib.MeasureTheory.Measure.Prokhorov
{E : Type u_1} [MeasurableSpace E] [TopologicalSpace E] [T2Space E] [BorelSpace E] {u : ℕ → NNReal} {K : ℕ → Set E} (hu : Filter.Tendsto u Filter.atTop (nhds 0)) (hK : ∀ (n : ℕ), IsCompact (K n)) (h : NormalSpace E ∨ Monotone K) : IsCompact {μ | ∀ (n : ℕ), μ (K n)ᶜ ≤ u n}
isCompact_setOf_probabilityMeasure_mass_eq_compl_isCompact_le 📋 Mathlib.MeasureTheory.Measure.Prokhorov
{E : Type u_1} [MeasurableSpace E] [TopologicalSpace E] [T2Space E] [BorelSpace E] {u : ℕ → NNReal} {K : ℕ → Set E} (hu : Filter.Tendsto u Filter.atTop (nhds 0)) (hK : ∀ (n : ℕ), IsCompact (K n)) (h : NormalSpace E ∨ Monotone K) : IsCompact {μ | ∀ (n : ℕ), μ (K n)ᶜ ≤ u n}
isCompact_setOfPred_finiteMeasure_mass_eq_compl_isCompact_le 📋 Mathlib.MeasureTheory.Measure.Prokhorov
{E : Type u_1} [MeasurableSpace E] [TopologicalSpace E] [T2Space E] [BorelSpace E] {u : ℕ → NNReal} {K : ℕ → Set E} (C : NNReal) (hu : Filter.Tendsto u Filter.atTop (nhds 0)) (hK : ∀ (n : ℕ), IsCompact (K n)) (h : NormalSpace E ∨ Monotone K) : IsCompact {μ | μ.mass = C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n}
isCompact_setOf_finiteMeasure_mass_eq_compl_isCompact_le 📋 Mathlib.MeasureTheory.Measure.Prokhorov
{E : Type u_1} [MeasurableSpace E] [TopologicalSpace E] [T2Space E] [BorelSpace E] {u : ℕ → NNReal} {K : ℕ → Set E} (C : NNReal) (hu : Filter.Tendsto u Filter.atTop (nhds 0)) (hK : ∀ (n : ℕ), IsCompact (K n)) (h : NormalSpace E ∨ Monotone K) : IsCompact {μ | μ.mass = C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n}
isCompact_setOfPred_finiteMeasure_mass_le_compl_isCompact_le 📋 Mathlib.MeasureTheory.Measure.Prokhorov
{E : Type u_1} [MeasurableSpace E] [TopologicalSpace E] [T2Space E] [BorelSpace E] {u : ℕ → NNReal} {K : ℕ → Set E} (C : NNReal) (hu : Filter.Tendsto u Filter.atTop (nhds 0)) (hK : ∀ (n : ℕ), IsCompact (K n)) (h : NormalSpace E ∨ Monotone K) : IsCompact {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n}
isCompact_setOf_finiteMeasure_mass_le_compl_isCompact_le 📋 Mathlib.MeasureTheory.Measure.Prokhorov
{E : Type u_1} [MeasurableSpace E] [TopologicalSpace E] [T2Space E] [BorelSpace E] {u : ℕ → NNReal} {K : ℕ → Set E} (C : NNReal) (hu : Filter.Tendsto u Filter.atTop (nhds 0)) (hK : ∀ (n : ℕ), IsCompact (K n)) (h : NormalSpace E ∨ Monotone K) : IsCompact {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n}
HasOpenLowerSections.exists_continuous_selection 📋 Mathlib.Topology.Semicontinuity.Michael
{α : Type u_1} {β : Type u_2} {f : α → Set β} [TopologicalSpace α] [NormalSpace α] [ParacompactSpace α] [AddCommGroup β] [Module ℝ β] [TopologicalSpace β] [ContinuousSMul ℝ β] [ContinuousAdd β] (hf : HasOpenLowerSections f) (hf_nonempty : ∀ (x : α), (f x).Nonempty) (hf_convex : ∀ (x : α), Convex ℝ (f x)) : ∃ h, Continuous h ∧ ∀ (x : α), h x ∈ f x
LowerHemicontinuous.exists_continuous_selection 📋 Mathlib.Topology.Semicontinuity.Michael
{α : Type u_1} {β : Type u_2} {f : α → Set β} [TopologicalSpace α] [NormalSpace α] [ParacompactSpace α] [AddCommGroup β] [Module ℝ β] [UniformSpace β] [IsUniformAddGroup β] [ContinuousSMul ℝ β] [LocallyConvexSpace ℝ β] [FirstCountableTopology β] [CompleteSpace β] (hf : LowerHemicontinuous f) (hf_nonempty : ∀ (x : α), (f x).Nonempty) (hf_convex : ∀ (x : α), Convex ℝ (f x)) (hf_isClosed : ∀ (x : α), IsClosed (f x)) : ∃ g, Continuous g ∧ ∀ (x : α), g x ∈ f x
IsClosed.not_normal_of_continuum_le_mk 📋 Mathlib.Topology.Separation.NotNormal
{X : Type u} [TopologicalSpace X] [TopologicalSpace.SeparableSpace X] {s : Set X} (hs : IsClosed s) [DiscreteTopology ↑s] (hmk : Cardinal.continuum ≤ Cardinal.mk ↑s) : ¬NormalSpace X
IsClosed.mk_lt_continuum 📋 Mathlib.Topology.Separation.NotNormal
{X : Type u} [TopologicalSpace X] [TopologicalSpace.SeparableSpace X] [NormalSpace X] {s : Set X} (hs : IsClosed s) [DiscreteTopology ↑s] : Cardinal.mk ↑s < Cardinal.continuum
IsClosed.two_pow_mk_lt_continuum 📋 Mathlib.Topology.Separation.NotNormal
{X : Type u} [TopologicalSpace X] [TopologicalSpace.SeparableSpace X] [NormalSpace X] {s : Set X} (hs : IsClosed s) [DiscreteTopology ↑s] : 2 ^ Cardinal.mk ↑s ≤ Cardinal.continuum
IsClosed.mk_lt_two_pow_mk_dense 📋 Mathlib.Topology.Separation.NotNormal
{X : Type u} [TopologicalSpace X] [NormalSpace X] {s d : Set X} (hs : IsClosed s) [DiscreteTopology ↑s] (hd : Dense d) : Cardinal.mk ↑s < 2 ^ Cardinal.mk ↑d
IsClosed.two_pow_mk_le_two_pow_mk_dense 📋 Mathlib.Topology.Separation.NotNormal
{X : Type u} [TopologicalSpace X] [NormalSpace X] {s d : Set X} (hs : IsClosed s) [DiscreteTopology ↑s] (hd : Dense d) : 2 ^ Cardinal.mk ↑s ≤ 2 ^ Cardinal.mk ↑d

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:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
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
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.
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