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

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsOpen (multibrotExt d)
Tactic:
rw [OnePoint.isOpen_iff_of_mem']
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsCompact (OnePoint.some ⁻¹' multibrotExt d)ᶜ ∧ IsOpen (OnePoint.some ⁻¹' multibrotExt d)

c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∞ ∈ multibrotExt d

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsCompact (OnePoint.some ⁻¹' multibrotExt d)ᶜ ∧ IsOpen (OnePoint.some ⁻¹' multibrotExt d)

c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∞ ∈ multibrotExt d
Tactic:
simp only [coe_preimage_multibrotExt, compl_compl]
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsCompact (multibrot d) ∧ IsOpen (multibrot d)ᶜ

c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∞ ∈ multibrotExt d

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsCompact (multibrot d) ∧ IsOpen (multibrot d)ᶜ

c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∞ ∈ multibrotExt d
Tactic:
use isCompact_multibrot, isCompact_multibrot.isClosed.isOpen_compl
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∞ ∈ multibrotExt d

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∞ ∈ multibrotExt d
Tactic:
exact multibrotExt_inf
State after:
no goals