associated_map_mk — Mathlib

English

If f: Associates(M) →* M has a right inverse hinv with respect to mk, then for all a ∈ M, a is associated to f(mk(a)).

Русский

Если f: Associates(M) →* M имеет правый обратный к mk, то для любого a ∈ M a ассоциировано с f(mk(a)).

LaTeX

$$$ {f : \operatorname{Associates}(M) \to^* M} (hinv : \text{RightInverse } f \operatorname{Associates.mk}) \to (\forall a : M, a ~^{\sim}_u f(\operatorname{Associates.mk} a)) $$$

Lean4

theorem associated_map_mk {f : Associates M →* M} (hinv : Function.RightInverse f Associates.mk) (a : M) :
    a ~ᵤ f (Associates.mk a) :=
  Associates.mk_eq_mk_iff_associated.1 (hinv (Associates.mk a)).symm

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