ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u<VAR>CommGroup 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)<GOAL>TopologicalGroup G
<VAR>G : Type u<VAR>AddCommGroup 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)<GOAL>TopologicalAddGroup G
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>N : AddSubgroup G<GOAL>IsOpenMap QuotientAddGroup.mk
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>N : Subgroup G<GOAL>IsOpenMap QuotientGroup.mk
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>N : Subgroup G<VAR>x : G<GOAL>𝓝 ↑x = Filter.map QuotientGroup.mk (𝓝 x)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>N : AddSubgroup G<VAR>x : G<GOAL>𝓝 ↑x = Filter.map QuotientAddGroup.mk (𝓝 x)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>FirstCountableTopology G<GOAL>∃ u, (𝓝 0).HasAntitoneBasis u ∧ ∀ (n : ℕ), u (n + 1) + u (n + 1) ⊆ u n
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>FirstCountableTopology G<GOAL>∃ u, (𝓝 1).HasAntitoneBasis u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>Sub G<VAR>self : ContinuousSub G<GOAL>Continuous fun p => p.1 - p.2
<VAR>G : Type u_1<VAR>TopologicalSpace G<VAR>Div G<VAR>self : ContinuousDiv G<GOAL>Continuous fun p => p.1 / p.2
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>Div G<VAR>ContinuousDiv G<VAR>f g : α → G<VAR>l : Filter α<VAR>a b : G<VAR>hf : Filter.Tendsto f l (𝓝 a)<VAR>hg : Filter.Tendsto g l (𝓝 b)<GOAL>Filter.Tendsto (fun x => f x / g x) l (𝓝 (a / b))
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>Sub G<VAR>ContinuousSub G<VAR>f g : α → G<VAR>l : Filter α<VAR>a b : G<VAR>hf : Filter.Tendsto f l (𝓝 a)<VAR>hg : Filter.Tendsto g l (𝓝 b)<GOAL>Filter.Tendsto (fun x => f x - g x) l (𝓝 (a - b))
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>Div G<VAR>ContinuousDiv G<VAR>b : G<VAR>c : G<VAR>f : α → G<VAR>l : Filter α<VAR>h : Filter.Tendsto f l (𝓝 c)<GOAL>Filter.Tendsto (fun k => b / f k) l (𝓝 (b / c))
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>Sub G<VAR>ContinuousSub G<VAR>b : G<VAR>c : G<VAR>f : α → G<VAR>l : Filter α<VAR>h : Filter.Tendsto f l (𝓝 c)<GOAL>Filter.Tendsto (fun k => b - f k) l (𝓝 (b - c))
<VAR>α : Type u<VAR>G : Type u_1<VAR>CommGroup G<VAR>TopologicalSpace G<VAR>ContinuousDiv G<VAR>b : G<VAR>c : G<VAR>f : α → G<VAR>l : Filter α<GOAL>Filter.Tendsto (fun k => b / f k) l (𝓝 (b / c)) ↔ Filter.Tendsto f l (𝓝 c)
<VAR>α : Type u<VAR>G : Type u_1<VAR>AddCommGroup G<VAR>TopologicalSpace G<VAR>ContinuousSub G<VAR>b : G<VAR>c : G<VAR>f : α → G<VAR>l : Filter α<GOAL>Filter.Tendsto (fun k => b - f k) l (𝓝 (b - c)) ↔ Filter.Tendsto f l (𝓝 c)
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>Div G<VAR>ContinuousDiv G<VAR>c : G<VAR>f : α → G<VAR>l : Filter α<VAR>h : Filter.Tendsto f l (𝓝 c)<VAR>b : G<GOAL>Filter.Tendsto (fun x => f x / b) l (𝓝 (c / b))
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>Sub G<VAR>ContinuousSub G<VAR>c : G<VAR>f : α → G<VAR>l : Filter α<VAR>h : Filter.Tendsto f l (𝓝 c)<VAR>b : G<GOAL>Filter.Tendsto (fun x => f x - b) l (𝓝 (c - b))
<VAR>α : Type u<VAR>G : Type u_1<VAR>CommGroupWithZero G<VAR>TopologicalSpace G<VAR>ContinuousDiv G<VAR>b : G<VAR>hb : b ≠ 0<VAR>c : G<VAR>f : α → G<VAR>l : Filter α<GOAL>Filter.Tendsto (fun x => f x / b) l (𝓝 (c / b)) ↔ Filter.Tendsto f l (𝓝 c)
<VAR>α : Type u<VAR>G : Type u_1<VAR>AddCommGroup G<VAR>TopologicalSpace G<VAR>ContinuousSub G<VAR>b : G<VAR>c : G<VAR>f : α → G<VAR>l : Filter α<GOAL>Filter.Tendsto (fun x => f x - b) l (𝓝 (c - b)) ↔ Filter.Tendsto f l (𝓝 c)
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>Div G<VAR>ContinuousDiv G<VAR>TopologicalSpace α<VAR>f g : α → G<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous fun x => f x / g x
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>Sub G<VAR>ContinuousSub G<VAR>TopologicalSpace α<VAR>f g : α → G<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous fun x => f x - g x
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Sub G<VAR>ContinuousSub G<VAR>a : G<GOAL>Continuous fun x => a - x
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Div G<VAR>ContinuousDiv G<VAR>a : G<GOAL>Continuous fun x => a / x
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Div G<VAR>ContinuousDiv G<VAR>a : G<GOAL>Continuous fun x => x / a
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Sub G<VAR>ContinuousSub G<VAR>a : G<GOAL>Continuous fun x => x - a
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>Sub G<VAR>ContinuousSub G<VAR>TopologicalSpace α<VAR>f g : α → G<VAR>x : α<VAR>hf : ContinuousAt f x<VAR>hg : ContinuousAt g x<GOAL>ContinuousAt (fun x => f x - g x) x
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>Div G<VAR>ContinuousDiv G<VAR>TopologicalSpace α<VAR>f g : α → G<VAR>x : α<VAR>hf : ContinuousAt f x<VAR>hg : ContinuousAt g x<GOAL>ContinuousAt (fun x => f x / g x) x
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>Sub G<VAR>ContinuousSub G<VAR>TopologicalSpace α<VAR>f g : α → G<VAR>s : Set α<VAR>x : α<VAR>hf : ContinuousWithinAt f s x<VAR>hg : ContinuousWithinAt g s x<GOAL>ContinuousWithinAt (fun x => f x - g x) s x
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>Div G<VAR>ContinuousDiv G<VAR>TopologicalSpace α<VAR>f g : α → G<VAR>s : Set α<VAR>x : α<VAR>hf : ContinuousWithinAt f s x<VAR>hg : ContinuousWithinAt g s x<GOAL>ContinuousWithinAt (fun x => f x / g x) s x
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>Sub G<VAR>ContinuousSub G<VAR>TopologicalSpace α<VAR>f g : α → G<VAR>s : Set α<VAR>hf : ContinuousOn f s<VAR>hg : ContinuousOn g s<GOAL>ContinuousOn (fun x => f x - g x) s
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>Div G<VAR>ContinuousDiv G<VAR>TopologicalSpace α<VAR>f g : α → G<VAR>s : Set α<VAR>hf : ContinuousOn f s<VAR>hg : ContinuousOn g s<GOAL>ContinuousOn (fun x => f x / g x) s
<VAR>G : Type w<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>x b : G<GOAL>(Homeomorph.subLeft x).symm b = -b + x
<VAR>G : Type w<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>x b : G<GOAL>(Homeomorph.subLeft x) b = x - b
<VAR>G : Type w<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>x b : G<GOAL>(Homeomorph.divLeft x) b = x / b
<VAR>G : Type w<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>x b : G<GOAL>(Homeomorph.divLeft x).symm b = b⁻¹ * x
<VAR>G : Type w<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>a : G<GOAL>IsOpenMap fun x => a - x
<VAR>G : Type w<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>a : G<GOAL>IsOpenMap fun x => a / x
<VAR>G : Type w<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>a : G<GOAL>IsClosedMap fun x => a - x
<VAR>G : Type w<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>a : G<GOAL>IsClosedMap fun x => a / x
<VAR>G : Type w<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>x b : G<GOAL>(Homeomorph.divRight x) b = b / x
<VAR>G : Type w<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>x b : G<GOAL>(Homeomorph.divRight x).symm b = b * x
<VAR>G : Type w<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>x b : G<GOAL>(Homeomorph.subRight x).symm b = b + x
<VAR>G : Type w<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>x b : G<GOAL>(Homeomorph.subRight x) b = b - x
<VAR>G : Type w<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>a : G<GOAL>IsOpenMap fun x => x / a
<VAR>G : Type w<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>a : G<GOAL>IsOpenMap fun x => x - a
<VAR>G : Type w<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>a : G<GOAL>IsClosedMap fun x => x - a
<VAR>G : Type w<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>a : G<GOAL>IsClosedMap fun x => x / a
<VAR>G : Type w<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>α : Type u_1<VAR>l : Filter α<VAR>x : G<VAR>u : α → G<GOAL>Filter.Tendsto (fun x_1 => u x_1 - x) l (𝓝 0) ↔ Filter.Tendsto u l (𝓝 x)
<VAR>G : Type w<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>α : Type u_1<VAR>l : Filter α<VAR>x : G<VAR>u : α → G<GOAL>Filter.Tendsto (fun x_1 => u x_1 / x) l (𝓝 1) ↔ Filter.Tendsto u l (𝓝 x)
<VAR>G : Type w<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>x : G<GOAL>Filter.comap (fun x_1 => x_1 / x) (𝓝 1) = 𝓝 x
<VAR>G : Type w<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>x : G<GOAL>Filter.comap (fun x_1 => x_1 - x) (𝓝 0) = 𝓝 x
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace β<VAR>AddGroup α<VAR>AddAction α β<VAR>ContinuousConstVAdd α β<VAR>s : Set α<VAR>t : Set β<VAR>ht : IsOpen t<GOAL>IsOpen (s +ᵥ t)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace β<VAR>Group α<VAR>MulAction α β<VAR>ContinuousConstSMul α β<VAR>s : Set α<VAR>t : Set β<VAR>ht : IsOpen t<GOAL>IsOpen (s • t)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace β<VAR>AddGroup α<VAR>AddAction α β<VAR>ContinuousConstVAdd α β<VAR>s : Set α<VAR>t : Set β<GOAL>s +ᵥ interior t ⊆ interior (s +ᵥ t)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace β<VAR>Group α<VAR>MulAction α β<VAR>ContinuousConstSMul α β<VAR>s : Set α<VAR>t : Set β<GOAL>s • interior t ⊆ interior (s • t)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace β<VAR>AddGroup α<VAR>AddAction α β<VAR>ContinuousConstVAdd α β<VAR>t : Set β<VAR>a : α<VAR>x : β<VAR>ht : t ∈ 𝓝 x<GOAL>a +ᵥ t ∈ 𝓝 (a +ᵥ x)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace β<VAR>Group α<VAR>MulAction α β<VAR>ContinuousConstSMul α β<VAR>t : Set β<VAR>a : α<VAR>x : β<VAR>ht : t ∈ 𝓝 x<GOAL>a • t ∈ 𝓝 (a • x)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace β<VAR>AddGroup α<VAR>AddAction α β<VAR>ContinuousConstVAdd α β<VAR>s : Set α<VAR>t : Set β<VAR>TopologicalSpace α<GOAL>interior s +ᵥ interior t ⊆ interior (s +ᵥ t)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace β<VAR>Group α<VAR>MulAction α β<VAR>ContinuousConstSMul α β<VAR>s : Set α<VAR>t : Set β<VAR>TopologicalSpace α<GOAL>interior s • interior t ⊆ interior (s • t)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>AddGroup α<VAR>AddAction α β<VAR>ContinuousNeg α<VAR>ContinuousVAdd α β<VAR>s : Set α<VAR>t : Set β<VAR>ht : IsClosed t<VAR>hs : IsCompact s<GOAL>IsClosed (s +ᵥ t)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Group α<VAR>MulAction α β<VAR>ContinuousInv α<VAR>ContinuousSMul α β<VAR>s : Set α<VAR>t : Set β<VAR>ht : IsClosed t<VAR>hs : IsCompact s<GOAL>IsClosed (s • t)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>AddGroup α<VAR>AddAction α β<VAR>ContinuousNeg α<VAR>ContinuousVAdd α β<VAR>CompactSpace α<GOAL>IsClosedMap Quotient.mk'
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Group α<VAR>MulAction α β<VAR>ContinuousInv α<VAR>ContinuousSMul α β<VAR>CompactSpace α<GOAL>IsClosedMap Quotient.mk'
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>AddGroup α<VAR>ContinuousConstVAdd α α<VAR>s t : Set α<GOAL>IsOpen t → IsOpen (s + t)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Group α<VAR>ContinuousConstSMul α α<VAR>s t : Set α<GOAL>IsOpen t → IsOpen (s * t)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>AddGroup α<VAR>ContinuousConstVAdd α α<VAR>s t : Set α<GOAL>s + interior t ⊆ interior (s + t)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Group α<VAR>ContinuousConstSMul α α<VAR>s t : Set α<GOAL>s * interior t ⊆ interior (s * t)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>AddGroup α<VAR>ContinuousConstVAdd α α<VAR>s t : Set α<GOAL>interior s + interior t ⊆ interior (s + t)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Group α<VAR>ContinuousConstSMul α α<VAR>s t : Set α<GOAL>interior s * interior t ⊆ interior (s * t)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Group α<VAR>ContinuousConstSMul α α<VAR>s : Set α<VAR>a : α<VAR>b : α<VAR>h : s ∈ 𝓝 b<GOAL>{a} * s ∈ 𝓝 (a * b)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>AddGroup α<VAR>ContinuousConstVAdd α α<VAR>s : Set α<VAR>a : α<VAR>b : α<VAR>h : s ∈ 𝓝 b<GOAL>{a} + s ∈ 𝓝 (a + b)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Group α<VAR>ContinuousConstSMul α α<VAR>s : Set α<VAR>a : α<VAR>h : s ∈ 𝓝 1<GOAL>{a} * s ∈ 𝓝 a
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>AddGroup α<VAR>ContinuousConstVAdd α α<VAR>s : Set α<VAR>a : α<VAR>h : s ∈ 𝓝 0<GOAL>{a} + s ∈ 𝓝 a
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>AddGroup α<VAR>ContinuousConstVAdd αᵃᵒᵖ α<VAR>s t : Set α<VAR>hs : IsOpen s<GOAL>IsOpen (s + t)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Group α<VAR>ContinuousConstSMul αᵐᵒᵖ α<VAR>s t : Set α<VAR>hs : IsOpen s<GOAL>IsOpen (s * t)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>AddGroup α<VAR>ContinuousConstVAdd αᵃᵒᵖ α<VAR>s t : Set α<GOAL>interior s + t ⊆ interior (s + t)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Group α<VAR>ContinuousConstSMul αᵐᵒᵖ α<VAR>s t : Set α<GOAL>interior s * t ⊆ interior (s * t)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>AddGroup α<VAR>ContinuousConstVAdd αᵃᵒᵖ α<VAR>s t : Set α<GOAL>interior s + interior t ⊆ interior (s + t)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Group α<VAR>ContinuousConstSMul αᵐᵒᵖ α<VAR>s t : Set α<GOAL>interior s * interior t ⊆ interior (s * t)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Group α<VAR>ContinuousConstSMul αᵐᵒᵖ α<VAR>s : Set α<VAR>a : α<VAR>b : α<VAR>h : s ∈ 𝓝 b<GOAL>s * {a} ∈ 𝓝 (b * a)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>AddGroup α<VAR>ContinuousConstVAdd αᵃᵒᵖ α<VAR>s : Set α<VAR>a : α<VAR>b : α<VAR>h : s ∈ 𝓝 b<GOAL>s + {a} ∈ 𝓝 (b + a)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>AddGroup α<VAR>ContinuousConstVAdd αᵃᵒᵖ α<VAR>s : Set α<VAR>a : α<VAR>h : s ∈ 𝓝 0<GOAL>s + {a} ∈ 𝓝 a
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Group α<VAR>ContinuousConstSMul αᵐᵒᵖ α<VAR>s : Set α<VAR>a : α<VAR>h : s ∈ 𝓝 1<GOAL>s * {a} ∈ 𝓝 a
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>s t : Set G<VAR>ht : IsOpen t<GOAL>IsOpen (s - t)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>s t : Set G<VAR>ht : IsOpen t<GOAL>IsOpen (s / t)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>s t : Set G<VAR>hs : IsOpen s<GOAL>IsOpen (s - t)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>s t : Set G<VAR>hs : IsOpen s<GOAL>IsOpen (s / t)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>s t : Set G<GOAL>interior s - t ⊆ interior (s - t)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>s t : Set G<GOAL>interior s / t ⊆ interior (s / t)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>s t : Set G<GOAL>s - interior t ⊆ interior (s - t)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>s t : Set G<GOAL>s / interior t ⊆ interior (s / t)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>s t : Set G<GOAL>interior s - interior t ⊆ interior (s - t)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>s t : Set G<GOAL>interior s / interior t ⊆ interior (s / t)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>s : Set G<VAR>hs : IsOpen s<VAR>t : Set G<GOAL>s * closure t = s * t
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>s : Set G<VAR>hs : IsOpen s<VAR>t : Set G<GOAL>s + closure t = s + t
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>t : Set G<VAR>ht : IsOpen t<VAR>s : Set G<GOAL>closure s + t = s + t
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>t : Set G<VAR>ht : IsOpen t<VAR>s : Set G<GOAL>closure s * t = s * t
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>s : Set G<VAR>hs : IsOpen s<VAR>t : Set G<GOAL>s / closure t = s / t
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>s : Set G<VAR>hs : IsOpen s<VAR>t : Set G<GOAL>s - closure t = s - t
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>t : Set G<VAR>ht : IsOpen t<VAR>s : Set G<GOAL>closure s / t = s / t
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>t : Set G<VAR>ht : IsOpen t<VAR>s : Set G<GOAL>closure s - t = s - t
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>s t : Set G<VAR>ht : IsClosed t<VAR>hs : IsCompact s<GOAL>IsClosed (s + t)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>s t : Set G<VAR>ht : IsClosed t<VAR>hs : IsCompact s<GOAL>IsClosed (s * t)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>s t : Set G<VAR>ht : IsClosed t<VAR>hs : IsCompact s<GOAL>IsClosed (t + s)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>s t : Set G<VAR>ht : IsClosed t<VAR>hs : IsCompact s<GOAL>IsClosed (t * s)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>H : Subgroup G<VAR>hH : IsCompact ↑H<GOAL>IsClosedMap QuotientGroup.mk
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>H : AddSubgroup G<VAR>hH : IsCompact ↑H<GOAL>IsClosedMap QuotientAddGroup.mk
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>s : Set G<GOAL>s ⊆ s + closure {0}
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>s : Set G<GOAL>s ⊆ s * closure {1}
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>K : Set G<VAR>hK : IsCompact K<GOAL>K * closure {1} = closure K
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>K : Set G<VAR>hK : IsCompact K<GOAL>K + closure {0} = closure K
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>F : Set G<VAR>hF : IsClosed F<GOAL>F * closure {1} = F
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>F : Set G<VAR>hF : IsClosed F<GOAL>F + closure {0} = F
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>t : Set G<VAR>ht : t * closure {1} = t<GOAL>tᶜ * closure {1} = tᶜ
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>t : Set G<VAR>ht : t + closure {0} = t<GOAL>tᶜ + closure {0} = tᶜ
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>t : Set G<GOAL>tᶜ + closure {0} = tᶜ ↔ t + closure {0} = t
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>t : Set G<GOAL>tᶜ * closure {1} = tᶜ ↔ t * closure {1} = t
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>U : Set G<VAR>hU : IsOpen U<GOAL>U * closure {1} = U
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>U : Set G<VAR>hU : IsOpen U<GOAL>U + closure {0} = U
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>ContinuousAdd G<VAR>h : IsClosed {0}<GOAL>T1Space G
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>ContinuousMul G<VAR>h : IsClosed {1}<GOAL>T1Space G
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>x y : G<GOAL>Inseparable x y ↔ x - y ∈ closure 0
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>x y : G<GOAL>Inseparable x y ↔ x / y ∈ closure 1
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<GOAL>T2Space G ↔ IsClosed {1}
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<GOAL>T2Space G ↔ IsClosed {0}
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>H : ∀ (x : G), x ≠ 1 → ∃ U ∈ 𝓝 1, x ∉ U<GOAL>T2Space G
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>H : ∀ (x : G), x ≠ 0 → ∃ U ∈ 𝓝 0, x ∉ U<GOAL>T2Space G
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>U : Set G<VAR>hU : U ∈ 𝓝 1<GOAL>∃ V ∈ 𝓝 1, IsClosed V ∧ V⁻¹ = V ∧ V * V ⊆ U
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>U : Set G<VAR>hU : U ∈ 𝓝 0<GOAL>∃ V ∈ 𝓝 0, IsClosed V ∧ -V = V ∧ V + V ⊆ U
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>S : Subgroup G<VAR>hS : Filter.Tendsto (⇑S.subtype) Filter.cofinite (Filter.cocompact G)<GOAL>ProperlyDiscontinuousSMul (↥S) G
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>S : AddSubgroup G<VAR>hS : Filter.Tendsto (⇑S.subtype) Filter.cofinite (Filter.cocompact G)<GOAL>ProperlyDiscontinuousVAdd (↥S) G
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>S : Subgroup G<VAR>hS : Filter.Tendsto (⇑S.subtype) Filter.cofinite (Filter.cocompact G)<GOAL>ProperlyDiscontinuousSMul (↥S.op) G
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>S : AddSubgroup G<VAR>hS : Filter.Tendsto (⇑S.subtype) Filter.cofinite (Filter.cocompact G)<GOAL>ProperlyDiscontinuousVAdd (↥S.op) G
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddZeroClass G<VAR>ContinuousAdd G<VAR>K U : Set G<VAR>hK : IsCompact K<VAR>hU : IsOpen U<VAR>hKU : K ⊆ U<GOAL>∃ V ∈ 𝓝 0, K + V ⊆ U
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>MulOneClass G<VAR>ContinuousMul G<VAR>K U : Set G<VAR>hK : IsCompact K<VAR>hU : IsOpen U<VAR>hKU : K ⊆ U<GOAL>∃ V ∈ 𝓝 1, K * V ⊆ U
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddZeroClass G<VAR>ContinuousAdd G<VAR>K U : Set G<VAR>hK : IsCompact K<VAR>hU : IsOpen U<VAR>hKU : K ⊆ U<GOAL>∃ V ∈ 𝓝 0, V + K ⊆ U
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>MulOneClass G<VAR>ContinuousMul G<VAR>K U : Set G<VAR>hK : IsCompact K<VAR>hU : IsOpen U<VAR>hKU : K ⊆ U<GOAL>∃ V ∈ 𝓝 1, V * K ⊆ U
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>K V : Set G<VAR>hK : IsCompact K<VAR>hV : (interior V).Nonempty<GOAL>∃ t, K ⊆ ⋃ g ∈ t, (fun x => g + x) ⁻¹' V
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>K V : Set G<VAR>hK : IsCompact K<VAR>hV : (interior V).Nonempty<GOAL>∃ t, K ⊆ ⋃ g ∈ t, (fun x => g * x) ⁻¹' V
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>NoncompactSpace G<VAR>K L : Set G<VAR>hK : IsCompact K<VAR>hL : IsCompact L<GOAL>∃ g, Disjoint K (g +ᵥ L)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>NoncompactSpace G<VAR>K L : Set G<VAR>hK : IsCompact K<VAR>hL : IsCompact L<GOAL>∃ g, Disjoint K (g • L)
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>L : Set G<VAR>Lcomp : IsCompact L<VAR>L1 : L ∈ 𝓝 1<GOAL>∃ K, IsCompact K ∧ IsClosed K ∧ K ⊆ L ∧ K ∈ 𝓝 1
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>L : Set G<VAR>Lcomp : IsCompact L<VAR>L1 : L ∈ 𝓝 0<GOAL>∃ K, IsCompact K ∧ IsClosed K ∧ K ⊆ L ∧ K ∈ 𝓝 0
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>K : Set G<VAR>hK : IsCompact K<VAR>x : G<VAR>h : K ∈ 𝓝 x<GOAL>LocallyCompactSpace G
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>K : Set G<VAR>hK : IsCompact K<VAR>x : G<VAR>h : K ∈ 𝓝 x<GOAL>LocallyCompactSpace G
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>WeaklyLocallyCompactSpace G<GOAL>LocallyCompactSpace G
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>WeaklyLocallyCompactSpace G<GOAL>LocallyCompactSpace G
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>TopologicalSpace α<VAR>Zero α<VAR>T1Space α<VAR>f : G → α<VAR>k : Set G<VAR>hk : IsCompact k<VAR>hf : Function.support f ⊆ k<VAR>h'f : Continuous f<GOAL>f = 0 ∨ LocallyCompactSpace G
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>TopologicalSpace α<VAR>Zero α<VAR>T1Space α<VAR>f : G → α<VAR>k : Set G<VAR>hk : IsCompact k<VAR>hf : Function.support f ⊆ k<VAR>h'f : Continuous f<GOAL>f = 0 ∨ LocallyCompactSpace G