liftIco_eq_lift_Icc — Mathlib

English

If f is p-periodic with f(a) = f(a+p), then lifting along Ico and lifting along Icc coincide via the endpoint-identification map.

Русский

Если f периодична с периодом p и f(a)=f(a+p), то подъем вдоль Ico и подъем вдоль Icc совпадают через отображение идентификации концов.

LaTeX

$$$$ \\mathrm{liftIco}(p,a,f) = \\mathrm{Quot}.\\mathrm{lift}( \\mathrm{restrict} (\\mathrm{Icc}(a, a+p))\, f) \\circ \\mathrm{equivIccQuot}(p,a) $$$$

Lean4

theorem liftIco_eq_lift_Icc {f : 𝕜 → B} (h : f a = f (a + p)) :
    liftIco p a f =
      Quot.lift (restrict (Icc a <| a + p) f)
          (by
            rintro _ _ ⟨_⟩
            exact h) ∘
        equivIccQuot p a :=
  rfl

Похожие утверждения