𝕜 : Type u_2
B : Type u_1
inst✝⁴ : LinearOrderedAddCommGroup 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝¹ : Archimedean 𝕜
inst✝ : TopologicalSpace B
f : 𝕜 → B
hf : f a = f (a + p)
hc : ContinuousOn f (Icc a (a + p))
⊢ Continuous
    (Quot.lift (restrict (Icc a (a + p)) f)
        (_ :
          ∀ (a_1 b : ↑(Icc a (a + p))),
            EndpointIdent p a a_1 b → restrict (Icc a (a + p)) f a_1 = restrict (Icc a (a + p)) f b) ∘
      ↑(equivIccQuot p a))
𝕜 : Type u_2
B : Type u_1
inst✝⁴ : LinearOrderedAddCommGroup 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝¹ : Archimedean 𝕜
inst✝ : TopologicalSpace B
f : 𝕜 → B
hf : f a = f (a + p)
hc : ContinuousOn f (Icc a (a + p))
⊢ Continuous (liftIco p a f)
rw [liftIco_eq_lift_Icc hf]
𝕜 : Type u_2
B : Type u_1
inst✝⁴ : LinearOrderedAddCommGroup 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝¹ : Archimedean 𝕜
inst✝ : TopologicalSpace B
f : 𝕜 → B
hf : f a = f (a + p)
hc : ContinuousOn f (Icc a (a + p))
⊢ Continuous
    (Quot.lift (restrict (Icc a (a + p)) f)
      (_ :
        ∀ (a_1 b : ↑(Icc a (a + p))),
          EndpointIdent p a a_1 b → restrict (Icc a (a + p)) f a_1 = restrict (Icc a (a + p)) f b))
𝕜 : Type u_2
B : Type u_1
inst✝⁴ : LinearOrderedAddCommGroup 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝¹ : Archimedean 𝕜
inst✝ : TopologicalSpace B
f : 𝕜 → B
hf : f a = f (a + p)
hc : ContinuousOn f (Icc a (a + p))
⊢ Continuous
    (Quot.lift (restrict (Icc a (a + p)) f)
        (_ :
          ∀ (a_1 b : ↑(Icc a (a + p))),
            EndpointIdent p a a_1 b → restrict (Icc a (a + p)) f a_1 = restrict (Icc a (a + p)) f b) ∘
      ↑(equivIccQuot p a))
refine' Continuous.comp _ (homeoIccQuot p a).continuous_toFun
no goals
𝕜 : Type u_2
B : Type u_1
inst✝⁴ : LinearOrderedAddCommGroup 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : OrderTopology 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝¹ : Archimedean 𝕜
inst✝ : TopologicalSpace B
f : 𝕜 → B
hf : f a = f (a + p)
hc : ContinuousOn f (Icc a (a + p))
⊢ Continuous
    (Quot.lift (restrict (Icc a (a + p)) f)
      (_ :
        ∀ (a_1 b : ↑(Icc a (a + p))),
          EndpointIdent p a a_1 b → restrict (Icc a (a + p)) f a_1 = restrict (Icc a (a + p)) f b))
exact continuous_coinduced_dom.mpr (continuousOn_iff_continuous_restrict.mp hc)