mul_const_inv — Mathlib

English

If f is antiperiodic with c ≠ 0, then the image of the shifted interval uIcc(a, a + c) under f is the entire range of f.

Русский

Если f антипериодична с c ≠ 0, тогда образ смещённого интервала uIcc(a, a + c) под f равен всему диапазону значений f.

LaTeX

$$$f[uIcc(a,a+c)] = \mathrm{range}(f)$$$

Lean4

theorem mul_const_inv [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α} (ha : a ≠ 0) :
    Antiperiodic (fun x => f (x * a⁻¹)) (c * a) :=
  h.const_inv_smul₀ <| (MulOpposite.op_ne_zero_iff a).mpr ha

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