smul_iff — Mathlib

English

Boundedness at a cusp is equivalent to boundedness after a change of cusp by SL action.

Русский

Ограниченность в стыке эквивалентна после смены стыка действием SL.

LaTeX

$$IsBoundedAt(g·c,f,k) ↔ IsBoundedAt(c,f|[k]g,k)$$

Lean4

theorem smul_iff : IsBoundedAt (g • c) f k ↔ IsBoundedAt c (f ∣[k] g) k :=
  by
  rw [IsBoundedAt, IsBoundedAt, (Equiv.mulLeft g⁻¹).forall_congr_left]
  simp [MulAction.mul_smul, ← SlashAction.slash_mul]

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