comp — Mathlib

English

If f' is a left-right inverse relation with f on s,t, then swapping the roles gives an inverse relation on t,s.

Русский

Если f' и f образуют взаимно обратимость на s,t, тогда f и f' образуют взаимно обратимость на t,s.

LaTeX

$$$$\\operatorname{InvOn}(f', f, s, t) \\Rightarrow \\operatorname{InvOn}(f, f', t, s).$$$$

Lean4

theorem comp (hf : InvOn f' f s t) (hg : InvOn g' g t p) (fst : MapsTo f s t) (g'pt : MapsTo g' p t) :
    InvOn (f' ∘ g') (g ∘ f) s p :=
  ⟨hf.1.comp hg.1 fst, hf.2.comp hg.2 g'pt⟩

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