ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Inv G<VAR>ContinuousInv G<VAR>x : G<GOAL>ContinuousAt Inv.inv x
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Neg G<VAR>ContinuousNeg G<VAR>a : G<GOAL>Filter.Tendsto Neg.neg (𝓝 a) (𝓝 (-a))
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Inv G<VAR>ContinuousInv G<VAR>a : G<GOAL>Filter.Tendsto Inv.inv (𝓝 a) (𝓝 a⁻¹)
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>Inv G<VAR>ContinuousInv G<VAR>f : α → G<VAR>l : Filter α<VAR>y : G<VAR>h : Filter.Tendsto f l (𝓝 y)<GOAL>Filter.Tendsto (fun x => (f x)⁻¹) l (𝓝 y⁻¹)
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>Neg G<VAR>ContinuousNeg G<VAR>f : α → G<VAR>l : Filter α<VAR>y : G<VAR>h : Filter.Tendsto f l (𝓝 y)<GOAL>Filter.Tendsto (fun x => -f x) l (𝓝 (-y))
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>Inv G<VAR>ContinuousInv G<VAR>TopologicalSpace α<VAR>f : α → G<VAR>hf : Continuous f<GOAL>Continuous fun x => (f x)⁻¹
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>Neg G<VAR>ContinuousNeg G<VAR>TopologicalSpace α<VAR>f : α → G<VAR>hf : Continuous f<GOAL>Continuous fun x => -f x
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>Inv G<VAR>ContinuousInv G<VAR>TopologicalSpace α<VAR>f : α → G<VAR>x : α<VAR>hf : ContinuousAt f x<GOAL>ContinuousAt (fun x => (f x)⁻¹) x
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>Neg G<VAR>ContinuousNeg G<VAR>TopologicalSpace α<VAR>f : α → G<VAR>x : α<VAR>hf : ContinuousAt f x<GOAL>ContinuousAt (fun x => -f x) x
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>Inv G<VAR>ContinuousInv G<VAR>TopologicalSpace α<VAR>f : α → G<VAR>s : Set α<VAR>hf : ContinuousOn f s<GOAL>ContinuousOn (fun x => (f x)⁻¹) s
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>Neg G<VAR>ContinuousNeg G<VAR>TopologicalSpace α<VAR>f : α → G<VAR>s : Set α<VAR>hf : ContinuousOn f s<GOAL>ContinuousOn (fun x => -f x) s
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>Inv G<VAR>ContinuousInv G<VAR>TopologicalSpace α<VAR>f : α → G<VAR>s : Set α<VAR>x : α<VAR>hf : ContinuousWithinAt f s x<GOAL>ContinuousWithinAt (fun x => (f x)⁻¹) s x
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>Neg G<VAR>ContinuousNeg G<VAR>TopologicalSpace α<VAR>f : α → G<VAR>s : Set α<VAR>x : α<VAR>hf : ContinuousWithinAt f s x<GOAL>ContinuousWithinAt (fun x => -f x) s x
<VAR>G₁ : Type u_2<VAR>G₂ : Type u_3<VAR>TopologicalSpace G₂<VAR>T2Space G₂<VAR>Neg G₁<VAR>Neg G₂<VAR>ContinuousNeg G₂<GOAL>IsClosed {f | ∀ (x : G₁), f (-x) = -f x}
<VAR>G₁ : Type u_2<VAR>G₂ : Type u_3<VAR>TopologicalSpace G₂<VAR>T2Space G₂<VAR>Inv G₁<VAR>Inv G₂<VAR>ContinuousInv G₂<GOAL>IsClosed {f | ∀ (x : G₁), f x⁻¹ = (f x)⁻¹}
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>InvolutiveNeg G<VAR>ContinuousNeg G<VAR>s : Set G<VAR>hs : IsCompact s<GOAL>IsCompact (-s)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>InvolutiveInv G<VAR>ContinuousInv G<VAR>s : Set G<VAR>hs : IsCompact s<GOAL>IsCompact s⁻¹
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>InvolutiveNeg G<VAR>ContinuousNeg G<GOAL>⇑(Homeomorph.neg G) = Neg.neg
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>InvolutiveInv G<VAR>ContinuousInv G<GOAL>⇑(Homeomorph.inv G) = Inv.inv
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>InvolutiveInv G<VAR>ContinuousInv G<GOAL>IsOpenMap Inv.inv
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>InvolutiveNeg G<VAR>ContinuousNeg G<GOAL>IsOpenMap Neg.neg
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>InvolutiveNeg G<VAR>ContinuousNeg G<GOAL>IsClosedMap Neg.neg
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>InvolutiveInv G<VAR>ContinuousInv G<GOAL>IsClosedMap Inv.inv
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>InvolutiveInv G<VAR>ContinuousInv G<VAR>s : Set G<VAR>hs : IsOpen s<GOAL>IsOpen s⁻¹
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>InvolutiveNeg G<VAR>ContinuousNeg G<VAR>s : Set G<VAR>hs : IsOpen s<GOAL>IsOpen (-s)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>InvolutiveInv G<VAR>ContinuousInv G<VAR>s : Set G<VAR>hs : IsClosed s<GOAL>IsClosed s⁻¹
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>InvolutiveNeg G<VAR>ContinuousNeg G<VAR>s : Set G<VAR>hs : IsClosed s<GOAL>IsClosed (-s)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>InvolutiveNeg G<VAR>ContinuousNeg G<VAR>s : Set G<GOAL>-closure s = closure (-s)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>InvolutiveInv G<VAR>ContinuousInv G<VAR>s : Set G<GOAL>(closure s)⁻¹ = closure s⁻¹
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>InvolutiveNeg G<VAR>ContinuousNeg G<VAR>TopologicalSpace α<VAR>f : α → G<GOAL>Continuous (-f) ↔ Continuous f
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>InvolutiveInv G<VAR>ContinuousInv G<VAR>TopologicalSpace α<VAR>f : α → G<GOAL>Continuous f⁻¹ ↔ Continuous f
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>InvolutiveInv G<VAR>ContinuousInv G<VAR>TopologicalSpace α<VAR>f : α → G<VAR>x : α<GOAL>ContinuousAt f⁻¹ x ↔ ContinuousAt f x
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>InvolutiveNeg G<VAR>ContinuousNeg G<VAR>TopologicalSpace α<VAR>f : α → G<VAR>x : α<GOAL>ContinuousAt (-f) x ↔ ContinuousAt f x
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>InvolutiveInv G<VAR>ContinuousInv G<VAR>TopologicalSpace α<VAR>f : α → G<VAR>s : Set α<GOAL>ContinuousOn f⁻¹ s ↔ ContinuousOn f s
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>InvolutiveNeg G<VAR>ContinuousNeg G<VAR>TopologicalSpace α<VAR>f : α → G<VAR>s : Set α<GOAL>ContinuousOn (-f) s ↔ ContinuousOn f s
<VAR>G : Type w<VAR>Neg G<VAR>ts : Set (TopologicalSpace G)<VAR>h : ∀ t ∈ ts, ContinuousNeg G<GOAL>ContinuousNeg G
<VAR>G : Type w<VAR>Inv G<VAR>ts : Set (TopologicalSpace G)<VAR>h : ∀ t ∈ ts, ContinuousInv G<GOAL>ContinuousInv G
<VAR>G : Type w<VAR>ι' : Sort u_1<VAR>Neg G<VAR>ts' : ι' → TopologicalSpace G<VAR>h' : ∀ (i : ι'), ContinuousNeg G<GOAL>ContinuousNeg G
<VAR>G : Type w<VAR>ι' : Sort u_1<VAR>Inv G<VAR>ts' : ι' → TopologicalSpace G<VAR>h' : ∀ (i : ι'), ContinuousInv G<GOAL>ContinuousInv G
<VAR>G : Type w<VAR>Inv G<VAR>t₁ t₂ : TopologicalSpace G<VAR>h₁ : ContinuousInv G<VAR>h₂ : ContinuousInv G<GOAL>ContinuousInv G
<VAR>G : Type w<VAR>Neg G<VAR>t₁ t₂ : TopologicalSpace G<VAR>h₁ : ContinuousNeg G<VAR>h₂ : ContinuousNeg G<GOAL>ContinuousNeg G
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Neg G<VAR>Neg H<VAR>TopologicalSpace G<VAR>TopologicalSpace H<VAR>ContinuousNeg H<VAR>f : G → H<VAR>hf : Inducing f<VAR>hf_inv : ∀ (x : G), f (-x) = -f x<GOAL>ContinuousNeg G
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Inv G<VAR>Inv H<VAR>TopologicalSpace G<VAR>TopologicalSpace H<VAR>ContinuousInv H<VAR>f : G → H<VAR>hf : Inducing f<VAR>hf_inv : ∀ (x : G), f x⁻¹ = (f x)⁻¹<GOAL>ContinuousInv G
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Inv G<VAR>Mul G<VAR>ContinuousMul G<VAR>ContinuousInv G<GOAL>Continuous fun g => g.1 * g.2 * g.1⁻¹
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Neg G<VAR>Add G<VAR>ContinuousAdd G<VAR>ContinuousNeg G<GOAL>Continuous fun g => g.1 + g.2 + -g.1
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Neg G<VAR>Add G<VAR>ContinuousAdd G<VAR>g : G<GOAL>Continuous fun h => g + h + -g
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Inv G<VAR>Mul G<VAR>ContinuousMul G<VAR>g : G<GOAL>Continuous fun h => g * h * g⁻¹
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Inv G<VAR>Mul G<VAR>ContinuousMul G<VAR>ContinuousInv G<VAR>h : G<GOAL>Continuous fun g => g * h * g⁻¹
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Neg G<VAR>Add G<VAR>ContinuousAdd G<VAR>ContinuousNeg G<VAR>h : G<GOAL>Continuous fun g => g + h + -g
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>z : ℤ<GOAL>Continuous fun a => z • a
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>z : ℤ<GOAL>Continuous fun a => a ^ z
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>TopologicalSpace α<VAR>f : α → G<VAR>h : Continuous f<VAR>z : ℤ<GOAL>Continuous fun b => z • f b
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>TopologicalSpace α<VAR>f : α → G<VAR>h : Continuous f<VAR>z : ℤ<GOAL>Continuous fun b => f b ^ z
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>s : Set G<VAR>z : ℤ<GOAL>ContinuousOn (fun x => x ^ z) s
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>s : Set G<VAR>z : ℤ<GOAL>ContinuousOn (fun x => z • x) s
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>x : G<VAR>z : ℤ<GOAL>ContinuousAt (fun x => z • x) x
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>x : G<VAR>z : ℤ<GOAL>ContinuousAt (fun x => x ^ z) x
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>α : Type u_1<VAR>l : Filter α<VAR>f : α → G<VAR>x : G<VAR>hf : Filter.Tendsto f l (𝓝 x)<VAR>z : ℤ<GOAL>Filter.Tendsto (fun x => z • f x) l (𝓝 (z • x))
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>α : Type u_1<VAR>l : Filter α<VAR>f : α → G<VAR>x : G<VAR>hf : Filter.Tendsto f l (𝓝 x)<VAR>z : ℤ<GOAL>Filter.Tendsto (fun x => f x ^ z) l (𝓝 (x ^ z))
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>TopologicalSpace α<VAR>f : α → G<VAR>x : α<VAR>s : Set α<VAR>hf : ContinuousWithinAt f s x<VAR>z : ℤ<GOAL>ContinuousWithinAt (fun x => z • f x) s x
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>TopologicalSpace α<VAR>f : α → G<VAR>x : α<VAR>s : Set α<VAR>hf : ContinuousWithinAt f s x<VAR>z : ℤ<GOAL>ContinuousWithinAt (fun x => f x ^ z) s x
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>TopologicalSpace α<VAR>f : α → G<VAR>x : α<VAR>hf : ContinuousAt f x<VAR>z : ℤ<GOAL>ContinuousAt (fun x => f x ^ z) x
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>TopologicalSpace α<VAR>f : α → G<VAR>x : α<VAR>hf : ContinuousAt f x<VAR>z : ℤ<GOAL>ContinuousAt (fun x => z • f x) x
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>TopologicalSpace α<VAR>f : α → G<VAR>s : Set α<VAR>hf : ContinuousOn f s<VAR>z : ℤ<GOAL>ContinuousOn (fun x => z • f x) s
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>TopologicalSpace α<VAR>f : α → G<VAR>s : Set α<VAR>hf : ContinuousOn f s<VAR>z : ℤ<GOAL>ContinuousOn (fun x => f x ^ z) s
<VAR>H : Type x<VAR>TopologicalSpace H<VAR>OrderedCommGroup H<VAR>ContinuousInv H<VAR>a : H<GOAL>Filter.Tendsto Inv.inv (𝓝[>] a) (𝓝[<] a⁻¹)
<VAR>H : Type x<VAR>TopologicalSpace H<VAR>OrderedAddCommGroup H<VAR>ContinuousNeg H<VAR>a : H<GOAL>Filter.Tendsto Neg.neg (𝓝[>] a) (𝓝[<] (-a))
<VAR>H : Type x<VAR>TopologicalSpace H<VAR>OrderedAddCommGroup H<VAR>ContinuousNeg H<VAR>a : H<GOAL>Filter.Tendsto Neg.neg (𝓝[<] a) (𝓝[>] (-a))
<VAR>H : Type x<VAR>TopologicalSpace H<VAR>OrderedCommGroup H<VAR>ContinuousInv H<VAR>a : H<GOAL>Filter.Tendsto Inv.inv (𝓝[<] a) (𝓝[>] a⁻¹)
<VAR>H : Type x<VAR>TopologicalSpace H<VAR>OrderedAddCommGroup H<VAR>ContinuousNeg H<VAR>a : H<GOAL>Filter.Tendsto Neg.neg (𝓝[>] (-a)) (𝓝[<] a)
<VAR>H : Type x<VAR>TopologicalSpace H<VAR>OrderedCommGroup H<VAR>ContinuousInv H<VAR>a : H<GOAL>Filter.Tendsto Inv.inv (𝓝[>] a⁻¹) (𝓝[<] a)
<VAR>H : Type x<VAR>TopologicalSpace H<VAR>OrderedAddCommGroup H<VAR>ContinuousNeg H<VAR>a : H<GOAL>Filter.Tendsto Neg.neg (𝓝[<] (-a)) (𝓝[>] a)
<VAR>H : Type x<VAR>TopologicalSpace H<VAR>OrderedCommGroup H<VAR>ContinuousInv H<VAR>a : H<GOAL>Filter.Tendsto Inv.inv (𝓝[<] a⁻¹) (𝓝[>] a)
<VAR>H : Type x<VAR>TopologicalSpace H<VAR>OrderedAddCommGroup H<VAR>ContinuousNeg H<VAR>a : H<GOAL>Filter.Tendsto Neg.neg (𝓝[≥] a) (𝓝[≤] (-a))
<VAR>H : Type x<VAR>TopologicalSpace H<VAR>OrderedCommGroup H<VAR>ContinuousInv H<VAR>a : H<GOAL>Filter.Tendsto Inv.inv (𝓝[≥] a) (𝓝[≤] a⁻¹)
<VAR>H : Type x<VAR>TopologicalSpace H<VAR>OrderedAddCommGroup H<VAR>ContinuousNeg H<VAR>a : H<GOAL>Filter.Tendsto Neg.neg (𝓝[≤] a) (𝓝[≥] (-a))
<VAR>H : Type x<VAR>TopologicalSpace H<VAR>OrderedCommGroup H<VAR>ContinuousInv H<VAR>a : H<GOAL>Filter.Tendsto Inv.inv (𝓝[≤] a) (𝓝[≥] a⁻¹)
<VAR>H : Type x<VAR>TopologicalSpace H<VAR>OrderedAddCommGroup H<VAR>ContinuousNeg H<VAR>a : H<GOAL>Filter.Tendsto Neg.neg (𝓝[≥] (-a)) (𝓝[≤] a)
<VAR>H : Type x<VAR>TopologicalSpace H<VAR>OrderedCommGroup H<VAR>ContinuousInv H<VAR>a : H<GOAL>Filter.Tendsto Inv.inv (𝓝[≥] a⁻¹) (𝓝[≤] a)
<VAR>H : Type x<VAR>TopologicalSpace H<VAR>OrderedCommGroup H<VAR>ContinuousInv H<VAR>a : H<GOAL>Filter.Tendsto Inv.inv (𝓝[≤] a⁻¹) (𝓝[≥] a)
<VAR>H : Type x<VAR>TopologicalSpace H<VAR>OrderedAddCommGroup H<VAR>ContinuousNeg H<VAR>a : H<GOAL>Filter.Tendsto Neg.neg (𝓝[≤] (-a)) (𝓝[≥] a)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<GOAL>Filter.comap Neg.neg (𝓝 0) = 𝓝 0
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<GOAL>Filter.comap Inv.inv (𝓝 1) = 𝓝 1
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<GOAL>Filter.map Inv.inv (𝓝 1) = 𝓝 1
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<GOAL>Filter.map Neg.neg (𝓝 0) = 𝓝 0
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>S : Set G<VAR>hS : S ∈ 𝓝 1<GOAL>S⁻¹ ∈ 𝓝 1
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>S : Set G<VAR>hS : S ∈ 𝓝 0<GOAL>-S ∈ 𝓝 0
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<GOAL>⇑(Homeomorph.shearMulRight G) = fun z => (z.1, z.1 * z.2)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<GOAL>⇑(Homeomorph.shearAddRight G) = fun z => (z.1, z.1 + z.2)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<GOAL>⇑(Homeomorph.shearMulRight G).symm = fun z => (z.1, z.1⁻¹ * z.2)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<GOAL>⇑(Homeomorph.shearAddRight G).symm = fun z => (z.1, -z.1 + z.2)
<VAR>G : Type w<VAR>H : Type x<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>F : Type u_1<VAR>Group H<VAR>TopologicalSpace H<VAR>FunLike F H G<VAR>MonoidHomClass F H G<VAR>f : F<VAR>hf : Inducing ⇑f<GOAL>TopologicalGroup H
<VAR>G : Type w<VAR>H : Type x<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>F : Type u_1<VAR>AddGroup H<VAR>TopologicalSpace H<VAR>FunLike F H G<VAR>AddMonoidHomClass F H G<VAR>f : F<VAR>hf : Inducing ⇑f<GOAL>TopologicalAddGroup H
<VAR>G : Type w<VAR>H : Type x<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>F : Type u_1<VAR>Group H<VAR>FunLike F H G<VAR>MonoidHomClass F H G<VAR>f : F<GOAL>TopologicalGroup H
<VAR>G : Type w<VAR>H : Type x<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>F : Type u_1<VAR>AddGroup H<VAR>FunLike F H G<VAR>AddMonoidHomClass F H G<VAR>f : F<GOAL>TopologicalAddGroup H
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>s : AddSubgroup G<GOAL>↑s.topologicalClosure = closure ↑s
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>s : Subgroup G<GOAL>↑s.topologicalClosure = closure ↑s
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>s : Subgroup G<GOAL>s ≤ s.topologicalClosure
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>s : AddSubgroup G<GOAL>s ≤ s.topologicalClosure
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>s : Subgroup G<GOAL>IsClosed ↑s.topologicalClosure
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>s : AddSubgroup G<GOAL>IsClosed ↑s.topologicalClosure
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>s : Subgroup G<VAR>t : Subgroup G<VAR>h : s ≤ t<VAR>ht : IsClosed ↑t<GOAL>s.topologicalClosure ≤ t
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>s : AddSubgroup G<VAR>t : AddSubgroup G<VAR>h : s ≤ t<VAR>ht : IsClosed ↑t<GOAL>s.topologicalClosure ≤ t
<VAR>G : Type w<VAR>H : Type x<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>AddGroup H<VAR>TopologicalSpace H<VAR>TopologicalAddGroup H<VAR>f : G →+ H<VAR>hf : Continuous ⇑f<VAR>hf' : DenseRange ⇑f<VAR>s : AddSubgroup G<VAR>hs : s.topologicalClosure = ⊤<GOAL>(AddSubgroup.map f s).topologicalClosure = ⊤
<VAR>G : Type w<VAR>H : Type x<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>Group H<VAR>TopologicalSpace H<VAR>TopologicalGroup H<VAR>f : G →* H<VAR>hf : Continuous ⇑f<VAR>hf' : DenseRange ⇑f<VAR>s : Subgroup G<VAR>hs : s.topologicalClosure = ⊤<GOAL>(Subgroup.map f s).topologicalClosure = ⊤
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>N : AddSubgroup G<VAR>N.Normal<GOAL>N.topologicalClosure.Normal
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>N : Subgroup G<VAR>N.Normal<GOAL>N.topologicalClosure.Normal
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>MulOneClass G<VAR>ContinuousMul G<VAR>g h : G<VAR>hg : g ∈ connectedComponent 1<VAR>hh : h ∈ connectedComponent 1<GOAL>g * h ∈ connectedComponent 1
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>AddZeroClass G<VAR>ContinuousAdd G<VAR>g h : G<VAR>hg : g ∈ connectedComponent 0<VAR>hh : h ∈ connectedComponent 0<GOAL>g + h ∈ connectedComponent 0
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>g : G<VAR>hg : g ∈ connectedComponent 1<GOAL>g⁻¹ ∈ connectedComponent 1
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>g : G<VAR>hg : g ∈ connectedComponent 0<GOAL>-g ∈ connectedComponent 0
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<GOAL>↑⊥.topologicalClosure = closure {0}
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<GOAL>↑⊥.topologicalClosure = closure {1}
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>s : Set G<VAR>hs : s ∈ 𝓝 1<GOAL>∃ V ∈ 𝓝 1, ∀ v ∈ V, ∀ w ∈ V, v / w ∈ s
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>s : Set G<VAR>hs : s ∈ 𝓝 0<GOAL>∃ V ∈ 𝓝 0, ∀ v ∈ V, ∀ w ∈ V, v - w ∈ s
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>x : G<GOAL>Filter.comap (fun x_1 => x_1 + -x) (𝓝 0) = 𝓝 x
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>x : G<GOAL>Filter.comap (fun x_1 => x_1 * x⁻¹) (𝓝 1) = 𝓝 x
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>x y : G<GOAL>Filter.map (fun x_1 => x + x_1) (𝓝 y) = 𝓝 (x + y)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>x y : G<GOAL>Filter.map (fun x_1 => x * x_1) (𝓝 y) = 𝓝 (x * y)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>x : G<GOAL>Filter.map (fun x_1 => x * x_1) (𝓝 1) = 𝓝 x
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>x : G<GOAL>Filter.map (fun x_1 => x + x_1) (𝓝 0) = 𝓝 x
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>x y : G<GOAL>Filter.map (fun x_1 => x_1 * x) (𝓝 y) = 𝓝 (y * x)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>x y : G<GOAL>Filter.map (fun x_1 => x_1 + x) (𝓝 y) = 𝓝 (y + x)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>x : G<GOAL>Filter.map (fun x_1 => x_1 * x) (𝓝 1) = 𝓝 x
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>x : G<GOAL>Filter.map (fun x_1 => x_1 + x) (𝓝 0) = 𝓝 x
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>ι : Sort u_1<VAR>p : ι → Prop<VAR>s : ι → Set G<VAR>hb : (𝓝 1).HasBasis p s<VAR>x : G<GOAL>(𝓝 x).HasBasis p fun i => {y | y / x ∈ s i}
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>ι : Sort u_1<VAR>p : ι → Prop<VAR>s : ι → Set G<VAR>hb : (𝓝 0).HasBasis p s<VAR>x : G<GOAL>(𝓝 x).HasBasis p fun i => {y | y - x ∈ s i}
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>x : G<VAR>s : Set G<GOAL>x ∈ closure s ↔ ∀ U ∈ 𝓝 0, ∃ y ∈ s, y - x ∈ U
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>x : G<VAR>s : Set G<GOAL>x ∈ closure s ↔ ∀ U ∈ 𝓝 1, ∃ y ∈ s, y / x ∈ U
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>M : Type u_1<VAR>hom : Type u_2<VAR>AddZeroClass M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>FunLike hom G M<VAR>AddMonoidHomClass hom G M<VAR>f : hom<VAR>hf : ContinuousAt (⇑f) 0<GOAL>Continuous ⇑f
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>M : Type u_1<VAR>hom : Type u_2<VAR>MulOneClass M<VAR>TopologicalSpace M<VAR>ContinuousMul M<VAR>FunLike hom G M<VAR>MonoidHomClass hom G M<VAR>f : hom<VAR>hf : ContinuousAt (⇑f) 1<GOAL>Continuous ⇑f
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>H : Type u_1<VAR>M : Type u_2<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousMul M<VAR>Group H<VAR>TopologicalSpace H<VAR>TopologicalGroup H<VAR>f : G →* H →* M<VAR>hf : ContinuousAt (fun x => (f x.1) x.2) (1, 1)<VAR>hl : ∀ (x : G), ContinuousAt (⇑(f x)) 1<VAR>hr : ∀ (y : H), ContinuousAt (fun x => (f x) y) 1<GOAL>Continuous fun x => (f x.1) x.2
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>H : Type u_1<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>AddGroup H<VAR>TopologicalSpace H<VAR>TopologicalAddGroup H<VAR>f : G →+ H →+ M<VAR>hf : ContinuousAt (fun x => (f x.1) x.2) (0, 0)<VAR>hl : ∀ (x : G), ContinuousAt (⇑(f x)) 0<VAR>hr : ∀ (y : H), ContinuousAt (fun x => (f x) y) 0<GOAL>Continuous fun x => (f x.1) x.2
<VAR>G : Type u_1<VAR>Group G<VAR>t t' : TopologicalSpace G<VAR>tg : TopologicalGroup G<VAR>tg' : TopologicalGroup G<VAR>h : 𝓝 1 = 𝓝 1<GOAL>t = t'
<VAR>G : Type u_1<VAR>AddGroup G<VAR>t t' : TopologicalSpace G<VAR>tg : TopologicalAddGroup G<VAR>tg' : TopologicalAddGroup G<VAR>h : 𝓝 0 = 𝓝 0<GOAL>t = t'
<VAR>G : Type u_1<VAR>AddGroup G<VAR>t t' : TopologicalSpace G<VAR>tg : TopologicalAddGroup G<VAR>tg' : TopologicalAddGroup G<GOAL>t = t' ↔ 𝓝 0 = 𝓝 0
<VAR>G : Type u_1<VAR>Group G<VAR>t t' : TopologicalSpace G<VAR>tg : TopologicalGroup G<VAR>tg' : TopologicalGroup G<GOAL>t = t' ↔ 𝓝 1 = 𝓝 1
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>hinv : Filter.Tendsto (fun x => -x) (𝓝 0) (𝓝 0)<VAR>hleft : ∀ (x₀ : G), 𝓝 x₀ = Filter.map (fun x => x₀ + x) (𝓝 0)<VAR>hconj : ∀ (x₀ : G), Filter.Tendsto (fun x => x₀ + x + -x₀) (𝓝 0) (𝓝 0)<GOAL>ContinuousNeg G
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>hinv : Filter.Tendsto (fun x => x⁻¹) (𝓝 1) (𝓝 1)<VAR>hleft : ∀ (x₀ : G), 𝓝 x₀ = Filter.map (fun x => x₀ * x) (𝓝 1)<VAR>hconj : ∀ (x₀ : G), Filter.Tendsto (fun x => x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)<GOAL>ContinuousInv G
<VAR>G : Type u<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>hmul : Filter.Tendsto (Function.uncurry fun x x_1 => x + x_1) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)<VAR>hinv : Filter.Tendsto (fun x => -x) (𝓝 0) (𝓝 0)<VAR>hleft : ∀ (x₀ : G), 𝓝 x₀ = Filter.map (fun x => x₀ + x) (𝓝 0)<VAR>hright : ∀ (x₀ : G), 𝓝 x₀ = Filter.map (fun x => x + x₀) (𝓝 0)<GOAL>TopologicalAddGroup G
<VAR>G : Type u<VAR>Group G<VAR>TopologicalSpace G<VAR>hmul : Filter.Tendsto (Function.uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)<VAR>hinv : Filter.Tendsto (fun x => x⁻¹) (𝓝 1) (𝓝 1)<VAR>hleft : ∀ (x₀ : G), 𝓝 x₀ = Filter.map (fun x => x₀ * x) (𝓝 1)<VAR>hright : ∀ (x₀ : G), 𝓝 x₀ = Filter.map (fun x => x * x₀) (𝓝 1)<GOAL>TopologicalGroup G
<VAR>G : Type u<VAR>Group G<VAR>TopologicalSpace G<VAR>hmul : Filter.Tendsto (Function.uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)<VAR>hinv : Filter.Tendsto (fun x => x⁻¹) (𝓝 1) (𝓝 1)<VAR>hleft : ∀ (x₀ : G), 𝓝 x₀ = Filter.map (fun x => x₀ * x) (𝓝 1)<VAR>hconj : ∀ (x₀ : G), Filter.Tendsto (fun x => x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)<GOAL>TopologicalGroup G
<VAR>G : Type u<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>hmul : Filter.Tendsto (Function.uncurry fun x x_1 => x + x_1) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)<VAR>hinv : Filter.Tendsto (fun x => -x) (𝓝 0) (𝓝 0)<VAR>hleft : ∀ (x₀ : G), 𝓝 x₀ = Filter.map (fun x => x₀ + x) (𝓝 0)<VAR>hconj : ∀ (x₀ : G), Filter.Tendsto (fun x => x₀ + x + -x₀) (𝓝 0) (𝓝 0)<GOAL>TopologicalAddGroup G