of_injective — Mathlib

English

The iterate-action type IterateMulAct f is countable for any f: α → α.

Русский

Тип действия на итераты IterateMulAct f счетен для любого отображения f: α → α.

LaTeX

$$Countable(IterateMulAct f)$$

Lean4

theorem of_injective {R M : Type*} [SMul R M] {N F} [SMul R N] [FunLike F M N] [MulActionHomClass F R M N] (f : F)
    {r : R} (h1 : Function.Injective f) (h2 : IsSMulRegular N r) : IsSMulRegular M r := fun x y h3 =>
  h1 <| h2 <| (map_smulₛₗ f r x).symm.trans ((congrArg f h3).trans (map_smulₛₗ f r y))

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