semiconjBy_map_iff — Mathlib

English

If f is injective, then SemiconjBy (f a) (f x) (f y) is equivalent to 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) \Leftrightarrow SemiconjBy a x y)$$$

Lean4

@[to_additive]
theorem semiconjBy_map_iff [MulHomClass F M N] {f : F} (hf : Function.Injective f) {x y : M} :
    SemiconjBy (f a) (f x) (f y) ↔ SemiconjBy a x y :=
  ⟨.of_map hf, (.map · f)⟩

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