leftInverse_lcomapDomain_mapDomain

English

Exact equality of left inverse maps: the left inverse of lcomapDomain equals mapDomain via comapDomain_mapDomain.

Русский

Точная эквивалентность левого обратного: leftInverse(lcomapDomain) = mapDomain через comapDomain_mapDomain.

LaTeX

$$$\\text{leftInverse}_{}(lcomapDomain f hf) = mapDomain f$$$

Lean4

theorem leftInverse_lcomapDomain_mapDomain (f : α → β) (hf : Function.Injective f) :
    Function.LeftInverse (lcomapDomain (R := R) (M := M) f hf) (mapDomain f) :=
  comapDomain_mapDomain f hf

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