[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
⊢ ∃ c, c ∈ Ioo a b ∧ IsExtrOn f (Icc a b) c
[PROOFSTEP]
have ne : (Icc a b).Nonempty :=
  nonempty_Icc.2
    (le_of_lt hab)
      -- Consider absolute min and max points
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
⊢ ∃ c, c ∈ Ioo a b ∧ IsExtrOn f (Icc a b) c
[PROOFSTEP]
obtain ⟨c, cmem, cle⟩ : ∃ c ∈ Icc a b, ∀ x ∈ Icc a b, f c ≤ f x := isCompact_Icc.exists_forall_le ne hfc
[GOAL]
case intro.intro
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : X
cmem : c ∈ Icc a b
cle : ∀ (x : X), x ∈ Icc a b → f c ≤ f x
⊢ ∃ c, c ∈ Ioo a b ∧ IsExtrOn f (Icc a b) c
[PROOFSTEP]
obtain ⟨C, Cmem, Cge⟩ : ∃ C ∈ Icc a b, ∀ x ∈ Icc a b, f x ≤ f C := isCompact_Icc.exists_forall_ge ne hfc
[GOAL]
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : X
cmem : c ∈ Icc a b
cle : ∀ (x : X), x ∈ Icc a b → f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ (x : X), x ∈ Icc a b → f x ≤ f C
⊢ ∃ c, c ∈ Ioo a b ∧ IsExtrOn f (Icc a b) c
[PROOFSTEP]
by_cases hc : f c = f a
[GOAL]
case pos
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : X
cmem : c ∈ Icc a b
cle : ∀ (x : X), x ∈ Icc a b → f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ (x : X), x ∈ Icc a b → f x ≤ f C
hc : f c = f a
⊢ ∃ c, c ∈ Ioo a b ∧ IsExtrOn f (Icc a b) c
[PROOFSTEP]
by_cases hC : f C = f a
[GOAL]
case pos
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : X
cmem : c ∈ Icc a b
cle : ∀ (x : X), x ∈ Icc a b → f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ (x : X), x ∈ Icc a b → f x ≤ f C
hc : f c = f a
hC : f C = f a
⊢ ∃ c, c ∈ Ioo a b ∧ IsExtrOn f (Icc a b) c
[PROOFSTEP]
have : ∀ x ∈ Icc a b, f x = f a := fun x hx =>
  le_antisymm (hC ▸ Cge x hx)
    (hc ▸ cle x hx)
      -- `f` is a constant, so we can take any point in `Ioo a b`
[GOAL]
case pos
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : X
cmem : c ∈ Icc a b
cle : ∀ (x : X), x ∈ Icc a b → f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ (x : X), x ∈ Icc a b → f x ≤ f C
hc : f c = f a
hC : f C = f a
this : ∀ (x : X), x ∈ Icc a b → f x = f a
⊢ ∃ c, c ∈ Ioo a b ∧ IsExtrOn f (Icc a b) c
[PROOFSTEP]
rcases nonempty_Ioo.2 hab with ⟨c', hc'⟩
[GOAL]
case pos.intro
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : X
cmem : c ∈ Icc a b
cle : ∀ (x : X), x ∈ Icc a b → f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ (x : X), x ∈ Icc a b → f x ≤ f C
hc : f c = f a
hC : f C = f a
this : ∀ (x : X), x ∈ Icc a b → f x = f a
c' : X
hc' : c' ∈ Ioo a b
⊢ ∃ c, c ∈ Ioo a b ∧ IsExtrOn f (Icc a b) c
[PROOFSTEP]
refine ⟨c', hc', Or.inl fun x hx ↦ ?_⟩
[GOAL]
case pos.intro
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : X
cmem : c ∈ Icc a b
cle : ∀ (x : X), x ∈ Icc a b → f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ (x : X), x ∈ Icc a b → f x ≤ f C
hc : f c = f a
hC : f C = f a
this : ∀ (x : X), x ∈ Icc a b → f x = f a
c' : X
hc' : c' ∈ Ioo a b
x : X
hx : x ∈ Icc a b
⊢ x ∈ {x | (fun x => f c' ≤ f x) x}
[PROOFSTEP]
simp only [mem_setOf_eq, this x hx, this c' (Ioo_subset_Icc_self hc'), le_rfl]
[GOAL]
case neg
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : X
cmem : c ∈ Icc a b
cle : ∀ (x : X), x ∈ Icc a b → f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ (x : X), x ∈ Icc a b → f x ≤ f C
hc : f c = f a
hC : ¬f C = f a
⊢ ∃ c, c ∈ Ioo a b ∧ IsExtrOn f (Icc a b) c
[PROOFSTEP]
refine' ⟨C, ⟨lt_of_le_of_ne Cmem.1 <| mt _ hC, lt_of_le_of_ne Cmem.2 <| mt _ hC⟩, Or.inr Cge⟩
[GOAL]
case neg.refine'_1
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : X
cmem : c ∈ Icc a b
cle : ∀ (x : X), x ∈ Icc a b → f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ (x : X), x ∈ Icc a b → f x ≤ f C
hc : f c = f a
hC : ¬f C = f a
⊢ a = C → f C = f a
case neg.refine'_2
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : X
cmem : c ∈ Icc a b
cle : ∀ (x : X), x ∈ Icc a b → f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ (x : X), x ∈ Icc a b → f x ≤ f C
hc : f c = f a
hC : ¬f C = f a
⊢ C = b → f C = f a
[PROOFSTEP]
exacts [fun h => by rw [h], fun h => by rw [h, hfI]]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : X
cmem : c ∈ Icc a b
cle : ∀ (x : X), x ∈ Icc a b → f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ (x : X), x ∈ Icc a b → f x ≤ f C
hc : f c = f a
hC : ¬f C = f a
h : a = C
⊢ f C = f a
[PROOFSTEP]
rw [h]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : X
cmem : c ∈ Icc a b
cle : ∀ (x : X), x ∈ Icc a b → f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ (x : X), x ∈ Icc a b → f x ≤ f C
hc : f c = f a
hC : ¬f C = f a
h : C = b
⊢ f C = f a
[PROOFSTEP]
rw [h, hfI]
[GOAL]
case neg
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : X
cmem : c ∈ Icc a b
cle : ∀ (x : X), x ∈ Icc a b → f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ (x : X), x ∈ Icc a b → f x ≤ f C
hc : ¬f c = f a
⊢ ∃ c, c ∈ Ioo a b ∧ IsExtrOn f (Icc a b) c
[PROOFSTEP]
refine' ⟨c, ⟨lt_of_le_of_ne cmem.1 <| mt _ hc, lt_of_le_of_ne cmem.2 <| mt _ hc⟩, Or.inl cle⟩
[GOAL]
case neg.refine'_1
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : X
cmem : c ∈ Icc a b
cle : ∀ (x : X), x ∈ Icc a b → f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ (x : X), x ∈ Icc a b → f x ≤ f C
hc : ¬f c = f a
⊢ a = c → f c = f a
case neg.refine'_2
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : X
cmem : c ∈ Icc a b
cle : ∀ (x : X), x ∈ Icc a b → f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ (x : X), x ∈ Icc a b → f x ≤ f C
hc : ¬f c = f a
⊢ c = b → f c = f a
[PROOFSTEP]
exacts [fun h => by rw [h], fun h => by rw [h, hfI]]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : X
cmem : c ∈ Icc a b
cle : ∀ (x : X), x ∈ Icc a b → f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ (x : X), x ∈ Icc a b → f x ≤ f C
hc : ¬f c = f a
h : a = c
⊢ f c = f a
[PROOFSTEP]
rw [h]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : X
cmem : c ∈ Icc a b
cle : ∀ (x : X), x ∈ Icc a b → f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ (x : X), x ∈ Icc a b → f x ≤ f C
hc : ¬f c = f a
h : c = b
⊢ f c = f a
[PROOFSTEP]
rw [h, hfI]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
⊢ ∃ c, c ∈ Ioo a b ∧ IsExtrOn f (Ioo a b) c
[PROOFSTEP]
have h : EqOn (extendFrom (Ioo a b) f) f (Ioo a b) := extendFrom_extends hfc
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
h : EqOn (extendFrom (Ioo a b) f) f (Ioo a b)
⊢ ∃ c, c ∈ Ioo a b ∧ IsExtrOn f (Ioo a b) c
[PROOFSTEP]
obtain ⟨c, hc, hfc⟩ : ∃ c ∈ Ioo a b, IsExtrOn (extendFrom (Ioo a b) f) (Icc a b) c :=
  exists_Ioo_extr_on_Icc hab (continuousOn_Icc_extendFrom_Ioo hab.ne hfc ha hb)
    ((eq_lim_at_left_extendFrom_Ioo hab ha).trans (eq_lim_at_right_extendFrom_Ioo hab hb).symm)
[GOAL]
case intro.intro
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc✝ : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
h : EqOn (extendFrom (Ioo a b) f) f (Ioo a b)
c : X
hc : c ∈ Ioo a b
hfc : IsExtrOn (extendFrom (Ioo a b) f) (Icc a b) c
⊢ ∃ c, c ∈ Ioo a b ∧ IsExtrOn f (Ioo a b) c
[PROOFSTEP]
exact ⟨c, hc, (hfc.on_subset Ioo_subset_Icc_self).congr h (h hc)⟩


[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]


[GOAL]
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module R W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f g : P →A[R] Q
h : f.toAffineMap = g.toAffineMap
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module R W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
g : P →A[R] Q
toAffineMap✝ : P →ᵃ[R] Q
cont✝ : Continuous toAffineMap✝.toFun
h : { toAffineMap := toAffineMap✝, cont := cont✝ }.toAffineMap = g.toAffineMap
⊢ { toAffineMap := toAffineMap✝, cont := cont✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module R W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
toAffineMap✝¹ : P →ᵃ[R] Q
cont✝¹ : Continuous toAffineMap✝¹.toFun
toAffineMap✝ : P →ᵃ[R] Q
cont✝ : Continuous toAffineMap✝.toFun
h :
  { toAffineMap := toAffineMap✝¹, cont := cont✝¹ }.toAffineMap =
    { toAffineMap := toAffineMap✝, cont := cont✝ }.toAffineMap
⊢ { toAffineMap := toAffineMap✝¹, cont := cont✝¹ } = { toAffineMap := toAffineMap✝, cont := cont✝ }
[PROOFSTEP]
congr
[GOAL]
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module R W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f g : P →A[R] Q
h : ↑f = ↑g
⊢ f = g
[PROOFSTEP]
ext a
[GOAL]
case h
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module R W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f g : P →A[R] Q
h : ↑f = ↑g
a : P
⊢ ↑f a = ↑g a
[PROOFSTEP]
exact ContinuousMap.congr_fun h a
[GOAL]
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module R W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P →A[R] Q
h : Continuous f.toFun
⊢ { toAffineMap := f.toAffineMap, cont := h } = f
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module R W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P →A[R] Q
h : Continuous f.toFun
x✝ : P
⊢ ↑{ toAffineMap := f.toAffineMap, cont := h } x✝ = ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module R W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
⊢ Nonempty Q
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup W
inst✝¹ : Module R W
inst✝ : TopologicalSpace W
f : V →L[R] W
⊢ ∀ (p v : V), ↑f (v +ᵥ p) = ↑↑f v +ᵥ ↑f p
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup W
inst✝¹ : Module R W
inst✝ : TopologicalSpace W
f : V →L[R] W
⊢ ↑(toContinuousAffineMap f) 0 = 0
[PROOFSTEP]
simp


[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Mul M
inst✝ : ContinuousMul M
a b : M
⊢ 𝓝 a * 𝓝 b ≤ 𝓝 (a * b)
[PROOFSTEP]
rw [← map₂_mul, ← map_uncurry_prod, ← nhds_prod_eq]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Mul M
inst✝ : ContinuousMul M
a b : M
⊢ map (Function.uncurry fun x x_1 => x * x_1) (𝓝 (a, b)) ≤ 𝓝 (a * b)
[PROOFSTEP]
exact continuous_mul.tendsto _
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace M
inst✝⁶ : Mul M
inst✝⁵ : ContinuousMul M
inst✝⁴ : TopologicalSpace N
inst✝³ : Monoid N
inst✝² : ContinuousMul N
inst✝¹ : T2Space N
f : ι → Nˣ
r₁ r₂ : N
l : Filter ι
inst✝ : NeBot l
h₁ : Tendsto (fun x => ↑(f x)) l (𝓝 r₁)
h₂ : Tendsto (fun x => ↑(f x)⁻¹) l (𝓝 r₂)
⊢ r₁ * r₂ = 1
[PROOFSTEP]
symm
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace M
inst✝⁶ : Mul M
inst✝⁵ : ContinuousMul M
inst✝⁴ : TopologicalSpace N
inst✝³ : Monoid N
inst✝² : ContinuousMul N
inst✝¹ : T2Space N
f : ι → Nˣ
r₁ r₂ : N
l : Filter ι
inst✝ : NeBot l
h₁ : Tendsto (fun x => ↑(f x)) l (𝓝 r₁)
h₂ : Tendsto (fun x => ↑(f x)⁻¹) l (𝓝 r₂)
⊢ 1 = r₁ * r₂
[PROOFSTEP]
simpa using h₁.mul h₂
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace M
inst✝⁶ : Mul M
inst✝⁵ : ContinuousMul M
inst✝⁴ : TopologicalSpace N
inst✝³ : Monoid N
inst✝² : ContinuousMul N
inst✝¹ : T2Space N
f : ι → Nˣ
r₁ r₂ : N
l : Filter ι
inst✝ : NeBot l
h₁ : Tendsto (fun x => ↑(f x)) l (𝓝 r₁)
h₂ : Tendsto (fun x => ↑(f x)⁻¹) l (𝓝 r₂)
⊢ r₂ * r₁ = 1
[PROOFSTEP]
symm
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace M
inst✝⁶ : Mul M
inst✝⁵ : ContinuousMul M
inst✝⁴ : TopologicalSpace N
inst✝³ : Monoid N
inst✝² : ContinuousMul N
inst✝¹ : T2Space N
f : ι → Nˣ
r₁ r₂ : N
l : Filter ι
inst✝ : NeBot l
h₁ : Tendsto (fun x => ↑(f x)) l (𝓝 r₁)
h₂ : Tendsto (fun x => ↑(f x)⁻¹) l (𝓝 r₂)
⊢ 1 = r₂ * r₁
[PROOFSTEP]
simpa using h₂.mul h₁
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Mul M✝
inst✝² : ContinuousMul M✝
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
⊢ Continuous fun p => p.fst * p.snd
[PROOFSTEP]
rw [continuous_iff_continuousAt]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Mul M✝
inst✝² : ContinuousMul M✝
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
⊢ ∀ (x : M × M), ContinuousAt (fun p => p.fst * p.snd) x
[PROOFSTEP]
rintro ⟨x₀, y₀⟩
[GOAL]
case mk
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Mul M✝
inst✝² : ContinuousMul M✝
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
⊢ ContinuousAt (fun p => p.fst * p.snd) (x₀, y₀)
[PROOFSTEP]
have key : (fun p : M × M => x₀ * p.1 * (p.2 * y₀)) = ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry (· * ·) :=
  by
  ext p
  simp [uncurry, mul_assoc]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Mul M✝
inst✝² : ContinuousMul M✝
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
⊢ (fun p => x₀ * p.fst * (p.snd * y₀)) = ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x x_1 => x * x_1
[PROOFSTEP]
ext p
[GOAL]
case h
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Mul M✝
inst✝² : ContinuousMul M✝
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
p : M × M
⊢ x₀ * p.fst * (p.snd * y₀) = (((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x x_1 => x * x_1) p
[PROOFSTEP]
simp [uncurry, mul_assoc]
[GOAL]
case mk
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Mul M✝
inst✝² : ContinuousMul M✝
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p => x₀ * p.fst * (p.snd * y₀)) = ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x x_1 => x * x_1
⊢ ContinuousAt (fun p => p.fst * p.snd) (x₀, y₀)
[PROOFSTEP]
have key₂ : ((fun x => x₀ * x) ∘ fun x => y₀ * x) = fun x => x₀ * y₀ * x :=
  by
  ext x
  simp [mul_assoc]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Mul M✝
inst✝² : ContinuousMul M✝
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p => x₀ * p.fst * (p.snd * y₀)) = ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x x_1 => x * x_1
⊢ ((fun x => x₀ * x) ∘ fun x => y₀ * x) = fun x => x₀ * y₀ * x
[PROOFSTEP]
ext x
[GOAL]
case h
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Mul M✝
inst✝² : ContinuousMul M✝
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p => x₀ * p.fst * (p.snd * y₀)) = ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x x_1 => x * x_1
x : M
⊢ ((fun x => x₀ * x) ∘ fun x => y₀ * x) x = x₀ * y₀ * x
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
case mk
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Mul M✝
inst✝² : ContinuousMul M✝
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p => x₀ * p.fst * (p.snd * y₀)) = ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x x_1 => x * x_1
key₂ : ((fun x => x₀ * x) ∘ fun x => y₀ * x) = fun x => x₀ * y₀ * x
⊢ ContinuousAt (fun p => p.fst * p.snd) (x₀, y₀)
[PROOFSTEP]
calc
  map (uncurry (· * ·)) (𝓝 (x₀, y₀)) = map (uncurry (· * ·)) (𝓝 x₀ ×ˢ 𝓝 y₀) := by rw [nhds_prod_eq]
  _ = map (fun p : M × M => x₀ * p.1 * (p.2 * y₀)) (𝓝 1 ×ˢ 𝓝 1) :=
    -- Porting note: `rw` was able to prove this
            -- Now it fails with `failed to rewrite using equation theorems for 'Function.uncurry'`
            -- and `failed to rewrite using equation theorems for 'Function.comp'`.
            -- Removing those two lemmas, the `rw` would succeed, but then needs a `rfl`.by
    simp_rw [uncurry, hleft x₀, hright y₀, prod_map_map_eq, Filter.map_map, Function.comp]
  _ = map ((fun x => x₀ * x) ∘ fun x => x * y₀) (map (uncurry (· * ·)) (𝓝 1 ×ˢ 𝓝 1)) := by rw [key, ← Filter.map_map]
  _ ≤ map ((fun x : M => x₀ * x) ∘ fun x => x * y₀) (𝓝 1) := (map_mono hmul)
  _ = 𝓝 (x₀ * y₀) := by rw [← Filter.map_map, ← hright, hleft y₀, Filter.map_map, key₂, ← hleft]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Mul M✝
inst✝² : ContinuousMul M✝
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p => x₀ * p.fst * (p.snd * y₀)) = ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x x_1 => x * x_1
key₂ : ((fun x => x₀ * x) ∘ fun x => y₀ * x) = fun x => x₀ * y₀ * x
⊢ map (uncurry fun x x_1 => x * x_1) (𝓝 (x₀, y₀)) = map (uncurry fun x x_1 => x * x_1) (𝓝 x₀ ×ˢ 𝓝 y₀)
[PROOFSTEP]
rw [nhds_prod_eq]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Mul M✝
inst✝² : ContinuousMul M✝
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p => x₀ * p.fst * (p.snd * y₀)) = ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x x_1 => x * x_1
key₂ : ((fun x => x₀ * x) ∘ fun x => y₀ * x) = fun x => x₀ * y₀ * x
⊢ map (uncurry fun x x_1 => x * x_1) (𝓝 x₀ ×ˢ 𝓝 y₀) = map (fun p => x₀ * p.fst * (p.snd * y₀)) (𝓝 1 ×ˢ 𝓝 1)
[PROOFSTEP]
simp_rw [uncurry, hleft x₀, hright y₀, prod_map_map_eq, Filter.map_map, Function.comp]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Mul M✝
inst✝² : ContinuousMul M✝
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p => x₀ * p.fst * (p.snd * y₀)) = ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x x_1 => x * x_1
key₂ : ((fun x => x₀ * x) ∘ fun x => y₀ * x) = fun x => x₀ * y₀ * x
⊢ map (fun p => x₀ * p.fst * (p.snd * y₀)) (𝓝 1 ×ˢ 𝓝 1) =
    map ((fun x => x₀ * x) ∘ fun x => x * y₀) (map (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1))
