ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>ι : Sort u_5<VAR>p : ι → Prop<VAR>V : ι → Set (β × β)<VAR>h : (𝓤 β).HasBasis p V<GOAL>𝓤 (α →ᵤ[𝔖] β) = ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<GOAL>𝓤 (α →ᵤ[𝔖] β) = ⨅ s ∈ 𝔖, ⨅ V ∈ 𝓤 β, 𝓟 (UniformOnFun.gen 𝔖 s V)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>hs : s ∈ 𝔖<VAR>V : Set (β × β)<VAR>hV : V ∈ 𝓤 β<GOAL>UniformOnFun.gen 𝔖 s V ∈ 𝓤 (α →ᵤ[𝔖] β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>ι : Sort u_5<VAR>p : ι → Prop<VAR>V : ι → Set (β × β)<VAR>h : (𝓤 β).HasBasis p V<VAR>f : α →ᵤ[𝔖] β<GOAL>𝓝 f = ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 {g | ∀ x ∈ s, ((UniformOnFun.toFun 𝔖) f x, (UniformOnFun.toFun 𝔖) g x) ∈ V i}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>f : α →ᵤ[𝔖] β<GOAL>𝓝 f = ⨅ s ∈ 𝔖, ⨅ V ∈ 𝓤 β, 𝓟 {g | ∀ x ∈ s, ((UniformOnFun.toFun 𝔖) f x, (UniformOnFun.toFun 𝔖) g x) ∈ V}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>f : α →ᵤ[𝔖] β<VAR>hs : s ∈ 𝔖<VAR>V : Set (β × β)<VAR>hV : V ∈ 𝓤 β<GOAL>{g | ∀ x ∈ s, ((UniformOnFun.toFun 𝔖) f x, (UniformOnFun.toFun 𝔖) g x) ∈ V} ∈ 𝓝 f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<GOAL>UniformContinuous fun f => (UniformOnFun.ofFun 𝔖) (UniformFun.toFun f)
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>u₁ u₂ : UniformSpace γ<VAR>hu : u₁ ≤ u₂<VAR>𝔖₁ 𝔖₂ : Set (Set α)<VAR>h𝔖 : 𝔖₂ ⊆ 𝔖₁<GOAL>UniformOnFun.uniformSpace α γ 𝔖₁ ≤ UniformOnFun.uniformSpace α γ 𝔖₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>x : α<VAR>hxs : x ∈ s<VAR>hs : s ∈ 𝔖<GOAL>UniformContinuous (Function.eval x ∘ ⇑(UniformOnFun.toFun 𝔖))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>x : α<VAR>hx : x ∈ ⋃₀ 𝔖<GOAL>UniformContinuous (Function.eval x ∘ ⇑(UniformOnFun.toFun 𝔖))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>h : ⋃₀ 𝔖 = Set.univ<VAR>x : α<GOAL>UniformContinuous (Function.eval x ∘ ⇑(UniformOnFun.toFun 𝔖))
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>𝔖 : Set (Set α)<VAR>u : ι → UniformSpace γ<GOAL>UniformOnFun.uniformSpace α γ 𝔖 = ⨅ i, UniformOnFun.uniformSpace α γ 𝔖
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>𝔖 : Set (Set α)<VAR>u₁ u₂ : UniformSpace γ<GOAL>UniformOnFun.uniformSpace α γ 𝔖 = UniformOnFun.uniformSpace α γ 𝔖 ⊓ UniformOnFun.uniformSpace α γ 𝔖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>f : γ → β<GOAL>UniformOnFun.uniformSpace α γ 𝔖 = UniformSpace.comap (fun x => f ∘ x) (UniformOnFun.uniformSpace α β 𝔖)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>UniformSpace γ<VAR>f : γ → β<VAR>hf : UniformContinuous f<GOAL>UniformContinuous (⇑(UniformOnFun.ofFun 𝔖) ∘ (fun x => f ∘ x) ∘ ⇑(UniformOnFun.toFun 𝔖))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>UniformSpace γ<VAR>f : γ → β<VAR>hf : UniformInducing f<GOAL>UniformInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ (fun x => f ∘ x) ∘ ⇑(UniformOnFun.toFun 𝔖))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>UniformSpace γ<VAR>f : γ → β<VAR>hf : UniformEmbedding f<GOAL>UniformEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ (fun x => f ∘ x) ∘ ⇑(UniformOnFun.toFun 𝔖))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>𝔗 : Set (Set γ)<VAR>f : γ → α<VAR>hf : Set.MapsTo (fun x => f '' x) 𝔗 𝔖<GOAL>UniformContinuous fun g => (UniformOnFun.ofFun 𝔗) ((UniformOnFun.toFun 𝔖) g ∘ f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>T2Space β<VAR>h : ⋃₀ 𝔖 = Set.univ<GOAL>T2Space (α →ᵤ[𝔖] β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<GOAL>UniformContinuous ((⋃₀ 𝔖).restrict ∘ ⇑(UniformOnFun.toFun 𝔖))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>h : ⋃₀ 𝔖 = Set.univ<GOAL>UniformContinuous ⇑(UniformOnFun.toFun 𝔖)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>TopologicalSpace α<VAR>f : α →ᵤ[𝔖] β<VAR>x : α<VAR>h𝔖 : ∃ V ∈ 𝔖, V ∈ 𝓝 x<VAR>hc : ContinuousAt ((UniformOnFun.toFun 𝔖) f) x<GOAL>ContinuousAt (fun fx => (UniformOnFun.toFun 𝔖) fx.1 fx.2) (f, x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>TopologicalSpace α<VAR>h𝔖 : ∀ (x : α), ∃ V ∈ 𝔖, V ∈ 𝓝 x<GOAL>ContinuousOn (fun fx => (UniformOnFun.toFun 𝔖) fx.1 fx.2) {fx | ContinuousAt ((UniformOnFun.toFun 𝔖) fx.1) fx.2}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_4<VAR>p : Filter ι<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>F : ι → α →ᵤ[𝔖] β<VAR>f : α →ᵤ[𝔖] β<GOAL>Filter.Tendsto F p (𝓝 f) ↔ ∀ s ∈ 𝔖, TendstoUniformlyOn (⇑(UniformOnFun.toFun 𝔖) ∘ F) ((UniformOnFun.toFun 𝔖) f) p s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>f : X → α →ᵤ[𝔖] β<GOAL>Continuous f ↔ ∀ s ∈ 𝔖, Continuous (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(UniformOnFun.toFun 𝔖) ∘ f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>TopologicalSpace α<VAR>h : RestrictGenTopology 𝔖<GOAL>IsClosed {f | Continuous ((UniformOnFun.toFun 𝔖) f)}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>t : TopologicalSpace α<VAR>h : t ≤ ⨆ s ∈ 𝔖, TopologicalSpace.coinduced Subtype.val inferInstance<GOAL>IsClosed {f | Continuous ((UniformOnFun.toFun 𝔖) f)}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>δ₁ : Type u_5<VAR>δ₂ : Type u_6<VAR>φ₁ : δ₁ → α<VAR>φ₂ : δ₂ → α<VAR>𝔗₁ : Set (Set δ₁)<VAR>𝔗₂ : Set (Set δ₂)<VAR>h_image₁ : Set.MapsTo (fun x => φ₁ '' x) 𝔗₁ 𝔖<VAR>h_image₂ : Set.MapsTo (fun x => φ₂ '' x) 𝔗₂ 𝔖<VAR>h_preimage₁ : Set.MapsTo (fun x => φ₁ ⁻¹' x) 𝔖 𝔗₁<VAR>h_preimage₂ : Set.MapsTo (fun x => φ₂ ⁻¹' x) 𝔖 𝔗₂<VAR>h_cover : ∀ S ∈ 𝔖, S ⊆ Set.range φ₁ ∪ Set.range φ₂<GOAL>UniformOnFun.uniformSpace α β 𝔖 = UniformSpace.comap (⇑(UniformOnFun.ofFun 𝔗₁) ∘ (fun x => x ∘ φ₁) ∘ ⇑(UniformOnFun.toFun 𝔖)) (UniformOnFun.uniformSpace δ₁ β 𝔗₁) ⊓ UniformSpace.comap (⇑(UniformOnFun.ofFun 𝔗₂) ∘ (fun x => x ∘ φ₂) ∘ ⇑(UniformOnFun.toFun 𝔖)) (UniformOnFun.uniformSpace δ₂ β 𝔗₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_4<VAR>UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>δ : ι → Type u_5<VAR>φ : (i : ι) → δ i → α<VAR>𝔗 : (i : ι) → Set (Set (δ i))<VAR>h_image : ∀ (i : ι), Set.MapsTo (fun x => φ i '' x) (𝔗 i) 𝔖<VAR>h_preimage : ∀ (i : ι), Set.MapsTo (fun x => φ i ⁻¹' x) 𝔖 (𝔗 i)<VAR>h_cover : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, Set.range (φ i)<GOAL>UniformOnFun.uniformSpace α β 𝔖 = ⨅ i, UniformSpace.comap (⇑(UniformOnFun.ofFun (𝔗 i)) ∘ (fun x => x ∘ φ i) ∘ ⇑(UniformOnFun.toFun 𝔖)) (UniformOnFun.uniformSpace (δ i) β (𝔗 i))
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>F : ι → X → α<VAR>x₀ : X<VAR>H : EquicontinuousAt F x₀<VAR>S : Set X<GOAL>EquicontinuousWithinAt F S x₀
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>F : ι → X → α<VAR>x₀ : X<VAR>S T : Set X<VAR>H : EquicontinuousWithinAt F T x₀<VAR>hST : S ⊆ T<GOAL>EquicontinuousWithinAt F S x₀
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>F : ι → X → α<VAR>x₀ : X<GOAL>EquicontinuousWithinAt F Set.univ x₀ ↔ EquicontinuousAt F x₀
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>F : ι → X → α<VAR>S : Set X<VAR>x₀ : ↑S<GOAL>EquicontinuousAt (S.restrict ∘ F) x₀ ↔ EquicontinuousWithinAt F S ↑x₀
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>F : ι → X → α<VAR>H : Equicontinuous F<VAR>S : Set X<GOAL>EquicontinuousOn F S
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>F : ι → X → α<VAR>S T : Set X<VAR>H : EquicontinuousOn F T<VAR>hST : S ⊆ T<GOAL>EquicontinuousOn F S
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>F : ι → X → α<GOAL>EquicontinuousOn F Set.univ ↔ Equicontinuous F
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>F : ι → X → α<VAR>S : Set X<GOAL>Equicontinuous (S.restrict ∘ F) ↔ EquicontinuousOn F S
<VAR>ι : Type u_1<VAR>α : Type u_7<VAR>β : Type u_9<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>F : ι → β → α<VAR>H : UniformEquicontinuous F<VAR>S : Set β<GOAL>UniformEquicontinuousOn F S
<VAR>ι : Type u_1<VAR>α : Type u_7<VAR>β : Type u_9<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>F : ι → β → α<VAR>S T : Set β<VAR>H : UniformEquicontinuousOn F T<VAR>hST : S ⊆ T<GOAL>UniformEquicontinuousOn F S
<VAR>ι : Type u_1<VAR>α : Type u_7<VAR>β : Type u_9<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>F : ι → β → α<GOAL>UniformEquicontinuousOn F Set.univ ↔ UniformEquicontinuous F
<VAR>ι : Type u_1<VAR>α : Type u_7<VAR>β : Type u_9<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>F : ι → β → α<VAR>S : Set β<GOAL>UniformEquicontinuous (S.restrict ∘ F) ↔ UniformEquicontinuousOn F S
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>h : IsEmpty ι<VAR>F : ι → X → α<VAR>x₀ : X<GOAL>EquicontinuousAt F x₀
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>h : IsEmpty ι<VAR>F : ι → X → α<VAR>S : Set X<VAR>x₀ : X<GOAL>EquicontinuousWithinAt F S x₀
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>IsEmpty ι<VAR>F : ι → X → α<GOAL>Equicontinuous F
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>IsEmpty ι<VAR>F : ι → X → α<VAR>S : Set X<GOAL>EquicontinuousOn F S
<VAR>ι : Type u_1<VAR>α : Type u_7<VAR>β : Type u_9<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>h : IsEmpty ι<VAR>F : ι → β → α<GOAL>UniformEquicontinuous F
<VAR>ι : Type u_1<VAR>α : Type u_7<VAR>β : Type u_9<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>h : IsEmpty ι<VAR>F : ι → β → α<VAR>S : Set β<GOAL>UniformEquicontinuousOn F S
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>Finite ι<VAR>F : ι → X → α<VAR>x₀ : X<GOAL>EquicontinuousAt F x₀ ↔ ∀ (i : ι), ContinuousAt (F i) x₀
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>Finite ι<VAR>F : ι → X → α<VAR>S : Set X<VAR>x₀ : X<GOAL>EquicontinuousWithinAt F S x₀ ↔ ∀ (i : ι), ContinuousWithinAt (F i) S x₀
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>Finite ι<VAR>F : ι → X → α<GOAL>Equicontinuous F ↔ ∀ (i : ι), Continuous (F i)
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>Finite ι<VAR>F : ι → X → α<VAR>S : Set X<GOAL>EquicontinuousOn F S ↔ ∀ (i : ι), ContinuousOn (F i) S
<VAR>ι : Type u_1<VAR>α : Type u_7<VAR>β : Type u_9<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>Finite ι<VAR>F : ι → β → α<GOAL>UniformEquicontinuous F ↔ ∀ (i : ι), UniformContinuous (F i)
<VAR>ι : Type u_1<VAR>α : Type u_7<VAR>β : Type u_9<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>Finite ι<VAR>F : ι → β → α<VAR>S : Set β<GOAL>UniformEquicontinuousOn F S ↔ ∀ (i : ι), UniformContinuousOn (F i) S
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>Unique ι<VAR>F : ι → X → α<VAR>x : X<GOAL>EquicontinuousAt F x ↔ ContinuousAt (F default) x
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>Unique ι<VAR>F : ι → X → α<VAR>S : Set X<VAR>x : X<GOAL>EquicontinuousWithinAt F S x ↔ ContinuousWithinAt (F default) S x
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>Unique ι<VAR>F : ι → X → α<GOAL>Equicontinuous F ↔ Continuous (F default)
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>Unique ι<VAR>F : ι → X → α<VAR>S : Set X<GOAL>EquicontinuousOn F S ↔ ContinuousOn (F default) S
<VAR>ι : Type u_1<VAR>α : Type u_7<VAR>β : Type u_9<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>Unique ι<VAR>F : ι → β → α<GOAL>UniformEquicontinuous F ↔ UniformContinuous (F default)
<VAR>ι : Type u_1<VAR>α : Type u_7<VAR>β : Type u_9<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>Unique ι<VAR>F : ι → β → α<VAR>S : Set β<GOAL>UniformEquicontinuousOn F S ↔ UniformContinuousOn (F default) S
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>F : ι → X → α<VAR>S : Set X<VAR>x₀ : X<VAR>hx₀ : x₀ ∈ S<GOAL>EquicontinuousWithinAt F S x₀ ↔ ∀ U ∈ uniformity α, ∃ V ∈ nhdsWithin x₀ S, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>F : ι → X → α<VAR>x₀ : X<GOAL>EquicontinuousAt F x₀ ↔ ∀ U ∈ uniformity α, ∃ V ∈ nhds x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
<VAR>ι : Type u_1<VAR>α : Type u_7<VAR>β : Type u_9<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>F : ι → β → α<VAR>h : UniformEquicontinuous F<GOAL>Equicontinuous F
<VAR>ι : Type u_1<VAR>α : Type u_7<VAR>β : Type u_9<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>F : ι → β → α<VAR>S : Set β<VAR>h : UniformEquicontinuousOn F S<GOAL>EquicontinuousOn F S
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>F : ι → X → α<VAR>x₀ : X<VAR>h : EquicontinuousAt F x₀<VAR>i : ι<GOAL>ContinuousAt (F i) x₀
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>F : ι → X → α<VAR>S : Set X<VAR>x₀ : X<VAR>h : EquicontinuousWithinAt F S x₀<VAR>i : ι<GOAL>ContinuousWithinAt (F i) S x₀
<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>H : Set (X → α)<VAR>x₀ : X<VAR>h : H.EquicontinuousAt x₀<VAR>f : X → α<VAR>hf : f ∈ H<GOAL>ContinuousAt f x₀
<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>H : Set (X → α)<VAR>S : Set X<VAR>x₀ : X<VAR>h : H.EquicontinuousWithinAt S x₀<VAR>f : X → α<VAR>hf : f ∈ H<GOAL>ContinuousWithinAt f S x₀
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>F : ι → X → α<VAR>h : Equicontinuous F<VAR>i : ι<GOAL>Continuous (F i)
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>F : ι → X → α<VAR>S : Set X<VAR>h : EquicontinuousOn F S<VAR>i : ι<GOAL>ContinuousOn (F i) S
<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>H : Set (X → α)<VAR>h : H.Equicontinuous<VAR>f : X → α<VAR>hf : f ∈ H<GOAL>Continuous f
<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>H : Set (X → α)<VAR>S : Set X<VAR>h : H.EquicontinuousOn S<VAR>f : X → α<VAR>hf : f ∈ H<GOAL>ContinuousOn f S
<VAR>ι : Type u_1<VAR>α : Type u_7<VAR>β : Type u_9<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>F : ι → β → α<VAR>h : UniformEquicontinuous F<VAR>i : ι<GOAL>UniformContinuous (F i)
<VAR>ι : Type u_1<VAR>α : Type u_7<VAR>β : Type u_9<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>F : ι → β → α<VAR>S : Set β<VAR>h : UniformEquicontinuousOn F S<VAR>i : ι<GOAL>UniformContinuousOn (F i) S
<VAR>α : Type u_7<VAR>β : Type u_9<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>H : Set (β → α)<VAR>h : H.UniformEquicontinuous<VAR>f : β → α<VAR>hf : f ∈ H<GOAL>UniformContinuous f
<VAR>α : Type u_7<VAR>β : Type u_9<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>H : Set (β → α)<VAR>S : Set β<VAR>h : H.UniformEquicontinuousOn S<VAR>f : β → α<VAR>hf : f ∈ H<GOAL>UniformContinuousOn f S
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>F : ι → X → α<VAR>x₀ : X<VAR>h : EquicontinuousAt F x₀<VAR>u : κ → ι<GOAL>EquicontinuousAt (F ∘ u) x₀
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>F : ι → X → α<VAR>S : Set X<VAR>x₀ : X<VAR>h : EquicontinuousWithinAt F S x₀<VAR>u : κ → ι<GOAL>EquicontinuousWithinAt (F ∘ u) S x₀
<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>H H' : Set (X → α)<VAR>x₀ : X<VAR>h : H.EquicontinuousAt x₀<VAR>hH : H' ⊆ H<GOAL>H'.EquicontinuousAt x₀
<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>H H' : Set (X → α)<VAR>S : Set X<VAR>x₀ : X<VAR>h : H.EquicontinuousWithinAt S x₀<VAR>hH : H' ⊆ H<GOAL>H'.EquicontinuousWithinAt S x₀
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>F : ι → X → α<VAR>h : Equicontinuous F<VAR>u : κ → ι<GOAL>Equicontinuous (F ∘ u)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>F : ι → X → α<VAR>S : Set X<VAR>h : EquicontinuousOn F S<VAR>u : κ → ι<GOAL>EquicontinuousOn (F ∘ u) S
<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>H H' : Set (X → α)<VAR>h : H.Equicontinuous<VAR>hH : H' ⊆ H<GOAL>H'.Equicontinuous
<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>H H' : Set (X → α)<VAR>S : Set X<VAR>h : H.EquicontinuousOn S<VAR>hH : H' ⊆ H<GOAL>H'.EquicontinuousOn S
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_7<VAR>β : Type u_9<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>F : ι → β → α<VAR>h : UniformEquicontinuous F<VAR>u : κ → ι<GOAL>UniformEquicontinuous (F ∘ u)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_7<VAR>β : Type u_9<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>F : ι → β → α<VAR>S : Set β<VAR>h : UniformEquicontinuousOn F S<VAR>u : κ → ι<GOAL>UniformEquicontinuousOn (F ∘ u) S
<VAR>α : Type u_7<VAR>β : Type u_9<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>H H' : Set (β → α)<VAR>h : H.UniformEquicontinuous<VAR>hH : H' ⊆ H<GOAL>H'.UniformEquicontinuous
<VAR>α : Type u_7<VAR>β : Type u_9<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>H H' : Set (β → α)<VAR>S : Set β<VAR>h : H.UniformEquicontinuousOn S<VAR>hH : H' ⊆ H<GOAL>H'.UniformEquicontinuousOn S
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>F : ι → X → α<VAR>x₀ : X<GOAL>EquicontinuousAt F x₀ ↔ EquicontinuousAt Subtype.val x₀
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>F : ι → X → α<VAR>S : Set X<VAR>x₀ : X<GOAL>EquicontinuousWithinAt F S x₀ ↔ EquicontinuousWithinAt Subtype.val S x₀
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>F : ι → X → α<GOAL>Equicontinuous F ↔ Equicontinuous Subtype.val
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>F : ι → X → α<VAR>S : Set X<GOAL>EquicontinuousOn F S ↔ EquicontinuousOn Subtype.val S
<VAR>ι : Type u_1<VAR>α : Type u_7<VAR>β : Type u_9<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>F : ι → β → α<GOAL>UniformEquicontinuous F ↔ UniformEquicontinuous Subtype.val
<VAR>ι : Type u_1<VAR>α : Type u_7<VAR>β : Type u_9<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>F : ι → β → α<VAR>S : Set β<GOAL>UniformEquicontinuousOn F S ↔ UniformEquicontinuousOn Subtype.val S
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>F : ι → X → α<VAR>x₀ : X<GOAL>EquicontinuousAt F x₀ ↔ ContinuousAt (⇑UniformFun.ofFun ∘ Function.swap F) x₀
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>F : ι → X → α<VAR>S : Set X<VAR>x₀ : X<GOAL>EquicontinuousWithinAt F S x₀ ↔ ContinuousWithinAt (⇑UniformFun.ofFun ∘ Function.swap F) S x₀
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>F : ι → X → α<GOAL>Equicontinuous F ↔ Continuous (⇑UniformFun.ofFun ∘ Function.swap F)
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>F : ι → X → α<VAR>S : Set X<GOAL>EquicontinuousOn F S ↔ ContinuousOn (⇑UniformFun.ofFun ∘ Function.swap F) S
<VAR>ι : Type u_1<VAR>α : Type u_7<VAR>β : Type u_9<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>F : ι → β → α<GOAL>UniformEquicontinuous F ↔ UniformContinuous (⇑UniformFun.ofFun ∘ Function.swap F)
<VAR>ι : Type u_1<VAR>α : Type u_7<VAR>β : Type u_9<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>F : ι → β → α<VAR>S : Set β<GOAL>UniformEquicontinuousOn F S ↔ UniformContinuousOn (⇑UniformFun.ofFun ∘ Function.swap F) S
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>α' : Type u_8<VAR>tX : TopologicalSpace X<VAR>u : κ → UniformSpace α'<VAR>F : ι → X → α'<VAR>S : Set X<VAR>x₀ : X<GOAL>EquicontinuousWithinAt F S x₀ ↔ ∀ (k : κ), EquicontinuousWithinAt F S x₀
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>α' : Type u_8<VAR>tX : TopologicalSpace X<VAR>u : κ → UniformSpace α'<VAR>F : ι → X → α'<VAR>x₀ : X<GOAL>EquicontinuousAt F x₀ ↔ ∀ (k : κ), EquicontinuousAt F x₀
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>α' : Type u_8<VAR>tX : TopologicalSpace X<VAR>u : κ → UniformSpace α'<VAR>F : ι → X → α'<GOAL>Equicontinuous F ↔ ∀ (k : κ), Equicontinuous F
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>α' : Type u_8<VAR>tX : TopologicalSpace X<VAR>u : κ → UniformSpace α'<VAR>F : ι → X → α'<VAR>S : Set X<GOAL>EquicontinuousOn F S ↔ ∀ (k : κ), EquicontinuousOn F S
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>uβ : UniformSpace β<VAR>u : κ → UniformSpace α'<VAR>F : ι → β → α'<GOAL>UniformEquicontinuous F ↔ ∀ (k : κ), UniformEquicontinuous F
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>uβ : UniformSpace β<VAR>u : κ → UniformSpace α'<VAR>F : ι → β → α'<VAR>S : Set β<GOAL>UniformEquicontinuousOn F S ↔ ∀ (k : κ), UniformEquicontinuousOn F S
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X' : Type u_4<VAR>α : Type u_7<VAR>uα : UniformSpace α<VAR>t : κ → TopologicalSpace X'<VAR>F : ι → X' → α<VAR>S : Set X'<VAR>x₀ : X'<VAR>k : κ<VAR>hk : EquicontinuousWithinAt F S x₀<GOAL>EquicontinuousWithinAt F S x₀
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X' : Type u_4<VAR>α : Type u_7<VAR>uα : UniformSpace α<VAR>t : κ → TopologicalSpace X'<VAR>F : ι → X' → α<VAR>x₀ : X'<VAR>k : κ<VAR>hk : EquicontinuousAt F x₀<GOAL>EquicontinuousAt F x₀
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X' : Type u_4<VAR>α : Type u_7<VAR>uα : UniformSpace α<VAR>t : κ → TopologicalSpace X'<VAR>F : ι → X' → α<VAR>k : κ<VAR>hk : Equicontinuous F<GOAL>Equicontinuous F
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X' : Type u_4<VAR>α : Type u_7<VAR>uα : UniformSpace α<VAR>t : κ → TopologicalSpace X'<VAR>F : ι → X' → α<VAR>S : Set X'<VAR>k : κ<VAR>hk : EquicontinuousOn F S<GOAL>EquicontinuousOn F S
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_7<VAR>β' : Type u_10<VAR>uα : UniformSpace α<VAR>u : κ → UniformSpace β'<VAR>F : ι → β' → α<VAR>k : κ<VAR>hk : UniformEquicontinuous F<GOAL>UniformEquicontinuous F
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_7<VAR>β' : Type u_10<VAR>uα : UniformSpace α<VAR>u : κ → UniformSpace β'<VAR>F : ι → β' → α<VAR>S : Set β'<VAR>k : κ<VAR>hk : UniformEquicontinuousOn F S<GOAL>UniformEquicontinuousOn F S
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>p : κ → Prop<VAR>s : κ → Set X<VAR>F : ι → X → α<VAR>x₀ : X<VAR>hX : (nhds x₀).HasBasis p s<GOAL>EquicontinuousAt F x₀ ↔ ∀ U ∈ uniformity α, ∃ k, p k ∧ ∀ x ∈ s k, ∀ (i : ι), (F i x₀, F i x) ∈ U