ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<GOAL>⇑0 = 0
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>v : V₁<GOAL>0 v = 0
<VAR>V : Type u_1<VAR>SeminormedAddCommGroup V<GOAL>∀ (a : V), (NormedAddGroupHom.id V) a = a
<VAR>V : Type u_1<VAR>SeminormedAddCommGroup V<GOAL>‖NormedAddGroupHom.id V‖ ≤ 1
<VAR>V : Type u_1<VAR>SeminormedAddCommGroup V<VAR>h : ∃ x, ‖x‖ ≠ 0<GOAL>‖NormedAddGroupHom.id V‖ = 1
<VAR>V : Type u_5<VAR>NormedAddCommGroup V<VAR>Nontrivial V<GOAL>‖NormedAddGroupHom.id V‖ = 1
<VAR>V : Type u_1<VAR>SeminormedAddCommGroup V<GOAL>⇑(NormedAddGroupHom.id V) = id
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : NormedAddGroupHom V₁ V₂<GOAL>⇑(-f) = -⇑f
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : NormedAddGroupHom V₁ V₂<VAR>v : V₁<GOAL>(-f) v = -f v
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : NormedAddGroupHom V₁ V₂<GOAL>‖-f‖ = ‖f‖
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f g : NormedAddGroupHom V₁ V₂<GOAL>⇑(f - g) = ⇑f - ⇑g
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f g : NormedAddGroupHom V₁ V₂<VAR>v : V₁<GOAL>(f - g) v = f v - g v
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>R : Type u_5<VAR>MonoidWithZero R<VAR>DistribMulAction R V₂<VAR>PseudoMetricSpace R<VAR>BoundedSMul R V₂<VAR>r : R<VAR>f : NormedAddGroupHom V₁ V₂<GOAL>⇑(r • f) = r • ⇑f
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>R : Type u_5<VAR>MonoidWithZero R<VAR>DistribMulAction R V₂<VAR>PseudoMetricSpace R<VAR>BoundedSMul R V₂<VAR>r : R<VAR>f : NormedAddGroupHom V₁ V₂<VAR>v : V₁<GOAL>(r • f) v = r • f v
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>r : ℕ<VAR>f : NormedAddGroupHom V₁ V₂<GOAL>⇑(r • f) = r • ⇑f
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>r : ℕ<VAR>f : NormedAddGroupHom V₁ V₂<VAR>v : V₁<GOAL>(r • f) v = r • f v
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>r : ℤ<VAR>f : NormedAddGroupHom V₁ V₂<GOAL>⇑(r • f) = r • ⇑f
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>r : ℤ<VAR>f : NormedAddGroupHom V₁ V₂<VAR>v : V₁<GOAL>(r • f) v = r • f v
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<GOAL>∀ (a : NormedAddGroupHom V₁ V₂) (a_1 : V₁), NormedAddGroupHom.coeAddHom a a_1 = a a_1
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>ι : Type u_5<VAR>s : Finset ι<VAR>f : ι → NormedAddGroupHom V₁ V₂<GOAL>⇑(∑ i ∈ s, f i) = ∑ i ∈ s, ⇑(f i)
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>ι : Type u_5<VAR>s : Finset ι<VAR>f : ι → NormedAddGroupHom V₁ V₂<VAR>v : V₁<GOAL>(∑ i ∈ s, f i) v = ∑ i ∈ s, (f i) v
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>SeminormedAddCommGroup V₃<VAR>g : NormedAddGroupHom V₂ V₃<VAR>f : NormedAddGroupHom V₁ V₂<GOAL>∀ (a : V₁), (g.comp f) a = g (f a)
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>SeminormedAddCommGroup V₃<VAR>g : NormedAddGroupHom V₂ V₃<VAR>f : NormedAddGroupHom V₁ V₂<GOAL>‖g.comp f‖ ≤ ‖g‖ * ‖f‖
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>SeminormedAddCommGroup V₃<VAR>f : NormedAddGroupHom V₁ V₂<VAR>g : NormedAddGroupHom V₂ V₃<VAR>C₁ C₂ : ℝ<VAR>hg : ‖g‖ ≤ C₂<VAR>hf : ‖f‖ ≤ C₁<GOAL>‖g.comp f‖ ≤ C₂ * C₁
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>SeminormedAddCommGroup V₃<VAR>f : NormedAddGroupHom V₁ V₂<VAR>g : NormedAddGroupHom V₂ V₃<VAR>C₁ C₂ C₃ : ℝ<VAR>h : C₃ = C₂ * C₁<VAR>hg : ‖g‖ ≤ C₂<VAR>hf : ‖f‖ ≤ C₁<GOAL>‖g.comp f‖ ≤ C₃
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>SeminormedAddCommGroup V₃<VAR>f : NormedAddGroupHom V₂ V₃<GOAL>f.comp 0 = 0
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>SeminormedAddCommGroup V₃<VAR>f : NormedAddGroupHom V₁ V₂<GOAL>NormedAddGroupHom.comp 0 f = 0
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>SeminormedAddCommGroup V₃<VAR>V₄ : Type u_5<VAR>SeminormedAddCommGroup V₄<VAR>h : NormedAddGroupHom V₃ V₄<VAR>g : NormedAddGroupHom V₂ V₃<VAR>f : NormedAddGroupHom V₁ V₂<GOAL>(h.comp g).comp f = h.comp (g.comp f)
<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>SeminormedAddCommGroup V₃<VAR>f : NormedAddGroupHom V₁ V₂<VAR>g : NormedAddGroupHom V₂ V₃<GOAL>⇑(g.comp f) = ⇑g ∘ ⇑f
<VAR>V : Type u_1<VAR>SeminormedAddCommGroup V<VAR>s : AddSubgroup V<VAR>self : ↥s<GOAL>(NormedAddGroupHom.incl s) self = ↑self
<VAR>V : Type u_1<VAR>SeminormedAddCommGroup V<VAR>V' : AddSubgroup V<VAR>x : ↥V'<GOAL>‖(NormedAddGroupHom.incl V') x‖ = ‖x‖
<VAR>V₁ : Type u_3<VAR>V₂ : Type u_4<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : NormedAddGroupHom V₁ V₂<VAR>v : V₁<GOAL>v ∈ f.ker ↔ f v = 0
<VAR>V₁ : Type u_3<VAR>V₂ : Type u_4<VAR>V₃ : Type u_5<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>SeminormedAddCommGroup V₃<VAR>f : NormedAddGroupHom V₁ V₂<VAR>g : NormedAddGroupHom V₂ V₃<VAR>h : g.comp f = 0<VAR>v : V₁<GOAL>↑((NormedAddGroupHom.ker.lift f g h) v) = f v
<VAR>V₁ : Type u_3<VAR>V₂ : Type u_4<VAR>V₃ : Type u_5<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>SeminormedAddCommGroup V₃<VAR>f : NormedAddGroupHom V₁ V₂<VAR>g : NormedAddGroupHom V₂ V₃<VAR>h : g.comp f = 0<GOAL>(NormedAddGroupHom.incl g.ker).comp (NormedAddGroupHom.ker.lift f g h) = f
<VAR>V₁ : Type u_3<VAR>V₂ : Type u_4<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<GOAL>NormedAddGroupHom.ker 0 = ⊤
<VAR>V₁ : Type u_3<VAR>V₂ : Type u_4<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : NormedAddGroupHom V₁ V₂<GOAL>↑f.ker = ⇑f ⁻¹' {0}
<VAR>V₁ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>V₂ : Type u_6<VAR>NormedAddCommGroup V₂<VAR>f : NormedAddGroupHom V₁ V₂<GOAL>IsClosed ↑f.ker
<VAR>V₁ : Type u_3<VAR>V₂ : Type u_4<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : NormedAddGroupHom V₁ V₂<VAR>v : V₂<GOAL>v ∈ f.range ↔ ∃ w, f w = v
<VAR>V₁ : Type u_3<VAR>V₂ : Type u_4<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : NormedAddGroupHom V₁ V₂<VAR>v : V₁<GOAL>f v ∈ f.range
<VAR>V₁ : Type u_3<VAR>V₂ : Type u_4<VAR>V₃ : Type u_5<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>SeminormedAddCommGroup V₃<VAR>f : NormedAddGroupHom V₁ V₂<VAR>g : NormedAddGroupHom V₂ V₃<GOAL>(g.comp f).range = AddSubgroup.map g.toAddMonoidHom f.range
<VAR>V₁ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>s : AddSubgroup V₁<GOAL>(NormedAddGroupHom.incl s).range = s
<VAR>V₁ : Type u_3<VAR>V₂ : Type u_4<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : NormedAddGroupHom V₁ V₂<GOAL>(f.comp (NormedAddGroupHom.incl ⊤)).range = f.range
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>SeminormedAddCommGroup V<VAR>SeminormedAddCommGroup W<VAR>f : NormedAddGroupHom V W<GOAL>f.NormNoninc ↔ ‖f‖ ≤ 1
<VAR>V₁ : Type u_3<VAR>V₂ : Type u_4<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<GOAL>NormedAddGroupHom.NormNoninc 0
<VAR>V : Type u_1<VAR>SeminormedAddCommGroup V<GOAL>(NormedAddGroupHom.id V).NormNoninc
<VAR>V₁ : Type u_3<VAR>V₂ : Type u_4<VAR>V₃ : Type u_5<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>SeminormedAddCommGroup V₃<VAR>g : NormedAddGroupHom V₂ V₃<VAR>f : NormedAddGroupHom V₁ V₂<VAR>hg : g.NormNoninc<VAR>hf : f.NormNoninc<GOAL>(g.comp f).NormNoninc
<VAR>V₁ : Type u_3<VAR>V₂ : Type u_4<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>f : NormedAddGroupHom V₁ V₂<GOAL>(-f).NormNoninc ↔ f.NormNoninc
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>SeminormedAddCommGroup V<VAR>SeminormedAddCommGroup W<VAR>f : NormedAddGroupHom V W<VAR>hf : Isometry ⇑f<VAR>v : V<GOAL>‖f v‖ = ‖v‖
<VAR>V : Type u_1<VAR>SeminormedAddCommGroup V<GOAL>Isometry ⇑(NormedAddGroupHom.id V)
<VAR>V₁ : Type u_3<VAR>V₂ : Type u_4<VAR>V₃ : Type u_5<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>SeminormedAddCommGroup V₃<VAR>g : NormedAddGroupHom V₂ V₃<VAR>f : NormedAddGroupHom V₁ V₂<VAR>hg : Isometry ⇑g<VAR>hf : Isometry ⇑f<GOAL>Isometry ⇑(g.comp f)
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>SeminormedAddCommGroup V<VAR>SeminormedAddCommGroup W<VAR>f : NormedAddGroupHom V W<VAR>hf : Isometry ⇑f<GOAL>f.NormNoninc
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>SeminormedAddCommGroup V<VAR>SeminormedAddCommGroup W<VAR>f g : NormedAddGroupHom V W<GOAL>f.comp (NormedAddGroupHom.Equalizer.ι f g) = g.comp (NormedAddGroupHom.Equalizer.ι f g)
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>V₁ : Type u_3<VAR>SeminormedAddCommGroup V<VAR>SeminormedAddCommGroup W<VAR>SeminormedAddCommGroup V₁<VAR>f g : NormedAddGroupHom V W<VAR>φ : NormedAddGroupHom V₁ V<VAR>h : f.comp φ = g.comp φ<VAR>v : V₁<GOAL>↑((NormedAddGroupHom.Equalizer.lift φ h) v) = φ v
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>V₁ : Type u_3<VAR>SeminormedAddCommGroup V<VAR>SeminormedAddCommGroup W<VAR>SeminormedAddCommGroup V₁<VAR>f g : NormedAddGroupHom V W<VAR>φ : NormedAddGroupHom V₁ V<VAR>h : f.comp φ = g.comp φ<GOAL>(NormedAddGroupHom.Equalizer.ι f g).comp (NormedAddGroupHom.Equalizer.lift φ h) = φ
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>V₁ : Type u_3<VAR>SeminormedAddCommGroup V<VAR>SeminormedAddCommGroup W<VAR>SeminormedAddCommGroup V₁<VAR>f g : NormedAddGroupHom V W<VAR>φ : { φ // f.comp φ = g.comp φ }<GOAL>NormedAddGroupHom.Equalizer.liftEquiv φ = NormedAddGroupHom.Equalizer.lift ↑φ ⋯
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>V₁ : Type u_3<VAR>SeminormedAddCommGroup V<VAR>SeminormedAddCommGroup W<VAR>SeminormedAddCommGroup V₁<VAR>f g : NormedAddGroupHom V W<VAR>ψ : NormedAddGroupHom V₁ ↥(f.equalizer g)<GOAL>↑(NormedAddGroupHom.Equalizer.liftEquiv.symm ψ) = (NormedAddGroupHom.Equalizer.ι f g).comp ψ
<VAR>V₁ : Type u_3<VAR>V₂ : Type u_4<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>W₁ : Type u_6<VAR>W₂ : Type u_7<VAR>SeminormedAddCommGroup W₁<VAR>SeminormedAddCommGroup W₂<VAR>f₁ g₁ : NormedAddGroupHom V₁ W₁<VAR>f₂ g₂ : NormedAddGroupHom V₂ W₂<VAR>φ : NormedAddGroupHom V₁ V₂<VAR>ψ : NormedAddGroupHom W₁ W₂<VAR>hf : ψ.comp f₁ = f₂.comp φ<VAR>hg : ψ.comp g₁ = g₂.comp φ<GOAL>(NormedAddGroupHom.Equalizer.ι f₂ g₂).comp (NormedAddGroupHom.Equalizer.map φ ψ hf hg) = φ.comp (NormedAddGroupHom.Equalizer.ι f₁ g₁)
<VAR>V₁ : Type u_3<VAR>SeminormedAddCommGroup V₁<VAR>W₁ : Type u_6<VAR>SeminormedAddCommGroup W₁<VAR>f₁ g₁ : NormedAddGroupHom V₁ W₁<GOAL>NormedAddGroupHom.Equalizer.map (NormedAddGroupHom.id V₁) (NormedAddGroupHom.id W₁) ⋯ ⋯ = NormedAddGroupHom.id ↥(f₁.equalizer g₁)
<VAR>V₁ : Type u_3<VAR>V₂ : Type u_4<VAR>V₃ : Type u_5<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>SeminormedAddCommGroup V₃<VAR>W₁ : Type u_6<VAR>W₂ : Type u_7<VAR>W₃ : Type u_8<VAR>SeminormedAddCommGroup W₁<VAR>SeminormedAddCommGroup W₂<VAR>SeminormedAddCommGroup W₃<VAR>f₁ : NormedAddGroupHom V₁ W₁<VAR>f₂ : NormedAddGroupHom V₂ W₂<VAR>f₃ : NormedAddGroupHom V₃ W₃<VAR>φ : NormedAddGroupHom V₁ V₂<VAR>ψ : NormedAddGroupHom W₁ W₂<VAR>φ' : NormedAddGroupHom V₂ V₃<VAR>ψ' : NormedAddGroupHom W₂ W₃<VAR>hf : ψ.comp f₁ = f₂.comp φ<VAR>hf' : ψ'.comp f₂ = f₃.comp φ'<GOAL>(ψ'.comp ψ).comp f₁ = f₃.comp (φ'.comp φ)
<VAR>V₁ : Type u_3<VAR>V₂ : Type u_4<VAR>V₃ : Type u_5<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>SeminormedAddCommGroup V₃<VAR>W₁ : Type u_6<VAR>W₂ : Type u_7<VAR>W₃ : Type u_8<VAR>SeminormedAddCommGroup W₁<VAR>SeminormedAddCommGroup W₂<VAR>SeminormedAddCommGroup W₃<VAR>f₁ g₁ : NormedAddGroupHom V₁ W₁<VAR>f₂ g₂ : NormedAddGroupHom V₂ W₂<VAR>f₃ g₃ : NormedAddGroupHom V₃ W₃<VAR>φ : NormedAddGroupHom V₁ V₂<VAR>ψ : NormedAddGroupHom W₁ W₂<VAR>φ' : NormedAddGroupHom V₂ V₃<VAR>ψ' : NormedAddGroupHom W₂ W₃<VAR>hf : ψ.comp f₁ = f₂.comp φ<VAR>hg : ψ.comp g₁ = g₂.comp φ<VAR>hf' : ψ'.comp f₂ = f₃.comp φ'<VAR>hg' : ψ'.comp g₂ = g₃.comp φ'<GOAL>(NormedAddGroupHom.Equalizer.map φ' ψ' hf' hg').comp (NormedAddGroupHom.Equalizer.map φ ψ hf hg) = NormedAddGroupHom.Equalizer.map (φ'.comp φ) (ψ'.comp ψ) ⋯ ⋯
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>SeminormedAddCommGroup V<VAR>SeminormedAddCommGroup W<VAR>f g : NormedAddGroupHom V W<GOAL>(NormedAddGroupHom.Equalizer.ι f g).NormNoninc
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>V₁ : Type u_3<VAR>SeminormedAddCommGroup V<VAR>SeminormedAddCommGroup W<VAR>SeminormedAddCommGroup V₁<VAR>f g : NormedAddGroupHom V W<VAR>φ : NormedAddGroupHom V₁ V<VAR>h : f.comp φ = g.comp φ<VAR>hφ : φ.NormNoninc<GOAL>(NormedAddGroupHom.Equalizer.lift φ h).NormNoninc
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>V₁ : Type u_3<VAR>SeminormedAddCommGroup V<VAR>SeminormedAddCommGroup W<VAR>SeminormedAddCommGroup V₁<VAR>f g : NormedAddGroupHom V W<VAR>φ : NormedAddGroupHom V₁ V<VAR>h : f.comp φ = g.comp φ<VAR>C : ℝ<VAR>hφ : ‖φ‖ ≤ C<GOAL>‖NormedAddGroupHom.Equalizer.lift φ h‖ ≤ C
<VAR>V₁ : Type u_3<VAR>V₂ : Type u_4<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>W₁ : Type u_6<VAR>W₂ : Type u_7<VAR>SeminormedAddCommGroup W₁<VAR>SeminormedAddCommGroup W₂<VAR>f₁ g₁ : NormedAddGroupHom V₁ W₁<VAR>f₂ g₂ : NormedAddGroupHom V₂ W₂<VAR>φ : NormedAddGroupHom V₁ V₂<VAR>ψ : NormedAddGroupHom W₁ W₂<VAR>hf : ψ.comp f₁ = f₂.comp φ<VAR>hg : ψ.comp g₁ = g₂.comp φ<VAR>hφ : φ.NormNoninc<GOAL>(NormedAddGroupHom.Equalizer.map φ ψ hf hg).NormNoninc
<VAR>V₁ : Type u_3<VAR>V₂ : Type u_4<VAR>SeminormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>W₁ : Type u_6<VAR>W₂ : Type u_7<VAR>SeminormedAddCommGroup W₁<VAR>SeminormedAddCommGroup W₂<VAR>f₁ g₁ : NormedAddGroupHom V₁ W₁<VAR>f₂ g₂ : NormedAddGroupHom V₂ W₂<VAR>φ : NormedAddGroupHom V₁ V₂<VAR>ψ : NormedAddGroupHom W₁ W₂<VAR>hf : ψ.comp f₁ = f₂.comp φ<VAR>hg : ψ.comp g₁ = g₂.comp φ<VAR>C : ℝ<VAR>hφ : ‖φ.comp (NormedAddGroupHom.Equalizer.ι f₁ g₁)‖ ≤ C<GOAL>‖NormedAddGroupHom.Equalizer.map φ ψ hf hg‖ ≤ C
<VAR>ι : Type uι<VAR>Fintype ι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>SeminormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : ⨂[𝕜] (i : ι), E i<GOAL>∀ (a : ContinuousMultilinearMap 𝕜 E F), ((PiTensorProduct.toDualContinuousMultilinearMap F) x) a = (PiTensorProduct.lift a.toMultilinearMap) x
<VAR>ι : Type uι<VAR>Fintype ι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>SeminormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : ⨂[𝕜] (i : ι), E i<GOAL>‖(PiTensorProduct.toDualContinuousMultilinearMap F) x‖ ≤ PiTensorProduct.projectiveSeminorm x
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type u_3<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<GOAL>PiTensorProduct.injectiveSeminorm = sSup {p | ∃ G x x_1, p = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (PiTensorProduct.toDualContinuousMultilinearMap G)}
<VAR>ι : Type uι<VAR>Fintype ι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<GOAL>BddAbove {p | ∃ G x x_1, p = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (PiTensorProduct.toDualContinuousMultilinearMap G)}
<VAR>ι : Type uι<VAR>Fintype ι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>x : ⨂[𝕜] (i : ι), E i<GOAL>PiTensorProduct.injectiveSeminorm x = ⨆ p, ↑p x
<VAR>ι : Type uι<VAR>Fintype ι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>SeminormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>x : ⨂[𝕜] (i : ι), E i<GOAL>‖(PiTensorProduct.lift f.toMultilinearMap) x‖ ≤ ‖f‖ * PiTensorProduct.injectiveSeminorm x
<VAR>ι : Type uι<VAR>Fintype ι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<GOAL>PiTensorProduct.injectiveSeminorm ≤ PiTensorProduct.projectiveSeminorm
<VAR>ι : Type uι<VAR>Fintype ι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>m : (i : ι) → E i<GOAL>PiTensorProduct.injectiveSeminorm (⨂ₜ[𝕜] (i : ι), m i) ≤ ∏ i : ι, ‖m i‖
<VAR>ι : Type uι<VAR>Fintype ι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>SeminormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>l : (⨂[𝕜] (i : ι), E i) →L[𝕜] F<GOAL>(PiTensorProduct.liftEquiv 𝕜 E F).symm l = (PiTensorProduct.lift.symm ↑l).mkContinuous ‖l‖ ⋯
<VAR>ι : Type uι<VAR>Fintype ι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>SeminormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : ContinuousMultilinearMap 𝕜 E F<GOAL>(PiTensorProduct.liftEquiv 𝕜 E F) f = (PiTensorProduct.lift f.toMultilinearMap).mkContinuous ‖f‖ ⋯
<VAR>ι : Type uι<VAR>Fintype ι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>SeminormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>x : ⨂[𝕜] (i : ι), E i<GOAL>((PiTensorProduct.liftIsometry 𝕜 E F) f) x = (PiTensorProduct.lift f.toMultilinearMap) x
<VAR>ι : Type uι<VAR>Fintype ι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<GOAL>∀ (a : (i : ι) → E i), (PiTensorProduct.tprodL 𝕜) a = (PiTensorProduct.tprod 𝕜) a
<VAR>ι : Type uι<VAR>Fintype ι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<GOAL>(PiTensorProduct.tprodL 𝕜).toMultilinearMap = PiTensorProduct.tprod 𝕜
<VAR>ι : Type uι<VAR>Fintype ι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>SeminormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>l : (⨂[𝕜] (i : ι), E i) →L[𝕜] F<GOAL>(PiTensorProduct.liftIsometry 𝕜 E F).symm l = l.compContinuousMultilinearMap (PiTensorProduct.tprodL 𝕜)
<VAR>ι : Type uι<VAR>Fintype ι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<GOAL>(PiTensorProduct.liftIsometry 𝕜 E (⨂[𝕜] (i : ι), E i)) (PiTensorProduct.tprodL 𝕜) = ContinuousLinearMap.id 𝕜 (⨂[𝕜] (i : ι), E i)
<VAR>ι : Type uι<VAR>Fintype ι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>E' : ι → Type u_1<VAR>(i : ι) → SeminormedAddCommGroup (E' i)<VAR>(i : ι) → NormedSpace 𝕜 (E' i)<VAR>f : (i : ι) → E i →L[𝕜] E' i<GOAL>↑(PiTensorProduct.mapL f) = PiTensorProduct.map fun i => ↑(f i)
<VAR>ι : Type uι<VAR>Fintype ι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>E' : ι → Type u_1<VAR>(i : ι) → SeminormedAddCommGroup (E' i)<VAR>(i : ι) → NormedSpace 𝕜 (E' i)<VAR>f : (i : ι) → E i →L[𝕜] E' i<VAR>x : ⨂[𝕜] (i : ι), E i<GOAL>(PiTensorProduct.mapL f) x = (PiTensorProduct.map fun i => ↑(f i)) x
<VAR>ι : Type uι<VAR>Fintype ι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>E' : ι → Type u_1<VAR>E'' : ι → Type u_2<VAR>(i : ι) → SeminormedAddCommGroup (E' i)<VAR>(i : ι) → NormedSpace 𝕜 (E' i)<VAR>(i : ι) → SeminormedAddCommGroup (E'' i)<VAR>(i : ι) → NormedSpace 𝕜 (E'' i)<VAR>g : (i : ι) → E' i →L[𝕜] E'' i<VAR>f : (i : ι) → E i →L[𝕜] E' i<GOAL>(PiTensorProduct.mapL fun i => (g i).comp (f i)) = (PiTensorProduct.mapL g).comp (PiTensorProduct.mapL f)
<VAR>ι : Type uι<VAR>Fintype ι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>SeminormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E' : ι → Type u_1<VAR>(i : ι) → SeminormedAddCommGroup (E' i)<VAR>(i : ι) → NormedSpace 𝕜 (E' i)<VAR>f : (i : ι) → E i →L[𝕜] E' i<VAR>h : ContinuousMultilinearMap 𝕜 E' F<GOAL>((PiTensorProduct.liftIsometry 𝕜 E' F) h).comp (PiTensorProduct.mapL f) = (PiTensorProduct.liftIsometry 𝕜 E F) (h.compContinuousLinearMap f)
<VAR>ι : Type uι<VAR>Fintype ι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<GOAL>(PiTensorProduct.mapL fun i => ContinuousLinearMap.id 𝕜 (E i)) = ContinuousLinearMap.id 𝕜 (⨂[𝕜] (i : ι), E i)
<VAR>ι : Type uι<VAR>Fintype ι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<GOAL>(PiTensorProduct.mapL fun i => 1) = 1
<VAR>ι : Type uι<VAR>Fintype ι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>f₁ f₂ : (i : ι) → E i →L[𝕜] E i<GOAL>(PiTensorProduct.mapL fun i => f₁ i * f₂ i) = PiTensorProduct.mapL f₁ * PiTensorProduct.mapL f₂
<VAR>ι : Type uι<VAR>Fintype ι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>f : (i : ι) → E i →L[𝕜] E i<GOAL>PiTensorProduct.mapLMonoidHom f = PiTensorProduct.mapL f
<VAR>ι : Type uι<VAR>Fintype ι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>f : (i : ι) → E i →L[𝕜] E i<VAR>n : ℕ<GOAL>PiTensorProduct.mapL (f ^ n) = PiTensorProduct.mapL f ^ n
<VAR>ι : Type uι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>E' : ι → Type u_1<VAR>(i : ι) → SeminormedAddCommGroup (E' i)<VAR>(i : ι) → NormedSpace 𝕜 (E' i)<VAR>f : (i : ι) → E i →L[𝕜] E' i<VAR>DecidableEq ι<VAR>i : ι<VAR>u : E i →L[𝕜] E' i<GOAL>(fun j => ↑(Function.update f i u j)) = Function.update (fun j => ↑(f j)) i ↑u
<VAR>ι : Type uι<VAR>Fintype ι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>E' : ι → Type u_1<VAR>(i : ι) → SeminormedAddCommGroup (E' i)<VAR>(i : ι) → NormedSpace 𝕜 (E' i)<VAR>f : (i : ι) → E i →L[𝕜] E' i<VAR>DecidableEq ι<VAR>i : ι<VAR>u v : E i →L[𝕜] E' i<GOAL>PiTensorProduct.mapL (Function.update f i (u + v)) = PiTensorProduct.mapL (Function.update f i u) + PiTensorProduct.mapL (Function.update f i v)
<VAR>ι : Type uι<VAR>Fintype ι<VAR>𝕜 : Type u𝕜<VAR>NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>E' : ι → Type u_1<VAR>(i : ι) → SeminormedAddCommGroup (E' i)<VAR>(i : ι) → NormedSpace 𝕜 (E' i)<VAR>f : (i : ι) → E i →L[𝕜] E' i<VAR>DecidableEq ι<VAR>i : ι<VAR>c : 𝕜<VAR>u : E i →L[𝕜] E' i<GOAL>PiTensorProduct.mapL (Function.update f i (c • u)) = c • PiTensorProduct.mapL (Function.update f i u)