[GOAL]
R : Type u
ι : Type v
n : ℕ
M : Fin (Nat.succ n) → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
inst✝¹⁸ : Semiring R
inst✝¹⁷ : (i : Fin (Nat.succ n)) → AddCommMonoid (M i)
inst✝¹⁶ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁵ : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹⁴ : AddCommMonoid M₂
inst✝¹³ : AddCommMonoid M₃
inst✝¹² : AddCommMonoid M₄
inst✝¹¹ : (i : Fin (Nat.succ n)) → Module R (M i)
inst✝¹⁰ : (i : ι) → Module R (M₁ i)
inst✝⁹ : (i : ι) → Module R (M₁' i)
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M₃
inst✝⁶ : Module R M₄
inst✝⁵ : (i : Fin (Nat.succ n)) → TopologicalSpace (M i)
inst✝⁴ : (i : ι) → TopologicalSpace (M₁ i)
inst✝³ : (i : ι) → TopologicalSpace (M₁' i)
inst✝² : TopologicalSpace M₂
inst✝¹ : TopologicalSpace M₃
inst✝ : TopologicalSpace M₄
f✝ f' : ContinuousMultilinearMap R M₁ M₂
f : MultilinearMap R M₁ M₂
hf : Continuous f.toFun
g : MultilinearMap R M₁ M₂
hg : Continuous g.toFun
h : { toMultilinearMap := f, cont := hf }.toMultilinearMap = { toMultilinearMap := g, cont := hg }.toMultilinearMap
⊢ { toMultilinearMap := f, cont := hf } = { toMultilinearMap := g, cont := hg }
[PROOFSTEP]
subst h
[GOAL]
R : Type u
ι : Type v
n : ℕ
M : Fin (Nat.succ n) → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
inst✝¹⁸ : Semiring R
inst✝¹⁷ : (i : Fin (Nat.succ n)) → AddCommMonoid (M i)
inst✝¹⁶ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁵ : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹⁴ : AddCommMonoid M₂
inst✝¹³ : AddCommMonoid M₃
inst✝¹² : AddCommMonoid M₄
inst✝¹¹ : (i : Fin (Nat.succ n)) → Module R (M i)
inst✝¹⁰ : (i : ι) → Module R (M₁ i)
inst✝⁹ : (i : ι) → Module R (M₁' i)
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M₃
inst✝⁶ : Module R M₄
inst✝⁵ : (i : Fin (Nat.succ n)) → TopologicalSpace (M i)
inst✝⁴ : (i : ι) → TopologicalSpace (M₁ i)
inst✝³ : (i : ι) → TopologicalSpace (M₁' i)
inst✝² : TopologicalSpace M₂
inst✝¹ : TopologicalSpace M₃
inst✝ : TopologicalSpace M₄
f✝ f' : ContinuousMultilinearMap R M₁ M₂
f : MultilinearMap R M₁ M₂
hf : Continuous f.toFun
hg : Continuous { toMultilinearMap := f, cont := hf }.toMultilinearMap.toFun
⊢ { toMultilinearMap := f, cont := hf } =
    { toMultilinearMap := { toMultilinearMap := f, cont := hf }.toMultilinearMap, cont := hg }
[PROOFSTEP]
rfl
[GOAL]
R : Type u
ι : Type v
n : ℕ
M : Fin (Nat.succ n) → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
inst✝¹⁸ : Semiring R
inst✝¹⁷ : (i : Fin (Nat.succ n)) → AddCommMonoid (M i)
inst✝¹⁶ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁵ : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹⁴ : AddCommMonoid M₂
inst✝¹³ : AddCommMonoid M₃
inst✝¹² : AddCommMonoid M₄
inst✝¹¹ : (i : Fin (Nat.succ n)) → Module R (M i)
inst✝¹⁰ : (i : ι) → Module R (M₁ i)
inst✝⁹ : (i : ι) → Module R (M₁' i)
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M₃
inst✝⁶ : Module R M₄
inst✝⁵ : (i : Fin (Nat.succ n)) → TopologicalSpace (M i)
inst✝⁴ : (i : ι) → TopologicalSpace (M₁ i)
inst✝³ : (i : ι) → TopologicalSpace (M₁' i)
inst✝² : TopologicalSpace M₂
inst✝¹ : TopologicalSpace M₃
inst✝ : TopologicalSpace M₄
f✝ f'✝ f f' : ContinuousMultilinearMap R M₁ M₂
⊢ f = f' ↔ ∀ (x : (i : ι) → M₁ i), ↑f x = ↑f' x
[PROOFSTEP]
rw [← toMultilinearMap_injective.eq_iff, MultilinearMap.ext_iff]
[GOAL]
R : Type u
ι : Type v
n : ℕ
M : Fin (Nat.succ n) → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
inst✝¹⁸ : Semiring R
inst✝¹⁷ : (i : Fin (Nat.succ n)) → AddCommMonoid (M i)
inst✝¹⁶ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁵ : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹⁴ : AddCommMonoid M₂
inst✝¹³ : AddCommMonoid M₃
inst✝¹² : AddCommMonoid M₄
inst✝¹¹ : (i : Fin (Nat.succ n)) → Module R (M i)
inst✝¹⁰ : (i : ι) → Module R (M₁ i)
inst✝⁹ : (i : ι) → Module R (M₁' i)
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M₃
inst✝⁶ : Module R M₄
inst✝⁵ : (i : Fin (Nat.succ n)) → TopologicalSpace (M i)
inst✝⁴ : (i : ι) → TopologicalSpace (M₁ i)
inst✝³ : (i : ι) → TopologicalSpace (M₁' i)
inst✝² : TopologicalSpace M₂
inst✝¹ : TopologicalSpace M₃
inst✝ : TopologicalSpace M₄
f✝ f'✝ f f' : ContinuousMultilinearMap R M₁ M₂
⊢ (∀ (x : (i : ι) → M₁ i), ↑f.toMultilinearMap x = ↑f'.toMultilinearMap x) ↔ ∀ (x : (i : ι) → M₁ i), ↑f x = ↑f' x
[PROOFSTEP]
rfl
[GOAL]
R : Type u
ι : Type v
n : ℕ
M : Fin (Nat.succ n) → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
inst✝¹⁸ : Semiring R
inst✝¹⁷ : (i : Fin (Nat.succ n)) → AddCommMonoid (M i)
inst✝¹⁶ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁵ : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹⁴ : AddCommMonoid M₂
inst✝¹³ : AddCommMonoid M₃
inst✝¹² : AddCommMonoid M₄
inst✝¹¹ : (i : Fin (Nat.succ n)) → Module R (M i)
inst✝¹⁰ : (i : ι) → Module R (M₁ i)
inst✝⁹ : (i : ι) → Module R (M₁' i)
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M₃
inst✝⁶ : Module R M₄
inst✝⁵ : (i : Fin (Nat.succ n)) → TopologicalSpace (M i)
inst✝⁴ : (i : ι) → TopologicalSpace (M₁ i)
inst✝³ : (i : ι) → TopologicalSpace (M₁' i)
inst✝² : TopologicalSpace M₂
inst✝¹ : TopologicalSpace M₃
inst✝ : TopologicalSpace M₄
f✝ f' : ContinuousMultilinearMap R M₁ M₂
g : M₂ →L[R] M₃
f : ContinuousMultilinearMap R M₁ M₂
⊢ ↑(ContinuousLinearMap.compContinuousMultilinearMap g f) = ↑g ∘ ↑f
[PROOFSTEP]
ext m
[GOAL]
case h
R : Type u
ι : Type v
n : ℕ
M : Fin (Nat.succ n) → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
inst✝¹⁸ : Semiring R
inst✝¹⁷ : (i : Fin (Nat.succ n)) → AddCommMonoid (M i)
inst✝¹⁶ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁵ : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹⁴ : AddCommMonoid M₂
inst✝¹³ : AddCommMonoid M₃
inst✝¹² : AddCommMonoid M₄
inst✝¹¹ : (i : Fin (Nat.succ n)) → Module R (M i)
inst✝¹⁰ : (i : ι) → Module R (M₁ i)
inst✝⁹ : (i : ι) → Module R (M₁' i)
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M₃
inst✝⁶ : Module R M₄
inst✝⁵ : (i : Fin (Nat.succ n)) → TopologicalSpace (M i)
inst✝⁴ : (i : ι) → TopologicalSpace (M₁ i)
inst✝³ : (i : ι) → TopologicalSpace (M₁' i)
inst✝² : TopologicalSpace M₂
inst✝¹ : TopologicalSpace M₃
inst✝ : TopologicalSpace M₄
f✝ f' : ContinuousMultilinearMap R M₁ M₂
g : M₂ →L[R] M₃
f : ContinuousMultilinearMap R M₁ M₂
m : (i : ι) → M₁ i
⊢ ↑(ContinuousLinearMap.compContinuousMultilinearMap g f) m = (↑g ∘ ↑f) m
[PROOFSTEP]
rfl
[GOAL]
R : Type u
ι : Type v
n : ℕ
M : Fin (Nat.succ n) → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
inst✝²¹ : Semiring R
inst✝²⁰ : (i : Fin (Nat.succ n)) → AddCommMonoid (M i)
inst✝¹⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁸ : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹⁷ : AddCommMonoid M₂
inst✝¹⁶ : AddCommMonoid M₃
inst✝¹⁵ : AddCommMonoid M₄
inst✝¹⁴ : (i : Fin (Nat.succ n)) → Module R (M i)
inst✝¹³ : (i : ι) → Module R (M₁ i)
inst✝¹² : (i : ι) → Module R (M₁' i)
inst✝¹¹ : Module R M₂
inst✝¹⁰ : Module R M₃
inst✝⁹ : Module R M₄
inst✝⁸ : (i : Fin (Nat.succ n)) → TopologicalSpace (M i)
inst✝⁷ : (i : ι) → TopologicalSpace (M₁ i)
inst✝⁶ : (i : ι) → TopologicalSpace (M₁' i)
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : TopologicalSpace M₃
inst✝³ : TopologicalSpace M₄
f✝ f' : ContinuousMultilinearMap R M₁ M₂
ι' : Type u_1
M' : ι' → Type u_2
inst✝² : (i : ι') → AddCommMonoid (M' i)
inst✝¹ : (i : ι') → TopologicalSpace (M' i)
inst✝ : (i : ι') → Module R (M' i)
f : (i : ι') → ContinuousMultilinearMap R M₁ (M' i)
⊢ (fun f i => ContinuousLinearMap.compContinuousMultilinearMap (ContinuousLinearMap.proj i) f) (pi f) = f
[PROOFSTEP]
ext
[GOAL]
case h.H
R : Type u
ι : Type v
n : ℕ
M : Fin (Nat.succ n) → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
inst✝²¹ : Semiring R
inst✝²⁰ : (i : Fin (Nat.succ n)) → AddCommMonoid (M i)
inst✝¹⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁸ : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹⁷ : AddCommMonoid M₂
inst✝¹⁶ : AddCommMonoid M₃
inst✝¹⁵ : AddCommMonoid M₄
inst✝¹⁴ : (i : Fin (Nat.succ n)) → Module R (M i)
inst✝¹³ : (i : ι) → Module R (M₁ i)
inst✝¹² : (i : ι) → Module R (M₁' i)
inst✝¹¹ : Module R M₂
inst✝¹⁰ : Module R M₃
inst✝⁹ : Module R M₄
inst✝⁸ : (i : Fin (Nat.succ n)) → TopologicalSpace (M i)
inst✝⁷ : (i : ι) → TopologicalSpace (M₁ i)
inst✝⁶ : (i : ι) → TopologicalSpace (M₁' i)
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : TopologicalSpace M₃
inst✝³ : TopologicalSpace M₄
f✝ f' : ContinuousMultilinearMap R M₁ M₂
ι' : Type u_1
M' : ι' → Type u_2
inst✝² : (i : ι') → AddCommMonoid (M' i)
inst✝¹ : (i : ι') → TopologicalSpace (M' i)
inst✝ : (i : ι') → Module R (M' i)
f : (i : ι') → ContinuousMultilinearMap R M₁ (M' i)
x✝¹ : ι'
x✝ : (i : ι) → M₁ i
⊢ ↑((fun f i => ContinuousLinearMap.compContinuousMultilinearMap (ContinuousLinearMap.proj i) f) (pi f) x✝¹) x✝ =
    ↑(f x✝¹) x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
ι : Type v
n : ℕ
M : Fin (Nat.succ n) → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
inst✝²¹ : Semiring R
inst✝²⁰ : (i : Fin (Nat.succ n)) → AddCommMonoid (M i)
inst✝¹⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁸ : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹⁷ : AddCommMonoid M₂
inst✝¹⁶ : AddCommMonoid M₃
inst✝¹⁵ : AddCommMonoid M₄
inst✝¹⁴ : (i : Fin (Nat.succ n)) → Module R (M i)
inst✝¹³ : (i : ι) → Module R (M₁ i)
inst✝¹² : (i : ι) → Module R (M₁' i)
inst✝¹¹ : Module R M₂
inst✝¹⁰ : Module R M₃
inst✝⁹ : Module R M₄
inst✝⁸ : (i : Fin (Nat.succ n)) → TopologicalSpace (M i)
inst✝⁷ : (i : ι) → TopologicalSpace (M₁ i)
inst✝⁶ : (i : ι) → TopologicalSpace (M₁' i)
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : TopologicalSpace M₃
inst✝³ : TopologicalSpace M₄
f✝ f' : ContinuousMultilinearMap R M₁ M₂
ι' : Type u_1
M' : ι' → Type u_2
inst✝² : (i : ι') → AddCommMonoid (M' i)
inst✝¹ : (i : ι') → TopologicalSpace (M' i)
inst✝ : (i : ι') → Module R (M' i)
f : ContinuousMultilinearMap R M₁ ((i : ι') → M' i)
⊢ pi ((fun f i => ContinuousLinearMap.compContinuousMultilinearMap (ContinuousLinearMap.proj i) f) f) = f
[PROOFSTEP]
ext
[GOAL]
case H.h
R : Type u
ι : Type v
n : ℕ
M : Fin (Nat.succ n) → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
inst✝²¹ : Semiring R
inst✝²⁰ : (i : Fin (Nat.succ n)) → AddCommMonoid (M i)
inst✝¹⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁸ : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹⁷ : AddCommMonoid M₂
inst✝¹⁶ : AddCommMonoid M₃
inst✝¹⁵ : AddCommMonoid M₄
inst✝¹⁴ : (i : Fin (Nat.succ n)) → Module R (M i)
inst✝¹³ : (i : ι) → Module R (M₁ i)
inst✝¹² : (i : ι) → Module R (M₁' i)
inst✝¹¹ : Module R M₂
inst✝¹⁰ : Module R M₃
inst✝⁹ : Module R M₄
inst✝⁸ : (i : Fin (Nat.succ n)) → TopologicalSpace (M i)
inst✝⁷ : (i : ι) → TopologicalSpace (M₁ i)
inst✝⁶ : (i : ι) → TopologicalSpace (M₁' i)
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : TopologicalSpace M₃
inst✝³ : TopologicalSpace M₄
f✝ f' : ContinuousMultilinearMap R M₁ M₂
ι' : Type u_1
M' : ι' → Type u_2
inst✝² : (i : ι') → AddCommMonoid (M' i)
inst✝¹ : (i : ι') → TopologicalSpace (M' i)
inst✝ : (i : ι') → Module R (M' i)
f : ContinuousMultilinearMap R M₁ ((i : ι') → M' i)
x✝¹ : (i : ι) → M₁ i
x✝ : ι'
⊢ ↑(pi ((fun f i => ContinuousLinearMap.compContinuousMultilinearMap (ContinuousLinearMap.proj i) f) f)) x✝¹ x✝ =
    ↑f x✝¹ x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
ι : Type v
n : ℕ
M : Fin (Nat.succ n) → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
inst✝¹⁸ : Semiring R
inst✝¹⁷ : (i : Fin (Nat.succ n)) → AddCommMonoid (M i)
inst✝¹⁶ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁵ : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹⁴ : AddCommMonoid M₂
inst✝¹³ : AddCommMonoid M₃
inst✝¹² : AddCommMonoid M₄
inst✝¹¹ : (i : Fin (Nat.succ n)) → Module R (M i)
inst✝¹⁰ : (i : ι) → Module R (M₁ i)
inst✝⁹ : (i : ι) → Module R (M₁' i)
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M₃
inst✝⁶ : Module R M₄
inst✝⁵ : (i : Fin (Nat.succ n)) → TopologicalSpace (M i)
inst✝⁴ : (i : ι) → TopologicalSpace (M₁ i)
inst✝³ : (i : ι) → TopologicalSpace (M₁' i)
inst✝² : TopologicalSpace M₂
inst✝¹ : TopologicalSpace M₃
inst✝ : TopologicalSpace M₄
f f' : ContinuousMultilinearMap R M₁ M₂
ι' : Type u_1
e : ι ≃ ι'
x✝¹ : ContinuousMultilinearMap R (fun x => M₂) M₃
x✝ : ι → M₂
⊢ ↑(domDomCongr e.symm (domDomCongr e x✝¹)) x✝ = ↑x✝¹ x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u
ι : Type v
n : ℕ
M : Fin (Nat.succ n) → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
inst✝¹⁸ : Semiring R
inst✝¹⁷ : (i : Fin (Nat.succ n)) → AddCommMonoid (M i)
inst✝¹⁶ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁵ : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹⁴ : AddCommMonoid M₂
inst✝¹³ : AddCommMonoid M₃
inst✝¹² : AddCommMonoid M₄
inst✝¹¹ : (i : Fin (Nat.succ n)) → Module R (M i)
inst✝¹⁰ : (i : ι) → Module R (M₁ i)
inst✝⁹ : (i : ι) → Module R (M₁' i)
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M₃
inst✝⁶ : Module R M₄
inst✝⁵ : (i : Fin (Nat.succ n)) → TopologicalSpace (M i)
inst✝⁴ : (i : ι) → TopologicalSpace (M₁ i)
inst✝³ : (i : ι) → TopologicalSpace (M₁' i)
inst✝² : TopologicalSpace M₂
inst✝¹ : TopologicalSpace M₃
inst✝ : TopologicalSpace M₄
f f' : ContinuousMultilinearMap R M₁ M₂
ι' : Type u_1
e : ι ≃ ι'
x✝¹ : ContinuousMultilinearMap R (fun x => M₂) M₃
x✝ : ι' → M₂
⊢ ↑(domDomCongr e (domDomCongr e.symm x✝¹)) x✝ = ↑x✝¹ x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u
ι : Type v
n : ℕ
M : Fin (Nat.succ n) → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
A : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousMul A
⊢ Continuous (MultilinearMap.mkPiAlgebraFin R n A).toFun
[PROOFSTEP]
change Continuous fun m => (List.ofFn m).prod
[GOAL]
R : Type u
ι : Type v
n : ℕ
M : Fin (Nat.succ n) → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
A : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousMul A
⊢ Continuous fun m => List.prod (List.ofFn m)
[PROOFSTEP]
simp_rw [List.ofFn_eq_map]
[GOAL]
R : Type u
ι : Type v
n : ℕ
M : Fin (Nat.succ n) → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
A : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousMul A
⊢ Continuous fun m => List.prod (List.map m (List.finRange n))
[PROOFSTEP]
exact continuous_list_prod _ fun i _ => continuous_apply _