[PROOFSTEP]
rw [key, ← Filter.map_map]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Mul M✝
inst✝² : ContinuousMul M✝
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p => x₀ * p.fst * (p.snd * y₀)) = ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x x_1 => x * x_1
key₂ : ((fun x => x₀ * x) ∘ fun x => y₀ * x) = fun x => x₀ * y₀ * x
⊢ map ((fun x => x₀ * x) ∘ fun x => x * y₀) (𝓝 1) = 𝓝 (x₀ * y₀)
[PROOFSTEP]
rw [← Filter.map_map, ← hright, hleft y₀, Filter.map_map, key₂, ← hleft]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Mul M✝
inst✝² : ContinuousMul M✝
M : Type u
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
⊢ ContinuousMul M
[PROOFSTEP]
apply ContinuousMul.of_nhds_one hmul hleft
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Mul M✝
inst✝² : ContinuousMul M✝
M : Type u
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
⊢ ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
[PROOFSTEP]
intro x₀
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Mul M✝
inst✝² : ContinuousMul M✝
M : Type u
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
x₀ : M
⊢ 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
[PROOFSTEP]
simp_rw [mul_comm, hleft x₀]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : TopologicalSpace X
M₁ : Type u_6
M₂ : Type u_7
inst✝⁴ : TopologicalSpace M₂
inst✝³ : T2Space M₂
inst✝² : Mul M₁
inst✝¹ : Mul M₂
inst✝ : ContinuousMul M₂
⊢ IsClosed {f | ∀ (x y : M₁), f (x * y) = f x * f y}
[PROOFSTEP]
simp only [setOf_forall]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : TopologicalSpace X
M₁ : Type u_6
M₂ : Type u_7
inst✝⁴ : TopologicalSpace M₂
inst✝³ : T2Space M₂
inst✝² : Mul M₁
inst✝¹ : Mul M₂
inst✝ : ContinuousMul M₂
⊢ IsClosed (⋂ (i : M₁) (i_1 : M₁), {x | x (i * i_1) = x i * x i_1})
[PROOFSTEP]
exact
  isClosed_iInter fun x =>
    isClosed_iInter fun y =>
      isClosed_eq
        (continuous_apply _)
          -- Porting note: proof was:
                    -- `((continuous_apply _).mul (continuous_apply _))`
        (by continuity)
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : TopologicalSpace X
M₁ : Type u_6
M₂ : Type u_7
inst✝⁴ : TopologicalSpace M₂
inst✝³ : T2Space M₂
inst✝² : Mul M₁
inst✝¹ : Mul M₂
inst✝ : ContinuousMul M₂
x y : M₁
⊢ Continuous fun x_1 => x_1 x * x_1 y
[PROOFSTEP]
continuity
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N✝ : Type u_5
inst✝⁶ : TopologicalSpace X
M : Type u_6
N : Type u_7
F : Type u_8
inst✝⁵ : Mul M
inst✝⁴ : Mul N
inst✝³ : MulHomClass F M N
inst✝² : TopologicalSpace M
inst✝¹ : TopologicalSpace N
inst✝ : ContinuousMul N
f : F
hf : Inducing ↑f
⊢ Continuous (↑f ∘ fun p => p.fst * p.snd)
[PROOFSTEP]
simpa only [(· ∘ ·), map_mul f] using hf.continuous.fst'.mul hf.continuous.snd'
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
s : Set M
hs : s ∈ 𝓝 1
⊢ ∃ V, IsOpen V ∧ 1 ∈ V ∧ ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v * w ∈ s
[PROOFSTEP]
have : (fun a : M × M => a.1 * a.2) ⁻¹' s ∈ 𝓝 ((1, 1) : M × M) := tendsto_mul (by simpa only [one_mul] using hs)
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
s : Set M
hs : s ∈ 𝓝 1
⊢ s ∈ 𝓝 (1 * 1)
[PROOFSTEP]
simpa only [one_mul] using hs
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
s : Set M
hs : s ∈ 𝓝 1
this : (fun a => a.fst * a.snd) ⁻¹' s ∈ 𝓝 (1, 1)
⊢ ∃ V, IsOpen V ∧ 1 ∈ V ∧ ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v * w ∈ s
[PROOFSTEP]
simpa only [prod_subset_iff] using exists_nhds_square this
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
⊢ ∃ V, V ∈ 𝓝 1 ∧ ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u
[PROOFSTEP]
rcases exists_nhds_one_split hu with ⟨W, W1, h⟩
[GOAL]
case intro.intro
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
W : Set M
W1 : W ∈ 𝓝 1
h : ∀ (v : M), v ∈ W → ∀ (w : M), w ∈ W → v * w ∈ u
⊢ ∃ V, V ∈ 𝓝 1 ∧ ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u
[PROOFSTEP]
rcases exists_nhds_one_split W1 with ⟨V, V1, h'⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
W : Set M
W1 : W ∈ 𝓝 1
h : ∀ (v : M), v ∈ W → ∀ (w : M), w ∈ W → v * w ∈ u
V : Set M
V1 : V ∈ 𝓝 1
h' : ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v * w ∈ W
⊢ ∃ V, V ∈ 𝓝 1 ∧ ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u
[PROOFSTEP]
use V, V1
[GOAL]
case right
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
W : Set M
W1 : W ∈ 𝓝 1
h : ∀ (v : M), v ∈ W → ∀ (w : M), w ∈ W → v * w ∈ u
V : Set M
V1 : V ∈ 𝓝 1
h' : ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v * w ∈ W
⊢ ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u
[PROOFSTEP]
intro v w s t v_in w_in s_in t_in
[GOAL]
case right
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
W : Set M
W1 : W ∈ 𝓝 1
h : ∀ (v : M), v ∈ W → ∀ (w : M), w ∈ W → v * w ∈ u
V : Set M
V1 : V ∈ 𝓝 1
h' : ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v * w ∈ W
v w s t : M
v_in : v ∈ V
w_in : w ∈ V
s_in : s ∈ V
t_in : t ∈ V
⊢ v * w * s * t ∈ u
[PROOFSTEP]
simpa only [mul_assoc] using h _ (h' v v_in w w_in) _ (h' s s_in t t_in)
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
U : Set M
hU : U ∈ 𝓝 1
⊢ ∃ V, IsOpen V ∧ 1 ∈ V ∧ V * V ⊆ U
[PROOFSTEP]
rcases exists_open_nhds_one_split hU with ⟨V, Vo, V1, hV⟩
[GOAL]
case intro.intro.intro
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
U : Set M
hU : U ∈ 𝓝 1
V : Set M
Vo : IsOpen V
V1 : 1 ∈ V
hV : ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v * w ∈ U
⊢ ∃ V, IsOpen V ∧ 1 ∈ V ∧ V * V ⊆ U
[PROOFSTEP]
use V, Vo, V1
[GOAL]
case right
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
U : Set M
hU : U ∈ 𝓝 1
V : Set M
Vo : IsOpen V
V1 : 1 ∈ V
hV : ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v * w ∈ U
⊢ V * V ⊆ U
[PROOFSTEP]
rintro _ ⟨x, y, hx, hy, rfl⟩
[GOAL]
case right.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
U : Set M
hU : U ∈ 𝓝 1
V : Set M
Vo : IsOpen V
V1 : 1 ∈ V
hV : ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v * w ∈ U
x y : M
hx : x ∈ V
hy : y ∈ V
⊢ (fun x x_1 => x * x_1) x y ∈ U
[PROOFSTEP]
exact hV _ hx _ hy
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
s t : Set M
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact (s * t)
[PROOFSTEP]
rw [← image_mul_prod]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
s t : Set M
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact ((fun x => x.fst * x.snd) '' s ×ˢ t)
[PROOFSTEP]
exact (hs.prod ht).image continuous_mul
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → α → M
x : Filter α
a : ι → M
x✝ : ∀ (i : ι), i ∈ [] → Tendsto (f i) x (𝓝 (a i))
⊢ Tendsto (fun b => List.prod (List.map (fun c => f c b) [])) x (𝓝 (List.prod (List.map a [])))
[PROOFSTEP]
simp [tendsto_const_nhds]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f✝ : ι → α → M
x : Filter α
a : ι → M
f : ι
l : List ι
h : ∀ (i : ι), i ∈ f :: l → Tendsto (f✝ i) x (𝓝 (a i))
⊢ Tendsto (fun b => List.prod (List.map (fun c => f✝ c b) (f :: l))) x (𝓝 (List.prod (List.map a (f :: l))))
[PROOFSTEP]
simp only [List.map_cons, List.prod_cons]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f✝ : ι → α → M
x : Filter α
a : ι → M
f : ι
l : List ι
h : ∀ (i : ι), i ∈ f :: l → Tendsto (f✝ i) x (𝓝 (a i))
⊢ Tendsto (fun b => f✝ f b * List.prod (List.map (fun c => f✝ c b) l)) x (𝓝 (a f * List.prod (List.map a l)))
[PROOFSTEP]
exact (h f (List.mem_cons_self _ _)).mul (tendsto_list_prod l fun c hc => h c (List.mem_cons_of_mem _ hc))
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
h : ∀ (i : ι), i ∈ l → ContinuousOn (f i) t
⊢ ContinuousOn (fun a => List.prod (List.map (fun i => f i a) l)) t
[PROOFSTEP]
intro x hx
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
h : ∀ (i : ι), i ∈ l → ContinuousOn (f i) t
x : X
hx : x ∈ t
⊢ ContinuousWithinAt (fun a => List.prod (List.map (fun i => f i a) l)) t x
[PROOFSTEP]
rw [continuousWithinAt_iff_continuousAt_restrict _ hx]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
h : ∀ (i : ι), i ∈ l → ContinuousOn (f i) t
x : X
hx : x ∈ t
⊢ ContinuousAt (restrict t fun a => List.prod (List.map (fun i => f i a) l)) { val := x, property := hx }
[PROOFSTEP]
refine' tendsto_list_prod _ fun i hi => _
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
h : ∀ (i : ι), i ∈ l → ContinuousOn (f i) t
x : X
hx : x ∈ t
i : ι
hi : i ∈ l
⊢ Tendsto (fun b => f i ↑b) (𝓝 { val := x, property := hx }) (𝓝 (f i ↑{ val := x, property := hx }))
[PROOFSTEP]
specialize h i hi x hx
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
x : X
hx : x ∈ t
i : ι
hi : i ∈ l
h : ContinuousWithinAt (f i) t x
⊢ Tendsto (fun b => f i ↑b) (𝓝 { val := x, property := hx }) (𝓝 (f i ↑{ val := x, property := hx }))
[PROOFSTEP]
rw [continuousWithinAt_iff_continuousAt_restrict _ hx] at h
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
x : X
hx : x ∈ t
i : ι
hi : i ∈ l
h : ContinuousAt (restrict t (f i)) { val := x, property := hx }
⊢ Tendsto (fun b => f i ↑b) (𝓝 { val := x, property := hx }) (𝓝 (f i ↑{ val := x, property := hx }))
[PROOFSTEP]
exact h
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
⊢ Continuous fun a => a ^ 0
[PROOFSTEP]
simpa using continuous_const
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
k : ℕ
⊢ Continuous fun a => a ^ (k + 1)
[PROOFSTEP]
simp only [pow_succ]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
k : ℕ
⊢ Continuous fun a => a * a ^ k
[PROOFSTEP]
exact continuous_id.mul (continuous_pow _)
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
a b : M
ha : b * a = 1
⊢ Tendsto (fun x => a * x) (cocompact M) (cocompact M)
[PROOFSTEP]
refine Filter.Tendsto.of_tendsto_comp ?_ (Filter.comap_cocompact_le (continuous_mul_left b))
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
a b : M
ha : b * a = 1
⊢ Tendsto ((fun b_1 => b * b_1) ∘ fun x => a * x) (cocompact M) (cocompact M)
[PROOFSTEP]
simp only [comp_mul_left, ha, one_mul]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
a b : M
ha : b * a = 1
⊢ Tendsto (fun x => x) (cocompact M) (cocompact M)
[PROOFSTEP]
exact Filter.tendsto_id
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
a b : M
ha : a * b = 1
⊢ Tendsto (fun x => x * a) (cocompact M) (cocompact M)
[PROOFSTEP]
refine Filter.Tendsto.of_tendsto_comp ?_ (Filter.comap_cocompact_le (continuous_mul_right b))
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
a b : M
ha : a * b = 1
⊢ Tendsto ((fun b_1 => b_1 * b) ∘ fun x => x * a) (cocompact M) (cocompact M)
[PROOFSTEP]
simp only [comp_mul_right, ha, mul_one]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
a b : M
ha : a * b = 1
⊢ Tendsto (fun x => x) (cocompact M) (cocompact M)
[PROOFSTEP]
exact Filter.tendsto_id
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace M
inst✝⁶ : Monoid M
inst✝⁵ : ContinuousMul M
R : Type u_6
A : Type u_7
inst✝⁴ : Monoid A
inst✝³ : SMul R A
inst✝² : IsScalarTower R A A
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousMul A
q : R
⊢ Continuous fun x => q • x
[PROOFSTEP]
simp (config := { singlePass := true }) only [← smul_one_mul q (_ : A)]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace M
inst✝⁶ : Monoid M
inst✝⁵ : ContinuousMul M
R : Type u_6
A : Type u_7
inst✝⁴ : Monoid A
inst✝³ : SMul R A
inst✝² : IsScalarTower R A A
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousMul A
q : R
⊢ Continuous fun x => q • 1 * x
[PROOFSTEP]
exact continuous_const.mul continuous_id
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace M
inst✝⁶ : Monoid M
inst✝⁵ : ContinuousMul M
R : Type u_6
A : Type u_7
inst✝⁴ : Monoid A
inst✝³ : SMul R A
inst✝² : SMulCommClass R A A
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousMul A
q : R
⊢ Continuous fun x => q • x
[PROOFSTEP]
simp (config := { singlePass := true }) only [← mul_smul_one q (_ : A)]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace M
inst✝⁶ : Monoid M
inst✝⁵ : ContinuousMul M
R : Type u_6
A : Type u_7
inst✝⁴ : Monoid A
inst✝³ : SMul R A
inst✝² : SMulCommClass R A A
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousMul A
q : R
⊢ Continuous fun x => x * q • 1
[PROOFSTEP]
exact continuous_id.mul continuous_const
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → α → M
x : Filter α
a : ι → M
s : Multiset ι
⊢ (∀ (i : ι), i ∈ s → Tendsto (f i) x (𝓝 (a i))) →
    Tendsto (fun b => Multiset.prod (Multiset.map (fun c => f c b) s)) x (𝓝 (Multiset.prod (Multiset.map a s)))
