Loogle!

Result

Found 1902 declarations mentioning IsTopologicalAddGroup. Of these, only the first 200 are shown.

• IsTopologicalAddGroup 📋 Mathlib.Topology.Algebra.Group.Defs
  (G : Type u) [TopologicalSpace G] [AddGroup G] : Prop
• IsTopologicalAddGroup.to_continuousSub 📋 Mathlib.Topology.Algebra.Group.Defs
  {G : Type u} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] : ContinuousSub G
• IsTopologicalAddGroup.toContinuousAdd 📋 Mathlib.Topology.Algebra.Group.Defs
  {G : Type u} {inst✝ : TopologicalSpace G} {inst✝¹ : AddGroup G} [self : IsTopologicalAddGroup G] : ContinuousAdd G
• IsTopologicalAddGroup.toContinuousNeg 📋 Mathlib.Topology.Algebra.Group.Defs
  {G : Type u} {inst✝ : TopologicalSpace G} {inst✝¹ : AddGroup G} [self : IsTopologicalAddGroup G] : ContinuousNeg G
• IsTopologicalAddGroup.mk 📋 Mathlib.Topology.Algebra.Group.Defs
  {G : Type u} [TopologicalSpace G] [AddGroup G] [toContinuousAdd : ContinuousAdd G] [toContinuousNeg : ContinuousNeg G] : IsTopologicalAddGroup G
• AddGroup.continuousConstSMul_int 📋 Mathlib.Topology.Algebra.Group.ZPow
  {A : Type u_3} [AddGroup A] [TopologicalSpace A] [IsTopologicalAddGroup A] : ContinuousConstSMul ℤ A
• AddGroup.continuousSMul_int 📋 Mathlib.Topology.Algebra.Group.ZPow
  {A : Type u_3} [AddGroup A] [TopologicalSpace A] [IsTopologicalAddGroup A] : ContinuousSMul ℤ A
• continuous_zsmul 📋 Mathlib.Topology.Algebra.Group.ZPow
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (z : ℤ) : Continuous fun a => z • a
• continuousAt_zsmul 📋 Mathlib.Topology.Algebra.Group.ZPow
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (x : G) (z : ℤ) : ContinuousAt (fun x => z • x) x
• continuousOn_zsmul 📋 Mathlib.Topology.Algebra.Group.ZPow
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s : Set G} (z : ℤ) : ContinuousOn (fun x => z • x) s
• Continuous.fun_zsmul 📋 Mathlib.Topology.Algebra.Group.ZPow
  {G : Type u_1} {α : Type u_2} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [TopologicalSpace α] {f : α → G} (h : Continuous f) (z : ℤ) : Continuous fun i => z • f i
• ContinuousAt.fun_zsmul 📋 Mathlib.Topology.Algebra.Group.ZPow
  {G : Type u_1} {α : Type u_2} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [TopologicalSpace α] {f : α → G} {x : α} (hf : ContinuousAt f x) (z : ℤ) : ContinuousAt (fun i => z • f i) x
• ContinuousOn.fun_zsmul 📋 Mathlib.Topology.Algebra.Group.ZPow
  {G : Type u_1} {α : Type u_2} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [TopologicalSpace α] {f : α → G} {s : Set α} (hf : ContinuousOn f s) (z : ℤ) : ContinuousOn (fun i => z • f i) s
• Continuous.zsmul 📋 Mathlib.Topology.Algebra.Group.ZPow
  {G : Type u_1} {α : Type u_2} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [TopologicalSpace α] {f : α → G} (h : Continuous f) (z : ℤ) : Continuous (z • f)
• ContinuousWithinAt.fun_zsmul 📋 Mathlib.Topology.Algebra.Group.ZPow
  {G : Type u_1} {α : Type u_2} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [TopologicalSpace α] {f : α → G} {x : α} {s : Set α} (hf : ContinuousWithinAt f s x) (z : ℤ) : ContinuousWithinAt (fun i => z • f i) s x
• ContinuousAt.zsmul 📋 Mathlib.Topology.Algebra.Group.ZPow
  {G : Type u_1} {α : Type u_2} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [TopologicalSpace α] {f : α → G} {x : α} (hf : ContinuousAt f x) (z : ℤ) : ContinuousAt (z • f) x
• ContinuousOn.zsmul 📋 Mathlib.Topology.Algebra.Group.ZPow
  {G : Type u_1} {α : Type u_2} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [TopologicalSpace α] {f : α → G} {s : Set α} (hf : ContinuousOn f s) (z : ℤ) : ContinuousOn (z • f) s
• ContinuousWithinAt.zsmul 📋 Mathlib.Topology.Algebra.Group.ZPow
  {G : Type u_1} {α : Type u_2} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [TopologicalSpace α] {f : α → G} {x : α} {s : Set α} (hf : ContinuousWithinAt f s x) (z : ℤ) : ContinuousWithinAt (z • f) s x
• Filter.Tendsto.zsmul 📋 Mathlib.Topology.Algebra.Group.ZPow
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {α : Type u_3} {l : Filter α} {f : α → G} {x : G} (hf : Filter.Tendsto f l (nhds x)) (z : ℤ) : Filter.Tendsto (fun x => z • f x) l (nhds (z • x))
• isTopologicalAddGroup_of_discreteTopology 📋 Mathlib.Topology.Algebra.Group.ContinuousInv
  {H : Type u_2} [TopologicalSpace H] [AddGroup H] [DiscreteTopology H] : IsTopologicalAddGroup H
• isTopologicalAddGroup_of_indiscreteTopology 📋 Mathlib.Topology.Algebra.Group.ContinuousInv
  {H : Type u_2} [TopologicalSpace H] [AddGroup H] [IndiscreteTopology H] : IsTopologicalAddGroup H
• topologicalAddGroup_of_discreteTopology 📋 Mathlib.Topology.Algebra.Group.ContinuousInv
  {H : Type u_2} [TopologicalSpace H] [AddGroup H] [DiscreteTopology H] : IsTopologicalAddGroup H
• topologicalAddGroup_of_indiscreteTopology 📋 Mathlib.Topology.Algebra.Group.ContinuousInv
  {H : Type u_2} [TopologicalSpace H] [AddGroup H] [IndiscreteTopology H] : IsTopologicalAddGroup H
• instIsTopologicalAddGroupAddOpposite 📋 Mathlib.Topology.Algebra.Group.Basic
  {α : Type u_3} [TopologicalSpace α] [AddGroup α] [IsTopologicalAddGroup α] : IsTopologicalAddGroup αᵃᵒᵖ
• instIsTopologicalAddGroupAdditiveOfIsTopologicalGroup 📋 Mathlib.Topology.Algebra.Group.Basic
  {G : Type u_5} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : IsTopologicalAddGroup (Additive G)
• instIsTopologicalGroupMultiplicativeOfIsTopologicalAddGroup 📋 Mathlib.Topology.Algebra.Group.Basic
  {G : Type u_5} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] : IsTopologicalGroup (Multiplicative G)
