Theorem: DiracSeq.continuous (ForML/Dirac.lean)

State before:
b : ℝ
⊢ Continuous (DiracSeq b)
Tactic:
refine Continuous.mul continuous_const ?_
State after:
b : ℝ
⊢ Continuous fun x => rexp (-(b * x) ^ 2)

State before:
b : ℝ
⊢ Continuous fun x => rexp (-(b * x) ^ 2)
Tactic:
refine Continuous.exp ?_
State after:
b : ℝ
⊢ Continuous fun x => -(b * x) ^ 2

State before:
b : ℝ
⊢ Continuous fun x => -(b * x) ^ 2
Tactic:
refine Continuous.neg ?_
State after:
b : ℝ
⊢ Continuous fun x => (b * x) ^ 2

State before:
b : ℝ
⊢ Continuous fun x => (b * x) ^ 2
Tactic:
refine Continuous.pow ?_ 2
State after:
b : ℝ
⊢ Continuous fun x => b * x

State before:
b : ℝ
⊢ Continuous fun x => b * x
Tactic:
refine Continuous.mul continuous_const continuous_id
State after:
no goals