[PROOFSTEP]
rcases s with ⟨l⟩
[GOAL]
case mk
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → α → M
x : Filter α
a : ι → M
s : Multiset ι
l : List ι
⊢ (∀ (i : ι), i ∈ Quot.mk Setoid.r l → Tendsto (f i) x (𝓝 (a i))) →
    Tendsto (fun b => Multiset.prod (Multiset.map (fun c => f c b) (Quot.mk Setoid.r l))) x
      (𝓝 (Multiset.prod (Multiset.map a (Quot.mk Setoid.r l))))
[PROOFSTEP]
simpa using tendsto_list_prod l
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
s : Multiset ι
⊢ (∀ (i : ι), i ∈ s → Continuous (f i)) → Continuous fun a => Multiset.prod (Multiset.map (fun i => f i a) s)
[PROOFSTEP]
rcases s with ⟨l⟩
[GOAL]
case mk
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
s : Multiset ι
l : List ι
⊢ (∀ (i : ι), i ∈ Quot.mk Setoid.r l → Continuous (f i)) →
    Continuous fun a => Multiset.prod (Multiset.map (fun i => f i a) (Quot.mk Setoid.r l))
[PROOFSTEP]
simpa using continuous_list_prod l
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
s : Multiset ι
t : Set X
⊢ (∀ (i : ι), i ∈ s → ContinuousOn (f i) t) → ContinuousOn (fun a => Multiset.prod (Multiset.map (fun i => f i a) s)) t
[PROOFSTEP]
rcases s with ⟨l⟩
[GOAL]
case mk
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
s : Multiset ι
t : Set X
l : List ι
⊢ (∀ (i : ι), i ∈ Quot.mk Setoid.r l → ContinuousOn (f i) t) →
    ContinuousOn (fun a => Multiset.prod (Multiset.map (fun i => f i a) (Quot.mk Setoid.r l))) t
