ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>s : Set α<VAR>p : Filter ι<VAR>UniformSpace γ<VAR>g : β → γ<VAR>hg : UniformContinuous g<VAR>hf : UniformCauchySeqOn F p s<GOAL>UniformCauchySeqOn (fun n => g ∘ F n) p s
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>s : Set α<VAR>p : Filter ι<VAR>ι' : Type u_1<VAR>α' : Type u_2<VAR>β' : Type u_3<VAR>UniformSpace β'<VAR>F' : ι' → α' → β'<VAR>p' : Filter ι'<VAR>s' : Set α'<VAR>h : UniformCauchySeqOn F p s<VAR>h' : UniformCauchySeqOn F' p' s'<GOAL>UniformCauchySeqOn (fun i => Prod.map (F i.1) (F' i.2)) (p ×ˢ p') (s ×ˢ s')
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>s : Set α<VAR>p : Filter ι<VAR>ι' : Type u_1<VAR>β' : Type u_2<VAR>UniformSpace β'<VAR>F' : ι' → α → β'<VAR>p' : Filter ι'<VAR>h : UniformCauchySeqOn F p s<VAR>h' : UniformCauchySeqOn F' p' s<GOAL>UniformCauchySeqOn (fun i a => (F i.1 a, F' i.2 a)) (p ×ˢ p') s
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>s : Set α<VAR>p : Filter ι<VAR>β' : Type u_1<VAR>UniformSpace β'<VAR>F' : ι → α → β'<VAR>h : UniformCauchySeqOn F p s<VAR>h' : UniformCauchySeqOn F' p s<GOAL>UniformCauchySeqOn (fun i a => (F i a, F' i a)) p s
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>s : Set α<VAR>x : α<VAR>p : Filter ι<VAR>hp : p.NeBot<VAR>hf : UniformCauchySeqOn F p s<VAR>hx : x ∈ s<GOAL>Cauchy (Filter.map (fun i => F i x) p)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>s : Set α<VAR>x : α<VAR>Nonempty ι<VAR>SemilatticeSup ι<VAR>hf : UniformCauchySeqOn F Filter.atTop s<VAR>hx : x ∈ s<GOAL>CauchySeq fun i => F i x
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s : Set α<VAR>l : Filter ι<VAR>l.IsCountablyGenerated<VAR>h : ∀ (u : ℕ → ι), Filter.Tendsto u Filter.atTop l → TendstoUniformlyOn (fun n => F (u n)) f Filter.atTop s<GOAL>TendstoUniformlyOn F f l s
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s : Set α<VAR>l : Filter ι<VAR>h : TendstoUniformlyOn F f l s<VAR>u : ℕ → ι<VAR>hu : Filter.Tendsto u Filter.atTop l<GOAL>TendstoUniformlyOn (fun n => F (u n)) f Filter.atTop s
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s : Set α<VAR>l : Filter ι<VAR>l.IsCountablyGenerated<GOAL>TendstoUniformlyOn F f l s ↔ ∀ (u : ℕ → ι), Filter.Tendsto u Filter.atTop l → TendstoUniformlyOn (fun n => F (u n)) f Filter.atTop s
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>l : Filter ι<VAR>l.IsCountablyGenerated<GOAL>TendstoUniformly F f l ↔ ∀ (u : ℕ → ι), Filter.Tendsto u Filter.atTop l → TendstoUniformly (fun n => F (u n)) f Filter.atTop
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<VAR>TopologicalSpace α<GOAL>TendstoLocallyUniformlyOn F f p Set.univ ↔ TendstoLocallyUniformly F f p
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s : Set α<VAR>p : Filter ι<VAR>TopologicalSpace α<GOAL>TendstoLocallyUniformlyOn F f p s ↔ ∀ x ∈ s, Filter.Tendsto (fun y => (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s : Set α<VAR>p : Filter ι<VAR>TopologicalSpace α<VAR>hs : IsOpen s<GOAL>TendstoLocallyUniformlyOn F f p s ↔ ∀ x ∈ s, Filter.Tendsto (fun y => (f y.2, F y.1 y.2)) (p ×ˢ 𝓝 x) (𝓤 β)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<VAR>TopologicalSpace α<GOAL>TendstoLocallyUniformly F f p ↔ ∀ (x : α), Filter.Tendsto (fun y => (f y.2, F y.1 y.2)) (p ×ˢ 𝓝 x) (𝓤 β)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s : Set α<VAR>p : Filter ι<VAR>TopologicalSpace α<GOAL>TendstoLocallyUniformlyOn F f p s ↔ TendstoLocallyUniformly (fun i x => F i ↑x) (f ∘ Subtype.val) p
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s : Set α<VAR>p : Filter ι<VAR>TopologicalSpace α<VAR>h : TendstoUniformlyOn F f p s<GOAL>TendstoLocallyUniformlyOn F f p s
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<VAR>TopologicalSpace α<VAR>h : TendstoUniformly F f p<GOAL>TendstoLocallyUniformly F f p
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>p : Filter ι<VAR>TopologicalSpace α<VAR>h : TendstoLocallyUniformlyOn F f p s<VAR>h' : s' ⊆ s<GOAL>TendstoLocallyUniformlyOn F f p s'
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<VAR>TopologicalSpace α<VAR>ι' : Sort u_1<VAR>S : ι' → Set α<VAR>hS : ∀ (i : ι'), IsOpen (S i)<VAR>h : ∀ (i : ι'), TendstoLocallyUniformlyOn F f p (S i)<GOAL>TendstoLocallyUniformlyOn F f p (⋃ i, S i)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<VAR>TopologicalSpace α<VAR>s : Set γ<VAR>S : γ → Set α<VAR>hS : ∀ i ∈ s, IsOpen (S i)<VAR>h : ∀ i ∈ s, TendstoLocallyUniformlyOn F f p (S i)<GOAL>TendstoLocallyUniformlyOn F f p (⋃ i ∈ s, S i)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<VAR>TopologicalSpace α<VAR>S : Set (Set α)<VAR>hS : ∀ s ∈ S, IsOpen s<VAR>h : ∀ s ∈ S, TendstoLocallyUniformlyOn F f p s<GOAL>TendstoLocallyUniformlyOn F f p (⋃₀ S)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<VAR>TopologicalSpace α<VAR>s₁ s₂ : Set α<VAR>hs₁ : IsOpen s₁<VAR>hs₂ : IsOpen s₂<VAR>h₁ : TendstoLocallyUniformlyOn F f p s₁<VAR>h₂ : TendstoLocallyUniformlyOn F f p s₂<GOAL>TendstoLocallyUniformlyOn F f p (s₁ ∪ s₂)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s : Set α<VAR>p : Filter ι<VAR>TopologicalSpace α<VAR>h : TendstoLocallyUniformly F f p<GOAL>TendstoLocallyUniformlyOn F f p s
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<VAR>TopologicalSpace α<VAR>CompactSpace α<GOAL>TendstoLocallyUniformly F f p ↔ TendstoUniformly F f p
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s : Set α<VAR>p : Filter ι<VAR>TopologicalSpace α<VAR>hs : IsCompact s<GOAL>TendstoLocallyUniformlyOn F f p s ↔ TendstoUniformlyOn F f p s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s : Set α<VAR>p : Filter ι<VAR>TopologicalSpace α<VAR>TopologicalSpace γ<VAR>t : Set γ<VAR>h : TendstoLocallyUniformlyOn F f p s<VAR>g : γ → α<VAR>hg : Set.MapsTo g t s<VAR>cg : ContinuousOn g t<GOAL>TendstoLocallyUniformlyOn (fun n => F n ∘ g) (f ∘ g) p t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<VAR>TopologicalSpace α<VAR>TopologicalSpace γ<VAR>h : TendstoLocallyUniformly F f p<VAR>g : γ → α<VAR>cg : Continuous g<GOAL>TendstoLocallyUniformly (fun n => F n ∘ g) (f ∘ g) p
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>s : Set α<VAR>TopologicalSpace α<VAR>LocallyCompactSpace α<VAR>G : ι → α → β<VAR>g : α → β<VAR>p : Filter ι<VAR>hs : IsOpen s<GOAL>[TendstoLocallyUniformlyOn G g p s, ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K, ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v].TFAE
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s : Set α<VAR>p : Filter ι<VAR>TopologicalSpace α<VAR>LocallyCompactSpace α<VAR>hs : IsOpen s<GOAL>TendstoLocallyUniformlyOn F f p s ↔ ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn F f p K
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<VAR>TopologicalSpace α<VAR>LocallyCompactSpace α<GOAL>TendstoLocallyUniformly F f p ↔ ∀ (K : Set α), IsCompact K → TendstoUniformlyOn F f p K
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s : Set α<VAR>p : Filter ι<VAR>TopologicalSpace α<GOAL>TendstoLocallyUniformlyOn F f p s ↔ ∀ x ∈ s, TendstoUniformlyOnFilter F f p (𝓝[s] x)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<VAR>TopologicalSpace α<GOAL>TendstoLocallyUniformly F f p ↔ ∀ (x : α), TendstoUniformlyOnFilter F f p (𝓝 x)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s : Set α<VAR>p : Filter ι<VAR>TopologicalSpace α<VAR>hf : TendstoLocallyUniformlyOn F f p s<VAR>a : α<VAR>ha : a ∈ s<GOAL>Filter.Tendsto (fun i => F i a) p (𝓝 (f a))
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s : Set α<VAR>p : Filter ι<VAR>TopologicalSpace α<VAR>p.NeBot<VAR>T2Space β<VAR>g : α → β<VAR>hf : TendstoLocallyUniformlyOn F f p s<VAR>hg : TendstoLocallyUniformlyOn F g p s<GOAL>Set.EqOn f g s
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s : Set α<VAR>p : Filter ι<VAR>TopologicalSpace α<VAR>G : ι → α → β<VAR>hf : TendstoLocallyUniformlyOn F f p s<VAR>hg : ∀ (n : ι), Set.EqOn (F n) (G n) s<GOAL>TendstoLocallyUniformlyOn G f p s
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s : Set α<VAR>p : Filter ι<VAR>TopologicalSpace α<VAR>g : α → β<VAR>hf : TendstoLocallyUniformlyOn F f p s<VAR>hg : Set.EqOn f g s<GOAL>TendstoLocallyUniformlyOn F g p s
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace β<VAR>f : α → β<VAR>s : Set α<VAR>x : α<VAR>TopologicalSpace α<VAR>hx : x ∈ s<VAR>L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u<GOAL>ContinuousWithinAt f s x
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace β<VAR>f : α → β<VAR>x : α<VAR>TopologicalSpace α<VAR>L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∃ F, ContinuousAt F x ∧ ∀ y ∈ t, (f y, F y) ∈ u<GOAL>ContinuousAt f x
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace β<VAR>f : α → β<VAR>s : Set α<VAR>TopologicalSpace α<VAR>L : ∀ x ∈ s, ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u<GOAL>ContinuousOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace β<VAR>f : α → β<VAR>s : Set α<VAR>TopologicalSpace α<VAR>L : ∀ u ∈ 𝓤 β, ∃ F, ContinuousOn F s ∧ ∀ y ∈ s, (f y, F y) ∈ u<GOAL>ContinuousOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace β<VAR>f : α → β<VAR>TopologicalSpace α<VAR>L : ∀ (x : α), ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∃ F, ContinuousAt F x ∧ ∀ y ∈ t, (f y, F y) ∈ u<GOAL>Continuous f
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace β<VAR>f : α → β<VAR>TopologicalSpace α<VAR>L : ∀ u ∈ 𝓤 β, ∃ F, Continuous F ∧ ∀ (y : α), (f y, F y) ∈ u<GOAL>Continuous f
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s : Set α<VAR>p : Filter ι<VAR>TopologicalSpace α<VAR>h : TendstoLocallyUniformlyOn F f p s<VAR>hc : ∀ᶠ (n : ι) in p, ContinuousOn (F n) s<VAR>p.NeBot<GOAL>ContinuousOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s : Set α<VAR>p : Filter ι<VAR>TopologicalSpace α<VAR>h : TendstoUniformlyOn F f p s<VAR>hc : ∀ᶠ (n : ι) in p, ContinuousOn (F n) s<VAR>p.NeBot<GOAL>ContinuousOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<VAR>TopologicalSpace α<VAR>h : TendstoLocallyUniformly F f p<VAR>hc : ∀ᶠ (n : ι) in p, Continuous (F n)<VAR>p.NeBot<GOAL>Continuous f
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<VAR>TopologicalSpace α<VAR>h : TendstoUniformly F f p<VAR>hc : ∀ᶠ (n : ι) in p, Continuous (F n)<VAR>p.NeBot<GOAL>Continuous f
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>TopologicalSpace α<VAR>h : ContinuousWithinAt f s x<VAR>hg : Filter.Tendsto g p (𝓝[s] x)<VAR>hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u<GOAL>Filter.Tendsto (fun n => F n (g n)) p (𝓝 (f x))
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>TopologicalSpace α<VAR>h : ContinuousAt f x<VAR>hg : Filter.Tendsto g p (𝓝 x)<VAR>hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u<GOAL>Filter.Tendsto (fun n => F n (g n)) p (𝓝 (f x))
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>TopologicalSpace α<VAR>h : TendstoLocallyUniformlyOn F f p s<VAR>hf : ContinuousWithinAt f s x<VAR>hx : x ∈ s<VAR>hg : Filter.Tendsto g p (𝓝[s] x)<GOAL>Filter.Tendsto (fun n => F n (g n)) p (𝓝 (f x))
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>TopologicalSpace α<VAR>h : TendstoUniformlyOn F f p s<VAR>hf : ContinuousWithinAt f s x<VAR>hg : Filter.Tendsto g p (𝓝[s] x)<GOAL>Filter.Tendsto (fun n => F n (g n)) p (𝓝 (f x))
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>TopologicalSpace α<VAR>h : TendstoLocallyUniformly F f p<VAR>hf : ContinuousAt f x<VAR>hg : Filter.Tendsto g p (𝓝 x)<GOAL>Filter.Tendsto (fun n => F n (g n)) p (𝓝 (f x))
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>TopologicalSpace α<VAR>h : TendstoUniformly F f p<VAR>hf : ContinuousAt f x<VAR>hg : Filter.Tendsto g p (𝓝 x)<GOAL>Filter.Tendsto (fun n => F n (g n)) p (𝓝 (f x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>ι : Type u_4<VAR>TopologicalSpace β<VAR>F : ι → β → α<VAR>x₀ : β<GOAL>EquicontinuousAt F x₀ ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>ι : Type u_4<VAR>PseudoMetricSpace β<VAR>F : ι → β → α<VAR>x₀ : β<GOAL>EquicontinuousAt F x₀ ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x : β), dist x x₀ < δ → ∀ (i : ι), dist (F i x₀) (F i x) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>ι : Type u_4<VAR>TopologicalSpace β<VAR>F : ι → β → α<VAR>x₀ : β<GOAL>EquicontinuousAt F x₀ ↔ ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ι), dist (F i x) (F i x') < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>ι : Type u_4<VAR>UniformSpace β<VAR>F : ι → β → α<GOAL>UniformEquicontinuous F ↔ ∀ ε > 0, ∀ᶠ (xy : β × β) in 𝓤 β, ∀ (i : ι), dist (F i xy.1) (F i xy.2) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>ι : Type u_4<VAR>PseudoMetricSpace β<VAR>F : ι → β → α<GOAL>UniformEquicontinuous F ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x y : β), dist x y < δ → ∀ (i : ι), dist (F i x) (F i y) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>ι : Type u_4<VAR>TopologicalSpace β<VAR>x₀ : β<VAR>b : β → ℝ<VAR>b_lim : Filter.Tendsto b (𝓝 x₀) (𝓝 0)<VAR>F : ι → β → α<VAR>H : ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) ≤ b x<GOAL>EquicontinuousAt F x₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>ι : Type u_4<VAR>PseudoMetricSpace β<VAR>b : ℝ → ℝ<VAR>b_lim : Filter.Tendsto b (𝓝 0) (𝓝 0)<VAR>F : ι → β → α<VAR>H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)<GOAL>UniformEquicontinuous F
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>ι : Type u_4<VAR>PseudoMetricSpace β<VAR>b : ℝ → ℝ<VAR>b_lim : Filter.Tendsto b (𝓝 0) (𝓝 0)<VAR>F : ι → β → α<VAR>H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)<GOAL>Equicontinuous F
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>UniformFun.toFun (UniformFun.ofFun f) = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →ᵤ β<GOAL>UniformFun.ofFun (UniformFun.toFun f) = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝔖 : Set (Set α)<VAR>f : α → β<GOAL>(UniformOnFun.toFun 𝔖) ((UniformOnFun.ofFun 𝔖) f) = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝔖 : Set (Set α)<VAR>f : α →ᵤ[𝔖] β<GOAL>(UniformOnFun.ofFun 𝔖) ((UniformOnFun.toFun 𝔖) f) = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝓑 : Filter (β × β)<GOAL>Filter.IsBasis (fun V => V ∈ 𝓑) (UniformFun.gen α β)
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>GaloisConnection (fun 𝓐 => Filter.map (UniformFun.phi α β) (𝓐 ×ˢ ⊤)) fun 𝓕 => UniformFun.filter α β 𝓕
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace β<GOAL>(𝓤 (α →ᵤ β)).HasBasis (fun x => x ∈ 𝓤 β) (UniformFun.gen α β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace β<VAR>ι : Sort u_5<VAR>p : ι → Prop<VAR>s : ι → Set (β × β)<VAR>h : (𝓤 β).HasBasis p s<GOAL>(𝓤 (α →ᵤ β)).HasBasis p (UniformFun.gen α β ∘ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_4<VAR>UniformSpace β<VAR>f : α →ᵤ β<VAR>p : ι → Prop<VAR>s : ι → Set (β × β)<VAR>h : (𝓤 β).HasBasis p s<GOAL>(𝓝 f).HasBasis p fun i => {g | (f, g) ∈ UniformFun.gen α β (s i)}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace β<VAR>f : α →ᵤ β<GOAL>(𝓝 f).HasBasis (fun V => V ∈ 𝓤 β) fun V => {g | (f, g) ∈ UniformFun.gen α β V}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace β<VAR>x : α<GOAL>UniformContinuous (Function.eval x ∘ ⇑UniformFun.toFun)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : α →ᵤ β<VAR>V : Set (β × β)<GOAL>(f, g) ∈ UniformFun.gen α β V ↔ ∀ (x : α), (UniformFun.toFun f x, UniformFun.toFun g x) ∈ V
<VAR>α : Type u_1<VAR>γ : Type u_3<GOAL>Monotone (@UniformFun.uniformSpace α γ)
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>u : ι → UniformSpace γ<GOAL>UniformFun.uniformSpace α γ = ⨅ i, UniformFun.uniformSpace α γ
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>u₁ u₂ : UniformSpace γ<GOAL>UniformFun.uniformSpace α γ = UniformFun.uniformSpace α γ ⊓ UniformFun.uniformSpace α γ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>UniformSpace β<VAR>UniformSpace γ<VAR>f : γ → β<VAR>hf : UniformInducing f<GOAL>UniformInducing (⇑UniformFun.ofFun ∘ (fun x => f ∘ x) ∘ ⇑UniformFun.toFun)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>UniformSpace β<VAR>UniformSpace γ<VAR>f : γ → β<VAR>hf : UniformEmbedding f<GOAL>UniformEmbedding (⇑UniformFun.ofFun ∘ (fun x => f ∘ x) ∘ ⇑UniformFun.toFun)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>UniformSpace β<VAR>f : γ → β<GOAL>UniformFun.uniformSpace α γ = UniformSpace.comap (fun x => f ∘ x) (UniformFun.uniformSpace α β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>UniformSpace β<VAR>UniformSpace γ<VAR>f : γ → β<VAR>hf : UniformContinuous f<GOAL>UniformContinuous (⇑UniformFun.ofFun ∘ (fun x => f ∘ x) ∘ ⇑UniformFun.toFun)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>UniformSpace β<VAR>f : γ → α<GOAL>UniformContinuous fun g => UniformFun.ofFun (UniformFun.toFun g ∘ f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace β<GOAL>UniformContinuous ⇑UniformFun.toFun
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_4<VAR>p : Filter ι<VAR>UniformSpace β<VAR>F : ι → α →ᵤ β<VAR>f : α →ᵤ β<GOAL>Filter.Tendsto F p (𝓝 f) ↔ TendstoUniformly (⇑UniformFun.toFun ∘ F) (UniformFun.toFun f) p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace β<VAR>TopologicalSpace α<GOAL>IsClosed {f | Continuous (UniformFun.toFun f)}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace β<VAR>δ₁ : Type u_6<VAR>δ₂ : Type u_7<VAR>φ₁ : δ₁ → α<VAR>φ₂ : δ₂ → α<VAR>h_cover : Set.range φ₁ ∪ Set.range φ₂ = Set.univ<GOAL>UniformFun.uniformSpace α β = UniformSpace.comap (⇑UniformFun.ofFun ∘ (fun x => x ∘ φ₁) ∘ ⇑UniformFun.toFun) (UniformFun.uniformSpace δ₁ β) ⊓ UniformSpace.comap (⇑UniformFun.ofFun ∘ (fun x => x ∘ φ₂) ∘ ⇑UniformFun.toFun) (UniformFun.uniformSpace δ₂ β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_4<VAR>UniformSpace β<VAR>δ : ι → Type u_6<VAR>φ : (i : ι) → δ i → α<VAR>h_cover : ∃ I, I.Finite ∧ ⋃ i ∈ I, Set.range (φ i) = Set.univ<GOAL>UniformFun.uniformSpace α β = ⨅ i, UniformSpace.comap (⇑UniformFun.ofFun ∘ (fun x => x ∘ φ i) ∘ ⇑UniformFun.toFun) (UniformFun.uniformSpace (δ i) β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝔖 : Set (Set α)<VAR>S : Set α<VAR>V : Set (β × β)<GOAL>UniformOnFun.gen 𝔖 S V = Prod.map (S.restrict ∘ ⇑UniformFun.toFun) (S.restrict ∘ ⇑UniformFun.toFun) ⁻¹' UniformFun.gen (↑S) β V
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝔖 : Set (Set α)<VAR>S S' : Set α<VAR>V V' : Set (β × β)<VAR>hS : S' ⊆ S<VAR>hV : V ⊆ V'<GOAL>UniformOnFun.gen 𝔖 S V ⊆ UniformOnFun.gen 𝔖 S' V'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝔖 : Set (Set α)<VAR>h : 𝔖.Nonempty<VAR>h' : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖<VAR>𝓑 : FilterBasis (β × β)<GOAL>Filter.IsBasis (fun SV => SV.1 ∈ 𝔖 ∧ SV.2 ∈ 𝓑) fun SV => UniformOnFun.gen 𝔖 SV.1 SV.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<GOAL>UniformOnFun.topologicalSpace α β 𝔖 = ⨅ s ∈ 𝔖, TopologicalSpace.induced (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(UniformOnFun.toFun 𝔖)) (UniformFun.topologicalSpace (↑s) β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_4<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>p : ι → Prop<VAR>s : ι → Set (β × β)<VAR>hb : (𝓤 β).HasBasis p s<VAR>S : Set α<GOAL>(𝓤 (α →ᵤ[𝔖] β)).HasBasis p fun i => UniformOnFun.gen 𝔖 S (s i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_4<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>h : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖<VAR>p : ι → Prop<VAR>s : ι → Set (β × β)<VAR>hb : (𝓤 β).HasBasis p s<GOAL>DirectedOn ((fun s => UniformSpace.comap s.restrict (UniformFun.uniformSpace (↑s) β)) ⁻¹'o GE.ge) 𝔖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_4<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>h : 𝔖.Nonempty<VAR>h' : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖<VAR>p : ι → Prop<VAR>s : ι → Set (β × β)<VAR>hb : (𝓤 β).HasBasis p s<GOAL>(𝓤 (α →ᵤ[𝔖] β)).HasBasis (fun Si => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si => UniformOnFun.gen 𝔖 Si.1 (s Si.2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>h : 𝔖.Nonempty<VAR>h' : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖<GOAL>(𝓤 (α →ᵤ[𝔖] β)).HasBasis (fun SV => SV.1 ∈ 𝔖 ∧ SV.2 ∈ 𝓤 β) fun SV => UniformOnFun.gen 𝔖 SV.1 SV.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>Nonempty ι<VAR>t : ι → Set α<VAR>p : ι' → Prop<VAR>V : ι' → Set (β × β)<VAR>ht : ∀ (i : ι), t i ∈ 𝔖<VAR>hdir : Directed (fun x x_1 => x ⊆ x_1) t<VAR>hex : ∀ s ∈ 𝔖, ∃ i, s ⊆ t i<VAR>hb : (𝓤 β).HasBasis p V<GOAL>(𝓤 (α →ᵤ[𝔖] β)).HasBasis (fun i => p i.2) fun i => UniformOnFun.gen 𝔖 (t i.1) (V i.2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>ι : Type u_5<VAR>Preorder ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>t : ι → Set α<VAR>V : ι → Set (β × β)<VAR>ht : ∀ (n : ι), t n ∈ 𝔖<VAR>hmono : Monotone t<VAR>hex : ∀ s ∈ 𝔖, ∃ n, s ⊆ t n<VAR>hb : (𝓤 β).HasAntitoneBasis V<GOAL>(𝓤 (α →ᵤ[𝔖] β)).HasAntitoneBasis fun n => UniformOnFun.gen 𝔖 (t n) (V n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>(𝓤 β).IsCountablyGenerated<VAR>t : ℕ → Set α<VAR>ht : ∀ (n : ℕ), t n ∈ 𝔖<VAR>hmono : Monotone t<VAR>hex : ∀ s ∈ 𝔖, ∃ n, s ⊆ t n<GOAL>(𝓤 (α →ᵤ[𝔖] β)).IsCountablyGenerated
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_4<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>f : α →ᵤ[𝔖] β<VAR>h : 𝔖.Nonempty<VAR>h' : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖<VAR>p : ι → Prop<VAR>s : ι → Set (β × β)<VAR>hb : (𝓤 β).HasBasis p s<GOAL>(𝓝 f).HasBasis (fun Si => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si => {g | (g, f) ∈ UniformOnFun.gen 𝔖 Si.1 (s Si.2)}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>f : α →ᵤ[𝔖] β<VAR>h : 𝔖.Nonempty<VAR>h' : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖<GOAL>(𝓝 f).HasBasis (fun SV => SV.1 ∈ 𝔖 ∧ SV.2 ∈ 𝓤 β) fun SV => {g | (g, f) ∈ UniformOnFun.gen 𝔖 SV.1 SV.2}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>h : s ∈ 𝔖<GOAL>UniformContinuous (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(UniformOnFun.toFun 𝔖))