Theorem: smul_cmmap_cont (Ray/Misc/Multilinear.lean)

State before:
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid A
inst✝³ : Module 𝕜 A
inst✝² : TopologicalSpace A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
⊢ Continuous (smulCmmapFn x xs)
Tactic:
apply Continuous.smul
State after:
case hf
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid A
inst✝³ : Module 𝕜 A
inst✝² : TopologicalSpace A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
⊢ Continuous fun x_1 => x.toFun fun x => x_1 0

case hg
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid A
inst✝³ : Module 𝕜 A
inst✝² : TopologicalSpace A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
⊢ Continuous fun x => xs.toFun fun i => x i.succ

State before:
case hf
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid A
inst✝³ : Module 𝕜 A
inst✝² : TopologicalSpace A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
⊢ Continuous fun x_1 => x.toFun fun x => x_1 0

case hg
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid A
inst✝³ : Module 𝕜 A
inst✝² : TopologicalSpace A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
⊢ Continuous fun x => xs.toFun fun i => x i.succ
Tactic:
repeat continuity
State after:
no goals

State before:
case hg
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid A
inst✝³ : Module 𝕜 A
inst✝² : TopologicalSpace A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
⊢ Continuous fun x => xs.toFun fun i => x i.succ
Tactic:
continuity
State after:
no goals