• OrderDual.instIsTopologicalAddGroup 📋 Mathlib.Topology.Algebra.Group.Basic
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] : IsTopologicalAddGroup Gᵒᵈ
• SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace 📋 Mathlib.Topology.Algebra.Group.Basic
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [TopologicalSpace.SeparableSpace G] [WeaklyLocallyCompactSpace G] : SigmaCompactSpace G
• Homeomorph.shearAddRight 📋 Mathlib.Topology.Algebra.Group.Basic
  (G : Type u_1) [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] : G × G ≃ₜ G × G
• Pi.isTopologicalAddGroup 📋 Mathlib.Topology.Algebra.Group.Basic
  {β : Type u_4} {C : β → Type u_5} [(b : β) → TopologicalSpace (C b)] [(b : β) → AddGroup (C b)] [∀ (b : β), IsTopologicalAddGroup (C b)] : IsTopologicalAddGroup ((b : β) → C b)
• Pi.topologicalAddGroup 📋 Mathlib.Topology.Algebra.Group.Basic
  {β : Type u_4} {C : β → Type u_5} [(b : β) → TopologicalSpace (C b)] [(b : β) → AddGroup (C b)] [∀ (b : β), IsTopologicalAddGroup (C b)] : IsTopologicalAddGroup ((b : β) → C b)
• Prod.instIsTopologicalAddGroup 📋 Mathlib.Topology.Algebra.Group.Basic
  {G : Type u_1} {H : Type u_2} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [TopologicalSpace H] [AddGroup H] [IsTopologicalAddGroup H] : IsTopologicalAddGroup (G × H)
• isTopologicalAddGroup_iInf 📋 Mathlib.Topology.Algebra.Group.Basic
  {G : Type u_1} {ι : Sort u_5} [AddGroup G] {ts' : ι → TopologicalSpace G} (h' : ∀ (i : ι), IsTopologicalAddGroup G) : IsTopologicalAddGroup G
• isTopologicalAddGroup_inf 📋 Mathlib.Topology.Algebra.Group.Basic
  {G : Type u_1} [AddGroup G] {t₁ t₂ : TopologicalSpace G} (h₁ : IsTopologicalAddGroup G) (h₂ : IsTopologicalAddGroup G) : IsTopologicalAddGroup G
• topologicalAddGroup_iInf 📋 Mathlib.Topology.Algebra.Group.Basic
  {G : Type u_1} {ι : Sort u_5} [AddGroup G] {ts' : ι → TopologicalSpace G} (h' : ∀ (i : ι), IsTopologicalAddGroup G) : IsTopologicalAddGroup G
• topologicalAddGroup_inf 📋 Mathlib.Topology.Algebra.Group.Basic
  {G : Type u_1} [AddGroup G] {t₁ t₂ : TopologicalSpace G} (h₁ : IsTopologicalAddGroup G) (h₂ : IsTopologicalAddGroup G) : IsTopologicalAddGroup G
• isTopologicalAddGroup_sInf 📋 Mathlib.Topology.Algebra.Group.Basic
  {G : Type u_1} [AddGroup G] {ts : Set (TopologicalSpace G)} (h : ∀ t ∈ ts, IsTopologicalAddGroup G) : IsTopologicalAddGroup G
• topologicalAddGroup_sInf 📋 Mathlib.Topology.Algebra.Group.Basic
  {G : Type u_1} [AddGroup G] {ts : Set (TopologicalSpace G)} (h : ∀ t ∈ ts, IsTopologicalAddGroup G) : IsTopologicalAddGroup G
• isTopologicalAddGroup_induced 📋 Mathlib.Topology.Algebra.Group.Basic
  {G : Type u_1} {H : Type u_2} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {F : Type u_5} [AddGroup H] [FunLike F H G] [AddMonoidHomClass F H G] (f : F) : IsTopologicalAddGroup H
• topologicalAddGroup_induced 📋 Mathlib.Topology.Algebra.Group.Basic
  {G : Type u_1} {H : Type u_2} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {F : Type u_5} [AddGroup H] [FunLike F H G] [AddMonoidHomClass F H G] (f : F) : IsTopologicalAddGroup H
• Topology.IsInducing.isTopologicalAddGroup 📋 Mathlib.Topology.Algebra.Group.Basic
  {G : Type u_1} {H : Type u_2} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {F : Type u_5} [AddGroup H] [TopologicalSpace H] [FunLike F H G] [AddMonoidHomClass F H G] (f : F) (hf : Topology.IsInducing ⇑f) : IsTopologicalAddGroup H
• Topology.IsInducing.topologicalAddGroup 📋 Mathlib.Topology.Algebra.Group.Basic
  {G : Type u_1} {H : Type u_2} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {F : Type u_5} [AddGroup H] [TopologicalSpace H] [FunLike F H G] [AddMonoidHomClass F H G] (f : F) (hf : Topology.IsInducing ⇑f) : IsTopologicalAddGroup H
• nhds_zero_symm 📋 Mathlib.Topology.Algebra.Group.Basic
  (G : Type u_1) [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] : Filter.comap Neg.neg (nhds 0) = nhds 0
• nhds_zero_symm' 📋 Mathlib.Topology.Algebra.Group.Basic
  (G : Type u_1) [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] : Filter.map Neg.neg (nhds 0) = nhds 0
• neg_mem_nhds_zero 📋 Mathlib.Topology.Algebra.Group.Basic
  (G : Type u_1) [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {S : Set G} (hS : S ∈ nhds 0) : -S ∈ nhds 0
• compact_covered_by_add_left_translates 📋 Mathlib.Topology.Algebra.Group.Basic
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {K V : Set G} (hK : IsCompact K) (hV : (interior V).Nonempty) : ∃ t, K ⊆ ⋃ g ∈ t, (fun x => g + x) ⁻¹' V
• exists_disjoint_vadd_of_isCompact 📋 Mathlib.Topology.Algebra.Group.Basic
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [NoncompactSpace G] {K L : Set G} (hK : IsCompact K) (hL : IsCompact L) : ∃ g, Disjoint K (g +ᵥ L)
• Homeomorph.shearAddRight_coe 📋 Mathlib.Topology.Algebra.Group.Basic
  (G : Type u_1) [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] : ⇑(Homeomorph.shearAddRight G) = fun z => (z.1, z.1 + z.2)
• Homeomorph.shearAddRight_symm_coe 📋 Mathlib.Topology.Algebra.Group.Basic
  (G : Type u_1) [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] : ⇑(Homeomorph.shearAddRight G).symm = fun z => (z.1, -z.1 + z.2)
• nhdsAddHom 📋 Mathlib.Topology.Algebra.Group.Neighborhood
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] : G →ₙ+ Filter G
• map_add_left_nhds_zero 📋 Mathlib.Topology.Algebra.Group.Neighborhood
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (x : G) : Filter.map (fun x_1 => x + x_1) (nhds 0) = nhds x
• map_add_right_nhds_zero 📋 Mathlib.Topology.Algebra.Group.Neighborhood
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (x : G) : Filter.map (fun x_1 => x_1 + x) (nhds 0) = nhds x
• IsTopologicalAddGroup.ext 📋 Mathlib.Topology.Algebra.Group.Neighborhood
  {G : Type u_2} [AddGroup G] {t t' : TopologicalSpace G} (tg : IsTopologicalAddGroup G) (tg' : IsTopologicalAddGroup G) (h : nhds 0 = nhds 0) : t = t'
