Theorem: MvPowerSeries.continuous_trunc' (DividedPowers/ForMathlib/RingTheory/MvPowerSeries/Trunc.lean)

State before:
σ : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
n✝ : σ →₀ ℕ
inst✝² inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
n : σ →₀ ℕ
⊢ Continuous ⇑(trunc' R n)
Tactic:
rw [continuous_induced_rng]
State after:
σ : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
n✝ : σ →₀ ℕ
inst✝² inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
n : σ →₀ ℕ
⊢ Continuous (MvPolynomial.toMvPowerSeries ∘ ⇑(trunc' R n))

State before:
σ : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
n✝ : σ →₀ ℕ
inst✝² inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
n : σ →₀ ℕ
⊢ Continuous (MvPolynomial.toMvPowerSeries ∘ ⇑(trunc' R n))
Tactic:
apply continuous_pi
State after:
case h
σ : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
n✝ : σ →₀ ℕ
inst✝² inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
n : σ →₀ ℕ
⊢ ∀ (i : σ →₀ ℕ), Continuous fun a => (MvPolynomial.toMvPowerSeries ∘ ⇑(trunc' R n)) a i

State before:
case h
σ : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
n✝ : σ →₀ ℕ
inst✝² inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
n : σ →₀ ℕ
⊢ ∀ (i : σ →₀ ℕ), Continuous fun a => (MvPolynomial.toMvPowerSeries ∘ ⇑(trunc' R n)) a i
Tactic:
intro m
State after:
case h
σ : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
n✝ : σ →₀ ℕ
inst✝² inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
n m : σ →₀ ℕ
⊢ Continuous fun a => (MvPolynomial.toMvPowerSeries ∘ ⇑(trunc' R n)) a m

State before:
case h
σ : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
n✝ : σ →₀ ℕ
inst✝² inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
n m : σ →₀ ℕ
⊢ Continuous fun a => (MvPolynomial.toMvPowerSeries ∘ ⇑(trunc' R n)) a m
Tactic:
simp only [Function.comp_apply, MvPolynomial.coe_def, coeff_trunc']
State after:
case h
σ : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
n✝ : σ →₀ ℕ
inst✝² inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
n m : σ →₀ ℕ
⊢ Continuous fun a => if m ≤ n then (coeff R m) a else 0

State before:
case h
σ : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
n✝ : σ →₀ ℕ
inst✝² inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
n m : σ →₀ ℕ
⊢ Continuous fun a => if m ≤ n then (coeff R m) a else 0
Tactic:
split_ifs with h
State after:
case pos
σ : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
n✝ : σ →₀ ℕ
inst✝² inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
n m : σ →₀ ℕ
h : m ≤ n
⊢ Continuous fun a => (coeff R m) a

case neg
σ : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
n✝ : σ →₀ ℕ
inst✝² inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
n m : σ →₀ ℕ
h : ¬m ≤ n
⊢ Continuous fun a => 0

State before:
case pos
σ : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
n✝ : σ →₀ ℕ
inst✝² inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
n m : σ →₀ ℕ
h : m ≤ n
⊢ Continuous fun a => (coeff R m) a
Tactic:
exact continuous_apply m
State after:
no goals

State before:
case neg
σ : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
n✝ : σ →₀ ℕ
inst✝² inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
n m : σ →₀ ℕ
h : ¬m ≤ n
⊢ Continuous fun a => 0
Tactic:
exact continuous_const
State after:
no goals