eqOn — Mathlib

English

If h is a left inverse relation on a set s, then the composition f' ∘ f agrees with the identity on s.

Русский

Если h задаёт левые обратности на множество s, то композиция f' ∘ f совпадает с тождеством на s.

LaTeX

$$$$ \\text{If } h : \\text{LeftInvOn } f' f s, \\; \\text{then } (f' \\circ f)|_s = \\mathrm{id}_s. $$$$

Lean4

theorem eqOn (h : LeftInvOn f' f s) : EqOn (f' ∘ f) id s :=
  h

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