• IsTopologicalAddGroup.ext_iff 📋 Mathlib.Topology.Algebra.Group.Neighborhood
  {G : Type u_2} [AddGroup G] {t t' : TopologicalSpace G} (tg : IsTopologicalAddGroup G) (tg' : IsTopologicalAddGroup G) : t = t' ↔ nhds 0 = nhds 0
• map_add_left_nhds 📋 Mathlib.Topology.Algebra.Group.Neighborhood
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (x y : G) : Filter.map (fun x_1 => x + x_1) (nhds y) = nhds (x + y)
• map_add_right_nhds 📋 Mathlib.Topology.Algebra.Group.Neighborhood
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (x y : G) : Filter.map (fun x_1 => x_1 + x) (nhds y) = nhds (y + x)
• nhds_add 📋 Mathlib.Topology.Algebra.Group.Neighborhood
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (x y : G) : nhds (x + y) = nhds x + nhds y
• nhds_translation_add_neg 📋 Mathlib.Topology.Algebra.Group.Neighborhood
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (x : G) : Filter.comap (fun x_1 => x_1 + -x) (nhds 0) = nhds x
• nhds_translation_neg_add 📋 Mathlib.Topology.Algebra.Group.Neighborhood
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (x : G) : Filter.comap (fun x_1 => -x + x_1) (nhds 0) = nhds x
• Filter.HasBasis.nhds_of_zero 📋 Mathlib.Topology.Algebra.Group.Neighborhood
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {ι : Sort u_2} {p : ι → Prop} {s : ι → Set G} (hb : (nhds 0).HasBasis p s) (x : G) : (nhds x).HasBasis p fun i => {y | y - x ∈ s i}
• Filter.HasBasis.nhds_zero_neg 📋 Mathlib.Topology.Algebra.Group.Neighborhood
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {ι : Sort u_2} {p : ι → Prop} {U : ι → Set G} (hU : (nhds 0).HasBasis p U) : (nhds 0).HasBasis p fun i => -U i
• Filter.HasBasis.nhds_of_zero' 📋 Mathlib.Topology.Algebra.Group.Neighborhood
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {ι : Sort u_2} {p : ι → Prop} {s : ι → Set G} (hb : (nhds 0).HasBasis p s) (x : G) : (nhds x).HasBasis p fun i => x +ᵥ s i
• continuous_of_continuousAt_zero 📋 Mathlib.Topology.Algebra.Group.Neighborhood
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {M : Type u_2} {hom : Type u_3} [AddZeroClass M] [TopologicalSpace M] [ContinuousAdd M] [FunLike hom G M] [AddMonoidHomClass hom G M] (f : hom) (hf : ContinuousAt (⇑f) 0) : Continuous ⇑f
• mem_closure_iff_nhds_zero 📋 Mathlib.Topology.Algebra.Group.Neighborhood
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {x : G} {s : Set G} : x ∈ closure s ↔ ∀ U ∈ nhds 0, ∃ y ∈ s, y - x ∈ U
• nhdsAddHom_apply 📋 Mathlib.Topology.Algebra.Group.Neighborhood
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (x : G) : nhdsAddHom x = nhds x
• continuous_of_tendsto_nhds_zero 📋 Mathlib.Topology.Algebra.Group.Neighborhood
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {M : Type u_2} {hom : Type u_3} [AddZeroClass M] [TopologicalSpace M] [ContinuousAdd M] [FunLike hom G M] [AddMonoidHomClass hom G M] (f : hom) (hf : Filter.Tendsto (⇑f) (nhds 0) (nhds 0)) : Continuous ⇑f
• IsTopologicalAddGroup.exists_antitone_basis_nhds_zero 📋 Mathlib.Topology.Algebra.Group.Neighborhood
  (G : Type u_1) [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [FirstCountableTopology G] : ∃ u, (nhds 0).HasAntitoneBasis u ∧ ∀ (n : ℕ), u (n + 1) + u (n + 1) ⊆ u n
• exists_nhds_half_neg 📋 Mathlib.Topology.Algebra.Group.Neighborhood
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s : Set G} (hs : s ∈ nhds 0) : ∃ V ∈ nhds 0, ∀ v ∈ V, ∀ w ∈ V, v - w ∈ s
• IsTopologicalAddGroup.isInducing_iff_nhds_zero 📋 Mathlib.Topology.Algebra.Group.Neighborhood
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {H : Type u_2} [AddGroup H] [TopologicalSpace H] [IsTopologicalAddGroup H] {F : Type u_3} [FunLike F G H] [AddMonoidHomClass F G H] {f : F} : Topology.IsInducing ⇑f ↔ nhds 0 = Filter.comap (⇑f) (nhds 0)
• IsTopologicalAddGroup.isOpenMap_iff_nhds_zero 📋 Mathlib.Topology.Algebra.Group.Neighborhood
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {H : Type u_2} [AddMonoid H] [TopologicalSpace H] [ContinuousConstVAdd H H] {F : Type u_3} [FunLike F G H] [AddMonoidHomClass F G H] {f : F} : IsOpenMap ⇑f ↔ nhds 0 ≤ Filter.map (⇑f) (nhds 0)
• IsTopologicalAddGroup.of_comm_of_nhds_zero 📋 Mathlib.Topology.Algebra.Group.Neighborhood
  {G : Type u_2} [AddCommGroup G] [TopologicalSpace G] (hadd : Filter.Tendsto (Function.uncurry fun x1 x2 => x1 + x2) (nhds 0 ×ˢ nhds 0) (nhds 0)) (hneg : Filter.Tendsto (fun x => -x) (nhds 0) (nhds 0)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x₀ + x) (nhds 0)) : IsTopologicalAddGroup G
• IsTopologicalAddGroup.of_nhds_zero' 📋 Mathlib.Topology.Algebra.Group.Neighborhood
  {G : Type u_2} [AddGroup G] [TopologicalSpace G] (hadd : Filter.Tendsto (Function.uncurry fun x1 x2 => x1 + x2) (nhds 0 ×ˢ nhds 0) (nhds 0)) (hneg : Filter.Tendsto (fun x => -x) (nhds 0) (nhds 0)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x₀ + x) (nhds 0)) (hright : ∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x + x₀) (nhds 0)) : IsTopologicalAddGroup G
