English
If f is p-periodic in the sense that f(a) = f(a+p), then lifting along the Ioc interval equals lifting along the Ico interval.
Русский
Если функция f периодична с периодом p в точке a, то подъем по интервалу Ioc равен подъем по интервалу Ico.
LaTeX
$$$$ \\mathrm{liftIoc}(p,a,f) = \\mathrm{liftIco}(p,a,f) \\quad \\text{whenever } f(a)=f(a+p). $$$$
Lean4
theorem liftIoc_eq_liftIco {f : 𝕜 → B} (hf : f a = f (a + p)) : liftIoc p a f = liftIco p a f :=
by
ext q
obtain ⟨x, hx, rfl⟩ := by simpa only [mem_image] using coe_image_Ico_eq p a ▸ mem_univ q
rw [liftIco_coe_apply hx]
obtain (⟨rfl, -⟩ | h) := by rwa [mem_Ico, le_iff_eq_or_lt, or_and_right] at hx
· rw [← coe_add_period, liftIoc_coe_apply (by simp [hp.out]), hf]
· exact liftIoc_coe_apply ⟨h.1, h.2.le⟩
