Theorem: multibrot_subset_closedBall (Ray/Dynamics/Multibrot/Basic.lean)

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ multibrot d ⊆ closedBall 0 2
Tactic:
intro c m
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
m : c ∈ multibrot d
⊢ c ∈ closedBall 0 2

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
m : c ∈ multibrot d
⊢ c ∈ closedBall 0 2
Tactic:
simp only [mem_closedBall, Complex.dist_eq, sub_zero]
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
m : c ∈ multibrot d
⊢ Complex.abs c ≤ 2

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
m : c ∈ multibrot d
⊢ Complex.abs c ≤ 2
Tactic:
exact multibrot_le_two m
State after:
no goals