liftIco — Mathlib

English

The liftIoc operator converts a function f: 𝕜 → B into a function AddCircle p → B by composing with the inverse of equivIoc p a and restricting to Ioc a (a+p).

Русский

Оператор liftIoc превращает функцию f: 𝕜 → B в функцию AddCircle p → B, композиции с обратной функцией equivIoc p a и ограничение на Ioc a (a+p).

LaTeX

$$$$ \mathrm{liftIoc}(p,a,f) = \mathrm{restrict}_{{\mathsf{Ioc}}\ a\ (a+p)} f \circ (\mathrm{equivIoc}(p,a))^{-1} $$$$

Lean4

/-- Given a function on `𝕜`, return the unique function on `AddCircle p` agreeing with `f` on
`[a, a + p)`. -/
def liftIco (f : 𝕜 → B) : AddCircle p → B :=
  restrict _ f ∘ AddCircle.equivIco p a

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