ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Ring R<VAR>AddCommGroup V<VAR>Module R V<VAR>TopologicalSpace V<VAR>AddCommGroup W<VAR>Module R W<VAR>TopologicalSpace W<VAR>f : V →L[R] W<GOAL>⇑f.toContinuousAffineMap = ⇑f
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Ring R<VAR>AddCommGroup V<VAR>Module R V<VAR>TopologicalSpace V<VAR>AddCommGroup W<VAR>Module R W<VAR>TopologicalSpace W<VAR>f : V →L[R] W<GOAL>f.toContinuousAffineMap 0 = 0
<VAR>α : Type u_3<VAR>UniformSpace α<VAR>Zero α<GOAL>↑α 0 = 0
<VAR>α : Type u_3<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>a : α<GOAL>↑α (-a) = -↑α a
<VAR>α : Type u_3<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>a b : α<GOAL>↑α (a - b) = ↑α a - ↑α b
<VAR>α : Type u_3<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>a b : α<GOAL>↑α (a + b) = ↑α a + ↑α b
<VAR>α : Type u_3<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<GOAL>∀ (a : α), UniformSpace.Completion.toCompl a = ↑α a
<VAR>α : Type u_3<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<GOAL>Continuous ⇑UniformSpace.Completion.toCompl
<VAR>α : Type u_3<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<GOAL>DenseInducing ⇑UniformSpace.Completion.toCompl
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>UniformSpace β<VAR>AddGroup β<VAR>UniformAddGroup β<VAR>CompleteSpace β<VAR>T0Space β<VAR>f : α →+ β<VAR>hf : Continuous ⇑f<VAR>a : α<GOAL>(f.extension hf) (↑α a) = f a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>UniformSpace β<VAR>AddGroup β<VAR>UniformAddGroup β<VAR>CompleteSpace β<VAR>T0Space β<VAR>f : α →+ β<VAR>hf : Continuous ⇑f<GOAL>Continuous ⇑(f.extension hf)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>UniformSpace β<VAR>AddGroup β<VAR>UniformAddGroup β<VAR>f : α →+ β<VAR>hf : Continuous ⇑f<GOAL>Continuous ⇑(f.completion hf)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>UniformSpace β<VAR>AddGroup β<VAR>UniformAddGroup β<VAR>f : α →+ β<VAR>hf : Continuous ⇑f<VAR>a : α<GOAL>(f.completion hf) (↑α a) = ↑β (f a)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>UniformSpace β<VAR>AddGroup β<VAR>UniformAddGroup β<GOAL>AddMonoidHom.completion 0 ⋯ = 0
<VAR>α : Type u_3<VAR>UniformSpace α<VAR>AddGroup α<VAR>UniformAddGroup α<VAR>γ : Type u_5<VAR>AddCommGroup γ<VAR>UniformSpace γ<VAR>UniformAddGroup γ<VAR>f g : α →+ γ<VAR>hf : Continuous ⇑f<VAR>hg : Continuous ⇑g<GOAL>(f + g).completion ⋯ = f.completion hf + g.completion hg
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>BaireSpace X<VAR>f : ℕ → Set X<VAR>ho : ∀ (n : ℕ), IsOpen (f n)<VAR>hd : ∀ (n : ℕ), Dense (f n)<GOAL>Dense (⋂ n, f n)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>BaireSpace X<VAR>S : Set (Set X)<VAR>ho : ∀ s ∈ S, IsOpen s<VAR>hS : S.Countable<VAR>hd : ∀ s ∈ S, Dense s<GOAL>Dense (⋂₀ S)
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>TopologicalSpace X<VAR>BaireSpace X<VAR>S : Set α<VAR>f : α → Set X<VAR>ho : ∀ s ∈ S, IsOpen (f s)<VAR>hS : S.Countable<VAR>hd : ∀ s ∈ S, Dense (f s)<GOAL>Dense (⋂ s ∈ S, f s)
<VAR>X : Type u_1<VAR>ι : Sort u_3<VAR>TopologicalSpace X<VAR>BaireSpace X<VAR>Countable ι<VAR>f : ι → Set X<VAR>ho : ∀ (i : ι), IsOpen (f i)<VAR>hd : ∀ (i : ι), Dense (f i)<GOAL>Dense (⋂ s, f s)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>BaireSpace X<VAR>s : Set X<GOAL>s ∈ residual X ↔ ∃ t ⊆ s, IsGδ t ∧ Dense t
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>BaireSpace X<VAR>p : X → Prop<GOAL>(∀ᶠ (x : X) in residual X, p x) ↔ ∃ t, IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>BaireSpace X<VAR>s : Set X<VAR>hs : s ∈ residual X<GOAL>Dense s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>BaireSpace X<VAR>S : Set (Set X)<VAR>ho : ∀ s ∈ S, IsGδ s<VAR>hS : S.Countable<VAR>hd : ∀ s ∈ S, Dense s<GOAL>Dense (⋂₀ S)
<VAR>X : Type u_1<VAR>ι : Sort u_3<VAR>TopologicalSpace X<VAR>BaireSpace X<VAR>Countable ι<VAR>f : ι → Set X<VAR>ho : ∀ (s : ι), IsGδ (f s)<VAR>hd : ∀ (s : ι), Dense (f s)<GOAL>Dense (⋂ s, f s)
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>TopologicalSpace X<VAR>BaireSpace X<VAR>S : Set α<VAR>f : (x : α) → x ∈ S → Set X<VAR>ho : ∀ (s : α) (H : s ∈ S), IsGδ (f s H)<VAR>hS : S.Countable<VAR>hd : ∀ (s : α) (H : s ∈ S), Dense (f s H)<GOAL>Dense (⋂ s, ⋂ (h : s ∈ S), f s h)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>BaireSpace X<VAR>s t : Set X<VAR>hs : IsGδ s<VAR>ht : IsGδ t<VAR>hsc : Dense s<VAR>htc : Dense t<GOAL>Dense (s ∩ t)
<VAR>X : Type u_1<VAR>ι : Sort u_3<VAR>TopologicalSpace X<VAR>BaireSpace X<VAR>Countable ι<VAR>s : Set X<VAR>hs : IsGδ s<VAR>hd : Dense s<VAR>f : ι → Set X<VAR>hc : ∀ (i : ι), IsClosed (f i)<VAR>hU : s ⊆ ⋃ i, f i<GOAL>Dense (⋃ i, interior (f i))
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>TopologicalSpace X<VAR>BaireSpace X<VAR>t : Set α<VAR>s : Set X<VAR>hs : IsGδ s<VAR>hd : Dense s<VAR>ht : t.Countable<VAR>f : α → Set X<VAR>hc : ∀ i ∈ t, IsClosed (f i)<VAR>hU : s ⊆ ⋃ i ∈ t, f i<GOAL>Dense (⋃ i ∈ t, interior (f i))
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>BaireSpace X<VAR>T : Set (Set X)<VAR>s : Set X<VAR>hs : IsGδ s<VAR>hd : Dense s<VAR>hc : T.Countable<VAR>hc' : ∀ t ∈ T, IsClosed t<VAR>hU : s ⊆ ⋃₀ T<GOAL>Dense (⋃ t ∈ T, interior t)
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>TopologicalSpace X<VAR>BaireSpace X<VAR>S : Set α<VAR>f : α → Set X<VAR>hc : ∀ s ∈ S, IsClosed (f s)<VAR>hS : S.Countable<VAR>hU : ⋃ s ∈ S, f s = Set.univ<GOAL>Dense (⋃ s ∈ S, interior (f s))
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>BaireSpace X<VAR>S : Set (Set X)<VAR>hc : ∀ s ∈ S, IsClosed s<VAR>hS : S.Countable<VAR>hU : ⋃₀ S = Set.univ<GOAL>Dense (⋃ s ∈ S, interior s)
<VAR>X : Type u_1<VAR>ι : Sort u_3<VAR>TopologicalSpace X<VAR>BaireSpace X<VAR>Countable ι<VAR>f : ι → Set X<VAR>hc : ∀ (i : ι), IsClosed (f i)<VAR>hU : ⋃ i, f i = Set.univ<GOAL>Dense (⋃ i, interior (f i))
<VAR>X : Type u_1<VAR>ι : Sort u_3<VAR>TopologicalSpace X<VAR>BaireSpace X<VAR>Nonempty X<VAR>Countable ι<VAR>f : ι → Set X<VAR>hc : ∀ (i : ι), IsClosed (f i)<VAR>hU : ⋃ i, f i = Set.univ<GOAL>∃ i, (interior (f i)).Nonempty
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>self : LocallyConnectedSpace α<VAR>x : α<GOAL>(𝓝 x).HasBasis (fun s => IsOpen s ∧ x ∈ s ∧ IsConnected s) id
<VAR>α : Type u<VAR>TopologicalSpace α<GOAL>LocallyConnectedSpace α ↔ ∀ (x : α), (𝓝 x).HasBasis (fun s => IsOpen s ∧ x ∈ s ∧ IsConnected s) id
<VAR>α : Type u<VAR>TopologicalSpace α<GOAL>LocallyConnectedSpace α ↔ ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen V ∧ x ∈ V ∧ IsConnected V
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LocallyConnectedSpace α<VAR>F : Set α<VAR>x : α<VAR>h : F ∈ 𝓝 x<GOAL>connectedComponentIn F x ∈ 𝓝 x
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LocallyConnectedSpace α<VAR>F : Set α<VAR>x : α<VAR>hF : IsOpen F<GOAL>IsOpen (connectedComponentIn F x)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LocallyConnectedSpace α<VAR>x : α<GOAL>IsOpen (connectedComponent x)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LocallyConnectedSpace α<VAR>x : α<GOAL>IsClopen (connectedComponent x)
<VAR>α : Type u<VAR>TopologicalSpace α<GOAL>LocallyConnectedSpace α ↔ ∀ (F : Set α), IsOpen F → ∀ x ∈ F, IsOpen (connectedComponentIn F x)
<VAR>α : Type u<VAR>TopologicalSpace α<GOAL>LocallyConnectedSpace α ↔ ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U
<VAR>α : Type u<VAR>TopologicalSpace α<GOAL>LocallyConnectedSpace α ↔ ∀ (x : α), (𝓝 x).HasBasis (fun s => s ∈ 𝓝 x ∧ IsPreconnected s) id
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>ι : Type u_3<VAR>b : α → ι → Set α<VAR>p : α → ι → Prop<VAR>hbasis : ∀ (x : α), (𝓝 x).HasBasis (p x) (b x)<VAR>hconnected : ∀ (x : α) (i : ι), p x i → IsPreconnected (b x i)<GOAL>LocallyConnectedSpace α
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LocallyConnectedSpace α<VAR>TopologicalSpace β<VAR>f : β → α<VAR>h : OpenEmbedding f<GOAL>LocallyConnectedSpace β
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LocallyConnectedSpace α<VAR>U : Set α<VAR>hU : IsOpen U<GOAL>LocallyConnectedSpace ↑U
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<GOAL>Function.Injective ContinuousAlternatingMap.toContinuousMultilinearMap
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<GOAL>Set.range ContinuousAlternatingMap.toContinuousMultilinearMap = {f | ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → f v = 0}
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>f : M [⋀^ι]→L[R] N<GOAL>Continuous ⇑f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>f : M [⋀^ι]→L[R] N<GOAL>⇑f.toContinuousMultilinearMap = ⇑f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>f : ContinuousMultilinearMap R (fun x => M) N<VAR>h : ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → f.toFun v = 0<GOAL>⇑{ toContinuousMultilinearMap := f, map_eq_zero_of_eq' := h } = ⇑f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>f : M [⋀^ι]→L[R] N<GOAL>⇑f.toAlternatingMap = ⇑f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>f g : M [⋀^ι]→L[R] N<VAR>H : ∀ (x : ι → M), f x = g x<GOAL>f = g
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>f g : M [⋀^ι]→L[R] N<GOAL>f = g ↔ ∀ (x : ι → M), f x = g x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<GOAL>Function.Injective ContinuousAlternatingMap.toAlternatingMap
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<GOAL>Set.range ContinuousAlternatingMap.toAlternatingMap = {f | Continuous ⇑f}
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>f : M [⋀^ι]→L[R] N<VAR>DecidableEq ι<VAR>m : ι → M<VAR>i : ι<VAR>x y : M<GOAL>f (Function.update m i (x + y)) = f (Function.update m i x) + f (Function.update m i y)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>f : M [⋀^ι]→L[R] N<VAR>DecidableEq ι<VAR>m : ι → M<VAR>i : ι<VAR>c : R<VAR>x : M<GOAL>f (Function.update m i (c • x)) = c • f (Function.update m i x)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>f : M [⋀^ι]→L[R] N<VAR>m : ι → M<VAR>i : ι<VAR>h : m i = 0<GOAL>f m = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>f : M [⋀^ι]→L[R] N<VAR>DecidableEq ι<VAR>m : ι → M<VAR>i : ι<GOAL>f (Function.update m i 0) = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>f : M [⋀^ι]→L[R] N<VAR>Nonempty ι<GOAL>f 0 = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>f : M [⋀^ι]→L[R] N<VAR>v : ι → M<VAR>i j : ι<VAR>h : v i = v j<VAR>hij : i ≠ j<GOAL>f v = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>f : M [⋀^ι]→L[R] N<VAR>v : ι → M<VAR>hv : ¬Function.Injective v<GOAL>f v = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>f : M [⋀^ι]→L[R] N<VAR>p : Submodule R N<VAR>h : ∀ (v : ι → M), f v ∈ p<VAR>v : (i : ι) → (fun x => M) i<GOAL>↑((f.codRestrict p h) v) = f v
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<GOAL>⇑0 = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<GOAL>ContinuousAlternatingMap.toContinuousMultilinearMap 0 = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<GOAL>ContinuousAlternatingMap.toAlternatingMap 0 = 0
<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>TopologicalSpace N<VAR>R' : Type u_7<VAR>A : Type u_9<VAR>Monoid R'<VAR>Semiring A<VAR>Module A M<VAR>Module A N<VAR>DistribMulAction R' N<VAR>ContinuousConstSMul R' N<VAR>SMulCommClass A R' N<VAR>f : M [⋀^ι]→L[A] N<VAR>c : R'<GOAL>⇑(c • f) = c • ⇑f
<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>TopologicalSpace N<VAR>R' : Type u_7<VAR>A : Type u_9<VAR>Monoid R'<VAR>Semiring A<VAR>Module A M<VAR>Module A N<VAR>DistribMulAction R' N<VAR>ContinuousConstSMul R' N<VAR>SMulCommClass A R' N<VAR>f : M [⋀^ι]→L[A] N<VAR>c : R'<VAR>v : ι → M<GOAL>(c • f) v = c • f v
<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>TopologicalSpace N<VAR>R' : Type u_7<VAR>A : Type u_9<VAR>Monoid R'<VAR>Semiring A<VAR>Module A M<VAR>Module A N<VAR>DistribMulAction R' N<VAR>ContinuousConstSMul R' N<VAR>SMulCommClass A R' N<VAR>c : R'<VAR>f : M [⋀^ι]→L[A] N<GOAL>(c • f).toContinuousMultilinearMap = c • f.toContinuousMultilinearMap
<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>TopologicalSpace N<VAR>R' : Type u_7<VAR>A : Type u_9<VAR>Monoid R'<VAR>Semiring A<VAR>Module A M<VAR>Module A N<VAR>DistribMulAction R' N<VAR>ContinuousConstSMul R' N<VAR>SMulCommClass A R' N<VAR>c : R'<VAR>f : M [⋀^ι]→L[A] N<GOAL>(c • f).toAlternatingMap = c • f.toAlternatingMap
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>f g : M [⋀^ι]→L[R] N<VAR>ContinuousAdd N<GOAL>⇑(f + g) = ⇑f + ⇑g
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>f g : M [⋀^ι]→L[R] N<VAR>ContinuousAdd N<VAR>v : ι → M<GOAL>(f + g) v = f v + g v
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>ContinuousAdd N<VAR>f g : M [⋀^ι]→L[R] N<GOAL>(f + g).toContinuousMultilinearMap = f.toContinuousMultilinearMap + g.toContinuousMultilinearMap
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>ContinuousAdd N<VAR>f g : M [⋀^ι]→L[R] N<GOAL>(f + g).toAlternatingMap = f.toAlternatingMap + g.toAlternatingMap
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>ContinuousAdd N<VAR>α : Type u_7<VAR>f : α → M [⋀^ι]→L[R] N<VAR>m : ι → M<VAR>s : Finset α<GOAL>(∑ a ∈ s, f a) m = ∑ a ∈ s, (f a) m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>ContinuousAdd N<VAR>f : M [⋀^ι]→L[R] N<GOAL>ContinuousAlternatingMap.toMultilinearAddHom f = f.toContinuousMultilinearMap
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>f : M [⋀^ι]→L[R] N<VAR>DecidableEq ι<VAR>m : ι → M<VAR>i : ι<VAR>x : M<GOAL>(f.toContinuousLinearMap m i) x = f (Function.update m i x)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>N' : Type u_5<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>AddCommMonoid N'<VAR>Module R N'<VAR>TopologicalSpace N'<VAR>f : M [⋀^ι]→L[R] N<VAR>g : M [⋀^ι]→L[R] N'<VAR>m : (i : ι) → (fun x => M) i<GOAL>(f.prod g) m = (f m, g m)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>ι' : Type u_7<VAR>M' : ι' → Type u_8<VAR>(i : ι') → AddCommMonoid (M' i)<VAR>(i : ι') → TopologicalSpace (M' i)<VAR>(i : ι') → Module R (M' i)<VAR>f : (i : ι') → M [⋀^ι]→L[R] M' i<GOAL>⇑(ContinuousAlternatingMap.pi f) = fun m j => (f j) m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>ι' : Type u_7<VAR>M' : ι' → Type u_8<VAR>(i : ι') → AddCommMonoid (M' i)<VAR>(i : ι') → TopologicalSpace (M' i)<VAR>(i : ι') → Module R (M' i)<VAR>f : (i : ι') → M [⋀^ι]→L[R] M' i<VAR>m : ι → M<VAR>j : ι'<GOAL>(ContinuousAlternatingMap.pi f) m j = (f j) m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>Subsingleton ι<VAR>i : ι<VAR>f : M →L[R] N<GOAL>((ContinuousAlternatingMap.ofSubsingleton R M N i) f).toContinuousMultilinearMap = (ContinuousMultilinearMap.ofSubsingleton R M N i) f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>Subsingleton ι<VAR>i : ι<VAR>f : M →L[R] N<VAR>x : ι → M<GOAL>((ContinuousAlternatingMap.ofSubsingleton R M N i) f) x = f (x i)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>Subsingleton ι<VAR>i : ι<VAR>f : M [⋀^ι]→L[R] N<VAR>x : M<GOAL>((ContinuousAlternatingMap.ofSubsingleton R M N i).symm f) x = f fun x_1 => x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>Subsingleton ι<VAR>i : ι<VAR>f : M →L[R] N<GOAL>((ContinuousAlternatingMap.ofSubsingleton R M N i) f).toAlternatingMap = (AlternatingMap.ofSubsingleton R M N i) ↑f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>IsEmpty ι<VAR>m : N<GOAL>∀ (a : (i : ι) → (fun x => M) i), (ContinuousAlternatingMap.constOfIsEmpty R M ι m) a = m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>IsEmpty ι<VAR>m : N<GOAL>(ContinuousAlternatingMap.constOfIsEmpty R M ι m).toContinuousMultilinearMap = ContinuousMultilinearMap.constOfIsEmpty R (fun x => M) m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>IsEmpty ι<VAR>m : N<GOAL>(ContinuousAlternatingMap.constOfIsEmpty R M ι m).toAlternatingMap = AlternatingMap.constOfIsEmpty R M ι m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>TopologicalSpace M'<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>g : M [⋀^ι]→L[R] N<VAR>f : M' →L[R] M<VAR>m : ι → M'<GOAL>(g.compContinuousLinearMap f) m = g (⇑f ∘ m)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>N' : Type u_5<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>AddCommMonoid N'<VAR>Module R N'<VAR>TopologicalSpace N'<VAR>g : N →L[R] N'<VAR>f : M [⋀^ι]→L[R] N<GOAL>⇑(g.compContinuousAlternatingMap f) = ⇑g ∘ ⇑f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>N' : Type u_5<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>AddCommMonoid N'<VAR>Module R N'<VAR>TopologicalSpace N'<VAR>e : N ≃L[R] N'<VAR>f : M [⋀^ι]→L[R] N<GOAL>⇑(e.compContinuousAlternatingMap f) = ⇑e ∘ ⇑f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>ι' : Type u_7<VAR>N : ι' → Type u_8<VAR>(i : ι') → AddCommMonoid (N i)<VAR>(i : ι') → TopologicalSpace (N i)<VAR>(i : ι') → Module R (N i)<VAR>f : (i : ι') → M [⋀^ι]→L[R] N i<GOAL>ContinuousAlternatingMap.piEquiv f = ContinuousAlternatingMap.pi f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>ι' : Type u_7<VAR>N : ι' → Type u_8<VAR>(i : ι') → AddCommMonoid (N i)<VAR>(i : ι') → TopologicalSpace (N i)<VAR>(i : ι') → Module R (N i)<VAR>f : M [⋀^ι]→L[R] ((i : ι') → N i)<VAR>i : ι'<GOAL>ContinuousAlternatingMap.piEquiv.symm f i = (ContinuousLinearMap.proj i).compContinuousAlternatingMap f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>n : ℕ<VAR>f : M [⋀^Fin (n + 1)]→L[R] N<VAR>m : Fin n → M<VAR>x y : M<GOAL>f (Fin.cons (x + y) m) = f (Fin.cons x m) + f (Fin.cons y m)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>n : ℕ<VAR>f : M [⋀^Fin (n + 1)]→L[R] N<VAR>m : Fin n → M<VAR>x y : M<GOAL>f (Matrix.vecCons (x + y) m) = f (Matrix.vecCons x m) + f (Matrix.vecCons y m)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>TopologicalSpace M<VAR>AddCommMonoid N<VAR>Module R N<VAR>TopologicalSpace N<VAR>n : ℕ<VAR>f : M [⋀^Fin (n + 1)]→L[R] N<VAR>m : Fin n → M<VAR>c : R<VAR>x : M<GOAL>f (Fin.cons (c • x) m) = c • f (Fin.cons x m)