liftIoc_eq_lift_Icc — Mathlib

English

Under a relation f(a)=f(a+p), the lift of f to Ioc agrees with the quotient lift of its restriction to Icc.

Русский

При условии f(a)=f(a+p) аппроксимация lift на Ioc совпадает с корректировкой по Icc ограниченного f.

LaTeX

$$$liftIoc\,p\,a\,f = Quot.lift (restrict (Icc(a, a+p))\,f) (by rintro _ _ ⟨_⟩, exact h) \\circ equivIccQuot p a$$$

Lean4

theorem liftIoc_eq_lift_Icc {f : 𝕜 → B} (h : f a = f (a + p)) :
    liftIoc p a f =
      Quot.lift (restrict (Icc a <| a + p) f)
          (by
            rintro _ _ ⟨_⟩
            exact h) ∘
        equivIccQuot p a :=
  by
  rw [← liftIco_eq_lift_Icc h]
  exact liftIoc_eq_liftIco h

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