case inl
M✝ : Type ?u.106576
α : Type ?u.106579
β : Type ?u.106582
G₀ : Type ?u.106585
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : GroupWithZero G₀
inst✝⁸ : MulAction G₀ α
inst✝⁷ : ContinuousConstSMul G₀ α
inst✝⁶ : TopologicalSpace β
f : β → α
b : β
c : G₀
s : Set β
𝕜 : Type u_1
M : Type u_2
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : T1Space M
inst✝¹ : Module 𝕜 M
inst✝ : ContinuousConstSMul 𝕜 M
⊢ IsClosedMap fun x => 0 • x

case inr
M✝ : Type ?u.106576
α : Type ?u.106579
β : Type ?u.106582
G₀ : Type ?u.106585
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : GroupWithZero G₀
inst✝⁸ : MulAction G₀ α
inst✝⁷ : ContinuousConstSMul G₀ α
inst✝⁶ : TopologicalSpace β
f : β → α
b : β
c✝ : G₀
s : Set β
𝕜 : Type u_1
M : Type u_2
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : T1Space M
inst✝¹ : Module 𝕜 M
inst✝ : ContinuousConstSMul 𝕜 M
c : 𝕜
hne : c ≠ 0
⊢ IsClosedMap fun x => c • x
M✝ : Type ?u.106576
α : Type ?u.106579
β : Type ?u.106582
G₀ : Type ?u.106585
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : GroupWithZero G₀
inst✝⁸ : MulAction G₀ α
inst✝⁷ : ContinuousConstSMul G₀ α
inst✝⁶ : TopologicalSpace β
f : β → α
b : β
c✝ : G₀
s : Set β
𝕜 : Type u_1
M : Type u_2
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : T1Space M
inst✝¹ : Module 𝕜 M
inst✝ : ContinuousConstSMul 𝕜 M
c : 𝕜
⊢ IsClosedMap fun x => c • x
rcases eq_or_ne c 0 with (rfl | hne)
case inl
M✝ : Type ?u.106576
α : Type ?u.106579
β : Type ?u.106582
G₀ : Type ?u.106585
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : GroupWithZero G₀
inst✝⁸ : MulAction G₀ α
inst✝⁷ : ContinuousConstSMul G₀ α
inst✝⁶ : TopologicalSpace β
f : β → α
b : β
c : G₀
s : Set β
𝕜 : Type u_1
M : Type u_2
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : T1Space M
inst✝¹ : Module 𝕜 M
inst✝ : ContinuousConstSMul 𝕜 M
⊢ IsClosedMap fun x => 0
case inl
M✝ : Type ?u.106576
α : Type ?u.106579
β : Type ?u.106582
G₀ : Type ?u.106585
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : GroupWithZero G₀
inst✝⁸ : MulAction G₀ α
inst✝⁷ : ContinuousConstSMul G₀ α
inst✝⁶ : TopologicalSpace β
f : β → α
b : β
c : G₀
s : Set β
𝕜 : Type u_1
M : Type u_2
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : T1Space M
inst✝¹ : Module 𝕜 M
inst✝ : ContinuousConstSMul 𝕜 M
⊢ IsClosedMap fun x => 0 • x
simp only [zero_smul]
no goals
case inl
M✝ : Type ?u.106576
α : Type ?u.106579
β : Type ?u.106582
G₀ : Type ?u.106585
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : GroupWithZero G₀
inst✝⁸ : MulAction G₀ α
inst✝⁷ : ContinuousConstSMul G₀ α
inst✝⁶ : TopologicalSpace β
f : β → α
b : β
c : G₀
s : Set β
𝕜 : Type u_1
M : Type u_2
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : T1Space M
inst✝¹ : Module 𝕜 M
inst✝ : ContinuousConstSMul 𝕜 M
⊢ IsClosedMap fun x => 0
exact isClosedMap_const
no goals
case inr
M✝ : Type ?u.106576
α : Type ?u.106579
β : Type ?u.106582
G₀ : Type ?u.106585
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : GroupWithZero G₀
inst✝⁸ : MulAction G₀ α
inst✝⁷ : ContinuousConstSMul G₀ α
inst✝⁶ : TopologicalSpace β
f : β → α
b : β
c✝ : G₀
s : Set β
𝕜 : Type u_1
M : Type u_2
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : T1Space M
inst✝¹ : Module 𝕜 M
inst✝ : ContinuousConstSMul 𝕜 M
c : 𝕜
hne : c ≠ 0
⊢ IsClosedMap fun x => c • x
exact (Homeomorph.smulOfNeZero c hne).isClosedMap