comap_conGen_of_bijective — Mathlib

English

If f is bijective, then Con.comap f H (conGen rel) equals conGen (λ x y, rel (f x) (f y)).

Русский

Если f биективна, то Con.comap f H (conGen rel) равняется conGen (λ x y, rel (f x) (f y)).

LaTeX

$$Con.comap f H (conGen rel) = conGen (fun x y ↦ rel (f x) (f y))$$

Lean4

@[to_additive]
theorem comap_conGen_of_bijective {M N : Type*} [Mul M] [Mul N] (f : M → N) (hf : Function.Bijective f)
    (H : ∀ (x y : M), f (x * y) = f x * f y) (rel : N → N → Prop) :
    Con.comap f H (conGen rel) = conGen (fun x y ↦ rel (f x) (f y)) :=
  comap_conGen_equiv (MulEquiv.ofBijective (MulHom.mk f H) hf) rel

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