[GOAL]
M : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SMul M α
inst✝³ : ContinuousConstSMul M α
inst✝² : TopologicalSpace β
f : β → M
g : β → α
b : β
s : Set β
inst✝¹ : SMul Mᵐᵒᵖ α
inst✝ : IsCentralScalar M α
c : M
⊢ Continuous fun x => MulOpposite.op c • x
[PROOFSTEP]
simpa only [op_smul_eq_smul] using continuous_const_smul c
[GOAL]
M : Type u_1
α✝ : Type u_2
β✝ : Type u_3
inst✝⁹ : TopologicalSpace α✝
inst✝⁸ : Monoid M
inst✝⁷ : MulAction M α✝
inst✝⁶ : ContinuousConstSMul M α✝
N : Type u_4
inst✝⁵ : Monoid N
α : Type u_5
β : Type u_6
inst✝⁴ : MulAction M α
inst✝³ : MulAction N β
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : ContinuousConstSMul N β
σ : M → N
⊢ IsClosed {f | ∀ (c : M) (x : α), f (c • x) = σ c • f x}
[PROOFSTEP]
simp only [Set.setOf_forall]
[GOAL]
M : Type u_1
α✝ : Type u_2
β✝ : Type u_3
inst✝⁹ : TopologicalSpace α✝
inst✝⁸ : Monoid M
inst✝⁷ : MulAction M α✝
inst✝⁶ : ContinuousConstSMul M α✝
N : Type u_4
inst✝⁵ : Monoid N
α : Type u_5
β : Type u_6
inst✝⁴ : MulAction M α
inst✝³ : MulAction N β
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : ContinuousConstSMul N β
σ : M → N
⊢ IsClosed (⋂ (i : M) (i_1 : α), {x | x (i • i_1) = σ i • x i_1})
[PROOFSTEP]
exact
  isClosed_iInter fun c => isClosed_iInter fun x => isClosed_eq (continuous_apply _) ((continuous_apply _).const_smul _)
