case H
𝕜 : Type u_1
B : Type ?u.98530
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x : AddCircle p
z✝ : 𝕜
hx : ↑z✝ ≠ ↑a
⊢ ContinuousAt ↑(equivIco p a) ↑z✝
𝕜 : Type u_1
B : Type ?u.98530
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x : AddCircle p
hx : x ≠ ↑a
⊢ ContinuousAt (↑(equivIco p a)) x
induction x using QuotientAddGroup.induction_on'
case H
𝕜 : Type u_1
B : Type ?u.98530
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x : AddCircle p
z✝ : 𝕜
hx : ↑z✝ ≠ ↑a
⊢ Filter.map (↑(equivIco p a) ∘ QuotientAddGroup.mk) (𝓝 z✝) ≤ 𝓝 (↑(equivIco p a) ↑z✝)
case H
𝕜 : Type u_1
B : Type ?u.98530
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x : AddCircle p
z✝ : 𝕜
hx : ↑z✝ ≠ ↑a
⊢ ContinuousAt ↑(equivIco p a) ↑z✝
rw [ContinuousAt, Filter.Tendsto, QuotientAddGroup.nhds_eq, Filter.map_map]
no goals
case H
𝕜 : Type u_1
B : Type ?u.98530
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x : AddCircle p
z✝ : 𝕜
hx : ↑z✝ ≠ ↑a
⊢ Filter.map (↑(equivIco p a) ∘ QuotientAddGroup.mk) (𝓝 z✝) ≤ 𝓝 (↑(equivIco p a) ↑z✝)
exact (continuousAt_toIcoMod hp.out a hx).codRestrict _