ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<VAR>hom : Type u_3<VAR>UniformSpace β<VAR>Group β<VAR>UniformGroup β<VAR>FunLike hom α β<VAR>MonoidHomClass hom α β<VAR>f : hom<VAR>h : Filter.Tendsto (⇑f) (𝓝 1) (𝓝 1)<GOAL>UniformContinuous ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>hom : Type u_3<VAR>UniformSpace β<VAR>AddGroup β<VAR>UniformAddGroup β<VAR>FunLike hom α β<VAR>AddMonoidHomClass hom α β<VAR>f : hom<VAR>h : Filter.Tendsto (⇑f) (𝓝 0) (𝓝 0)<GOAL>UniformContinuous ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<VAR>hom : Type u_3<VAR>UniformSpace β<VAR>Group β<VAR>UniformGroup β<VAR>FunLike hom α β<VAR>MonoidHomClass hom α β<VAR>f : hom<VAR>hf : ContinuousAt (⇑f) 1<GOAL>UniformContinuous ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>hom : Type u_3<VAR>UniformSpace β<VAR>AddGroup β<VAR>UniformAddGroup β<VAR>FunLike hom α β<VAR>AddMonoidHomClass hom α β<VAR>f : hom<VAR>hf : ContinuousAt (⇑f) 0<GOAL>UniformContinuous ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<VAR>UniformSpace β<VAR>Group β<VAR>UniformGroup β<VAR>f : α →* β<VAR>hf : ContinuousAt (⇑f) 1<GOAL>UniformContinuous ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>UniformSpace β<VAR>AddGroup β<VAR>UniformAddGroup β<VAR>f : α →+ β<VAR>hf : ContinuousAt (⇑f) 0<GOAL>UniformContinuous ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<VAR>hom : Type u_3<VAR>UniformSpace β<VAR>DiscreteTopology β<VAR>Group β<VAR>UniformGroup β<VAR>FunLike hom α β<VAR>MonoidHomClass hom α β<VAR>f : hom<GOAL>UniformContinuous ⇑f ↔ IsOpen ↑(↑f).ker
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>hom : Type u_3<VAR>UniformSpace β<VAR>DiscreteTopology β<VAR>AddGroup β<VAR>UniformAddGroup β<VAR>FunLike hom α β<VAR>AddMonoidHomClass hom α β<VAR>f : hom<GOAL>UniformContinuous ⇑f ↔ IsOpen ↑(↑f).ker
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>hom : Type u_3<VAR>UniformSpace β<VAR>AddGroup β<VAR>UniformAddGroup β<VAR>FunLike hom α β<VAR>AddMonoidHomClass hom α β<VAR>f : hom<VAR>h : Continuous ⇑f<GOAL>UniformContinuous ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<VAR>hom : Type u_3<VAR>UniformSpace β<VAR>Group β<VAR>UniformGroup β<VAR>FunLike hom α β<VAR>MonoidHomClass hom α β<VAR>f : hom<VAR>h : Continuous ⇑f<GOAL>UniformContinuous ⇑f
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<VAR>ι : Type u_3<VAR>Preorder ι<VAR>u v : ι → α<VAR>hu : CauchySeq u<VAR>hv : CauchySeq v<GOAL>CauchySeq (u * v)
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>ι : Type u_3<VAR>Preorder ι<VAR>u v : ι → α<VAR>hu : CauchySeq u<VAR>hv : CauchySeq v<GOAL>CauchySeq (u + v)
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>ι : Type u_3<VAR>Preorder ι<VAR>u : ι → α<VAR>x : α<VAR>hu : CauchySeq u<GOAL>CauchySeq fun n => u n + x
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<VAR>ι : Type u_3<VAR>Preorder ι<VAR>u : ι → α<VAR>x : α<VAR>hu : CauchySeq u<GOAL>CauchySeq fun n => u n * x
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<VAR>ι : Type u_3<VAR>Preorder ι<VAR>u : ι → α<VAR>x : α<VAR>hu : CauchySeq u<GOAL>CauchySeq fun n => x * u n
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>ι : Type u_3<VAR>Preorder ι<VAR>u : ι → α<VAR>x : α<VAR>hu : CauchySeq u<GOAL>CauchySeq fun n => x + u n
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>ι : Type u_3<VAR>Preorder ι<VAR>u : ι → α<VAR>h : CauchySeq u<GOAL>CauchySeq (-u)
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<VAR>ι : Type u_3<VAR>Preorder ι<VAR>u : ι → α<VAR>h : CauchySeq u<GOAL>CauchySeq u⁻¹
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<VAR>s : Set α<GOAL>TotallyBounded s ↔ ∀ U ∈ 𝓝 1, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, y • U
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>s : Set α<GOAL>TotallyBounded s ↔ ∀ U ∈ 𝓝 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>l' : Filter β<VAR>f f' : ι → β → α<VAR>g g' : β → α<VAR>hf : TendstoUniformlyOnFilter f g l l'<VAR>hf' : TendstoUniformlyOnFilter f' g' l l'<GOAL>TendstoUniformlyOnFilter (f + f') (g + g') l l'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>l' : Filter β<VAR>f f' : ι → β → α<VAR>g g' : β → α<VAR>hf : TendstoUniformlyOnFilter f g l l'<VAR>hf' : TendstoUniformlyOnFilter f' g' l l'<GOAL>TendstoUniformlyOnFilter (f * f') (g * g') l l'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>l' : Filter β<VAR>f f' : ι → β → α<VAR>g g' : β → α<VAR>hf : TendstoUniformlyOnFilter f g l l'<VAR>hf' : TendstoUniformlyOnFilter f' g' l l'<GOAL>TendstoUniformlyOnFilter (f - f') (g - g') l l'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>l' : Filter β<VAR>f f' : ι → β → α<VAR>g g' : β → α<VAR>hf : TendstoUniformlyOnFilter f g l l'<VAR>hf' : TendstoUniformlyOnFilter f' g' l l'<GOAL>TendstoUniformlyOnFilter (f / f') (g / g') l l'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>f f' : ι → β → α<VAR>g g' : β → α<VAR>s : Set β<VAR>hf : TendstoUniformlyOn f g l s<VAR>hf' : TendstoUniformlyOn f' g' l s<GOAL>TendstoUniformlyOn (f * f') (g * g') l s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>f f' : ι → β → α<VAR>g g' : β → α<VAR>s : Set β<VAR>hf : TendstoUniformlyOn f g l s<VAR>hf' : TendstoUniformlyOn f' g' l s<GOAL>TendstoUniformlyOn (f + f') (g + g') l s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>f f' : ι → β → α<VAR>g g' : β → α<VAR>s : Set β<VAR>hf : TendstoUniformlyOn f g l s<VAR>hf' : TendstoUniformlyOn f' g' l s<GOAL>TendstoUniformlyOn (f - f') (g - g') l s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>f f' : ι → β → α<VAR>g g' : β → α<VAR>s : Set β<VAR>hf : TendstoUniformlyOn f g l s<VAR>hf' : TendstoUniformlyOn f' g' l s<GOAL>TendstoUniformlyOn (f / f') (g / g') l s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>f f' : ι → β → α<VAR>g g' : β → α<VAR>hf : TendstoUniformly f g l<VAR>hf' : TendstoUniformly f' g' l<GOAL>TendstoUniformly (f + f') (g + g') l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>f f' : ι → β → α<VAR>g g' : β → α<VAR>hf : TendstoUniformly f g l<VAR>hf' : TendstoUniformly f' g' l<GOAL>TendstoUniformly (f * f') (g * g') l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>f f' : ι → β → α<VAR>g g' : β → α<VAR>hf : TendstoUniformly f g l<VAR>hf' : TendstoUniformly f' g' l<GOAL>TendstoUniformly (f / f') (g / g') l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>f f' : ι → β → α<VAR>g g' : β → α<VAR>hf : TendstoUniformly f g l<VAR>hf' : TendstoUniformly f' g' l<GOAL>TendstoUniformly (f - f') (g - g') l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>f f' : ι → β → α<VAR>s : Set β<VAR>hf : UniformCauchySeqOn f l s<VAR>hf' : UniformCauchySeqOn f' l s<GOAL>UniformCauchySeqOn (f + f') l s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>f f' : ι → β → α<VAR>s : Set β<VAR>hf : UniformCauchySeqOn f l s<VAR>hf' : UniformCauchySeqOn f' l s<GOAL>UniformCauchySeqOn (f * f') l s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>f f' : ι → β → α<VAR>s : Set β<VAR>hf : UniformCauchySeqOn f l s<VAR>hf' : UniformCauchySeqOn f' l s<GOAL>UniformCauchySeqOn (f - f') l s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>Group α<VAR>UniformGroup α<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>f f' : ι → β → α<VAR>s : Set β<VAR>hf : UniformCauchySeqOn f l s<VAR>hf' : UniformCauchySeqOn f' l s<GOAL>UniformCauchySeqOn (f / f') l s
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<GOAL>𝓤 G = Filter.comap (fun p => p.2 - p.1) (𝓝 0)
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<GOAL>𝓤 G = Filter.comap (fun p => p.2 / p.1) (𝓝 1)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>CompactSpace G<GOAL>UniformAddGroup G
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>CompactSpace G<GOAL>UniformGroup G
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>T2Space G<VAR>H : AddSubgroup G<VAR>DiscreteTopology ↥H<GOAL>Filter.Tendsto Subtype.val Filter.cofinite (Filter.cocompact G)
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>T2Space G<VAR>H : Subgroup G<VAR>DiscreteTopology ↥H<GOAL>Filter.Tendsto Subtype.val Filter.cofinite (Filter.cocompact G)
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>T2Space G<VAR>H : Type u_2<VAR>Group H<VAR>f : H →* G<VAR>hf : Function.Injective ⇑f<VAR>hf' : DiscreteTopology ↥f.range<GOAL>Filter.Tendsto (⇑f) Filter.cofinite (Filter.cocompact G)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>T2Space G<VAR>H : Type u_2<VAR>AddGroup H<VAR>f : H →+ G<VAR>hf : Function.Injective ⇑f<VAR>hf' : DiscreteTopology ↥f.range<GOAL>Filter.Tendsto (⇑f) Filter.cofinite (Filter.cocompact G)
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>F : ι → α → G<VAR>f : α → G<VAR>p : Filter ι<GOAL>TendstoUniformly F f p ↔ ∀ u ∈ 𝓝 1, ∀ᶠ (i : ι) in p, ∀ (a : α), F i a / f a ∈ u
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>F : ι → α → G<VAR>f : α → G<VAR>p : Filter ι<GOAL>TendstoUniformly F f p ↔ ∀ u ∈ 𝓝 0, ∀ᶠ (i : ι) in p, ∀ (a : α), F i a - f a ∈ u
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>F : ι → α → G<VAR>f : α → G<VAR>p : Filter ι<VAR>s : Set α<GOAL>TendstoUniformlyOn F f p s ↔ ∀ u ∈ 𝓝 1, ∀ᶠ (i : ι) in p, ∀ a ∈ s, F i a / f a ∈ u
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>F : ι → α → G<VAR>f : α → G<VAR>p : Filter ι<VAR>s : Set α<GOAL>TendstoUniformlyOn F f p s ↔ ∀ u ∈ 𝓝 0, ∀ᶠ (i : ι) in p, ∀ a ∈ s, F i a - f a ∈ u
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>F : ι → α → G<VAR>f : α → G<VAR>p : Filter ι<GOAL>TendstoLocallyUniformly F f p ↔ ∀ u ∈ 𝓝 1, ∀ (x : α), ∃ t ∈ 𝓝 x, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a / f a ∈ u
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>F : ι → α → G<VAR>f : α → G<VAR>p : Filter ι<GOAL>TendstoLocallyUniformly F f p ↔ ∀ u ∈ 𝓝 0, ∀ (x : α), ∃ t ∈ 𝓝 x, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a - f a ∈ u
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>F : ι → α → G<VAR>f : α → G<VAR>p : Filter ι<VAR>s : Set α<GOAL>TendstoLocallyUniformlyOn F f p s ↔ ∀ u ∈ 𝓝 1, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a / f a ∈ u
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>F : ι → α → G<VAR>f : α → G<VAR>p : Filter ι<VAR>s : Set α<GOAL>TendstoLocallyUniformlyOn F f p s ↔ ∀ u ∈ 𝓝 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a - f a ∈ u
<VAR>G : Type u_1<VAR>CommGroup G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<GOAL>UniformGroup G
<VAR>G : Type u_1<VAR>AddCommGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<GOAL>UniformAddGroup G
<VAR>G : Type u_2<VAR>u : UniformSpace G<VAR>AddGroup G<VAR>UniformAddGroup G<GOAL>TopologicalAddGroup.toUniformSpace G = u
<VAR>G : Type u_2<VAR>u : UniformSpace G<VAR>Group G<VAR>UniformGroup G<GOAL>TopologicalGroup.toUniformSpace G = u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>hom : Type u_3<VAR>TopologicalSpace α<VAR>AddGroup α<VAR>TopologicalAddGroup α<VAR>TopologicalSpace β<VAR>AddGroup β<VAR>FunLike hom β α<VAR>AddMonoidHomClass hom β α<VAR>e : hom<VAR>de : DenseInducing ⇑e<VAR>x₀ : α<GOAL>Filter.Tendsto (fun t => t.2 - t.1) (Filter.comap (fun p => (e p.1, e p.2)) (𝓝 (x₀, x₀))) (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>hom : Type u_3<VAR>TopologicalSpace α<VAR>Group α<VAR>TopologicalGroup α<VAR>TopologicalSpace β<VAR>Group β<VAR>FunLike hom β α<VAR>MonoidHomClass hom β α<VAR>e : hom<VAR>de : DenseInducing ⇑e<VAR>x₀ : α<GOAL>Filter.Tendsto (fun t => t.2 / t.1) (Filter.comap (fun p => (e p.1, e p.2)) (𝓝 (x₀, x₀))) (𝓝 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_4<VAR>G : Type u_5<VAR>TopologicalSpace α<VAR>AddCommGroup α<VAR>TopologicalAddGroup α<VAR>TopologicalSpace β<VAR>AddCommGroup β<VAR>TopologicalSpace δ<VAR>AddCommGroup δ<VAR>UniformSpace G<VAR>AddCommGroup G<VAR>e : β →+ α<VAR>de : DenseInducing ⇑e<VAR>φ : β →+ δ →+ G<VAR>hφ : Continuous fun p => (φ p.1) p.2<VAR>W' : Set G<VAR>W'_nhd : W' ∈ 𝓝 0<VAR>x₀ : α<VAR>y₁ : δ<GOAL>∃ U₂ ∈ Filter.comap (⇑e) (𝓝 x₀), ∀ x ∈ U₂, ∀ x' ∈ U₂, (fun p => (φ p.1) p.2) (x' - x, y₁) ∈ W'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>G : Type u_5<VAR>TopologicalSpace α<VAR>AddCommGroup α<VAR>TopologicalAddGroup α<VAR>TopologicalSpace β<VAR>AddCommGroup β<VAR>TopologicalSpace γ<VAR>AddCommGroup γ<VAR>TopologicalAddGroup γ<VAR>TopologicalSpace δ<VAR>AddCommGroup δ<VAR>UniformSpace G<VAR>AddCommGroup G<VAR>UniformAddGroup G<VAR>e : β →+ α<VAR>de : DenseInducing ⇑e<VAR>f : δ →+ γ<VAR>df : DenseInducing ⇑f<VAR>φ : β →+ δ →+ G<VAR>hφ : Continuous fun p => (φ p.1) p.2<VAR>W' : Set G<VAR>W'_nhd : W' ∈ 𝓝 0<VAR>x₀ : α<VAR>y₀ : γ<GOAL>∃ U ∈ Filter.comap (⇑e) (𝓝 x₀), ∃ V ∈ Filter.comap (⇑f) (𝓝 y₀), ∀ x ∈ U, ∀ x' ∈ U, ∀ y ∈ V, ∀ y' ∈ V, (fun p => (φ p.1) p.2) (x', y') - (fun p => (φ p.1) p.2) (x, y) ∈ W'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>G : Type u_5<VAR>TopologicalSpace α<VAR>AddCommGroup α<VAR>TopologicalAddGroup α<VAR>TopologicalSpace β<VAR>AddCommGroup β<VAR>TopologicalSpace γ<VAR>AddCommGroup γ<VAR>TopologicalAddGroup γ<VAR>TopologicalSpace δ<VAR>AddCommGroup δ<VAR>UniformSpace G<VAR>AddCommGroup G<VAR>UniformAddGroup G<VAR>T0Space G<VAR>CompleteSpace G<VAR>e : β →+ α<VAR>de : DenseInducing ⇑e<VAR>f : δ →+ γ<VAR>df : DenseInducing ⇑f<VAR>φ : β →+ δ →+ G<VAR>hφ : Continuous fun p => (φ p.1) p.2<GOAL>Continuous (⋯.extend fun p => (φ p.1) p.2)
<VAR>self : TopCat.GlueData<VAR>i j : self.J<GOAL>OpenEmbedding ⇑(self.f i j)
<VAR>D : TopCat.GlueData<GOAL>Function.Surjective ⇑D.π
<VAR>D : TopCat.GlueData<VAR>U : Set ↑D.glued<GOAL>IsOpen U ↔ ∀ (i : D.J), IsOpen (⇑(D.ι i) ⁻¹' U)
<VAR>D : TopCat.GlueData<VAR>x : ↑D.glued<GOAL>∃ i y, (D.ι i) y = x
<VAR>D : TopCat.GlueData<GOAL>Equivalence D.Rel
<VAR>D : TopCat.GlueData<VAR>x y : ↑(∐ D.U)<VAR>h : D.π x = D.π y<GOAL>EqvGen (CategoryTheory.Limits.Types.CoequalizerRel ⇑D.diagram.fstSigmaMap ⇑D.diagram.sndSigmaMap) x y
<VAR>D : TopCat.GlueData<VAR>i j : D.J<VAR>x : ↑(D.U i)<VAR>y : ↑(D.U j)<GOAL>(D.ι i) x = (D.ι j) y ↔ D.Rel ⟨i, x⟩ ⟨j, y⟩
<VAR>D : TopCat.GlueData<VAR>i : D.J<GOAL>Function.Injective ⇑(D.ι i)
<VAR>D : TopCat.GlueData<VAR>i j : D.J<GOAL>Set.range ⇑(D.ι i) ∩ Set.range ⇑(D.ι j) = Set.range ⇑(D.f i j ≫ D.ι i)
<VAR>D : TopCat.GlueData<VAR>i j : D.J<GOAL>⇑(D.ι j) ⁻¹' Set.range ⇑(D.ι i) = Set.range ⇑(D.f j i)
<VAR>D : TopCat.GlueData<VAR>i j : D.J<VAR>U : Set ↑(D.U i)<GOAL>⇑(D.ι j) ⁻¹' (⇑(D.ι i) '' U) = ⇑(D.f j i) '' (⇑(D.t j i ≫ D.f i j) ⁻¹' U)
<VAR>D : TopCat.GlueData<VAR>i j : D.J<VAR>U : Set ↑(D.U i)<GOAL>⇑(D.ι j) ⁻¹' (⇑(D.ι i) '' U) = ⇑(D.t i j ≫ D.f j i) '' (⇑(D.f i j) ⁻¹' U)
<VAR>D : TopCat.GlueData<VAR>i : D.J<VAR>U : TopologicalSpace.Opens ↑(D.U i)<GOAL>IsOpen (⇑(D.ι i) '' ↑U)
<VAR>D : TopCat.GlueData<VAR>i : D.J<GOAL>OpenEmbedding ⇑(D.ι i)
<VAR>self : TopCat.GlueData.MkCore<VAR>i : self.J<GOAL>self.V i i = ⊤
<VAR>self : TopCat.GlueData.MkCore<VAR>i j : self.J<VAR>k : self.J<VAR>x : ↥(self.V i j)<GOAL>↑x ∈ self.V i k → ↑((self.t i j) x) ∈ self.V j k
<VAR>self : TopCat.GlueData.MkCore<VAR>i : self.J<GOAL>⇑(self.t i i) = id
<VAR>self : TopCat.GlueData.MkCore<VAR>i j k : self.J<VAR>x : ↥(self.V i j)<VAR>h : ↑x ∈ self.V i k<GOAL>↑((self.t j k) ⟨↑((self.t i j) x), ⋯⟩) = ↑((self.t i k) ⟨↑x, h⟩)
<VAR>h : TopCat.GlueData.MkCore<VAR>i j : h.J<VAR>x : ↥(h.V j i)<GOAL>(h.t i j) ((h.t j i) x) = x
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>J : Type u<VAR>U : J → TopologicalSpace.Opens α<GOAL>(TopCat.GlueData.ofOpenSubsets U).J = J
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>J : Type u<VAR>U : J → TopologicalSpace.Opens α<VAR>i : (TopCat.GlueData.MkCore.mk (fun i => (TopologicalSpace.Opens.toTopCat (TopCat.of α)).obj (U i)) (fun i j => (TopologicalSpace.Opens.map (U i).inclusion).obj (U j)) (fun i j => { toFun := fun x => ⟨⟨↑↑x, ⋯⟩, ⋯⟩, continuous_toFun := ⋯ }) ⋯ ⋯ ⋯ ⋯).J × (TopCat.GlueData.MkCore.mk (fun i => (TopologicalSpace.Opens.toTopCat (TopCat.of α)).obj (U i)) (fun i j => (TopologicalSpace.Opens.map (U i).inclusion).obj (U j)) (fun i j => { toFun := fun x => ⟨⟨↑↑x, ⋯⟩, ⋯⟩, continuous_toFun := ⋯ }) ⋯ ⋯ ⋯ ⋯).J<GOAL>(TopCat.GlueData.ofOpenSubsets U).V i = (TopologicalSpace.Opens.toTopCat ((TopologicalSpace.Opens.toTopCat (TopCat.of α)).obj (U i.1))).obj ((TopologicalSpace.Opens.map (U i.1).inclusion).obj (U i.2))
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>J : Type u<VAR>U : J → TopologicalSpace.Opens α<VAR>i j : (TopCat.GlueData.MkCore.mk (fun i => (TopologicalSpace.Opens.toTopCat (TopCat.of α)).obj (U i)) (fun i j => (TopologicalSpace.Opens.map (U i).inclusion).obj (U j)) (fun i j => { toFun := fun x => ⟨⟨↑↑x, ⋯⟩, ⋯⟩, continuous_toFun := ⋯ }) ⋯ ⋯ ⋯ ⋯).J<GOAL>(TopCat.GlueData.ofOpenSubsets U).f i j = ((TopologicalSpace.Opens.map (U i).inclusion).obj (U j)).inclusion
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>J : Type u<VAR>U : J → TopologicalSpace.Opens α<GOAL>∀ (a : (TopCat.GlueData.MkCore.mk (fun i => (TopologicalSpace.Opens.toTopCat (TopCat.of α)).obj (U i)) (fun i j => (TopologicalSpace.Opens.map (U i).inclusion).obj (U j)) (fun i j => { toFun := fun x => ⟨⟨↑↑x, ⋯⟩, ⋯⟩, continuous_toFun := ⋯ }) ⋯ ⋯ ⋯ ⋯).J), (TopCat.GlueData.ofOpenSubsets U).U a = (TopologicalSpace.Opens.toTopCat (TopCat.of α)).obj (U a)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>J : Type u<VAR>U : J → TopologicalSpace.Opens α<VAR>i j : (TopCat.GlueData.MkCore.mk (fun i => (TopologicalSpace.Opens.toTopCat (TopCat.of α)).obj (U i)) (fun i j => (TopologicalSpace.Opens.map (U i).inclusion).obj (U j)) (fun i j => { toFun := fun x => ⟨⟨↑↑x, ⋯⟩, ⋯⟩, continuous_toFun := ⋯ }) ⋯ ⋯ ⋯ ⋯).J<GOAL>(TopCat.GlueData.ofOpenSubsets U).t i j = { toFun := fun x => ⟨⟨↑↑x, ⋯⟩, ⋯⟩, continuous_toFun := ⋯ }
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>J : Type u<VAR>U : J → TopologicalSpace.Opens α<VAR>i : J<GOAL>(TopCat.GlueData.ofOpenSubsets U).ι i ≫ TopCat.GlueData.fromOpenSubsetsGlue U = (U i).inclusion
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>J : Type u<VAR>U : J → TopologicalSpace.Opens α<GOAL>Function.Injective ⇑(TopCat.GlueData.fromOpenSubsetsGlue U)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>J : Type u<VAR>U : J → TopologicalSpace.Opens α<GOAL>IsOpenMap ⇑(TopCat.GlueData.fromOpenSubsetsGlue U)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>J : Type u<VAR>U : J → TopologicalSpace.Opens α<GOAL>OpenEmbedding ⇑(TopCat.GlueData.fromOpenSubsetsGlue U)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>J : Type u<VAR>U : J → TopologicalSpace.Opens α<GOAL>Set.range ⇑(TopCat.GlueData.fromOpenSubsetsGlue U) = ⋃ i, ↑(U i)
<VAR>H : Type u<VAR>TopologicalSpace H<VAR>self : StructureGroupoid H<VAR>e e' : PartialHomeomorph H H<GOAL>e ∈ self.members → e' ∈ self.members → e ≫ₕ e' ∈ self.members
<VAR>H : Type u<VAR>TopologicalSpace H<VAR>self : StructureGroupoid H<VAR>e : PartialHomeomorph H H<GOAL>e ∈ self.members → e.symm ∈ self.members
<VAR>H : Type u<VAR>TopologicalSpace H<VAR>self : StructureGroupoid H<GOAL>PartialHomeomorph.refl H ∈ self.members
<VAR>H : Type u<VAR>TopologicalSpace H<VAR>self : StructureGroupoid H<VAR>e : PartialHomeomorph H H<GOAL>(∀ x ∈ e.source, ∃ s, IsOpen s ∧ x ∈ s ∧ e.restr s ∈ self.members) → e ∈ self.members
<VAR>H : Type u<VAR>TopologicalSpace H<VAR>self : StructureGroupoid H<VAR>e e' : PartialHomeomorph H H<GOAL>e ∈ self.members → e' ≈ e → e' ∈ self.members
<VAR>H : Type u<VAR>TopologicalSpace H<VAR>G : StructureGroupoid H<VAR>e e' : PartialHomeomorph H H<VAR>he : e ∈ G<VAR>he' : e' ∈ G<GOAL>e ≫ₕ e' ∈ G
<VAR>H : Type u<VAR>TopologicalSpace H<VAR>G : StructureGroupoid H<VAR>e : PartialHomeomorph H H<VAR>he : e ∈ G<GOAL>e.symm ∈ G
<VAR>H : Type u<VAR>TopologicalSpace H<VAR>G : StructureGroupoid H<GOAL>PartialHomeomorph.refl H ∈ G
<VAR>H : Type u<VAR>TopologicalSpace H<VAR>G : StructureGroupoid H<VAR>e : PartialHomeomorph H H<VAR>h : ∀ x ∈ e.source, ∃ s, IsOpen s ∧ x ∈ s ∧ e.restr s ∈ G<GOAL>e ∈ G
<VAR>H : Type u<VAR>TopologicalSpace H<VAR>G : StructureGroupoid H<VAR>e e' : PartialHomeomorph H H<VAR>he : e ∈ G<VAR>h : e' ≈ e<GOAL>e' ∈ G
<VAR>H : Type u<VAR>TopologicalSpace H<VAR>G : StructureGroupoid H<VAR>e e' : PartialHomeomorph H H<VAR>h : e ≈ e'<GOAL>e ∈ G ↔ e' ∈ G
<VAR>H : Type u<VAR>TopologicalSpace H<VAR>G₁ G₂ : StructureGroupoid H<GOAL>G₁ ≤ G₂ ↔ ∀ e ∈ G₁, e ∈ G₂
<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>self : Pregroupoid H<VAR>f : H → H<VAR>u : Set H<GOAL>IsOpen u → (∀ x ∈ u, ∃ v, IsOpen v ∧ x ∈ v ∧ self.property f (u ∩ v)) → self.property f u
<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>self : Pregroupoid H<VAR>f g : H → H<VAR>u : Set H<GOAL>IsOpen u → (∀ x ∈ u, g x = f x) → self.property f u → self.property g u
<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>self : Pregroupoid H<GOAL>self.property id Set.univ
<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>self : Pregroupoid H<VAR>f g : H → H<VAR>u v : Set H<GOAL>self.property f u → self.property g v → IsOpen u → IsOpen v → IsOpen (u ∩ f ⁻¹' v) → self.property (g ∘ f) (u ∩ f ⁻¹' v)
<VAR>H : Type u<VAR>TopologicalSpace H<VAR>PG : Pregroupoid H<VAR>e : PartialHomeomorph H H<GOAL>e ∈ PG.groupoid ↔ PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target
<VAR>H : Type u<VAR>TopologicalSpace H<VAR>PG₁ PG₂ : Pregroupoid H<VAR>h : ∀ (f : H → H) (s : Set H), PG₁.property f s → PG₂.property f s<GOAL>PG₁.groupoid ≤ PG₂.groupoid
<VAR>H : Type u<VAR>TopologicalSpace H<VAR>PG : Pregroupoid H<VAR>e e' : PartialHomeomorph H H<VAR>he' : e ≈ e'<VAR>he : PG.property (↑e) e.source<GOAL>PG.property (↑e') e'.source
<VAR>H : Type u<VAR>TopologicalSpace H<VAR>G : StructureGroupoid H<VAR>self : ClosedUnderRestriction G<VAR>e : PartialHomeomorph H H<GOAL>e ∈ G → ∀ (s : Set H), IsOpen s → e.restr s ∈ G
<VAR>H : Type u<VAR>TopologicalSpace H<VAR>G : StructureGroupoid H<VAR>ClosedUnderRestriction G<VAR>e : PartialHomeomorph H H<VAR>he : e ∈ G<VAR>s : Set H<VAR>hs : IsOpen s<GOAL>e.restr s ∈ G
<VAR>H : Type u<VAR>TopologicalSpace H<VAR>s : Set H<VAR>hs : IsOpen s<GOAL>PartialHomeomorph.ofSet s hs ∈ idRestrGroupoid
<VAR>H : Type u<VAR>TopologicalSpace H<VAR>G : StructureGroupoid H<GOAL>ClosedUnderRestriction G ↔ idRestrGroupoid ≤ G
<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>self : ChartedSpace H M<VAR>x : M<GOAL>x ∈ (ChartedSpace.chartAt x).source