• IsTopologicalAddGroup.of_nhds_zero 📋 Mathlib.Topology.Algebra.Group.Neighborhood
  {G : Type u_2} [AddGroup G] [TopologicalSpace G] (hadd : Filter.Tendsto (Function.uncurry fun x1 x2 => x1 + x2) (nhds 0 ×ˢ nhds 0) (nhds 0)) (hneg : Filter.Tendsto (fun x => -x) (nhds 0) (nhds 0)) (hleft : ∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x₀ + x) (nhds 0)) (haddConj : ∀ (x₀ : G), Filter.Tendsto (fun x => x₀ + x + -x₀) (nhds 0) (nhds 0)) : IsTopologicalAddGroup G
• continuous_of_continuousAt_zero₂ 📋 Mathlib.Topology.Algebra.Group.Neighborhood
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {H : Type u_2} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] [AddGroup H] [TopologicalSpace H] [IsTopologicalAddGroup H] (f : G →+ H →+ M) (hf : ContinuousAt (fun x => (f x.1) x.2) (0, 0)) (hl : ∀ (x : G), ContinuousAt (⇑(f x)) 0) (hr : ∀ (y : H), ContinuousAt (fun x => (f x) y) 0) : Continuous fun x => (f x.1) x.2
• IsTopologicalAddGroup.leftUniformSpace 📋 Mathlib.Topology.Algebra.IsUniformGroup.Defs
  (G : Type u_1) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] : UniformSpace G
• IsTopologicalAddGroup.rightUniformSpace 📋 Mathlib.Topology.Algebra.IsUniformGroup.Defs
  (G : Type u_1) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] : UniformSpace G
• IsLeftUniformAddGroup.toIsTopologicalAddGroup 📋 Mathlib.Topology.Algebra.IsUniformGroup.Defs
  {G : Type u_4} {inst✝ : UniformSpace G} {inst✝¹ : AddGroup G} [self : IsLeftUniformAddGroup G] : IsTopologicalAddGroup G
• IsRightUniformAddGroup.toIsTopologicalAddGroup 📋 Mathlib.Topology.Algebra.IsUniformGroup.Defs
  {G : Type u_4} {inst✝ : UniformSpace G} {inst✝¹ : AddGroup G} [self : IsRightUniformAddGroup G] : IsTopologicalAddGroup G
• IsUniformAddGroup.isTopologicalAddGroup 📋 Mathlib.Topology.Algebra.IsUniformGroup.Defs
  {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] : IsTopologicalAddGroup α
• IsUniformAddGroup.to_topologicalAddGroup 📋 Mathlib.Topology.Algebra.IsUniformGroup.Defs
  {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] : IsTopologicalAddGroup α
• isUniformAddGroup_of_addCommGroup 📋 Mathlib.Topology.Algebra.IsUniformGroup.Defs
  {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] : IsUniformAddGroup G
• uniformity_eq_comap_nhds_zero' 📋 Mathlib.Topology.Algebra.IsUniformGroup.Defs
  (G : Type u_1) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] : uniformity G = Filter.comap (fun p => p.2 + -p.1) (nhds 0)
• uniformity_eq_comap_nhds_zero_left 📋 Mathlib.Topology.Algebra.IsUniformGroup.Defs
  (G : Type u_1) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] : uniformity G = Filter.comap (fun p => -p.1 + p.2) (nhds 0)
• IsLeftUniformAddGroup.mk 📋 Mathlib.Topology.Algebra.IsUniformGroup.Defs
  {G : Type u_4} [UniformSpace G] [AddGroup G] [toIsTopologicalAddGroup : IsTopologicalAddGroup G] (uniformity_eq : uniformity G = Filter.comap (fun x => -x.1 + x.2) (nhds 0)) : IsLeftUniformAddGroup G
• IsRightUniformAddGroup.mk 📋 Mathlib.Topology.Algebra.IsUniformGroup.Defs
  {G : Type u_4} [UniformSpace G] [AddGroup G] [toIsTopologicalAddGroup : IsTopologicalAddGroup G] (uniformity_eq : uniformity G = Filter.comap (fun x => x.2 + -x.1) (nhds 0)) : IsRightUniformAddGroup G
