comp — Mathlib

English

If hf' and hg' are left inverses on appropriate sets and hf maps S to T, then the composition f' ∘ g' is a left inverse on S for g ∘ f.

Русский

Если hf' и hg' — левые обратно на соответствующих множествах и hf отображает S в T, то композиция f' ∘ g' является левым обратным на S для g ∘ f.

LaTeX

$$$$ \\text{LeftInvOn } (f' \\circ g') (g \\circ f) S. $$$$

Lean4

theorem comp (hf' : LeftInvOn f' f s) (hg' : LeftInvOn g' g t) (hf : MapsTo f s t) : LeftInvOn (f' ∘ g') (g ∘ f) s :=
  fun x h =>
  calc
    (f' ∘ g') ((g ∘ f) x) = f' (f x) := congr_arg f' (hg' (hf h))
    _ = x := hf' h

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