ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>F : Type u_4<VAR>NormedField 𝕜<VAR>(i : ι) → TopologicalSpace (E i)<VAR>(i : ι) → AddCommGroup (E i)<VAR>(i : ι) → Module 𝕜 (E i)<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>∀ (i : ι), ContinuousSMul 𝕜 (E i)<VAR>α : Type u_5<VAR>p : α → ContinuousMultilinearMap 𝕜 E F<VAR>q : ContinuousMultilinearMap 𝕜 E F<VAR>h : HasSum p q<VAR>m : (i : ι) → E i<GOAL>HasSum (fun a => (p a) m) (q m)
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>F : Type u_4<VAR>NormedField 𝕜<VAR>(i : ι) → TopologicalSpace (E i)<VAR>(i : ι) → AddCommGroup (E i)<VAR>(i : ι) → Module 𝕜 (E i)<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>∀ (i : ι), ContinuousSMul 𝕜 (E i)<VAR>T2Space F<VAR>α : Type u_5<VAR>p : α → ContinuousMultilinearMap 𝕜 E F<VAR>hp : Summable p<VAR>m : (i : ι) → E i<GOAL>(∑' (a : α), p a) m = ∑' (a : α), (p a) m
<VAR>K : Type u_1<VAR>Field K<VAR>UniformSpace K<VAR>self : CompletableTopField K<VAR>F : Filter K<GOAL>Cauchy F → 𝓝 0 ⊓ F = ⊥ → Cauchy (Filter.map (fun x => x⁻¹) F)
<VAR>K : Type u_1<VAR>Field K<VAR>UniformSpace K<VAR>CompletableTopField K<VAR>x : hat K<VAR>h : x ≠ 0<GOAL>ContinuousAt UniformSpace.Completion.hatInv x
<VAR>K : Type u_1<VAR>Field K<VAR>UniformSpace K<VAR>TopologicalDivisionRing K<VAR>x : K<VAR>h : x ≠ 0<GOAL>(↑K x).hatInv = ↑K x⁻¹
<VAR>K : Type u_1<VAR>Field K<VAR>UniformSpace K<VAR>TopologicalDivisionRing K<VAR>CompletableTopField K<VAR>x : K<GOAL>(↑K x)⁻¹ = ↑K x⁻¹
<VAR>K : Type u_1<VAR>Field K<VAR>UniformSpace K<VAR>TopologicalDivisionRing K<VAR>CompletableTopField K<VAR>UniformAddGroup K<VAR>x : hat K<VAR>x_ne : x ≠ 0<GOAL>x * x.hatInv = 1
<VAR>α : Type u_1<VAR>Ring α<VAR>UniformSpace α<GOAL>↑α 1 = 1
<VAR>α : Type u_1<VAR>Ring α<VAR>UniformSpace α<VAR>TopologicalRing α<VAR>a b : α<GOAL>↑α (a * b) = ↑α a * ↑α b
<VAR>α : Type u_1<VAR>Ring α<VAR>UniformSpace α<VAR>TopologicalRing α<VAR>UniformAddGroup α<GOAL>Continuous fun p => p.1 * p.2
<VAR>α : Type u_1<VAR>Ring α<VAR>UniformSpace α<VAR>TopologicalRing α<VAR>UniformAddGroup α<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>f g : β → UniformSpace.Completion α<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous fun b => f b * g b
<VAR>α : Type u_1<VAR>Ring α<VAR>UniformSpace α<VAR>TopologicalRing α<VAR>UniformAddGroup α<GOAL>Continuous ⇑UniformSpace.Completion.coeRingHom
<VAR>A : Type u_2<VAR>Ring A<VAR>UniformSpace A<VAR>UniformAddGroup A<VAR>TopologicalRing A<VAR>R : Type u_3<VAR>CommSemiring R<VAR>Algebra R A<VAR>UniformContinuousConstSMul R A<VAR>r : R<GOAL>(UniformSpace.Completion.map fun x => r • x) = fun x => ↑A ((algebraMap R A) r) * x
<VAR>A : Type u_2<VAR>Ring A<VAR>UniformSpace A<VAR>UniformAddGroup A<VAR>TopologicalRing A<VAR>R : Type u_3<VAR>CommSemiring R<VAR>Algebra R A<VAR>UniformContinuousConstSMul R A<VAR>r : R<GOAL>(algebraMap R (UniformSpace.Completion A)) r = ↑A ((algebraMap R A) r)
<VAR>α : Type u_2<VAR>CommRing α<VAR>TopologicalSpace α<VAR>TopologicalRing α<GOAL>inseparableSetoid α = Submodule.quotientRel ⊥.closure
<VAR>α : Type u<VAR>r : CommRing α<VAR>TopologicalSpace α<VAR>TopologicalRing α<GOAL>SeparationQuotient α = (α ⧸ ⊥.closure)
<VAR>A : Type u_1<VAR>ι : Type u_2<VAR>Ring A<VAR>B : ι → AddSubgroup A<VAR>self : RingSubgroupsBasis B<VAR>x : A<VAR>i : ι<GOAL>∃ j, ↑(B j) ⊆ (fun x_1 => x * x_1) ⁻¹' ↑(B i)
<VAR>A : Type u_1<VAR>ι : Type u_2<VAR>Ring A<VAR>B : ι → AddSubgroup A<VAR>self : RingSubgroupsBasis B<VAR>i j : ι<GOAL>∃ k, B k ≤ B i ⊓ B j
<VAR>A : Type u_1<VAR>ι : Type u_2<VAR>Ring A<VAR>B : ι → AddSubgroup A<VAR>self : RingSubgroupsBasis B<VAR>i : ι<GOAL>∃ j, ↑(B j) * ↑(B j) ⊆ ↑(B i)
<VAR>A : Type u_1<VAR>ι : Type u_2<VAR>Ring A<VAR>B : ι → AddSubgroup A<VAR>self : RingSubgroupsBasis B<VAR>x : A<VAR>i : ι<GOAL>∃ j, ↑(B j) ⊆ (fun x_1 => x_1 * x) ⁻¹' ↑(B i)
<VAR>A : Type u_3<VAR>ι : Type u_4<VAR>CommRing A<VAR>B : ι → AddSubgroup A<VAR>inter : ∀ (i j : ι), ∃ k, B k ≤ B i ⊓ B j<VAR>mul : ∀ (i : ι), ∃ j, ↑(B j) * ↑(B j) ⊆ ↑(B i)<VAR>leftMul : ∀ (x : A) (i : ι), ∃ j, ↑(B j) ⊆ (fun y => x * y) ⁻¹' ↑(B i)<GOAL>RingSubgroupsBasis B
<VAR>A : Type u_1<VAR>ι : Type u_2<VAR>Ring A<VAR>Nonempty ι<VAR>B : ι → AddSubgroup A<VAR>hB : RingSubgroupsBasis B<VAR>V : Set A<GOAL>V ∈ RingFilterBasis.toAddGroupFilterBasis ↔ ∃ i, V = ↑(B i)
<VAR>A : Type u_1<VAR>ι : Type u_2<VAR>Ring A<VAR>Nonempty ι<VAR>B : ι → AddSubgroup A<VAR>hB : RingSubgroupsBasis B<VAR>i : ι<GOAL>↑(B i) ∈ RingFilterBasis.toAddGroupFilterBasis
<VAR>A : Type u_1<VAR>ι : Type u_2<VAR>Ring A<VAR>Nonempty ι<VAR>B : ι → AddSubgroup A<VAR>hB : RingSubgroupsBasis B<GOAL>(𝓝 0).HasBasis (fun x => True) fun i => ↑(B i)
<VAR>A : Type u_1<VAR>ι : Type u_2<VAR>Ring A<VAR>Nonempty ι<VAR>B : ι → AddSubgroup A<VAR>hB : RingSubgroupsBasis B<VAR>a : A<GOAL>(𝓝 a).HasBasis (fun x => True) fun i => {b | b - a ∈ B i}
<VAR>A : Type u_1<VAR>ι : Type u_2<VAR>Ring A<VAR>Nonempty ι<VAR>B : ι → AddSubgroup A<VAR>hB : RingSubgroupsBasis B<GOAL>NonarchimedeanRing A
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>B : ι → Submodule R A<VAR>self : SubmodulesRingBasis B<VAR>a : A<VAR>i : ι<GOAL>∃ j, a • B j ≤ B i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>B : ι → Submodule R A<VAR>self : SubmodulesRingBasis B<VAR>i j : ι<GOAL>∃ k, B k ≤ B i ⊓ B j
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>B : ι → Submodule R A<VAR>self : SubmodulesRingBasis B<VAR>i : ι<GOAL>∃ j, ↑(B j) * ↑(B j) ⊆ ↑(B i)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>B : ι → Submodule R A<VAR>hB : SubmodulesRingBasis B<GOAL>RingSubgroupsBasis fun i => (B i).toAddSubgroup
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CommRing R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>TopologicalSpace R<VAR>B : ι → Submodule R M<VAR>self : SubmodulesBasis B<VAR>i j : ι<GOAL>∃ k, B k ≤ B i ⊓ B j
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CommRing R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>TopologicalSpace R<VAR>B : ι → Submodule R M<VAR>self : SubmodulesBasis B<VAR>m : M<VAR>i : ι<GOAL>∀ᶠ (a : R) in 𝓝 0, a • m ∈ B i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CommRing R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>TopologicalSpace R<VAR>Nonempty ι<VAR>B : ι → Submodule R M<VAR>hB : SubmodulesBasis B<GOAL>NonarchimedeanAddGroup M
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>TopologicalSpace R<VAR>B : ι → Submodule R A<VAR>hB : SubmodulesRingBasis B<VAR>hsmul : ∀ (m : A) (i : ι), ∀ᶠ (a : R) in 𝓝 0, a • m ∈ B i<GOAL>SubmodulesBasis B
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CommRing R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>BR : RingFilterBasis R<VAR>B : ι → Submodule R M<VAR>self : BR.SubmodulesBasis B<VAR>m : M<VAR>i : ι<GOAL>∃ U ∈ BR, U ⊆ (fun x => x • m) ⁻¹' ↑(B i)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CommRing R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>BR : RingFilterBasis R<VAR>B : ι → Submodule R M<VAR>self : BR.SubmodulesBasis B<VAR>i j : ι<GOAL>∃ k, B k ≤ B i ⊓ B j
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CommRing R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>BR : RingFilterBasis R<VAR>B : ι → Submodule R M<VAR>hB : BR.SubmodulesBasis B<GOAL>SubmodulesBasis B
<VAR>ι : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>hom : Type u_4<VAR>TopologicalSpace G<VAR>UniformSpace M<VAR>AddGroup G<VAR>AddGroup M<VAR>TopologicalAddGroup G<VAR>UniformAddGroup M<VAR>FunLike hom G M<VAR>AddMonoidHomClass hom G M<VAR>F : ι → hom<VAR>hf : EquicontinuousAt (DFunLike.coe ∘ F) 0<GOAL>Equicontinuous (DFunLike.coe ∘ F)
<VAR>ι : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>hom : Type u_4<VAR>TopologicalSpace G<VAR>UniformSpace M<VAR>Group G<VAR>Group M<VAR>TopologicalGroup G<VAR>UniformGroup M<VAR>FunLike hom G M<VAR>MonoidHomClass hom G M<VAR>F : ι → hom<VAR>hf : EquicontinuousAt (DFunLike.coe ∘ F) 1<GOAL>Equicontinuous (DFunLike.coe ∘ F)
<VAR>ι : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>hom : Type u_4<VAR>UniformSpace G<VAR>UniformSpace M<VAR>AddGroup G<VAR>AddGroup M<VAR>UniformAddGroup G<VAR>UniformAddGroup M<VAR>FunLike hom G M<VAR>AddMonoidHomClass hom G M<VAR>F : ι → hom<VAR>hf : EquicontinuousAt (DFunLike.coe ∘ F) 0<GOAL>UniformEquicontinuous (DFunLike.coe ∘ F)
<VAR>ι : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>hom : Type u_4<VAR>UniformSpace G<VAR>UniformSpace M<VAR>Group G<VAR>Group M<VAR>UniformGroup G<VAR>UniformGroup M<VAR>FunLike hom G M<VAR>MonoidHomClass hom G M<VAR>F : ι → hom<VAR>hf : EquicontinuousAt (DFunLike.coe ∘ F) 1<GOAL>UniformEquicontinuous (DFunLike.coe ∘ F)
<VAR>G : Type u_1<VAR>AddCommGroup G<VAR>B : AddGroupFilterBasis G<GOAL>UniformAddGroup G
<VAR>G : Type u_1<VAR>AddCommGroup G<VAR>B : AddGroupFilterBasis G<VAR>F : Filter G<GOAL>Cauchy F ↔ F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>K : TopologicalSpace.PositiveCompacts G<GOAL>LocallyCompactSpace G
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>K : TopologicalSpace.PositiveCompacts G<GOAL>LocallyCompactSpace G
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Semiring R<VAR>TopologicalSpace R<VAR>TopologicalSemiring R<VAR>Semiring S<VAR>p : Polynomial S<VAR>f : S →+* R<GOAL>Continuous fun x => Polynomial.eval₂ f x p
<VAR>R : Type u_1<VAR>Semiring R<VAR>TopologicalSpace R<VAR>TopologicalSemiring R<VAR>p : Polynomial R<GOAL>Continuous fun x => Polynomial.eval x p
<VAR>R : Type u_1<VAR>Semiring R<VAR>TopologicalSpace R<VAR>TopologicalSemiring R<VAR>p : Polynomial R<VAR>a : R<GOAL>ContinuousAt (fun x => Polynomial.eval x p) a
<VAR>R : Type u_1<VAR>Semiring R<VAR>TopologicalSpace R<VAR>TopologicalSemiring R<VAR>p : Polynomial R<VAR>s : Set R<VAR>a : R<GOAL>ContinuousWithinAt (fun x => Polynomial.eval x p) s a
<VAR>R : Type u_1<VAR>Semiring R<VAR>TopologicalSpace R<VAR>TopologicalSemiring R<VAR>p : Polynomial R<VAR>s : Set R<GOAL>ContinuousOn (fun x => Polynomial.eval x p) s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>TopologicalSpace A<VAR>TopologicalSemiring A<VAR>p : Polynomial R<GOAL>Continuous fun x => (Polynomial.aeval x) p
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>TopologicalSpace A<VAR>TopologicalSemiring A<VAR>p : Polynomial R<VAR>a : A<GOAL>ContinuousAt (fun x => (Polynomial.aeval x) p) a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>TopologicalSpace A<VAR>TopologicalSemiring A<VAR>p : Polynomial R<VAR>s : Set A<VAR>a : A<GOAL>ContinuousWithinAt (fun x => (Polynomial.aeval x) p) s a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>TopologicalSpace A<VAR>TopologicalSemiring A<VAR>p : Polynomial R<VAR>s : Set A<GOAL>ContinuousOn (fun x => (Polynomial.aeval x) p) s
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>k : Type u_3<VAR>α : Type u_4<VAR>Semiring R<VAR>Ring S<VAR>LinearOrderedField k<VAR>f : R →+* S<VAR>abv : S → k<VAR>IsAbsoluteValue abv<VAR>p : Polynomial R<VAR>hd : 0 < p.degree<VAR>hf : f p.leadingCoeff ≠ 0<VAR>l : Filter α<VAR>z : α → S<VAR>hz : Filter.Tendsto (abv ∘ z) l Filter.atTop<GOAL>Filter.Tendsto (fun x => abv (Polynomial.eval₂ f (z x) p)) l Filter.atTop
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>α : Type u_3<VAR>Ring R<VAR>LinearOrderedField k<VAR>abv : R → k<VAR>IsAbsoluteValue abv<VAR>p : Polynomial R<VAR>h : 0 < p.degree<VAR>l : Filter α<VAR>z : α → R<VAR>hz : Filter.Tendsto (abv ∘ z) l Filter.atTop<GOAL>Filter.Tendsto (fun x => abv (Polynomial.eval (z x) p)) l Filter.atTop
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>k : Type u_3<VAR>α : Type u_4<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>LinearOrderedField k<VAR>abv : A → k<VAR>IsAbsoluteValue abv<VAR>p : Polynomial R<VAR>hd : 0 < p.degree<VAR>h₀ : (algebraMap R A) p.leadingCoeff ≠ 0<VAR>l : Filter α<VAR>z : α → A<VAR>hz : Filter.Tendsto (abv ∘ z) l Filter.atTop<GOAL>Filter.Tendsto (fun x => abv ((Polynomial.aeval (z x)) p)) l Filter.atTop
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>NormedRing R<VAR>IsAbsoluteValue norm<VAR>p : Polynomial R<VAR>h : 0 < p.degree<VAR>l : Filter α<VAR>z : α → R<VAR>hz : Filter.Tendsto (fun x => ‖z x‖) l Filter.atTop<GOAL>Filter.Tendsto (fun x => ‖Polynomial.eval (z x) p‖) l Filter.atTop
<VAR>R : Type u_2<VAR>NormedRing R<VAR>IsAbsoluteValue norm<VAR>ProperSpace R<VAR>p : Polynomial R<GOAL>∃ x, ∀ (y : R), ‖Polynomial.eval x p‖ ≤ ‖Polynomial.eval y p‖
<VAR>F : Type u_3<VAR>K : Type u_4<VAR>CommRing F<VAR>NormedField K<VAR>p : Polynomial F<VAR>f : F →+* K<VAR>B : ℝ<VAR>hB : B < 0<VAR>h1 : p.Monic<VAR>h2 : Polynomial.Splits f p<VAR>h3 : ∀ z ∈ (Polynomial.map f p).roots, ‖z‖ ≤ B<GOAL>p = 1
<VAR>F : Type u_3<VAR>K : Type u_4<VAR>CommRing F<VAR>NormedField K<VAR>p : Polynomial F<VAR>f : F →+* K<VAR>B : ℝ<VAR>i : ℕ<VAR>h1 : p.Monic<VAR>h2 : Polynomial.Splits f p<VAR>h3 : ∀ z ∈ (Polynomial.map f p).roots, ‖z‖ ≤ B<GOAL>‖(Polynomial.map f p).coeff i‖ ≤ B ^ (p.natDegree - i) * ↑(p.natDegree.choose i)
<VAR>F : Type u_3<VAR>K : Type u_4<VAR>CommRing F<VAR>NormedField K<VAR>B : ℝ<VAR>d : ℕ<VAR>f : F →+* K<VAR>p : Polynomial F<VAR>h1 : p.Monic<VAR>h2 : Polynomial.Splits f p<VAR>h3 : p.natDegree ≤ d<VAR>h4 : ∀ z ∈ (Polynomial.map f p).roots, ‖z‖ ≤ B<VAR>i : ℕ<GOAL>‖(Polynomial.map f p).coeff i‖ ≤ max B 1 ^ d * ↑(d.choose (d / 2))
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<VAR>self : ContinuousMultilinearMap R M₁ M₂<GOAL>Continuous self.toFun
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<GOAL>Function.Injective ContinuousMultilinearMap.toMultilinearMap
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<VAR>f : ContinuousMultilinearMap R M₁ M₂<GOAL>Continuous ⇑f
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<VAR>f : ContinuousMultilinearMap R M₁ M₂<GOAL>⇑f.toMultilinearMap = ⇑f
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<VAR>f f' : ContinuousMultilinearMap R M₁ M₂<VAR>H : ∀ (x : (i : ι) → M₁ i), f x = f' x<GOAL>f = f'
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<VAR>f f' : ContinuousMultilinearMap R M₁ M₂<GOAL>f = f' ↔ ∀ (x : (i : ι) → M₁ i), f x = f' x
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<VAR>f : ContinuousMultilinearMap R M₁ M₂<VAR>DecidableEq ι<VAR>m : (i : ι) → M₁ i<VAR>i : ι<VAR>x y : M₁ i<GOAL>f (Function.update m i (x + y)) = f (Function.update m i x) + f (Function.update m i y)
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<VAR>f : ContinuousMultilinearMap R M₁ M₂<VAR>DecidableEq ι<VAR>m : (i : ι) → M₁ i<VAR>i : ι<VAR>c : R<VAR>x : M₁ i<GOAL>f (Function.update m i (c • x)) = c • f (Function.update m i x)
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<VAR>f : ContinuousMultilinearMap R M₁ M₂<VAR>m : (i : ι) → M₁ i<VAR>i : ι<VAR>h : m i = 0<GOAL>f m = 0
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<VAR>f : ContinuousMultilinearMap R M₁ M₂<VAR>Nonempty ι<GOAL>f 0 = 0
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<VAR>m : (i : ι) → M₁ i<GOAL>0 m = 0
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<GOAL>ContinuousMultilinearMap.toMultilinearMap 0 = 0
<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<VAR>R' : Type u_1<VAR>A : Type u_3<VAR>Monoid R'<VAR>Semiring A<VAR>(i : ι) → Module A (M₁ i)<VAR>Module A M₂<VAR>DistribMulAction R' M₂<VAR>ContinuousConstSMul R' M₂<VAR>SMulCommClass A R' M₂<VAR>f : ContinuousMultilinearMap A M₁ M₂<VAR>c : R'<VAR>m : (i : ι) → M₁ i<GOAL>(c • f) m = c • f m
<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<VAR>R' : Type u_1<VAR>A : Type u_3<VAR>Monoid R'<VAR>Semiring A<VAR>(i : ι) → Module A (M₁ i)<VAR>Module A M₂<VAR>DistribMulAction R' M₂<VAR>ContinuousConstSMul R' M₂<VAR>SMulCommClass A R' M₂<VAR>c : R'<VAR>f : ContinuousMultilinearMap A M₁ M₂<GOAL>(c • f).toMultilinearMap = c • f.toMultilinearMap
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<VAR>f f' : ContinuousMultilinearMap R M₁ M₂<VAR>ContinuousAdd M₂<VAR>m : (i : ι) → M₁ i<GOAL>(f + f') m = f m + f' m
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<VAR>ContinuousAdd M₂<VAR>f g : ContinuousMultilinearMap R M₁ M₂<GOAL>(f + g).toMultilinearMap = f.toMultilinearMap + g.toMultilinearMap
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<VAR>ContinuousAdd M₂<VAR>α : Type u_1<VAR>f : α → ContinuousMultilinearMap R M₁ M₂<VAR>m : (i : ι) → M₁ i<VAR>s : Finset α<GOAL>(∑ a ∈ s, f a) m = ∑ a ∈ s, (f a) m
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>M₃ : Type w₃<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>Module R M₃<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<VAR>TopologicalSpace M₃<VAR>f : ContinuousMultilinearMap R M₁ M₂<VAR>g : ContinuousMultilinearMap R M₁ M₃<VAR>m : (i : ι) → M₁ i<GOAL>(f.prod g) m = (f m, g m)
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>(i : ι) → Module R (M₁ i)<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>ι' : Type u_1<VAR>M' : ι' → Type u_2<VAR>(i : ι') → AddCommMonoid (M' i)<VAR>(i : ι') → TopologicalSpace (M' i)<VAR>(i : ι') → Module R (M' i)<VAR>f : (i : ι') → ContinuousMultilinearMap R M₁ (M' i)<GOAL>⇑(ContinuousMultilinearMap.pi f) = fun m j => (f j) m
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>(i : ι) → Module R (M₁ i)<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>ι' : Type u_1<VAR>M' : ι' → Type u_2<VAR>(i : ι') → AddCommMonoid (M' i)<VAR>(i : ι') → TopologicalSpace (M' i)<VAR>(i : ι') → Module R (M' i)<VAR>f : (i : ι') → ContinuousMultilinearMap R M₁ (M' i)<VAR>m : (i : ι) → M₁ i<VAR>j : ι'<GOAL>(ContinuousMultilinearMap.pi f) m j = (f j) m
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<VAR>f : ContinuousMultilinearMap R M₁ M₂<VAR>p : Submodule R M₂<VAR>h : ∀ (v : (i : ι) → M₁ i), f v ∈ p<GOAL>(f.codRestrict p h).toMultilinearMap = f.codRestrict p h
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<VAR>f : ContinuousMultilinearMap R M₁ M₂<VAR>p : Submodule R M₂<VAR>h : ∀ (v : (i : ι) → M₁ i), f v ∈ p<VAR>v : (i : ι) → M₁ i<GOAL>↑((f.codRestrict p h) v) = f v
<VAR>R : Type u<VAR>ι : Type v<VAR>M₂ : Type w₂<VAR>M₃ : Type w₃<VAR>Semiring R<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M₂<VAR>Module R M₃<VAR>TopologicalSpace M₂<VAR>TopologicalSpace M₃<VAR>Subsingleton ι<VAR>i : ι<VAR>f : ContinuousMultilinearMap R (fun x => M₂) M₃<VAR>x : M₂<GOAL>((ContinuousMultilinearMap.ofSubsingleton R M₂ M₃ i).symm f) x = f fun x_1 => x
<VAR>R : Type u<VAR>ι : Type v<VAR>M₂ : Type w₂<VAR>M₃ : Type w₃<VAR>Semiring R<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M₂<VAR>Module R M₃<VAR>TopologicalSpace M₂<VAR>TopologicalSpace M₃<VAR>Subsingleton ι<VAR>i : ι<VAR>f : M₂ →L[R] M₃<VAR>x : ι → M₂<GOAL>((ContinuousMultilinearMap.ofSubsingleton R M₂ M₃ i) f) x = f (x i)
<VAR>R : Type u<VAR>ι : Type v<VAR>M₂ : Type w₂<VAR>M₃ : Type w₃<VAR>Semiring R<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M₂<VAR>Module R M₃<VAR>TopologicalSpace M₂<VAR>TopologicalSpace M₃<VAR>Subsingleton ι<VAR>i : ι<VAR>f : M₂ →L[R] M₃<GOAL>((ContinuousMultilinearMap.ofSubsingleton R M₂ M₃ i) f).toMultilinearMap = (MultilinearMap.ofSubsingleton R M₂ M₃ i) ↑f
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<VAR>IsEmpty ι<VAR>m : M₂<GOAL>∀ (a : (i : ι) → M₁ i), (ContinuousMultilinearMap.constOfIsEmpty R M₁ m) a = m
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₂ : Type w₂<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>AddCommMonoid M₂<VAR>(i : ι) → Module R (M₁ i)<VAR>Module R M₂<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>TopologicalSpace M₂<VAR>IsEmpty ι<VAR>m : M₂<GOAL>(ContinuousMultilinearMap.constOfIsEmpty R M₁ m).toMultilinearMap = MultilinearMap.constOfIsEmpty R M₁ m
<VAR>R : Type u<VAR>ι : Type v<VAR>M₁ : ι → Type w₁<VAR>M₁' : ι → Type w₁'<VAR>M₄ : Type w₄<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M₁ i)<VAR>(i : ι) → AddCommMonoid (M₁' i)<VAR>AddCommMonoid M₄<VAR>(i : ι) → Module R (M₁ i)<VAR>(i : ι) → Module R (M₁' i)<VAR>Module R M₄<VAR>(i : ι) → TopologicalSpace (M₁ i)<VAR>(i : ι) → TopologicalSpace (M₁' i)<VAR>TopologicalSpace M₄<VAR>g : ContinuousMultilinearMap R M₁' M₄<VAR>f : (i : ι) → M₁ i →L[R] M₁' i<VAR>m : (i : ι) → M₁ i<GOAL>(g.compContinuousLinearMap f) m = g fun i => (f i) (m i)