• Homeomorph.subLeft 📋 Mathlib.Topology.Algebra.Group.ContinuousDiv
  {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (x : G) : G ≃ₜ G
• Homeomorph.subRight 📋 Mathlib.Topology.Algebra.Group.ContinuousDiv
  {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (x : G) : G ≃ₜ G
• isClosedMap_sub_left 📋 Mathlib.Topology.Algebra.Group.ContinuousDiv
  {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (a : G) : IsClosedMap fun x => a - x
• isClosedMap_sub_right 📋 Mathlib.Topology.Algebra.Group.ContinuousDiv
  {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (a : G) : IsClosedMap fun x => x - a
• isOpenMap_sub_left 📋 Mathlib.Topology.Algebra.Group.ContinuousDiv
  {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (a : G) : IsOpenMap fun x => a - x
• isOpenMap_sub_right 📋 Mathlib.Topology.Algebra.Group.ContinuousDiv
  {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (a : G) : IsOpenMap fun x => x - a
• nhds_translation_sub 📋 Mathlib.Topology.Algebra.Group.ContinuousDiv
  {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (x : G) : Filter.comap (fun x_1 => x_1 - x) (nhds 0) = nhds x
• Filter.map_subLeft_nhds 📋 Mathlib.Topology.Algebra.Group.ContinuousDiv
  {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {c a : G} : Filter.map (fun x => c - x) (nhds a) = nhds (c - a)
• Filter.map_subRight_nhds 📋 Mathlib.Topology.Algebra.Group.ContinuousDiv
  {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {c a : G} : Filter.map (fun x => x - c) (nhds a) = nhds (a - c)
• Homeomorph.coe_subLeft 📋 Mathlib.Topology.Algebra.Group.ContinuousDiv
  {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (a : G) : ⇑(Homeomorph.subLeft a) = fun x => a - x
• Homeomorph.coe_subRight 📋 Mathlib.Topology.Algebra.Group.ContinuousDiv
  {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (a : G) : ⇑(Homeomorph.subRight a) = fun x => x - a
• Homeomorph.subLeft_apply 📋 Mathlib.Topology.Algebra.Group.ContinuousDiv
  {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (x b : G) : (Homeomorph.subLeft x) b = x - b
• Homeomorph.subRight_apply 📋 Mathlib.Topology.Algebra.Group.ContinuousDiv
  {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (x b : G) : (Homeomorph.subRight x) b = b - x
• tendsto_sub_nhds_zero_iff 📋 Mathlib.Topology.Algebra.Group.ContinuousDiv
  {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {α : Type u_3} {l : Filter α} {x : G} {u : α → G} : Filter.Tendsto (fun x_1 => u x_1 - x) l (nhds 0) ↔ Filter.Tendsto u l (nhds x)
• Filter.tendsto_const_sub_iff 📋 Mathlib.Topology.Algebra.Group.ContinuousDiv
  {G : Type u_1} {α : Type u_2} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (b : G) {c : G} {f : α → G} {l : Filter α} : Filter.Tendsto (fun k => b - f k) l (nhds (b - c)) ↔ Filter.Tendsto f l (nhds c)
• Homeomorph.subRight_symm_apply 📋 Mathlib.Topology.Algebra.Group.ContinuousDiv
  {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (x b : G) : (Homeomorph.subRight x).symm b = b + x
• Homeomorph.subLeft_symm_apply 📋 Mathlib.Topology.Algebra.Group.ContinuousDiv
  {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (x b : G) : (Homeomorph.subLeft x).symm b = -b + x
• eq_of_tendsto_sub_nhds_zero 📋 Mathlib.Topology.Algebra.Group.ContinuousDiv
  {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {α : Type u_3} {l : Filter α} [l.NeBot] [T2Space G] {f g : α → G} {a b : G} (hf : Filter.Tendsto f l (nhds a)) (hg : Filter.Tendsto g l (nhds b)) : Filter.Tendsto (fun x => f x - g x) l (nhds 0) → a = b
• tendsto_sub_nhds_zero_iff_eq 📋 Mathlib.Topology.Algebra.Group.ContinuousDiv
  {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {α : Type u_3} {l : Filter α} [l.NeBot] [T2Space G] {f g : α → G} {a b : G} (hf : Filter.Tendsto f l (nhds a)) (hg : Filter.Tendsto g l (nhds b)) : Filter.Tendsto (fun x => f x - g x) l (nhds 0) ↔ a = b
• Filter.map_subLeft_nhdsNE 📋 Mathlib.Topology.Algebra.Group.ContinuousDiv
  {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {c a : G} : Filter.map (fun x => c - x) (nhdsWithin a {a}ᶜ) = nhdsWithin (c - a) {c - a}ᶜ
• Filter.map_subRight_nhdsNE 📋 Mathlib.Topology.Algebra.Group.ContinuousDiv
  {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {c a : G} : Filter.map (fun x => x - c) (nhdsWithin a {a}ᶜ) = nhdsWithin (a - c) {a - c}ᶜ
• AddSubgroup.connectedComponentOfZero 📋 Mathlib.Topology.Algebra.Group.Subgroup
  (G : Type u_3) [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] : AddSubgroup G
• AddSubgroup.topologicalClosure 📋 Mathlib.Topology.Algebra.Group.Subgroup
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (s : AddSubgroup G) : AddSubgroup G
• AddSubgroup.is_normal_topologicalClosure 📋 Mathlib.Topology.Algebra.Group.Subgroup
  {G : Type u_3} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (N : AddSubgroup G) [N.Normal] : N.topologicalClosure.Normal
• AddSubgroup.isClosed_topologicalClosure 📋 Mathlib.Topology.Algebra.Group.Subgroup
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (s : AddSubgroup G) : IsClosed ↑s.topologicalClosure
• AddSubgroup.le_topologicalClosure 📋 Mathlib.Topology.Algebra.Group.Subgroup
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (s : AddSubgroup G) : s ≤ s.topologicalClosure
• AddSubgroup.topologicalClosure_coe 📋 Mathlib.Topology.Algebra.Group.Subgroup
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s : AddSubgroup G} : ↑s.topologicalClosure = closure ↑s
• AddSubgroup.instIsTopologicalAddGroupSubtypeMem 📋 Mathlib.Topology.Algebra.Group.Subgroup
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (S : AddSubgroup G) : IsTopologicalAddGroup ↥S
• AddSubgroup.coe_topologicalClosure_bot 📋 Mathlib.Topology.Algebra.Group.Subgroup
  (G : Type u_1) [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] : ↑⊥.topologicalClosure = closure {0}
• AddSubgroup.topologicalClosure_mono 📋 Mathlib.Topology.Algebra.Group.Subgroup
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s t : AddSubgroup G} (h : s ≤ t) : s.topologicalClosure ≤ t.topologicalClosure
• AddSubgroup.topologicalClosure_minimal 📋 Mathlib.Topology.Algebra.Group.Subgroup
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (s : AddSubgroup G) {t : AddSubgroup G} (h : s ≤ t) (ht : IsClosed ↑t) : s.topologicalClosure ≤ t
• AddSubgroup.isAddCommutative_topologicalClosure 📋 Mathlib.Topology.Algebra.Group.Subgroup
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [T2Space G] (s : AddSubgroup G) [IsAddCommutative ↥s] : IsAddCommutative ↥s.topologicalClosure
• DenseRange.topologicalClosure_map_addSubgroup 📋 Mathlib.Topology.Algebra.Group.Subgroup
  {G : Type u_1} {H : Type u_2} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [AddGroup H] [TopologicalSpace H] [IsTopologicalAddGroup H] {f : G →+ H} (hf : Continuous ⇑f) (hf' : DenseRange ⇑f) {s : AddSubgroup G} (hs : s.topologicalClosure = ⊤) : (AddSubgroup.map f s).topologicalClosure = ⊤
• AddSubgroup.addCommGroupTopologicalClosure 📋 Mathlib.Topology.Algebra.Group.Subgroup
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [T2Space G] (s : AddSubgroup G) (hs : ∀ (x y : ↥s), x + y = y + x) : AddCommGroup ↥s.topologicalClosure
• AddSubgroup.properlyDiscontinuousVAdd_opposite_of_tendsto_cofinite 📋 Mathlib.Topology.Algebra.Group.Subgroup
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (S : AddSubgroup G) (hS : Filter.Tendsto (⇑S.subtype) Filter.cofinite (Filter.cocompact G)) : ProperlyDiscontinuousVAdd (↥S.op) G
• AddSubgroup.properlyDiscontinuousVAdd_of_tendsto_cofinite 📋 Mathlib.Topology.Algebra.Group.Subgroup
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (S : AddSubgroup G) (hS : Filter.Tendsto (⇑S.subtype) Filter.cofinite (Filter.cocompact G)) : ProperlyDiscontinuousVAdd (↥S) G
• IsTopologicalAddGroup.regularSpace 📋 Mathlib.Topology.Algebra.Group.Pointwise
  (G : Type w) [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] : RegularSpace G
• IsCompact.locallyCompactSpace_of_mem_nhds_of_addGroup 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {K : Set G} (hK : IsCompact K) {x : G} (h : K ∈ nhds x) : LocallyCompactSpace G
• IsTopologicalAddGroup.t2Space_iff_zero_closed 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] : T2Space G ↔ IsClosed {0}
• IsOpen.sub_left 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s t : Set G} (ht : IsOpen t) : IsOpen (s - t)
• IsOpen.sub_right 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s t : Set G} (hs : IsOpen s) : IsOpen (s - t)
• IsClosed.add_left_of_isCompact 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s t : Set G} (ht : IsClosed t) (hs : IsCompact s) : IsClosed (s + t)
• IsClosed.add_right_of_isCompact 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s t : Set G} (ht : IsClosed t) (hs : IsCompact s) : IsClosed (t + s)
• HasCompactSupport.eq_zero_or_locallyCompactSpace_of_addGroup 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} {α : Type u} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [TopologicalSpace α] [Zero α] [T1Space α] {f : G → α} (hf : HasCompactSupport f) (h'f : Continuous f) : f = 0 ∨ LocallyCompactSpace G
• addGroup_inseparable_iff 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {x y : G} : Inseparable x y ↔ x - y ∈ closure 0
• IsOpen.closure_sub 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {t : Set G} (ht : IsOpen t) (s : Set G) : closure s - t = s - t
• IsOpen.sub_closure 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s : Set G} (hs : IsOpen s) (t : Set G) : s - closure t = s - t
• subset_interior_sub_left 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s t : Set G} : interior s - t ⊆ interior (s - t)
• subset_interior_sub_right 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s t : Set G} : s - interior t ⊆ interior (s - t)
• eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_addGroup 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} {α : Type u} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [TopologicalSpace α] [Zero α] [T1Space α] {f : G → α} {k : Set G} (hk : IsCompact k) (hf : Function.support f ⊆ k) (h'f : Continuous f) : f = 0 ∨ LocallyCompactSpace G
• subset_interior_sub 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s t : Set G} : interior s - interior t ⊆ interior (s - t)
• IsClosed.add_closure_zero_eq 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {F : Set G} (hF : IsClosed F) : F + closure {0} = F
• IsOpen.add_closure_zero_eq 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {U : Set G} (hU : IsOpen U) : U + closure {0} = U
• IsCompact.add_closure_zero_eq_closure 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {K : Set G} (hK : IsCompact K) : K + closure {0} = closure K
• closure_subset_add_self_of_mem_nhds_zero 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {U : Set G} (hU : U ∈ nhds 0) : closure U ⊆ U + U
• IsTopologicalAddGroup.t2Space_of_zero_sep 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (H : ∀ (x : G), x ≠ 0 → ∃ U ∈ nhds 0, x ∉ U) : T2Space G
• closure_subset_add_left_of_mem_nhds_zero 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {U : Set G} (V : Set G) (hU : U ∈ nhds 0) : closure V ⊆ U + V
• closure_subset_add_right_of_mem_nhds_zero 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {V : Set G} (U : Set G) (hV : V ∈ nhds 0) : closure U ⊆ U + V
• IsOpen.add_closure 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s : Set G} (hs : IsOpen s) (t : Set G) : s + closure t = s + t
• IsOpen.closure_add 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {t : Set G} (ht : IsOpen t) (s : Set G) : closure s + t = s + t
• Filter.HasBasis.iInter_add_left_eq_closure 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {ι : Type u_1} {s : Set G} {p : ι → Prop} {U : ι → Set G} (hU : (nhds 0).HasBasis p U) : ⋂ i, ⋂ (_ : p i), U i + s = closure s
• Filter.HasBasis.iInter_add_right_eq_closure 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {ι : Type u_1} {s : Set G} {p : ι → Prop} {U : ι → Set G} (hU : (nhds 0).HasBasis p U) : ⋂ i, ⋂ (_ : p i), s + U i = closure s
• Filter.HasBasis.iInter_closure_add_left_eq_closure 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {ι : Type u_1} {s : Set G} {p : ι → Prop} {U : ι → Set G} (hU : (nhds 0).HasBasis p U) : ⋂ i, ⋂ (_ : p i), closure (U i + s) = closure s
• Filter.HasBasis.iInter_closure_add_right_eq_closure 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {ι : Type u_1} {s : Set G} {p : ι → Prop} {U : ι → Set G} (hU : (nhds 0).HasBasis p U) : ⋂ i, ⋂ (_ : p i), closure (s + U i) = closure s
• IsClosed.iInter_closure_add_left_eq 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {ι : Type u_1} {s : Set G} (hs : IsClosed s) {p : ι → Prop} {U : ι → Set G} (hU : (nhds 0).HasBasis p U) : ⋂ i, ⋂ (_ : p i), closure (U i + s) = s
• IsClosed.iInter_closure_add_right_eq 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {ι : Type u_1} {s : Set G} (hs : IsClosed s) {p : ι → Prop} {U : ι → Set G} (hU : (nhds 0).HasBasis p U) : ⋂ i, ⋂ (_ : p i), closure (s + U i) = s
• compl_add_closure_zero_eq 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {t : Set G} (ht : t + closure {0} = t) : tᶜ + closure {0} = tᶜ
• exists_closed_nhds_zero_neg_eq_add_subset 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {U : Set G} (hU : U ∈ nhds 0) : ∃ V ∈ nhds 0, IsClosed V ∧ -V = V ∧ V + V ⊆ U
• compl_add_closure_zero_eq_iff 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {t : Set G} : tᶜ + closure {0} = tᶜ ↔ t + closure {0} = t
• IsDiscrete.exists_nhds_eq_zero_of_image_addLeft_inter_nonempty 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (S : AddSubgroup G) (hS : IsDiscrete ↑S) : ∃ U ∈ nhds 0, -U = U ∧ ∀ g ∈ S, ((fun x => g + x) '' U ∩ U).Nonempty → g = 0
• IsDiscrete.exists_nhds_eq_zero_of_image_addRight_inter_nonempty 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (S : AddSubgroup G) (hS : IsDiscrete ↑S) : ∃ U ∈ nhds 0, -U = U ∧ ∀ g ∈ S, ((fun x => x + g) '' U ∩ U).Nonempty → g = 0
• QuotientAddGroup.instIsTopologicalAddGroup 📋 Mathlib.Topology.Algebra.Group.Quotient
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (N : AddSubgroup G) [N.Normal] : IsTopologicalAddGroup (G ⧸ N)
• QuotientAddGroup.instT3Space 📋 Mathlib.Topology.Algebra.Group.Quotient
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (N : AddSubgroup G) [N.Normal] [hN : IsClosed ↑N] : T3Space (G ⧸ N)
• QuotientAddGroup.isClosedMap_coe 📋 Mathlib.Topology.Algebra.Group.Quotient
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {H : AddSubgroup G} (hH : IsCompact ↑H) : IsClosedMap QuotientAddGroup.mk
• UniformEquiv.neg 📋 Mathlib.Topology.Algebra.IsUniformGroup.Basic
  (G : Type u_1) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] : G ≃ᵤ G
• IsTopologicalAddGroup.completeSpace_rightUniformSpace_iff_leftUniformSpace 📋 Mathlib.Topology.Algebra.IsUniformGroup.Basic
  (G : Type u_1) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] : CompleteSpace G ↔ CompleteSpace G
• AddOpposite.opUniformEquivLeft 📋 Mathlib.Topology.Algebra.IsUniformGroup.Basic
  (G : Type u_2) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] : G ≃ᵤ Gᵃᵒᵖ
• AddOpposite.opUniformEquivRight 📋 Mathlib.Topology.Algebra.IsUniformGroup.Basic
  (G : Type u_2) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] : G ≃ᵤ Gᵃᵒᵖ
• AddOpposite.comap_op_leftUniformSpace 📋 Mathlib.Topology.Algebra.IsUniformGroup.Basic
  (G : Type u_1) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] : UniformSpace.comap AddOpposite.op (IsTopologicalAddGroup.leftUniformSpace Gᵃᵒᵖ) = IsTopologicalAddGroup.rightUniformSpace G
• AddOpposite.comap_op_rightUniformSpace 📋 Mathlib.Topology.Algebra.IsUniformGroup.Basic
  (G : Type u_1) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] : UniformSpace.comap AddOpposite.op (IsTopologicalAddGroup.rightUniformSpace Gᵃᵒᵖ) = IsTopologicalAddGroup.leftUniformSpace G
• comap_neg_leftUniformSpace 📋 Mathlib.Topology.Algebra.IsUniformGroup.Basic
  (G : Type u_1) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] : UniformSpace.comap (⇑(Equiv.neg G)) (IsTopologicalAddGroup.leftUniformSpace G) = IsTopologicalAddGroup.rightUniformSpace G
• QuotientAddGroup.completeSpace_left' 📋 Mathlib.Topology.Algebra.IsUniformGroup.Basic
  (G : Type u) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [FirstCountableTopology G] (N : AddSubgroup G) [N.Normal] [hG : CompleteSpace G] : CompleteSpace (G ⧸ N)
• QuotientAddGroup.completeSpace_right' 📋 Mathlib.Topology.Algebra.IsUniformGroup.Basic
  (G : Type u) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [FirstCountableTopology G] (N : AddSubgroup G) [N.Normal] [CompleteSpace G] : CompleteSpace (G ⧸ N)
• AddSubgroup.isClosed_of_discrete 📋 Mathlib.Topology.Algebra.IsUniformGroup.Basic
  {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [T2Space G] {H : AddSubgroup G} [DiscreteTopology ↥H] : IsClosed ↑H
• AddSubgroup.tendsto_coe_cofinite_of_discrete 📋 Mathlib.Topology.Algebra.IsUniformGroup.Basic
  {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [T2Space G] (H : AddSubgroup G) (hH : IsDiscrete ↑H) : Filter.Tendsto Subtype.val Filter.cofinite (Filter.cocompact G)
• IsTopologicalAddGroup.tendstoUniformly_iff 📋 Mathlib.Topology.Algebra.IsUniformGroup.Basic
  {ι : Type u_1} {α : Type u_2} {G : Type u_3} [AddGroup G] [u : UniformSpace G] [IsTopologicalAddGroup G] (F : ι → α → G) (f : α → G) (p : Filter ι) (hu : IsTopologicalAddGroup.rightUniformSpace G = u) : TendstoUniformly F f p ↔ ∀ u_1 ∈ nhds 0, ∀ᶠ (i : ι) in p, ∀ (a : α), F i a - f a ∈ u_1
• IsTopologicalAddGroup.tendstoUniformlyOn_iff 📋 Mathlib.Topology.Algebra.IsUniformGroup.Basic
  {ι : Type u_1} {α : Type u_2} {G : Type u_3} [AddGroup G] [u : UniformSpace G] [IsTopologicalAddGroup G] (F : ι → α → G) (f : α → G) (p : Filter ι) (s : Set α) (hu : IsTopologicalAddGroup.rightUniformSpace G = u) : TendstoUniformlyOn F f p s ↔ ∀ u_1 ∈ nhds 0, ∀ᶠ (i : ι) in p, ∀ a ∈ s, F i a - f a ∈ u_1
• IsTopologicalAddGroup.tendstoLocallyUniformly_iff 📋 Mathlib.Topology.Algebra.IsUniformGroup.Basic
  {ι : Type u_1} {α : Type u_2} {G : Type u_3} [AddGroup G] [u : UniformSpace G] [IsTopologicalAddGroup G] [TopologicalSpace α] (F : ι → α → G) (f : α → G) (p : Filter ι) (hu : IsTopologicalAddGroup.rightUniformSpace G = u) : TendstoLocallyUniformly F f p ↔ ∀ u_1 ∈ nhds 0, ∀ (x : α), ∃ t ∈ nhds x, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a - f a ∈ u_1
• IsTopologicalAddGroup.uniformCauchySeqOn_iff 📋 Mathlib.Topology.Algebra.IsUniformGroup.Basic
  {ι : Type u_1} {α : Type u_2} {G : Type u_3} [AddGroup G] [u : UniformSpace G] [IsTopologicalAddGroup G] (F : ι → α → G) (p : Filter ι) (s : Set α) (hu : IsTopologicalAddGroup.rightUniformSpace G = u) : UniformCauchySeqOn F p s ↔ ∀ u_1 ∈ nhds 0, ∀ᶠ (m : ι × ι) in p ×ˢ p, ∀ a ∈ s, F m.2 a - F m.1 a ∈ u_1
• IsTopologicalAddGroup.tendstoLocallyUniformlyOn_iff 📋 Mathlib.Topology.Algebra.IsUniformGroup.Basic
  {ι : Type u_1} {α : Type u_2} {G : Type u_3} [AddGroup G] [u : UniformSpace G] [IsTopologicalAddGroup G] [TopologicalSpace α] (F : ι → α → G) (f : α → G) (p : Filter ι) (s : Set α) (hu : IsTopologicalAddGroup.rightUniformSpace G = u) : TendstoLocallyUniformlyOn F f p s ↔ ∀ u_1 ∈ nhds 0, ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a - f a ∈ u_1
• tendsto_sub_comap_self 📋 Mathlib.Topology.Algebra.IsUniformGroup.Basic
  {α : Type u_1} {β : Type u_2} {hom : Type u_3} [TopologicalSpace α] [AddGroup α] [IsTopologicalAddGroup α] [TopologicalSpace β] [AddGroup β] [FunLike hom β α] [AddMonoidHomClass hom β α] {e : hom} (de : IsDenseInducing ⇑e) (x₀ : α) : Filter.Tendsto (fun t => t.2 - t.1) (Filter.comap (fun p => (e p.1, e p.2)) (nhds (x₀, x₀))) (nhds 0)
• AddMonoidHom.tendsto_coe_cofinite_of_discrete 📋 Mathlib.Topology.Algebra.IsUniformGroup.Basic
  {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [T2Space G] {H : Type u_2} [AddGroup H] {f : H →+ G} (hf : Function.Injective ⇑f) (hf' : IsDiscrete ↑f.range) : Filter.Tendsto (⇑f) Filter.cofinite (Filter.cocompact G)
• IsDenseInducing.extend_Z_bilin 📋 Mathlib.Topology.Algebra.IsUniformGroup.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {G : Type u_5} [TopologicalSpace α] [AddCommGroup α] [IsTopologicalAddGroup α] [TopologicalSpace β] [AddCommGroup β] [TopologicalSpace γ] [AddCommGroup γ] [IsTopologicalAddGroup γ] [TopologicalSpace δ] [AddCommGroup δ] [UniformSpace G] [AddCommGroup G] {e : β →+ α} (de : IsDenseInducing ⇑e) {f : δ →+ γ} (df : IsDenseInducing ⇑f) {φ : β →+ δ →+ G} (hφ : Continuous fun p => (φ p.1) p.2) [IsUniformAddGroup G] [T0Space G] [CompleteSpace G] : Continuous (⋯.extend fun p => (φ p.1) p.2)
• ContinuousAddMonoidHom.instAddCommGroup 📋 Mathlib.Topology.Algebra.ContinuousMonoidHom
  (A : Type u_2) (E : Type u_6) [AddMonoid A] [TopologicalSpace A] [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] : AddCommGroup (A →ₜ+ E)
• ContinuousAddMonoidHom.neg 📋 Mathlib.Topology.Algebra.ContinuousMonoidHom
  (E : Type u_6) [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] : E →ₜ+ E
• ContinuousAddMonoidHom.neg_toFun 📋 Mathlib.Topology.Algebra.ContinuousMonoidHom
  (E : Type u_6) [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] (a✝ : E) : (ContinuousAddMonoidHom.neg E) a✝ = -a✝
• AddGroupTopology.mk 📋 Mathlib.Topology.Algebra.Group.GroupTopology
  {α : Type u} [AddGroup α] (toTopologicalSpace : TopologicalSpace α) (toIsTopologicalAddGroup : IsTopologicalAddGroup α) : AddGroupTopology α
• AddGroupTopology.toIsTopologicalAddGroup 📋 Mathlib.Topology.Algebra.Group.GroupTopology
  {α : Type u} [AddGroup α] (self : AddGroupTopology α) : IsTopologicalAddGroup α
• IsSemitopologicalRing.toIsTopologicalAddGroup 📋 Mathlib.Topology.Algebra.Ring.Basic
  {R : Type u_1} [NonUnitalNonAssocRing R] [TopologicalSpace R] [IsSemitopologicalRing R] : IsTopologicalAddGroup R
• IsTopologicalRing.isTopologicalAddGroup 📋 Mathlib.Topology.Algebra.Ring.Basic
  {R : Type u_1} [NonUnitalNonAssocRing R] [TopologicalSpace R] [IsTopologicalRing R] : IsTopologicalAddGroup R
• IsTopologicalRing.to_topologicalAddGroup 📋 Mathlib.Topology.Algebra.Ring.Basic
  {R : Type u_1} [NonUnitalNonAssocRing R] [TopologicalSpace R] [IsTopologicalRing R] : IsTopologicalAddGroup R
• IsTopologicalRing.of_addGroup_of_nhds_zero 📋 Mathlib.Topology.Algebra.Ring.Basic
  {R : Type u_2} [NonUnitalNonAssocRing R] [TopologicalSpace R] [IsTopologicalAddGroup R] (hmul : Filter.Tendsto (Function.uncurry fun x1 x2 => x1 * x2) (nhds 0 ×ˢ nhds 0) (nhds 0)) (hmul_left : ∀ (x₀ : R), Filter.Tendsto (fun x => x₀ * x) (nhds 0) (nhds 0)) (hmul_right : ∀ (x₀ : R), Filter.Tendsto (fun x => x * x₀) (nhds 0) (nhds 0)) : IsTopologicalRing R
• LinearOrderedAddCommGroup.toIsTopologicalAddGroup 📋 Mathlib.Topology.Algebra.Order.Group
  {G : Type u_1} [TopologicalSpace G] [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [OrderTopology G] : IsTopologicalAddGroup G
• IsTopologicalRing.of_norm 📋 Mathlib.Topology.Algebra.Order.Field
  {R : Type u_1} {𝕜 : Type u_2} [NonUnitalNonAssocRing R] [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace R] [IsTopologicalAddGroup R] (norm : R → 𝕜) (norm_nonneg : ∀ (x : R), 0 ≤ norm x) (norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y) (nhds_basis : (nhds 0).HasBasis (fun x => 0 < x) fun ε => {x | norm x < ε}) : IsTopologicalRing R
• Submodule.t3_quotient_of_isClosed 📋 Mathlib.Topology.Algebra.Module.Basic
  {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] (S : Submodule R M) [IsTopologicalAddGroup M] [IsClosed ↑S] : T3Space (M ⧸ S)
• Submodule.isTopologicalAddGroup_quotient 📋 Mathlib.Topology.Algebra.Module.Basic
  {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] (S : Submodule R M) [IsTopologicalAddGroup M] : IsTopologicalAddGroup (M ⧸ S)
• Submodule.topologicalAddGroup_quotient 📋 Mathlib.Topology.Algebra.Module.Basic
  {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] (S : Submodule R M) [IsTopologicalAddGroup M] : IsTopologicalAddGroup (M ⧸ S)
• Submodule.continuousSMul_quotient 📋 Mathlib.Topology.Algebra.Module.Basic
  {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] (S : Submodule R M) [TopologicalSpace R] [IsTopologicalAddGroup M] [ContinuousSMul R M] : ContinuousSMul R (M ⧸ S)
• Submodule.isTopologicalAddGroup 📋 Mathlib.Topology.Algebra.Module.Basic
  {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [IsTopologicalAddGroup M] (S : Submodule R M) : IsTopologicalAddGroup ↥S
• Submodule.topologicalAddGroup 📋 Mathlib.Topology.Algebra.Module.Basic
  {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [IsTopologicalAddGroup M] (S : Submodule R M) : IsTopologicalAddGroup ↥S
• ContinuousSMul.of_nhds_zero 📋 Mathlib.Topology.Algebra.Module.Basic
  {R : Type u_1} {M : Type u_2} [Ring R] [TopologicalSpace R] [TopologicalSpace M] [AddCommGroup M] [Module R M] [IsTopologicalRing R] [IsTopologicalAddGroup M] (hmul : Filter.Tendsto (fun p => p.1 • p.2) (nhds 0 ×ˢ nhds 0) (nhds 0)) (hmulleft : ∀ (m : M), Filter.Tendsto (fun a => a • m) (nhds 0) (nhds 0)) (hmulright : ∀ (a : R), Filter.Tendsto (fun m => a • m) (nhds 0) (nhds 0)) : ContinuousSMul R M
• ContinuousLinearMap.instIntCastIdOfIsTopologicalAddGroup 📋 Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
  {R : Type u_1} [Ring R] {M : Type u_4} [TopologicalSpace M] [AddCommGroup M] [Module R M] [IsTopologicalAddGroup M] : IntCast (M →L[R] M)
• ContinuousLinearMap.ring 📋 Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
  {R : Type u_1} [Ring R] {M : Type u_4} [TopologicalSpace M] [AddCommGroup M] [Module R M] [IsTopologicalAddGroup M] : Ring (M →L[R] M)
• ContinuousLinearMap.addCommGroup 📋 Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
  {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {M : Type u_4} [TopologicalSpace M] [AddCommGroup M] {M₂ : Type u_5} [TopologicalSpace M₂] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [IsTopologicalAddGroup M₂] : AddCommGroup (M →SL[σ₁₂] M₂)
• ContinuousLinearMap.neg 📋 Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
  {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {M : Type u_4} [TopologicalSpace M] [AddCommGroup M] {M₂ : Type u_5} [TopologicalSpace M₂] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [IsTopologicalAddGroup M₂] : Neg (M →SL[σ₁₂] M₂)

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