liftIoc — Mathlib

English

Given a function on 𝕜, liftIoc produces a function on AddCircle p that agrees with f on the interval (a, a+p].

Русский

Дано функцию на 𝕜, liftIoc порождает функцию на AddCircle p, которая совпадает с f на интервале (a, a+p].

LaTeX

$$$$ \mathrm{liftIoc}(p,a,f) = $(restrict $f$) \circ (\mathrm{equivIoc}(p,a)) $$ on $(a,a+p]$$$

Lean4

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

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