ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>B : Type u<VAR>F : Type v<VAR>E : B → Type w₁<VAR>B' : Type w₂<VAR>TopologicalSpace B'<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>TopologicalSpace F<VAR>TopologicalSpace B<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>f : B' → B<VAR>x : B'<GOAL>Continuous (Bundle.TotalSpace.mk x)
<GOAL>AbsoluteValue.abs.uniformSpace = PseudoMetricSpace.toUniformSpace
<GOAL>UniformContinuous ⇑CompareReals.compareEquiv
<GOAL>UniformContinuous ⇑CompareReals.compareEquiv.symm
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>R : Type u_2<VAR>CommRing R<VAR>abv : AbsoluteValue R 𝕜<GOAL>(𝓤 R).HasBasis (fun x => 0 < x) fun ε => {p | abv (p.2 - p.1) < ε}
<VAR>α : Type u<VAR>UniformSpace α<VAR>self : AbstractCompletion α<GOAL>UniformInducing self.coe
<VAR>α : Type u<VAR>UniformSpace α<VAR>self : AbstractCompletion α<GOAL>CompleteSpace self.space
<VAR>α : Type u<VAR>UniformSpace α<VAR>self : AbstractCompletion α<GOAL>DenseRange self.coe
<VAR>α : Type u<VAR>UniformSpace α<VAR>self : AbstractCompletion α<GOAL>T0Space self.space
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>pkg : AbstractCompletion α<GOAL>closure (Set.range pkg.coe) = Set.univ
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>pkg : AbstractCompletion α<GOAL>DenseInducing pkg.coe
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>pkg : AbstractCompletion α<GOAL>UniformContinuous pkg.coe
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>pkg : AbstractCompletion α<GOAL>Continuous pkg.coe
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>p : pkg.space → Prop<VAR>a : pkg.space<VAR>hp : IsClosed {a | p a}<VAR>ih : ∀ (a : α), p (pkg.coe a)<GOAL>p a
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>T2Space β<VAR>f g : pkg.space → β<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>h : ∀ (a : α), f (pkg.coe a) = g (pkg.coe a)<GOAL>f = g
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>f : α → β<VAR>hf : UniformContinuous f<GOAL>pkg.extend f = ⋯.extend f
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>f : α → β<VAR>T2Space β<VAR>hf : UniformContinuous f<VAR>a : α<GOAL>pkg.extend f (pkg.coe a) = f a
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>f : α → β<VAR>CompleteSpace β<GOAL>UniformContinuous (pkg.extend f)
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>f : α → β<VAR>CompleteSpace β<GOAL>Continuous (pkg.extend f)
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>f : α → β<VAR>CompleteSpace β<VAR>T0Space β<VAR>hf : UniformContinuous f<VAR>g : pkg.space → β<VAR>hg : UniformContinuous g<VAR>h : ∀ (a : α), f a = g (pkg.coe a)<GOAL>pkg.extend f = g
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>CompleteSpace β<VAR>T0Space β<VAR>f : pkg.space → β<VAR>hf : UniformContinuous f<GOAL>pkg.extend (f ∘ pkg.coe) = f
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>pkg' : AbstractCompletion β<VAR>f : α → β<GOAL>UniformContinuous (pkg.map pkg' f)
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>pkg' : AbstractCompletion β<VAR>f : α → β<GOAL>Continuous (pkg.map pkg' f)
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>pkg' : AbstractCompletion β<VAR>f : α → β<VAR>hf : UniformContinuous f<VAR>a : α<GOAL>pkg.map pkg' f (pkg.coe a) = pkg'.coe (f a)
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>pkg' : AbstractCompletion β<VAR>f : α → β<VAR>g : pkg.space → pkg'.space<VAR>hg : UniformContinuous g<VAR>h : ∀ (a : α), pkg'.coe (f a) = g (pkg.coe a)<GOAL>pkg.map pkg' f = g
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>pkg : AbstractCompletion α<GOAL>pkg.map pkg id = id
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>pkg' : AbstractCompletion β<VAR>γ : Type u_3<VAR>UniformSpace γ<VAR>CompleteSpace γ<VAR>T0Space γ<VAR>f : β → γ<VAR>g : α → β<VAR>hf : UniformContinuous f<VAR>hg : UniformContinuous g<GOAL>pkg'.extend f ∘ pkg.map pkg' g = pkg.extend (f ∘ g)
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>pkg' : AbstractCompletion β<VAR>γ : Type u_3<VAR>UniformSpace γ<VAR>pkg'' : AbstractCompletion γ<VAR>g : β → γ<VAR>f : α → β<VAR>hg : UniformContinuous g<VAR>hf : UniformContinuous f<GOAL>pkg'.map pkg'' g ∘ pkg.map pkg' f = pkg.map pkg'' (g ∘ f)
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>pkg pkg' : AbstractCompletion α<GOAL>UniformContinuous (pkg.compare pkg')
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>pkg pkg' : AbstractCompletion α<VAR>a : α<GOAL>pkg.compare pkg' (pkg.coe a) = pkg'.coe a
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>pkg pkg' : AbstractCompletion α<GOAL>pkg.compare pkg' ∘ pkg'.compare pkg = id
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>pkg pkg' : AbstractCompletion α<GOAL>UniformContinuous ⇑(pkg.compareEquiv pkg')
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>pkg pkg' : AbstractCompletion α<GOAL>UniformContinuous ⇑(pkg.compareEquiv pkg').symm
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>pkg pkg' : AbstractCompletion α<VAR>γ : Type u_3<VAR>TopologicalSpace γ<VAR>T3Space γ<VAR>f : α → γ<VAR>cont_f : Continuous f<GOAL>(∀ (a : pkg.space), Filter.Tendsto f (Filter.comap pkg.coe (nhds a)) (nhds (⋯.extend f a))) → ⋯.extend f ∘ pkg'.compare pkg = ⋯.extend f
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>pkg' : AbstractCompletion β<VAR>γ : Type u_3<VAR>UniformSpace γ<VAR>T0Space γ<VAR>f : α → β → γ<VAR>hf : UniformContinuous (Function.uncurry f)<VAR>a : α<VAR>b : β<GOAL>pkg.extend₂ pkg' f (pkg.coe a) (pkg'.coe b) = f a b
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>pkg' : AbstractCompletion β<VAR>γ : Type u_3<VAR>UniformSpace γ<VAR>f : α → β → γ<VAR>CompleteSpace γ<GOAL>UniformContinuous₂ (pkg.extend₂ pkg' f)
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>pkg' : AbstractCompletion β<VAR>γ : Type u_3<VAR>UniformSpace γ<VAR>pkg'' : AbstractCompletion γ<VAR>f : α → β → γ<GOAL>UniformContinuous₂ (pkg.map₂ pkg' pkg'' f)
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>pkg' : AbstractCompletion β<VAR>γ : Type u_3<VAR>UniformSpace γ<VAR>pkg'' : AbstractCompletion γ<VAR>δ : Type u_4<VAR>TopologicalSpace δ<VAR>f : α → β → γ<VAR>a : δ → pkg.space<VAR>b : δ → pkg'.space<VAR>ha : Continuous a<VAR>hb : Continuous b<GOAL>Continuous fun d => pkg.map₂ pkg' pkg'' f (a d) (b d)
<VAR>α : Type u_1<VAR>UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>UniformSpace β<VAR>pkg' : AbstractCompletion β<VAR>γ : Type u_3<VAR>UniformSpace γ<VAR>pkg'' : AbstractCompletion γ<VAR>a : α<VAR>b : β<VAR>f : α → β → γ<VAR>hf : UniformContinuous₂ f<GOAL>pkg.map₂ pkg' pkg'' f (pkg.coe a) (pkg'.coe b) = pkg''.coe (f a b)
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>UniformSpace α<VAR>UniformSpace β<VAR>self : α ≃ᵤ β<GOAL>UniformContinuous self.invFun
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>UniformSpace α<VAR>UniformSpace β<VAR>self : α ≃ᵤ β<GOAL>UniformContinuous self.toFun
<VAR>α : Type u<VAR>β : Type u_1<VAR>UniformSpace α<VAR>UniformSpace β<GOAL>Function.Injective UniformEquiv.toEquiv
<VAR>α : Type u<VAR>β : Type u_1<VAR>UniformSpace α<VAR>UniformSpace β<VAR>a : α ≃ β<VAR>b : UniformContinuous a.toFun<VAR>c : UniformContinuous a.invFun<GOAL>⇑{ toEquiv := a, uniformContinuous_toFun := b, uniformContinuous_invFun := c } = ⇑a
<VAR>α : Type u<VAR>β : Type u_1<VAR>UniformSpace α<VAR>UniformSpace β<VAR>h : α ≃ᵤ β<GOAL>⇑h.toEquiv = ⇑h
<VAR>α : Type u<VAR>β : Type u_1<VAR>UniformSpace α<VAR>UniformSpace β<VAR>h : α ≃ᵤ β<GOAL>⇑h.symm = ⇑h.symm
<VAR>α : Type u<VAR>β : Type u_1<VAR>UniformSpace α<VAR>UniformSpace β<VAR>h h' : α ≃ᵤ β<VAR>H : ∀ (x : α), h x = h' x<GOAL>h = h'
<VAR>α : Type u_4<VAR>UniformSpace α<GOAL>⇑(UniformEquiv.refl α) = id
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>UniformSpace α<VAR>UniformSpace β<VAR>UniformSpace γ<VAR>h₁ : α ≃ᵤ β<VAR>h₂ : β ≃ᵤ γ<VAR>a : α<GOAL>(h₁.trans h₂) a = h₂ (h₁ a)
<VAR>α : Type u<VAR>β : Type u_1<VAR>UniformSpace α<VAR>UniformSpace β<VAR>a : α ≃ β<VAR>b : UniformContinuous a.toFun<VAR>c : UniformContinuous a.invFun<GOAL>⇑{ toEquiv := a, uniformContinuous_toFun := b, uniformContinuous_invFun := c }.symm = ⇑a.symm
<VAR>α : Type u<VAR>UniformSpace α<GOAL>(UniformEquiv.refl α).symm = UniformEquiv.refl α
<VAR>α : Type u<VAR>β : Type u_1<VAR>UniformSpace α<VAR>UniformSpace β<VAR>h : α ≃ᵤ β<GOAL>UniformContinuous ⇑h
<VAR>α : Type u<VAR>β : Type u_1<VAR>UniformSpace α<VAR>UniformSpace β<VAR>h : α ≃ᵤ β<GOAL>Continuous ⇑h
<VAR>α : Type u<VAR>β : Type u_1<VAR>UniformSpace α<VAR>UniformSpace β<VAR>h : α ≃ᵤ β<GOAL>UniformContinuous ⇑h.symm
<VAR>α : Type u<VAR>β : Type u_1<VAR>UniformSpace α<VAR>UniformSpace β<VAR>h : α ≃ᵤ β<GOAL>Continuous ⇑h.symm
<VAR>α : Type u<VAR>β : Type u_1<VAR>UniformSpace α<VAR>UniformSpace β<VAR>e : α ≃ᵤ β<GOAL>⇑e.toHomeomorph = ⇑e
<VAR>α : Type u<VAR>β : Type u_1<VAR>UniformSpace α<VAR>UniformSpace β<VAR>e : α ≃ᵤ β<GOAL>⇑e.toHomeomorph.symm = ⇑e.symm
<VAR>α : Type u<VAR>β : Type u_1<VAR>UniformSpace α<VAR>UniformSpace β<VAR>h : α ≃ᵤ β<VAR>x : β<GOAL>h (h.symm x) = x
<VAR>α : Type u<VAR>β : Type u_1<VAR>UniformSpace α<VAR>UniformSpace β<VAR>h : α ≃ᵤ β<VAR>x : α<GOAL>h.symm (h x) = x
<VAR>α : Type u<VAR>β : Type u_1<VAR>UniformSpace α<VAR>UniformSpace β<VAR>h : α ≃ᵤ β<GOAL>Function.Bijective ⇑h
<VAR>α : Type u<VAR>β : Type u_1<VAR>UniformSpace α<VAR>UniformSpace β<VAR>h : α ≃ᵤ β<GOAL>Function.Injective ⇑h
<VAR>α : Type u<VAR>β : Type u_1<VAR>UniformSpace α<VAR>UniformSpace β<VAR>h : α ≃ᵤ β<GOAL>Function.Surjective ⇑h
<VAR>α : Type u<VAR>β : Type u_1<VAR>UniformSpace α<VAR>UniformSpace β<VAR>h : α ≃ᵤ β<GOAL>⇑h.symm ∘ ⇑h = id
<VAR>α : Type u<VAR>β : Type u_1<VAR>UniformSpace α<VAR>UniformSpace β<VAR>h : α ≃ᵤ β<GOAL>⇑h ∘ ⇑h.symm = id
<VAR>α : Type u<VAR>β : Type u_1<VAR>UniformSpace α<VAR>UniformSpace β<VAR>h : α ≃ᵤ β<GOAL>Set.range ⇑h = Set.univ
<VAR>α : Type u<VAR>β : Type u_1<VAR>UniformSpace α<VAR>UniformSpace β<VAR>h : α ≃ᵤ β<GOAL>Set.image ⇑h.symm = Set.preimage ⇑h
<VAR>α : Type u<VAR>β : Type u_1<VAR>UniformSpace α<VAR>UniformSpace β<VAR>h : α ≃ᵤ β<GOAL>Set.preimage ⇑h.symm = Set.image ⇑h
<VAR>α : Type u<VAR>β : Type u_1<VAR>UniformSpace α<VAR>UniformSpace β<VAR>h : α ≃ᵤ β<VAR>s : Set β<GOAL>⇑h '' (⇑h ⁻¹' s) = s
<VAR>α : Type u<VAR>β : Type u_1<VAR>UniformSpace α<VAR>UniformSpace β<VAR>h : α ≃ᵤ β<VAR>s : Set α<GOAL>⇑h ⁻¹' (⇑h '' s) = s
<VAR>α : Type u<VAR>β : Type u_1<VAR>UniformSpace α<VAR>UniformSpace β<VAR>h : α ≃ᵤ β<GOAL>UniformInducing ⇑h
<VAR>α : Type u<VAR>β : Type u_1<VAR>UniformSpace α<VAR>UniformSpace β<VAR>h : α ≃ᵤ β<GOAL>UniformSpace.comap (⇑h) inst✝ = inst✝¹
<VAR>α : Type u<VAR>β : Type u_1<VAR>UniformSpace α<VAR>UniformSpace β<VAR>h : α ≃ᵤ β<GOAL>UniformEmbedding ⇑h
<VAR>α : Type u<VAR>β : Type u_1<VAR>UniformSpace α<VAR>UniformSpace β<VAR>h : α ≃ᵤ β<GOAL>CompleteSpace α ↔ CompleteSpace β
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>UniformSpace α<VAR>UniformSpace β<VAR>UniformSpace γ<VAR>UniformSpace δ<VAR>h₁ : α ≃ᵤ β<VAR>h₂ : γ ≃ᵤ δ<GOAL>(h₁.prodCongr h₂).symm = h₁.symm.prodCongr h₂.symm
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>UniformSpace α<VAR>UniformSpace β<VAR>UniformSpace γ<VAR>UniformSpace δ<VAR>h₁ : α ≃ᵤ β<VAR>h₂ : γ ≃ᵤ δ<GOAL>⇑(h₁.prodCongr h₂) = Prod.map ⇑h₁ ⇑h₂
<VAR>α : Type u<VAR>β : Type u_1<VAR>UniformSpace α<VAR>UniformSpace β<GOAL>(UniformEquiv.prodComm α β).symm = UniformEquiv.prodComm β α
<VAR>α : Type u<VAR>β : Type u_1<VAR>UniformSpace α<VAR>UniformSpace β<GOAL>⇑(UniformEquiv.prodComm α β) = Prod.swap
<VAR>α : Type u<VAR>UniformSpace α<GOAL>⇑(UniformEquiv.prodPunit α) = fun p => p.1
<VAR>α : Type u<VAR>UniformSpace α<GOAL>⇑(UniformEquiv.punitProd α) = Prod.snd
<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>β : ι' → Type u_6<VAR>(j : ι') → UniformSpace (β j)<VAR>e : ι ≃ ι'<GOAL>(UniformEquiv.piCongrLeft e).toEquiv = Equiv.piCongrLeft β e
<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>β : ι' → Type u_6<VAR>(j : ι') → UniformSpace (β j)<VAR>e : ι ≃ ι'<GOAL>∀ (a : (b : ι) → β (e.symm.symm b)) (a_1 : ι'), (UniformEquiv.piCongrLeft e) a a_1 = (Equiv.piCongrLeft' β e.symm).symm a a_1
<VAR>ι : Type u_4<VAR>β₁ : ι → Type u_5<VAR>β₂ : ι → Type u_6<VAR>(i : ι) → UniformSpace (β₁ i)<VAR>(i : ι) → UniformSpace (β₂ i)<VAR>F : (i : ι) → β₁ i ≃ᵤ β₂ i<VAR>H : (a : ι) → β₁ a<VAR>a : ι<GOAL>(UniformEquiv.piCongrRight F) H a = (F a) (H a)
<VAR>ι : Type u_4<VAR>β₁ : ι → Type u_5<VAR>β₂ : ι → Type u_6<VAR>(i : ι) → UniformSpace (β₁ i)<VAR>(i : ι) → UniformSpace (β₂ i)<VAR>F : (i : ι) → β₁ i ≃ᵤ β₂ i<GOAL>(UniformEquiv.piCongrRight F).toEquiv = Equiv.piCongrRight fun i => (F i).toEquiv
<VAR>ι : Type u_4<VAR>β₁ : ι → Type u_5<VAR>β₂ : ι → Type u_6<VAR>(i : ι) → UniformSpace (β₁ i)<VAR>(i : ι) → UniformSpace (β₂ i)<VAR>F : (i : ι) → β₁ i ≃ᵤ β₂ i<GOAL>(UniformEquiv.piCongrRight F).symm = UniformEquiv.piCongrRight fun i => (F i).symm
<VAR>ι₁ : Type u_4<VAR>ι₂ : Type u_5<VAR>β₁ : ι₁ → Type u_6<VAR>β₂ : ι₂ → Type u_7<VAR>(i₁ : ι₁) → UniformSpace (β₁ i₁)<VAR>(i₂ : ι₂) → UniformSpace (β₂ i₂)<VAR>e : ι₁ ≃ ι₂<VAR>F : (i₁ : ι₁) → β₁ i₁ ≃ᵤ β₂ (e i₁)<GOAL>∀ (a : (i : ι₁) → β₁ i) (i₂ : ι₂), (UniformEquiv.piCongr e F) a i₂ = ⋯ ▸ (Equiv.piCongrRight fun i => (F i).toEquiv) a (e.symm i₂)
<VAR>ι₁ : Type u_4<VAR>ι₂ : Type u_5<VAR>β₁ : ι₁ → Type u_6<VAR>β₂ : ι₂ → Type u_7<VAR>(i₁ : ι₁) → UniformSpace (β₁ i₁)<VAR>(i₂ : ι₂) → UniformSpace (β₂ i₂)<VAR>e : ι₁ ≃ ι₂<VAR>F : (i₁ : ι₁) → β₁ i₁ ≃ᵤ β₂ (e i₁)<GOAL>(UniformEquiv.piCongr e F).toEquiv = (Equiv.piCongrRight fun i => (F i).toEquiv).trans (Equiv.piCongrLeft β₂ e)
<VAR>ι : Type u_4<VAR>α : Type u_5<VAR>Unique ι<VAR>UniformSpace α<GOAL>⇑(UniformEquiv.funUnique ι α) = fun f => f default
<VAR>ι : Type u_4<VAR>α : Type u_5<VAR>Unique ι<VAR>UniformSpace α<GOAL>⇑(UniformEquiv.funUnique ι α).symm = uniqueElim
<VAR>α : Fin 2 → Type u<VAR>(i : Fin 2) → UniformSpace (α i)<GOAL>⇑(UniformEquiv.piFinTwo α).symm = fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
<VAR>α : Fin 2 → Type u<VAR>(i : Fin 2) → UniformSpace (α i)<GOAL>⇑(UniformEquiv.piFinTwo α) = fun f => (f 0, f 1)
<VAR>α : Type u_4<VAR>UniformSpace α<GOAL>⇑(UniformEquiv.finTwoArrow α).symm = fun x => ![x.1, x.2]
<VAR>α : Type u_4<VAR>UniformSpace α<GOAL>⇑(UniformEquiv.finTwoArrow α) = fun f => (f 0, f 1)
<VAR>b : ℝ≥0∞<GOAL>IsOpen (Set.Ico 0 b)
<VAR>r : ℝ≥0<GOAL>Set.range ENNReal.ofNNReal ∈ 𝓝 ↑r
<VAR>α : Type u_1<VAR>f : Filter α<VAR>m : α → ℝ≥0<VAR>a : ℝ≥0<GOAL>Filter.Tendsto (fun a => ↑(m a)) f (𝓝 ↑a) ↔ Filter.Tendsto m f (𝓝 a)
<VAR>α : Type u_4<VAR>TopologicalSpace α<VAR>f : α → ℝ≥0<GOAL>(Continuous fun a => ↑(f a)) ↔ Continuous f
<VAR>r : ℝ≥0<GOAL>𝓝 ↑r = Filter.map ENNReal.ofNNReal (𝓝 r)
<VAR>α : Type u_4<VAR>l : Filter α<VAR>x : ℝ≥0<VAR>f : ℝ≥0∞ → α<GOAL>Filter.Tendsto f (𝓝 ↑x) l ↔ Filter.Tendsto (f ∘ ENNReal.ofNNReal) (𝓝 x) l
<VAR>α : Type u_4<VAR>TopologicalSpace α<VAR>x : ℝ≥0<VAR>f : ℝ≥0∞ → α<GOAL>ContinuousAt f ↑x ↔ ContinuousAt (f ∘ ENNReal.ofNNReal) x
<VAR>r p : ℝ≥0<GOAL>𝓝 (↑r, ↑p) = Filter.map (fun p => (↑p.1, ↑p.2)) (𝓝 (r, p))
<VAR>α : Type u_1<VAR>f : Filter α<VAR>m : α → ℝ<VAR>a : ℝ<VAR>h : Filter.Tendsto m f (𝓝 a)<GOAL>Filter.Tendsto (fun a => ENNReal.ofReal (m a)) f (𝓝 (ENNReal.ofReal a))
<VAR>a : ℝ≥0∞<VAR>ha : a ≠ ⊤<GOAL>Filter.Tendsto ENNReal.toNNReal (𝓝 a) (𝓝 a.toNNReal)
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f g : α → ℝ≥0∞<VAR>hfi : ∀ᶠ (x : α) in l, f x ≠ ⊤<VAR>hgi : ∀ᶠ (x : α) in l, g x ≠ ⊤<VAR>hfg : (fun x => (f x).toReal) =ᶠ[l] fun x => (g x).toReal<GOAL>f =ᶠ[l] g
<GOAL>ContinuousOn ENNReal.toNNReal {a | a ≠ ⊤}
<VAR>a : ℝ≥0∞<VAR>ha : a ≠ ⊤<GOAL>Filter.Tendsto ENNReal.toReal (𝓝 a) (𝓝 a.toReal)
<GOAL>ContinuousOn ENNReal.toReal {a | a ≠ ⊤}
<VAR>x : ℝ≥0∞<VAR>hx : x ≠ ⊤<GOAL>ContinuousAt ENNReal.toReal x
<GOAL>𝓝 ⊤ = ⨅ r, 𝓟 (Set.Ioi ↑r)
<GOAL>(𝓝 ⊤).HasBasis (fun a => a < ⊤) fun a => Set.Ioi a
<VAR>α : Type u_1<VAR>m : α → ℝ≥0∞<VAR>f : Filter α<GOAL>Filter.Tendsto m f (𝓝 ⊤) ↔ ∀ (x : ℝ≥0), ∀ᶠ (a : α) in f, ↑x < m a
<VAR>α : Type u_1<VAR>m : α → ℝ≥0∞<VAR>f : Filter α<GOAL>Filter.Tendsto m f (𝓝 ⊤) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in f, ↑n < m a
<VAR>α : Type u_1<VAR>m : α → ℝ≥0∞<VAR>f : Filter α<VAR>h : ∀ (n : ℕ), ∀ᶠ (a : α) in f, ↑n < m a<GOAL>Filter.Tendsto m f (𝓝 ⊤)
<GOAL>Filter.Tendsto (fun n => ↑n) Filter.atTop (𝓝 ⊤)
<VAR>α : Type u_1<VAR>f : α → ℝ≥0<VAR>l : Filter α<GOAL>Filter.Tendsto (fun x => ↑(f x)) l (𝓝 ⊤) ↔ Filter.Tendsto f l Filter.atTop
<VAR>α : Type u_1<VAR>f : α → ℝ<VAR>l : Filter α<GOAL>Filter.Tendsto (fun x => ENNReal.ofReal (f x)) l (𝓝 ⊤) ↔ Filter.Tendsto f l Filter.atTop
<GOAL>Filter.Tendsto ENNReal.ofReal Filter.atTop (𝓝 ⊤)
<GOAL>(𝓝 0).HasBasis (fun a => 0 < a) Set.Iic
<VAR>r : ℝ≥0<GOAL>(𝓝[>] ↑r).NeBot
<VAR>n : ℕ<GOAL>(𝓝[>] ↑n).NeBot
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>(𝓝[>] OfNat.ofNat n).NeBot
<VAR>x : ℝ≥0∞<VAR>NeZero x<GOAL>(𝓝[<] x).NeBot
<VAR>x : ℝ≥0∞<VAR>xt : x ≠ ⊤<GOAL>(𝓝 x).HasBasis (fun x => x ≠ 0) fun ε => Set.Icc (x - ε) (x + ε)
<VAR>x : ℝ≥0∞<VAR>xt : x ≠ ⊤<GOAL>(𝓝 x).HasBasis (fun x => 0 < x) fun ε => Set.Icc (x - ε) (x + ε)
<VAR>x ε : ℝ≥0∞<VAR>xt : x ≠ ⊤<VAR>ε0 : ε ≠ 0<GOAL>Set.Icc (x - ε) (x + ε) ∈ 𝓝 x
<VAR>x : ℝ≥0∞<VAR>xt : x ≠ ⊤<GOAL>𝓝 x = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 (Set.Icc (x - ε) (x + ε))
<VAR>x : ℝ≥0∞<GOAL>⨅ ε, ⨅ (_ : ε > 0), 𝓟 (Set.Icc (x - ε) (x + ε)) ≤ 𝓝 x
<VAR>α : Type u_1<VAR>f : Filter α<VAR>u : α → ℝ≥0∞<VAR>a : ℝ≥0∞<VAR>h : ∀ ε > 0, ∀ᶠ (x : α) in f, u x ∈ Set.Icc (a - ε) (a + ε)<GOAL>Filter.Tendsto u f (𝓝 a)
<VAR>α : Type u_1<VAR>f : Filter α<VAR>u : α → ℝ≥0∞<VAR>a : ℝ≥0∞<VAR>ha : a ≠ ⊤<GOAL>Filter.Tendsto u f (𝓝 a) ↔ ∀ ε > 0, ∀ᶠ (x : α) in f, u x ∈ Set.Icc (a - ε) (a + ε)
<VAR>α : Type u_1<VAR>f : Filter α<VAR>u : α → ℝ≥0∞<GOAL>Filter.Tendsto u f (𝓝 0) ↔ ∀ ε > 0, ∀ᶠ (x : α) in f, u x ≤ ε
<VAR>β : Type u_2<VAR>Nonempty β<VAR>SemilatticeSup β<VAR>f : β → ℝ≥0∞<VAR>a : ℝ≥0∞<VAR>ha : a ≠ ⊤<GOAL>Filter.Tendsto f Filter.atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ∈ Set.Icc (a - ε) (a + ε)
<VAR>β : Type u_2<VAR>Nonempty β<VAR>SemilatticeSup β<VAR>f : β → ℝ≥0∞<GOAL>Filter.Tendsto f Filter.atTop (𝓝 0) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ≤ ε
<VAR>a b : ℝ≥0∞<GOAL>a ≠ ⊤ ∨ b ≠ ⊤ → Filter.Tendsto (fun p => p.1 - p.2) (𝓝 (a, b)) (𝓝 (a - b))
<VAR>α : Type u_1<VAR>f : Filter α<VAR>ma mb : α → ℝ≥0∞<VAR>a b : ℝ≥0∞<VAR>hma : Filter.Tendsto ma f (𝓝 a)<VAR>hmb : Filter.Tendsto mb f (𝓝 b)<VAR>h : a ≠ ⊤ ∨ b ≠ ⊤<GOAL>Filter.Tendsto (fun a => ma a - mb a) f (𝓝 (a - b))
<VAR>a b : ℝ≥0∞<VAR>ha : a ≠ 0 ∨ b ≠ ⊤<VAR>hb : b ≠ 0 ∨ a ≠ ⊤<GOAL>Filter.Tendsto (fun p => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))
<VAR>α : Type u_1<VAR>f : Filter α<VAR>ma mb : α → ℝ≥0∞<VAR>a b : ℝ≥0∞<VAR>hma : Filter.Tendsto ma f (𝓝 a)<VAR>ha : a ≠ 0 ∨ b ≠ ⊤<VAR>hmb : Filter.Tendsto mb f (𝓝 b)<VAR>hb : b ≠ 0 ∨ a ≠ ⊤<GOAL>Filter.Tendsto (fun a => ma a * mb a) f (𝓝 (a * b))
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f g : α → ℝ≥0∞<VAR>s : Set α<VAR>hf : ContinuousOn f s<VAR>hg : ContinuousOn g s<VAR>h₁ : ∀ x ∈ s, f x ≠ 0 ∨ g x ≠ ⊤<VAR>h₂ : ∀ x ∈ s, g x ≠ 0 ∨ f x ≠ ⊤<GOAL>ContinuousOn (fun x => f x * g x) s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f g : α → ℝ≥0∞<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>h₁ : ∀ (x : α), f x ≠ 0 ∨ g x ≠ ⊤<VAR>h₂ : ∀ (x : α), g x ≠ 0 ∨ f x ≠ ⊤<GOAL>Continuous fun x => f x * g x
<VAR>α : Type u_1<VAR>f : Filter α<VAR>m : α → ℝ≥0∞<VAR>a b : ℝ≥0∞<VAR>hm : Filter.Tendsto m f (𝓝 b)<VAR>hb : b ≠ 0 ∨ a ≠ ⊤<GOAL>Filter.Tendsto (fun b => a * m b) f (𝓝 (a * b))
<VAR>α : Type u_1<VAR>f : Filter α<VAR>m : α → ℝ≥0∞<VAR>a b : ℝ≥0∞<VAR>hm : Filter.Tendsto m f (𝓝 a)<VAR>ha : a ≠ 0 ∨ b ≠ ⊤<GOAL>Filter.Tendsto (fun x => m x * b) f (𝓝 (a * b))
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>f : ι → α → ℝ≥0∞<VAR>x : Filter α<VAR>a : ι → ℝ≥0∞<VAR>s : Finset ι<VAR>h : ∀ i ∈ s, Filter.Tendsto (f i) x (𝓝 (a i))<VAR>h' : ∀ i ∈ s, a i ≠ ⊤<GOAL>Filter.Tendsto (fun b => ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a c))
<VAR>a b : ℝ≥0∞<VAR>h : a ≠ ⊤ ∨ b ≠ 0<GOAL>ContinuousAt (fun x => a * x) b
<VAR>a b : ℝ≥0∞<VAR>h : a ≠ ⊤ ∨ b ≠ 0<GOAL>ContinuousAt (fun x => x * a) b
<VAR>a : ℝ≥0∞<VAR>ha : a ≠ ⊤<GOAL>Continuous fun x => a * x
<VAR>a : ℝ≥0∞<VAR>ha : a ≠ ⊤<GOAL>Continuous fun x => x * a
<VAR>c : ℝ≥0∞<VAR>c_ne_zero : c ≠ 0<GOAL>Continuous fun x => x / c
<VAR>n : ℕ<GOAL>Continuous fun a => a ^ n
<GOAL>ContinuousOn (fun p => p.1 - p.2) {p | p ≠ (⊤, ⊤)}
<VAR>a : ℝ≥0∞<VAR>a_ne_top : a ≠ ⊤<GOAL>Continuous fun x => a - x
<VAR>a : ℝ≥0<GOAL>Continuous fun x => ↑a - x
<VAR>a : ℝ≥0∞<GOAL>ContinuousOn (fun x => a - x) {x | x ≠ ⊤}
<VAR>a : ℝ≥0∞<GOAL>Continuous fun x => x - a
<VAR>α : Type u_1<VAR>f : Filter α<VAR>m : α → ℝ≥0∞<VAR>a : ℝ≥0∞<VAR>n : ℕ<VAR>hm : Filter.Tendsto m f (𝓝 a)<GOAL>Filter.Tendsto (fun x => m x ^ n) f (𝓝 (a ^ n))
<VAR>x y : ℝ≥0∞<VAR>h : ∀ a < 1, a * x ≤ y<GOAL>x ≤ y
<VAR>ι : Sort u_4<VAR>f : ι → ℝ≥0∞<VAR>a : ℝ≥0∞<VAR>h : a = ⊤ → ⨅ i, f i = 0 → ∃ i, f i = 0<VAR>h0 : a = 0 → Nonempty ι<GOAL>⨅ i, a * f i = a * ⨅ i, f i
<VAR>ι : Sort u_4<VAR>Nonempty ι<VAR>f : ι → ℝ≥0∞<VAR>a : ℝ≥0∞<VAR>h : a = ⊤ → ⨅ i, f i = 0 → ∃ i, f i = 0<GOAL>⨅ i, a * f i = a * ⨅ i, f i
<VAR>ι : Sort u_4<VAR>f : ι → ℝ≥0∞<VAR>a : ℝ≥0∞<VAR>h : a = ⊤ → ⨅ i, f i = 0 → ∃ i, f i = 0<VAR>h0 : a = 0 → Nonempty ι<GOAL>⨅ i, f i * a = (⨅ i, f i) * a
<VAR>ι : Sort u_4<VAR>Nonempty ι<VAR>f : ι → ℝ≥0∞<VAR>a : ℝ≥0∞<VAR>h : a = ⊤ → ⨅ i, f i = 0 → ∃ i, f i = 0<GOAL>⨅ i, f i * a = (⨅ i, f i) * a
<VAR>ι : Sort u_4<VAR>x : ι → ℝ≥0∞<GOAL>(iInf x)⁻¹ = ⨆ i, (x i)⁻¹
<VAR>ι : Sort u_4<VAR>x : ι → ℝ≥0∞<GOAL>(iSup x)⁻¹ = ⨅ i, (x i)⁻¹
<VAR>ι : Type u_4<VAR>x : ι → ℝ≥0∞<VAR>l : Filter ι<GOAL>(Filter.limsup x l)⁻¹ = Filter.liminf (fun i => (x i)⁻¹) l
<VAR>ι : Type u_4<VAR>x : ι → ℝ≥0∞<VAR>l : Filter ι<GOAL>(Filter.liminf x l)⁻¹ = Filter.limsup (fun i => (x i)⁻¹) l
<VAR>α : Type u_1<VAR>f : Filter α<VAR>m : α → ℝ≥0∞<VAR>a : ℝ≥0∞<GOAL>Filter.Tendsto (fun x => (m x)⁻¹) f (𝓝 a⁻¹) ↔ Filter.Tendsto m f (𝓝 a)
<VAR>α : Type u_1<VAR>f : Filter α<VAR>ma mb : α → ℝ≥0∞<VAR>a b : ℝ≥0∞<VAR>hma : Filter.Tendsto ma f (𝓝 a)<VAR>ha : a ≠ 0 ∨ b ≠ 0<VAR>hmb : Filter.Tendsto mb f (𝓝 b)<VAR>hb : b ≠ ⊤ ∨ a ≠ ⊤<GOAL>Filter.Tendsto (fun a => ma a / mb a) f (𝓝 (a / b))
<VAR>α : Type u_1<VAR>f : Filter α<VAR>m : α → ℝ≥0∞<VAR>a b : ℝ≥0∞<VAR>hm : Filter.Tendsto m f (𝓝 b)<VAR>hb : b ≠ ⊤ ∨ a ≠ ⊤<GOAL>Filter.Tendsto (fun b => a / m b) f (𝓝 (a / b))
<VAR>α : Type u_1<VAR>f : Filter α<VAR>m : α → ℝ≥0∞<VAR>a b : ℝ≥0∞<VAR>hm : Filter.Tendsto m f (𝓝 a)<VAR>ha : a ≠ 0 ∨ b ≠ 0<GOAL>Filter.Tendsto (fun x => m x / b) f (𝓝 (a / b))
<VAR>a : ℝ≥0∞<VAR>ι : Sort u_4<VAR>s : ι → ℝ≥0∞<VAR>Nonempty ι<GOAL>iSup s + a = ⨆ b, s b + a
<VAR>a : ℝ≥0∞<VAR>ι : Sort u_4<VAR>p : ι → Prop<VAR>h : ∃ i, p i<VAR>f : ι → ℝ≥0∞<GOAL>(⨆ i, ⨆ (_ : p i), f i) + a = ⨆ i, ⨆ (_ : p i), f i + a
<VAR>a : ℝ≥0∞<VAR>ι : Sort u_4<VAR>p : ι → Prop<VAR>h : ∃ i, p i<VAR>f : ι → ℝ≥0∞<GOAL>a + ⨆ i, ⨆ (_ : p i), f i = ⨆ i, ⨆ (_ : p i), a + f i
<VAR>a : ℝ≥0∞<VAR>ι : Type u_4<VAR>s : Set ι<VAR>hs : s.Nonempty<VAR>f : ι → ℝ≥0∞<GOAL>(⨆ i ∈ s, f i) + a = ⨆ i ∈ s, f i + a
<VAR>a : ℝ≥0∞<VAR>ι : Type u_4<VAR>s : Set ι<VAR>hs : s.Nonempty<VAR>f : ι → ℝ≥0∞<GOAL>a + ⨆ i ∈ s, f i = ⨆ i ∈ s, a + f i
<VAR>a : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>hs : s.Nonempty<GOAL>sSup s + a = ⨆ b ∈ s, b + a
<VAR>a : ℝ≥0∞<VAR>ι : Sort u_4<VAR>s : ι → ℝ≥0∞<VAR>Nonempty ι<GOAL>a + iSup s = ⨆ b, a + s b
<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>Nonempty ι<VAR>Nonempty ι'<VAR>f : ι → ℝ≥0∞<VAR>g : ι' → ℝ≥0∞<VAR>a : ℝ≥0∞<VAR>h : ∀ (i : ι) (j : ι'), f i + g j ≤ a<GOAL>iSup f + iSup g ≤ a
<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>p : ι → Prop<VAR>q : ι' → Prop<VAR>hp : ∃ i, p i<VAR>hq : ∃ j, q j<VAR>f : ι → ℝ≥0∞<VAR>g : ι' → ℝ≥0∞<VAR>a : ℝ≥0∞<VAR>h : ∀ (i : ι), p i → ∀ (j : ι'), q j → f i + g j ≤ a<GOAL>(⨆ i, ⨆ (_ : p i), f i) + ⨆ j, ⨆ (_ : q j), g j ≤ a
<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>s : Set ι<VAR>t : Set ι'<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<VAR>f : ι → ℝ≥0∞<VAR>g : ι' → ℝ≥0∞<VAR>a : ℝ≥0∞<VAR>h : ∀ i ∈ s, ∀ j ∈ t, f i + g j ≤ a<GOAL>(⨆ i ∈ s, f i) + ⨆ j ∈ t, g j ≤ a