𝕜 : Type u_1
B : Type ?u.10078
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
⊢ ContinuousWithinAt ((fun x => p - x) ∘ toIcoMod hp (-a) ∘ Neg.neg) (Iic x) x
𝕜 : Type u_1
B : Type ?u.10078
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
⊢ ContinuousWithinAt (toIocMod hp a) (Iic x) x
rw [(funext fun y => Eq.trans (by rw [neg_neg]) <| toIocMod_neg _ _ _ :
    toIocMod hp a = (fun x => p - x) ∘ toIcoMod hp (-a) ∘ Neg.neg)]
𝕜 : Type u_1
B : Type ?u.10078
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
this : ContinuousNeg 𝕜
⊢ ContinuousWithinAt ((fun x => p - x) ∘ toIcoMod hp (-a) ∘ Neg.neg) (Iic x) x
𝕜 : Type u_1
B : Type ?u.10078
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
⊢ ContinuousWithinAt ((fun x => p - x) ∘ toIcoMod hp (-a) ∘ Neg.neg) (Iic x) x
have : ContinuousNeg 𝕜 := TopologicalAddGroup.toContinuousNeg
no goals
𝕜 : Type u_1
B : Type ?u.10078
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
this : ContinuousNeg 𝕜
⊢ ContinuousWithinAt ((fun x => p - x) ∘ toIcoMod hp (-a) ∘ Neg.neg) (Iic x) x
exact
  (continuous_sub_left _).continuousAt.comp_continuousWithinAt <|
    (continuous_right_toIcoMod _ _ _).comp continuous_neg.continuousWithinAt fun y => neg_le_neg
no goals
𝕜 : Type u_1
B : Type ?u.10078
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x y : 𝕜
⊢ toIocMod hp a y = toIocMod hp a (- -y)
rw [neg_neg]