of_smul_eq — Mathlib

English

If f: M → N preserves smul in the sense f(c) • x = c • x for all c and x, and M acts pretransitively on α, then N acts pretransitively on α as well.

Русский

Если отображение f сохраняет умножение действий: f(c)•x = c•x, и M действует предпереставимо на α, тогда N действует предпереставимо на α.

LaTeX

$$$\\forall c\\in M, x\\in α: f(c) \\cdot x = c \\cdot x \\implies \\text{IsPretransitive } N \\alpha$$$

Lean4

@[to_additive]
theorem of_smul_eq {M N α : Type*} [SMul M α] [SMul N α] [IsPretransitive M α] (f : M → N)
    (hf : ∀ {c : M} {x : α}, f c • x = c • x) : IsPretransitive N α where
  exists_smul_eq x y := (exists_smul_eq x y).elim fun m h ↦ ⟨f m, hf.trans h⟩

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