of_map — Mathlib

English

If f is injective and SemiconjBy (f a) (f x) (f y), then SemiconjBy a x y.

Русский

Если f инъективно и существует полусопряжение между f a, f x и f y, то имеется полусопряжение между a, x и y.

LaTeX

$$$Function.Injective f \rightarrow SemiconjBy (f a) (f x) (f y) \Rightarrow SemiconjBy a x y$$$

Lean4

@[to_additive]
protected theorem of_map [MulHomClass F M N] {f : F} (hf : Function.Injective f) (h : SemiconjBy (f a) (f x) (f y)) :
    SemiconjBy a x y :=
  hf (by simpa only [SemiconjBy, map_mul] using h)

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