[PROOFSTEP]
simpa using continuousOn_list_prod l
[GOAL]
ι : Type u_1
α : Type u_2
X✝ : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace M✝
inst✝² : CommMonoid M✝
inst✝¹ : ContinuousMul M✝
X : Type u_6
M : Type u_7
inst✝ : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ (i : ι), i ∈ s → f i =ᶠ[l] g i
⊢ ∏ i in s, f i =ᶠ[l] ∏ i in s, g i
[PROOFSTEP]
replace hs : ∀ᶠ x in l, ∀ i ∈ s, f i x = g i x
[GOAL]
case hs
ι : Type u_1
α : Type u_2
X✝ : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace M✝
inst✝² : CommMonoid M✝
inst✝¹ : ContinuousMul M✝
X : Type u_6
M : Type u_7
inst✝ : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ (i : ι), i ∈ s → f i =ᶠ[l] g i
⊢ ∀ᶠ (x : X) in l, ∀ (i : ι), i ∈ s → f i x = g i x
[PROOFSTEP]
rwa [eventually_all_finset]
[GOAL]
ι : Type u_1
α : Type u_2
X✝ : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace M✝
inst✝² : CommMonoid M✝
inst✝¹ : ContinuousMul M✝
X : Type u_6
M : Type u_7
inst✝ : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ᶠ (x : X) in l, ∀ (i : ι), i ∈ s → f i x = g i x
⊢ ∏ i in s, f i =ᶠ[l] ∏ i in s, g i
[PROOFSTEP]
filter_upwards [hs] with x hx
[GOAL]
case h
ι : Type u_1
α : Type u_2
X✝ : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace M✝
inst✝² : CommMonoid M✝
inst✝¹ : ContinuousMul M✝
X : Type u_6
M : Type u_7
inst✝ : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ᶠ (x : X) in l, ∀ (i : ι), i ∈ s → f i x = g i x
x : X
hx : ∀ (i : ι), i ∈ s → f i x = g i x
⊢ Finset.prod s (fun i => f i) x = Finset.prod s (fun i => g i) x
[PROOFSTEP]
simp only [Finset.prod_apply, Finset.prod_congr rfl hx]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace M✝
inst✝² : CommMonoid M✝
inst✝¹ : ContinuousMul M✝
M : Type u_6
inst✝ : CommMonoid M
f : ι → X → M
hf : LocallyFinite fun i => mulSupport (f i)
x₀ : X
⊢ ∃ I, ∀ᶠ (x : X) in 𝓝 x₀, (mulSupport fun i => f i x) ⊆ ↑I
[PROOFSTEP]
rcases hf x₀ with ⟨U, hxU, hUf⟩
[GOAL]
case intro.intro
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace M✝
inst✝² : CommMonoid M✝
inst✝¹ : ContinuousMul M✝
M : Type u_6
inst✝ : CommMonoid M
f : ι → X → M
hf : LocallyFinite fun i => mulSupport (f i)
x₀ : X
U : Set X
hxU : U ∈ 𝓝 x₀
hUf : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ U)}
⊢ ∃ I, ∀ᶠ (x : X) in 𝓝 x₀, (mulSupport fun i => f i x) ⊆ ↑I
[PROOFSTEP]
refine' ⟨hUf.toFinset, mem_of_superset hxU fun y hy i hi => _⟩
[GOAL]
case intro.intro
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace M✝
inst✝² : CommMonoid M✝
inst✝¹ : ContinuousMul M✝
M : Type u_6
inst✝ : CommMonoid M
f : ι → X → M
hf : LocallyFinite fun i => mulSupport (f i)
x₀ : X
U : Set X
hxU : U ∈ 𝓝 x₀
hUf : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ U)}
y : X
hy : y ∈ U
i : ι
hi : i ∈ mulSupport fun i => f i y
⊢ i ∈ ↑(Finite.toFinset hUf)
[PROOFSTEP]
rw [hUf.coe_toFinset]
[GOAL]
case intro.intro
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace M✝
inst✝² : CommMonoid M✝
inst✝¹ : ContinuousMul M✝
M : Type u_6
inst✝ : CommMonoid M
f : ι → X → M
hf : LocallyFinite fun i => mulSupport (f i)
x₀ : X
U : Set X
hxU : U ∈ 𝓝 x₀
hUf : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ U)}
y : X
hy : y ∈ U
i : ι
hi : i ∈ mulSupport fun i => f i y
⊢ i ∈ {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ U)}
[PROOFSTEP]
exact ⟨y, hi, hy⟩
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous (f i)
hf : LocallyFinite fun i => mulSupport (f i)
⊢ Continuous fun x => ∏ᶠ (i : ι), f i x
[PROOFSTEP]
refine' continuous_iff_continuousAt.2 fun x => _
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous (f i)
hf : LocallyFinite fun i => mulSupport (f i)
x : X
⊢ ContinuousAt (fun x => ∏ᶠ (i : ι), f i x) x
[PROOFSTEP]
rcases finprod_eventually_eq_prod hf x with ⟨s, hs⟩
[GOAL]
case intro
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous (f i)
hf : LocallyFinite fun i => mulSupport (f i)
x : X
s : Finset ι
hs : ∀ᶠ (y : X) in 𝓝 x, ∏ᶠ (i : ι), f i y = ∏ i in s, f i y
⊢ ContinuousAt (fun x => ∏ᶠ (i : ι), f i x) x
[PROOFSTEP]
refine' ContinuousAt.congr _ (EventuallyEq.symm hs)
[GOAL]
case intro
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous (f i)
hf : LocallyFinite fun i => mulSupport (f i)
x : X
s : Finset ι
hs : ∀ᶠ (y : X) in 𝓝 x, ∏ᶠ (i : ι), f i y = ∏ i in s, f i y
⊢ ContinuousAt (fun x => ∏ i in s, f i x) x
[PROOFSTEP]
exact tendsto_finset_prod _ fun i _ => (hc i).continuousAt
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
p : ι → Prop
hc : ∀ (i : ι), p i → Continuous (f i)
hf : LocallyFinite fun i => mulSupport (f i)
⊢ Continuous fun x => ∏ᶠ (i : ι) (_ : p i), f i x
[PROOFSTEP]
simp only [← finprod_subtype_eq_finprod_cond]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
p : ι → Prop
hc : ∀ (i : ι), p i → Continuous (f i)
hf : LocallyFinite fun i => mulSupport (f i)
⊢ Continuous fun x => ∏ᶠ (j : { i // p i }), f (↑j) x
[PROOFSTEP]
exact continuous_finprod (fun i => hc i i.2) (hf.comp_injective Subtype.coe_injective)
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : TopologicalSpace X
ι' : Sort u_6
inst✝ : Mul M
ts : ι' → TopologicalSpace M
h' : ∀ (i : ι'), ContinuousMul M
⊢ ContinuousMul M
[PROOFSTEP]
rw [← sInf_range]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : TopologicalSpace X
ι' : Sort u_6
inst✝ : Mul M
ts : ι' → TopologicalSpace M
h' : ∀ (i : ι'), ContinuousMul M
⊢ ContinuousMul M
[PROOFSTEP]
exact continuousMul_sInf (Set.forall_range_iff.mpr h')
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : TopologicalSpace X
ι' : Sort u_6
inst✝ : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
⊢ ContinuousMul M
[PROOFSTEP]
rw [inf_eq_iInf]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : TopologicalSpace X
ι' : Sort u_6
inst✝ : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
⊢ ContinuousMul M
[PROOFSTEP]
refine' continuousMul_iInf fun b => _
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : TopologicalSpace X
ι' : Sort u_6
inst✝ : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
b : Bool
⊢ ContinuousMul M
[PROOFSTEP]
cases b
[GOAL]
case false
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : TopologicalSpace X
ι' : Sort u_6
inst✝ : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
⊢ ContinuousMul M
[PROOFSTEP]
assumption
[GOAL]
case true
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : TopologicalSpace X
ι' : Sort u_6
inst✝ : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
⊢ ContinuousMul M
[PROOFSTEP]
assumption