[GOAL]
M : Type u_1
α : Type u_2
β : Type u_3
G : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : ContinuousConstSMul G α
f : β → α
l : Filter β
a : α
c : G
h : Tendsto (fun x => c • f x) l (𝓝 (c • a))
⊢ Tendsto f l (𝓝 a)
[PROOFSTEP]
simpa only [inv_smul_smul] using h.const_smul c⁻¹
[GOAL]
M : Type u_1
α : Type u_2
β : Type u_3
G : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : ContinuousConstSMul G α
inst✝ : TopologicalSpace β
f : β → α
b : β
s : Set β
c : G
⊢ (Continuous fun x => c • f x) ↔ Continuous f
[PROOFSTEP]
simp only [continuous_iff_continuousAt, continuousAt_const_smul_iff]
[GOAL]
M : Type u_1
α : Type u_2
β : Type u_3
G : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : ContinuousConstSMul G α
inst✝ : TopologicalSpace β
f : β → α
b : β
s✝ : Set β
c : G
s : Set α
hs : Dense s
⊢ Dense (c • s)
[PROOFSTEP]
rw [dense_iff_closure_eq] at hs ⊢
[GOAL]
M : Type u_1
α : Type u_2
β : Type u_3
G : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : ContinuousConstSMul G α
inst✝ : TopologicalSpace β
f : β → α
b : β
s✝ : Set β
c : G
s : Set α
hs : closure s = univ
⊢ closure (c • s) = univ
[PROOFSTEP]
rw [closure_smul, hs, smul_set_univ]
[GOAL]
M : Type u_1
α : Type u_2
β : Type u_3
G₀ : Type u_4
inst✝⁹ : TopologicalSpace α
inst✝⁸ : GroupWithZero G₀
inst✝⁷ : MulAction G₀ α
inst✝⁶ : ContinuousConstSMul G₀ α
inst✝⁵ : TopologicalSpace β
f : β → α
b : β
c✝ : G₀
s✝ : Set β
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
c : G₀
s : Set E
⊢ closure (c • s) = c • closure s
[PROOFSTEP]
rcases eq_or_ne c 0 with (rfl | hc)
[GOAL]
case inl
M : Type u_1
α : Type u_2
β : Type u_3
G₀ : Type u_4
inst✝⁹ : TopologicalSpace α
inst✝⁸ : GroupWithZero G₀
inst✝⁷ : MulAction G₀ α
inst✝⁶ : ContinuousConstSMul G₀ α
inst✝⁵ : TopologicalSpace β
f : β → α
b : β
c : G₀
s✝ : Set β
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
s : Set E
⊢ closure (0 • s) = 0 • closure s
[PROOFSTEP]
rcases eq_empty_or_nonempty s with (rfl | hs)
[GOAL]
case inl.inl
M : Type u_1
α : Type u_2
β : Type u_3
G₀ : Type u_4
inst✝⁹ : TopologicalSpace α
inst✝⁸ : GroupWithZero G₀
inst✝⁷ : MulAction G₀ α
inst✝⁶ : ContinuousConstSMul G₀ α
inst✝⁵ : TopologicalSpace β
f : β → α
b : β
c : G₀
s : Set β
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
⊢ closure (0 • ∅) = 0 • closure ∅
[PROOFSTEP]
simp
[GOAL]
case inl.inr
M : Type u_1
α : Type u_2
β : Type u_3
G₀ : Type u_4
inst✝⁹ : TopologicalSpace α
inst✝⁸ : GroupWithZero G₀
inst✝⁷ : MulAction G₀ α
inst✝⁶ : ContinuousConstSMul G₀ α
inst✝⁵ : TopologicalSpace β
f : β → α
b : β
c : G₀
s✝ : Set β
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
s : Set E
hs : Set.Nonempty s
⊢ closure (0 • s) = 0 • closure s
[PROOFSTEP]
rw [zero_smul_set hs, zero_smul_set hs.closure]
[GOAL]
case inl.inr
M : Type u_1
α : Type u_2
β : Type u_3
G₀ : Type u_4
inst✝⁹ : TopologicalSpace α
inst✝⁸ : GroupWithZero G₀
inst✝⁷ : MulAction G₀ α
inst✝⁶ : ContinuousConstSMul G₀ α
inst✝⁵ : TopologicalSpace β
f : β → α
b : β
c : G₀
s✝ : Set β
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
s : Set E
hs : Set.Nonempty s
⊢ closure 0 = 0
[PROOFSTEP]
exact closure_singleton
[GOAL]
case inr
M : Type u_1
α : Type u_2
β : Type u_3
G₀ : Type u_4
inst✝⁹ : TopologicalSpace α
inst✝⁸ : GroupWithZero G₀
inst✝⁷ : MulAction G₀ α
inst✝⁶ : ContinuousConstSMul G₀ α
inst✝⁵ : TopologicalSpace β
f : β → α
b : β
c✝ : G₀
s✝ : Set β
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
c : G₀
s : Set E
hc : c ≠ 0
⊢ closure (c • s) = c • closure s
[PROOFSTEP]
exact ((Homeomorph.smulOfNeZero c hc).image_closure s).symm
[GOAL]
M✝ : Type u_1
α : Type u_2
β : Type u_3
G₀ : Type u_4
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : GroupWithZero G₀
inst✝⁸ : MulAction G₀ α
inst✝⁷ : ContinuousConstSMul G₀ α
inst✝⁶ : TopologicalSpace β
f : β → α
b : β
c✝ : G₀
s : Set β
𝕜 : Type u_5
M : Type u_6
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : T1Space M
inst✝¹ : Module 𝕜 M
inst✝ : ContinuousConstSMul 𝕜 M
c : 𝕜
⊢ IsClosedMap fun x => c • x
[PROOFSTEP]
rcases eq_or_ne c 0 with (rfl | hne)
[GOAL]
case inl
M✝ : Type u_1
α : Type u_2
β : Type u_3
G₀ : Type u_4
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : GroupWithZero G₀
inst✝⁸ : MulAction G₀ α
inst✝⁷ : ContinuousConstSMul G₀ α
inst✝⁶ : TopologicalSpace β
f : β → α
b : β
c : G₀
s : Set β
𝕜 : Type u_5
M : Type u_6
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : T1Space M
inst✝¹ : Module 𝕜 M
inst✝ : ContinuousConstSMul 𝕜 M
⊢ IsClosedMap fun x => 0 • x
[PROOFSTEP]
simp only [zero_smul]
[GOAL]
case inl
M✝ : Type u_1
α : Type u_2
β : Type u_3
G₀ : Type u_4
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : GroupWithZero G₀
inst✝⁸ : MulAction G₀ α
inst✝⁷ : ContinuousConstSMul G₀ α
inst✝⁶ : TopologicalSpace β
f : β → α
b : β
c : G₀
s : Set β
𝕜 : Type u_5
M : Type u_6
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : T1Space M
inst✝¹ : Module 𝕜 M
inst✝ : ContinuousConstSMul 𝕜 M
⊢ IsClosedMap fun x => 0
[PROOFSTEP]
exact isClosedMap_const
[GOAL]
case inr
M✝ : Type u_1
α : Type u_2
β : Type u_3
G₀ : Type u_4
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : GroupWithZero G₀
inst✝⁸ : MulAction G₀ α
inst✝⁷ : ContinuousConstSMul G₀ α
inst✝⁶ : TopologicalSpace β
f : β → α
b : β
c✝ : G₀
s : Set β
𝕜 : Type u_5
M : Type u_6
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
[PROOFSTEP]
exact (Homeomorph.smulOfNeZero c hne).isClosedMap
[GOAL]
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝³ : Group Γ
T : Type u_5
inst✝² : TopologicalSpace T
inst✝¹ : MulAction Γ T
inst✝ : ContinuousConstSMul Γ T
U : Set T
hU : IsOpen U
⊢ IsOpen (Quotient.mk' '' U)
[PROOFSTEP]
rw [isOpen_coinduced, MulAction.quotient_preimage_image_eq_union_mul U]
[GOAL]
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝³ : Group Γ
T : Type u_5
inst✝² : TopologicalSpace T
inst✝¹ : MulAction Γ T
inst✝ : ContinuousConstSMul Γ T
U : Set T
hU : IsOpen U
⊢ IsOpen (⋃ (g : Γ), (fun x x_1 => x • x_1) g '' U)
[PROOFSTEP]
exact isOpen_iUnion fun γ => isOpenMap_smul γ U hU
[GOAL]
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
⊢ T2Space (Quotient (MulAction.orbitRel Γ T))
[PROOFSTEP]
letI := MulAction.orbitRel Γ T
[GOAL]
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
⊢ T2Space (Quotient (MulAction.orbitRel Γ T))
[PROOFSTEP]
set Q := Quotient (MulAction.orbitRel Γ T)
[GOAL]
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
⊢ T2Space (Quotient (MulAction.orbitRel Γ T))
[PROOFSTEP]
rw [t2Space_iff_nhds]
[GOAL]
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
⊢ ∀ {x y : Quotient (MulAction.orbitRel Γ T)}, x ≠ y → ∃ U, U ∈ 𝓝 x ∧ ∃ V, V ∈ 𝓝 y ∧ Disjoint U V
[PROOFSTEP]
let f : T → Q := Quotient.mk'
[GOAL]
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
⊢ ∀ {x y : Quotient (MulAction.orbitRel Γ T)}, x ≠ y → ∃ U, U ∈ 𝓝 x ∧ ∃ V, V ∈ 𝓝 y ∧ Disjoint U V
[PROOFSTEP]
have f_op : IsOpenMap f := isOpenMap_quotient_mk'_mul
[GOAL]
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
⊢ ∀ {x y : Quotient (MulAction.orbitRel Γ T)}, x ≠ y → ∃ U, U ∈ 𝓝 x ∧ ∃ V, V ∈ 𝓝 y ∧ Disjoint U V
[PROOFSTEP]
rintro ⟨x₀⟩ ⟨y₀⟩ (hxy : f x₀ ≠ f y₀)
[GOAL]
case mk.mk
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
x✝ : Quotient (MulAction.orbitRel Γ T)
x₀ : T
y✝ : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
⊢ ∃ U, U ∈ 𝓝 (Quot.mk Setoid.r x₀) ∧ ∃ V, V ∈ 𝓝 (Quot.mk Setoid.r y₀) ∧ Disjoint U V
[PROOFSTEP]
show ∃ U ∈ 𝓝 (f x₀), ∃ V ∈ 𝓝 (f y₀), _
[GOAL]
case mk.mk
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
x✝ : Quotient (MulAction.orbitRel Γ T)
x₀ : T
y✝ : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
⊢ ∃ U, U ∈ 𝓝 (f x₀) ∧ ∃ V, V ∈ 𝓝 (f y₀) ∧ Disjoint U V
[PROOFSTEP]
have hγx₀y₀ : ∀ γ : Γ, γ • x₀ ≠ y₀ := not_exists.mp (mt Quotient.sound hxy.symm : _)
[GOAL]
case mk.mk
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
x✝ : Quotient (MulAction.orbitRel Γ T)
x₀ : T
y✝ : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
⊢ ∃ U, U ∈ 𝓝 (f x₀) ∧ ∃ V, V ∈ 𝓝 (f y₀) ∧ Disjoint U V
[PROOFSTEP]
obtain ⟨K₀, hK₀, K₀_in⟩ := exists_compact_mem_nhds x₀
[GOAL]
case mk.mk.intro.intro
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
x✝ : Quotient (MulAction.orbitRel Γ T)
x₀ : T
y✝ : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
⊢ ∃ U, U ∈ 𝓝 (f x₀) ∧ ∃ V, V ∈ 𝓝 (f y₀) ∧ Disjoint U V
[PROOFSTEP]
obtain ⟨L₀, hL₀, L₀_in⟩ := exists_compact_mem_nhds y₀
[GOAL]
case mk.mk.intro.intro.intro.intro
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
x✝ : Quotient (MulAction.orbitRel Γ T)
x₀ : T
y✝ : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
L₀ : Set T
hL₀ : IsCompact L₀
L₀_in : L₀ ∈ 𝓝 y₀
⊢ ∃ U, U ∈ 𝓝 (f x₀) ∧ ∃ V, V ∈ 𝓝 (f y₀) ∧ Disjoint U V
[PROOFSTEP]
let bad_Γ_set := {γ : Γ | (γ • ·) '' K₀ ∩ L₀ ≠ ∅}
[GOAL]
case mk.mk.intro.intro.intro.intro
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
x✝ : Quotient (MulAction.orbitRel Γ T)
x₀ : T
y✝ : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
L₀ : Set T
hL₀ : IsCompact L₀
L₀_in : L₀ ∈ 𝓝 y₀
bad_Γ_set : Set Γ := {γ | (fun x => γ • x) '' K₀ ∩ L₀ ≠ ∅}
⊢ ∃ U, U ∈ 𝓝 (f x₀) ∧ ∃ V, V ∈ 𝓝 (f y₀) ∧ Disjoint U V
[PROOFSTEP]
have bad_Γ_finite : bad_Γ_set.Finite := finite_disjoint_inter_image (Γ := Γ) hK₀ hL₀
[GOAL]
case mk.mk.intro.intro.intro.intro
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
x✝ : Quotient (MulAction.orbitRel Γ T)
x₀ : T
y✝ : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
L₀ : Set T
hL₀ : IsCompact L₀
L₀_in : L₀ ∈ 𝓝 y₀
bad_Γ_set : Set Γ := {γ | (fun x => γ • x) '' K₀ ∩ L₀ ≠ ∅}
bad_Γ_finite : Set.Finite bad_Γ_set
⊢ ∃ U, U ∈ 𝓝 (f x₀) ∧ ∃ V, V ∈ 𝓝 (f y₀) ∧ Disjoint U V
[PROOFSTEP]
choose u v hu hv u_v_disjoint using fun γ => t2_separation_nhds (hγx₀y₀ γ)
[GOAL]
case mk.mk.intro.intro.intro.intro
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
x✝ : Quotient (MulAction.orbitRel Γ T)
x₀ : T
y✝ : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
L₀ : Set T
hL₀ : IsCompact L₀
L₀_in : L₀ ∈ 𝓝 y₀
bad_Γ_set : Set Γ := {γ | (fun x => γ • x) '' K₀ ∩ L₀ ≠ ∅}
bad_Γ_finite : Set.Finite bad_Γ_set
u v : Γ → Set T
hu : ∀ (γ : Γ), u γ ∈ 𝓝 (γ • x₀)
hv : ∀ (γ : Γ), v γ ∈ 𝓝 y₀
u_v_disjoint : ∀ (γ : Γ), Disjoint (u γ) (v γ)
⊢ ∃ U, U ∈ 𝓝 (f x₀) ∧ ∃ V, V ∈ 𝓝 (f y₀) ∧ Disjoint U V
[PROOFSTEP]
let U₀₀ := ⋂ γ ∈ bad_Γ_set, (γ • ·) ⁻¹' u γ
[GOAL]
case mk.mk.intro.intro.intro.intro
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
x✝ : Quotient (MulAction.orbitRel Γ T)
x₀ : T
y✝ : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
L₀ : Set T
hL₀ : IsCompact L₀
L₀_in : L₀ ∈ 𝓝 y₀
bad_Γ_set : Set Γ := {γ | (fun x => γ • x) '' K₀ ∩ L₀ ≠ ∅}
bad_Γ_finite : Set.Finite bad_Γ_set
u v : Γ → Set T
hu : ∀ (γ : Γ), u γ ∈ 𝓝 (γ • x₀)
hv : ∀ (γ : Γ), v γ ∈ 𝓝 y₀
u_v_disjoint : ∀ (γ : Γ), Disjoint (u γ) (v γ)
U₀₀ : Set T := ⋂ (γ : Γ) (_ : γ ∈ bad_Γ_set), (fun x => γ • x) ⁻¹' u γ
⊢ ∃ U, U ∈ 𝓝 (f x₀) ∧ ∃ V, V ∈ 𝓝 (f y₀) ∧ Disjoint U V
[PROOFSTEP]
let U₀ := U₀₀ ∩ K₀
[GOAL]
case mk.mk.intro.intro.intro.intro
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
x✝ : Quotient (MulAction.orbitRel Γ T)
x₀ : T
y✝ : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
L₀ : Set T
hL₀ : IsCompact L₀
L₀_in : L₀ ∈ 𝓝 y₀
bad_Γ_set : Set Γ := {γ | (fun x => γ • x) '' K₀ ∩ L₀ ≠ ∅}
bad_Γ_finite : Set.Finite bad_Γ_set
u v : Γ → Set T
hu : ∀ (γ : Γ), u γ ∈ 𝓝 (γ • x₀)
hv : ∀ (γ : Γ), v γ ∈ 𝓝 y₀
u_v_disjoint : ∀ (γ : Γ), Disjoint (u γ) (v γ)
U₀₀ : Set T := ⋂ (γ : Γ) (_ : γ ∈ bad_Γ_set), (fun x => γ • x) ⁻¹' u γ
U₀ : Set T := U₀₀ ∩ K₀
⊢ ∃ U, U ∈ 𝓝 (f x₀) ∧ ∃ V, V ∈ 𝓝 (f y₀) ∧ Disjoint U V
[PROOFSTEP]
let V₀₀ := ⋂ γ ∈ bad_Γ_set, v γ
[GOAL]
case mk.mk.intro.intro.intro.intro
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
x✝ : Quotient (MulAction.orbitRel Γ T)
x₀ : T
y✝ : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
L₀ : Set T
hL₀ : IsCompact L₀
L₀_in : L₀ ∈ 𝓝 y₀
bad_Γ_set : Set Γ := {γ | (fun x => γ • x) '' K₀ ∩ L₀ ≠ ∅}
bad_Γ_finite : Set.Finite bad_Γ_set
u v : Γ → Set T
hu : ∀ (γ : Γ), u γ ∈ 𝓝 (γ • x₀)
hv : ∀ (γ : Γ), v γ ∈ 𝓝 y₀
u_v_disjoint : ∀ (γ : Γ), Disjoint (u γ) (v γ)
U₀₀ : Set T := ⋂ (γ : Γ) (_ : γ ∈ bad_Γ_set), (fun x => γ • x) ⁻¹' u γ
U₀ : Set T := U₀₀ ∩ K₀
V₀₀ : Set T := ⋂ (γ : Γ) (_ : γ ∈ bad_Γ_set), v γ
⊢ ∃ U, U ∈ 𝓝 (f x₀) ∧ ∃ V, V ∈ 𝓝 (f y₀) ∧ Disjoint U V
[PROOFSTEP]
let V₀ := V₀₀ ∩ L₀
[GOAL]
case mk.mk.intro.intro.intro.intro
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
x✝ : Quotient (MulAction.orbitRel Γ T)
x₀ : T
y✝ : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
L₀ : Set T
hL₀ : IsCompact L₀
L₀_in : L₀ ∈ 𝓝 y₀
bad_Γ_set : Set Γ := {γ | (fun x => γ • x) '' K₀ ∩ L₀ ≠ ∅}
bad_Γ_finite : Set.Finite bad_Γ_set
u v : Γ → Set T
hu : ∀ (γ : Γ), u γ ∈ 𝓝 (γ • x₀)
hv : ∀ (γ : Γ), v γ ∈ 𝓝 y₀
u_v_disjoint : ∀ (γ : Γ), Disjoint (u γ) (v γ)
U₀₀ : Set T := ⋂ (γ : Γ) (_ : γ ∈ bad_Γ_set), (fun x => γ • x) ⁻¹' u γ
U₀ : Set T := U₀₀ ∩ K₀
V₀₀ : Set T := ⋂ (γ : Γ) (_ : γ ∈ bad_Γ_set), v γ
V₀ : Set T := V₀₀ ∩ L₀
⊢ ∃ U, U ∈ 𝓝 (f x₀) ∧ ∃ V, V ∈ 𝓝 (f y₀) ∧ Disjoint U V
[PROOFSTEP]
have U_nhds : f '' U₀ ∈ 𝓝 (f x₀) :=
  by
  refine f_op.image_mem_nhds (inter_mem ((biInter_mem bad_Γ_finite).mpr fun γ _ => ?_) K₀_in)
  exact (continuous_const_smul _).continuousAt (hu γ)
[GOAL]
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
x✝ : Quotient (MulAction.orbitRel Γ T)
x₀ : T
y✝ : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
L₀ : Set T
hL₀ : IsCompact L₀
L₀_in : L₀ ∈ 𝓝 y₀
bad_Γ_set : Set Γ := {γ | (fun x => γ • x) '' K₀ ∩ L₀ ≠ ∅}
bad_Γ_finite : Set.Finite bad_Γ_set
u v : Γ → Set T
hu : ∀ (γ : Γ), u γ ∈ 𝓝 (γ • x₀)
hv : ∀ (γ : Γ), v γ ∈ 𝓝 y₀
u_v_disjoint : ∀ (γ : Γ), Disjoint (u γ) (v γ)
U₀₀ : Set T := ⋂ (γ : Γ) (_ : γ ∈ bad_Γ_set), (fun x => γ • x) ⁻¹' u γ
U₀ : Set T := U₀₀ ∩ K₀
V₀₀ : Set T := ⋂ (γ : Γ) (_ : γ ∈ bad_Γ_set), v γ
V₀ : Set T := V₀₀ ∩ L₀
⊢ f '' U₀ ∈ 𝓝 (f x₀)
[PROOFSTEP]
refine f_op.image_mem_nhds (inter_mem ((biInter_mem bad_Γ_finite).mpr fun γ _ => ?_) K₀_in)
[GOAL]
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
x✝¹ : Quotient (MulAction.orbitRel Γ T)
x₀ : T
y✝ : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
L₀ : Set T
hL₀ : IsCompact L₀
L₀_in : L₀ ∈ 𝓝 y₀
bad_Γ_set : Set Γ := {γ | (fun x => γ • x) '' K₀ ∩ L₀ ≠ ∅}
bad_Γ_finite : Set.Finite bad_Γ_set
u v : Γ → Set T
hu : ∀ (γ : Γ), u γ ∈ 𝓝 (γ • x₀)
hv : ∀ (γ : Γ), v γ ∈ 𝓝 y₀
u_v_disjoint : ∀ (γ : Γ), Disjoint (u γ) (v γ)
U₀₀ : Set T := ⋂ (γ : Γ) (_ : γ ∈ bad_Γ_set), (fun x => γ • x) ⁻¹' u γ
U₀ : Set T := U₀₀ ∩ K₀
V₀₀ : Set T := ⋂ (γ : Γ) (_ : γ ∈ bad_Γ_set), v γ
V₀ : Set T := V₀₀ ∩ L₀
γ : Γ
x✝ : γ ∈ bad_Γ_set
⊢ (fun x => γ • x) ⁻¹' u γ ∈ 𝓝 x₀
[PROOFSTEP]
exact (continuous_const_smul _).continuousAt (hu γ)
[GOAL]
case mk.mk.intro.intro.intro.intro
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
x✝ : Quotient (MulAction.orbitRel Γ T)
x₀ : T
y✝ : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
L₀ : Set T
hL₀ : IsCompact L₀
L₀_in : L₀ ∈ 𝓝 y₀
bad_Γ_set : Set Γ := {γ | (fun x => γ • x) '' K₀ ∩ L₀ ≠ ∅}
bad_Γ_finite : Set.Finite bad_Γ_set
u v : Γ → Set T
hu : ∀ (γ : Γ), u γ ∈ 𝓝 (γ • x₀)
hv : ∀ (γ : Γ), v γ ∈ 𝓝 y₀
u_v_disjoint : ∀ (γ : Γ), Disjoint (u γ) (v γ)
U₀₀ : Set T := ⋂ (γ : Γ) (_ : γ ∈ bad_Γ_set), (fun x => γ • x) ⁻¹' u γ
U₀ : Set T := U₀₀ ∩ K₀
V₀₀ : Set T := ⋂ (γ : Γ) (_ : γ ∈ bad_Γ_set), v γ
V₀ : Set T := V₀₀ ∩ L₀
U_nhds : f '' U₀ ∈ 𝓝 (f x₀)
⊢ ∃ U, U ∈ 𝓝 (f x₀) ∧ ∃ V, V ∈ 𝓝 (f y₀) ∧ Disjoint U V
[PROOFSTEP]
have V_nhds : f '' V₀ ∈ 𝓝 (f y₀) :=
  f_op.image_mem_nhds (inter_mem ((biInter_mem bad_Γ_finite).mpr fun γ _ => hv γ) L₀_in)
[GOAL]
case mk.mk.intro.intro.intro.intro
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
x✝ : Quotient (MulAction.orbitRel Γ T)
x₀ : T
y✝ : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
L₀ : Set T
hL₀ : IsCompact L₀
L₀_in : L₀ ∈ 𝓝 y₀
bad_Γ_set : Set Γ := {γ | (fun x => γ • x) '' K₀ ∩ L₀ ≠ ∅}
bad_Γ_finite : Set.Finite bad_Γ_set
u v : Γ → Set T
hu : ∀ (γ : Γ), u γ ∈ 𝓝 (γ • x₀)
hv : ∀ (γ : Γ), v γ ∈ 𝓝 y₀
u_v_disjoint : ∀ (γ : Γ), Disjoint (u γ) (v γ)
U₀₀ : Set T := ⋂ (γ : Γ) (_ : γ ∈ bad_Γ_set), (fun x => γ • x) ⁻¹' u γ
U₀ : Set T := U₀₀ ∩ K₀
V₀₀ : Set T := ⋂ (γ : Γ) (_ : γ ∈ bad_Γ_set), v γ
V₀ : Set T := V₀₀ ∩ L₀
U_nhds : f '' U₀ ∈ 𝓝 (f x₀)
V_nhds : f '' V₀ ∈ 𝓝 (f y₀)
⊢ ∃ U, U ∈ 𝓝 (f x₀) ∧ ∃ V, V ∈ 𝓝 (f y₀) ∧ Disjoint U V
[PROOFSTEP]
refine' ⟨f '' U₀, U_nhds, f '' V₀, V_nhds, MulAction.disjoint_image_image_iff.2 _⟩
[GOAL]
case mk.mk.intro.intro.intro.intro
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
x✝ : Quotient (MulAction.orbitRel Γ T)
x₀ : T
y✝ : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
L₀ : Set T
hL₀ : IsCompact L₀
L₀_in : L₀ ∈ 𝓝 y₀
bad_Γ_set : Set Γ := {γ | (fun x => γ • x) '' K₀ ∩ L₀ ≠ ∅}
bad_Γ_finite : Set.Finite bad_Γ_set
u v : Γ → Set T
hu : ∀ (γ : Γ), u γ ∈ 𝓝 (γ • x₀)
hv : ∀ (γ : Γ), v γ ∈ 𝓝 y₀
u_v_disjoint : ∀ (γ : Γ), Disjoint (u γ) (v γ)
U₀₀ : Set T := ⋂ (γ : Γ) (_ : γ ∈ bad_Γ_set), (fun x => γ • x) ⁻¹' u γ
U₀ : Set T := U₀₀ ∩ K₀
V₀₀ : Set T := ⋂ (γ : Γ) (_ : γ ∈ bad_Γ_set), v γ
V₀ : Set T := V₀₀ ∩ L₀
U_nhds : f '' U₀ ∈ 𝓝 (f x₀)
V_nhds : f '' V₀ ∈ 𝓝 (f y₀)
⊢ ∀ (x : T), x ∈ U₀ → ∀ (g : Γ), ¬g • x ∈ V₀
[PROOFSTEP]
rintro x ⟨x_in_U₀₀, x_in_K₀⟩ γ
[GOAL]
case mk.mk.intro.intro.intro.intro.intro
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
x✝ : Quotient (MulAction.orbitRel Γ T)
x₀ : T
y✝ : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
L₀ : Set T
hL₀ : IsCompact L₀
L₀_in : L₀ ∈ 𝓝 y₀
bad_Γ_set : Set Γ := {γ | (fun x => γ • x) '' K₀ ∩ L₀ ≠ ∅}
bad_Γ_finite : Set.Finite bad_Γ_set
u v : Γ → Set T
hu : ∀ (γ : Γ), u γ ∈ 𝓝 (γ • x₀)
hv : ∀ (γ : Γ), v γ ∈ 𝓝 y₀
u_v_disjoint : ∀ (γ : Γ), Disjoint (u γ) (v γ)
U₀₀ : Set T := ⋂ (γ : Γ) (_ : γ ∈ bad_Γ_set), (fun x => γ • x) ⁻¹' u γ
U₀ : Set T := U₀₀ ∩ K₀
V₀₀ : Set T := ⋂ (γ : Γ) (_ : γ ∈ bad_Γ_set), v γ
V₀ : Set T := V₀₀ ∩ L₀
U_nhds : f '' U₀ ∈ 𝓝 (f x₀)
V_nhds : f '' V₀ ∈ 𝓝 (f y₀)
x : T
x_in_U₀₀ : x ∈ U₀₀
x_in_K₀ : x ∈ K₀
γ : Γ
⊢ ¬γ • x ∈ V₀
[PROOFSTEP]
by_cases H : γ ∈ bad_Γ_set
[GOAL]
case pos
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
x✝ : Quotient (MulAction.orbitRel Γ T)
x₀ : T
y✝ : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
L₀ : Set T
hL₀ : IsCompact L₀
L₀_in : L₀ ∈ 𝓝 y₀
bad_Γ_set : Set Γ := {γ | (fun x => γ • x) '' K₀ ∩ L₀ ≠ ∅}
bad_Γ_finite : Set.Finite bad_Γ_set
u v : Γ → Set T
hu : ∀ (γ : Γ), u γ ∈ 𝓝 (γ • x₀)
hv : ∀ (γ : Γ), v γ ∈ 𝓝 y₀
u_v_disjoint : ∀ (γ : Γ), Disjoint (u γ) (v γ)
U₀₀ : Set T := ⋂ (γ : Γ) (_ : γ ∈ bad_Γ_set), (fun x => γ • x) ⁻¹' u γ
U₀ : Set T := U₀₀ ∩ K₀
V₀₀ : Set T := ⋂ (γ : Γ) (_ : γ ∈ bad_Γ_set), v γ
V₀ : Set T := V₀₀ ∩ L₀
U_nhds : f '' U₀ ∈ 𝓝 (f x₀)
V_nhds : f '' V₀ ∈ 𝓝 (f y₀)
x : T
x_in_U₀₀ : x ∈ U₀₀
x_in_K₀ : x ∈ K₀
γ : Γ
H : γ ∈ bad_Γ_set
⊢ ¬γ • x ∈ V₀
[PROOFSTEP]
exact fun h => (u_v_disjoint γ).le_bot ⟨mem_iInter₂.mp x_in_U₀₀ γ H, mem_iInter₂.mp h.1 γ H⟩
[GOAL]
case neg
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
x✝ : Quotient (MulAction.orbitRel Γ T)
x₀ : T
y✝ : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
L₀ : Set T
hL₀ : IsCompact L₀
L₀_in : L₀ ∈ 𝓝 y₀
bad_Γ_set : Set Γ := {γ | (fun x => γ • x) '' K₀ ∩ L₀ ≠ ∅}
bad_Γ_finite : Set.Finite bad_Γ_set
u v : Γ → Set T
hu : ∀ (γ : Γ), u γ ∈ 𝓝 (γ • x₀)
hv : ∀ (γ : Γ), v γ ∈ 𝓝 y₀
u_v_disjoint : ∀ (γ : Γ), Disjoint (u γ) (v γ)
U₀₀ : Set T := ⋂ (γ : Γ) (_ : γ ∈ bad_Γ_set), (fun x => γ • x) ⁻¹' u γ
U₀ : Set T := U₀₀ ∩ K₀
V₀₀ : Set T := ⋂ (γ : Γ) (_ : γ ∈ bad_Γ_set), v γ
V₀ : Set T := V₀₀ ∩ L₀
U_nhds : f '' U₀ ∈ 𝓝 (f x₀)
V_nhds : f '' V₀ ∈ 𝓝 (f y₀)
x : T
x_in_U₀₀ : x ∈ U₀₀
x_in_K₀ : x ∈ K₀
γ : Γ
H : ¬γ ∈ bad_Γ_set
⊢ ¬γ • x ∈ V₀
[PROOFSTEP]
rintro ⟨-, h'⟩
[GOAL]
case neg.intro
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
x✝ : Quotient (MulAction.orbitRel Γ T)
x₀ : T
y✝ : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
L₀ : Set T
hL₀ : IsCompact L₀
L₀_in : L₀ ∈ 𝓝 y₀
bad_Γ_set : Set Γ := {γ | (fun x => γ • x) '' K₀ ∩ L₀ ≠ ∅}
bad_Γ_finite : Set.Finite bad_Γ_set
u v : Γ → Set T
hu : ∀ (γ : Γ), u γ ∈ 𝓝 (γ • x₀)
hv : ∀ (γ : Γ), v γ ∈ 𝓝 y₀
u_v_disjoint : ∀ (γ : Γ), Disjoint (u γ) (v γ)
U₀₀ : Set T := ⋂ (γ : Γ) (_ : γ ∈ bad_Γ_set), (fun x => γ • x) ⁻¹' u γ
U₀ : Set T := U₀₀ ∩ K₀
V₀₀ : Set T := ⋂ (γ : Γ) (_ : γ ∈ bad_Γ_set), v γ
V₀ : Set T := V₀₀ ∩ L₀
U_nhds : f '' U₀ ∈ 𝓝 (f x₀)
V_nhds : f '' V₀ ∈ 𝓝 (f y₀)
x : T
x_in_U₀₀ : x ∈ U₀₀
x_in_K₀ : x ∈ K₀
γ : Γ
H : ¬γ ∈ bad_Γ_set
h' : γ • x ∈ L₀
⊢ False
[PROOFSTEP]
simp only [image_smul, Classical.not_not, mem_setOf_eq, Ne.def] at H 
[GOAL]
case neg.intro
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
x✝ : Quotient (MulAction.orbitRel Γ T)
x₀ : T
y✝ : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
L₀ : Set T
hL₀ : IsCompact L₀
L₀_in : L₀ ∈ 𝓝 y₀
bad_Γ_set : Set Γ := {γ | (fun x => γ • x) '' K₀ ∩ L₀ ≠ ∅}
bad_Γ_finite : Set.Finite bad_Γ_set
u v : Γ → Set T
hu : ∀ (γ : Γ), u γ ∈ 𝓝 (γ • x₀)
hv : ∀ (γ : Γ), v γ ∈ 𝓝 y₀
u_v_disjoint : ∀ (γ : Γ), Disjoint (u γ) (v γ)
U₀₀ : Set T := ⋂ (γ : Γ) (_ : γ ∈ bad_Γ_set), (fun x => γ • x) ⁻¹' u γ
U₀ : Set T := U₀₀ ∩ K₀
V₀₀ : Set T := ⋂ (γ : Γ) (_ : γ ∈ bad_Γ_set), v γ
V₀ : Set T := V₀₀ ∩ L₀
U_nhds : f '' U₀ ∈ 𝓝 (f x₀)
V_nhds : f '' V₀ ∈ 𝓝 (f y₀)
x : T
x_in_U₀₀ : x ∈ U₀₀
x_in_K₀ : x ∈ K₀
γ : Γ
h' : γ • x ∈ L₀
H : γ • K₀ ∩ L₀ = ∅
⊢ False
[PROOFSTEP]
exact eq_empty_iff_forall_not_mem.mp H (γ • x) ⟨mem_image_of_mem _ x_in_K₀, h'⟩
[GOAL]
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
G₀ : Type u_6
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G₀ α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousConstSMul G₀ α
c : G₀
s : Set α
x : α
hs : s ∈ 𝓝 x
hc : c ≠ 0
⊢ c • s ∈ 𝓝 (c • x)
[PROOFSTEP]
rw [mem_nhds_iff] at hs ⊢
[GOAL]
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
G₀ : Type u_6
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G₀ α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousConstSMul G₀ α
c : G₀
s : Set α
x : α
hs : ∃ t, t ⊆ s ∧ IsOpen t ∧ x ∈ t
hc : c ≠ 0
⊢ ∃ t, t ⊆ c • s ∧ IsOpen t ∧ c • x ∈ t
[PROOFSTEP]
obtain ⟨U, hs', hU, hU'⟩ := hs
[GOAL]
case intro.intro.intro
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
G₀ : Type u_6
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G₀ α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousConstSMul G₀ α
c : G₀
s : Set α
x : α
hc : c ≠ 0
U : Set α
hs' : U ⊆ s
hU : IsOpen U
hU' : x ∈ U
⊢ ∃ t, t ⊆ c • s ∧ IsOpen t ∧ c • x ∈ t
[PROOFSTEP]
exact ⟨c • U, Set.smul_set_mono hs', hU.smul₀ hc, Set.smul_mem_smul_set hU'⟩
[GOAL]
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
G₀ : Type u_6
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G₀ α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousConstSMul G₀ α
c : G₀
s : Set α
x : α
hc : c ≠ 0
⊢ c • s ∈ 𝓝 (c • x) ↔ s ∈ 𝓝 x
[PROOFSTEP]
refine' ⟨fun h => _, fun h => set_smul_mem_nhds_smul h hc⟩
[GOAL]
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
G₀ : Type u_6
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G₀ α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousConstSMul G₀ α
c : G₀
s : Set α
x : α
hc : c ≠ 0
h : c • s ∈ 𝓝 (c • x)
⊢ s ∈ 𝓝 x
[PROOFSTEP]
rw [← inv_smul_smul₀ hc x, ← inv_smul_smul₀ hc s]
[GOAL]
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
G₀ : Type u_6
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G₀ α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousConstSMul G₀ α
c : G₀
s : Set α
x : α
hc : c ≠ 0
h : c • s ∈ 𝓝 (c • x)
⊢ c⁻¹ • c • s ∈ 𝓝 (c⁻¹ • c • x)
[PROOFSTEP]
exact set_smul_mem_nhds_smul h (inv_ne_zero hc)
[GOAL]
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁷ : Group Γ
T : Type u_5
inst✝⁶ : TopologicalSpace T
inst✝⁵ : MulAction Γ T
G₀ : Type u_6
inst✝⁴ : GroupWithZero G₀
inst✝³ : AddMonoid α
inst✝² : DistribMulAction G₀ α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousConstSMul G₀ α
s : Set α
c : G₀
hc : c ≠ 0
⊢ c • s ∈ 𝓝 0 ↔ s ∈ 𝓝 0
[PROOFSTEP]
refine' Iff.trans _ (set_smul_mem_nhds_smul_iff hc)
[GOAL]
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁷ : Group Γ
T : Type u_5
inst✝⁶ : TopologicalSpace T
inst✝⁵ : MulAction Γ T
G₀ : Type u_6
inst✝⁴ : GroupWithZero G₀
inst✝³ : AddMonoid α
inst✝² : DistribMulAction G₀ α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousConstSMul G₀ α
s : Set α
c : G₀
hc : c ≠ 0
⊢ c • s ∈ 𝓝 0 ↔ c • s ∈ 𝓝 (c • 0)
[PROOFSTEP]
rw [smul_zero]
