comp — Mathlib

English

If f ⟂ RightInverse g and h ⟂ RightInverse i, then h ∘ f ⟂ g ∘ i.

Русский

Если f и g образуют правый обратный, и h и i образуют правый обратный, то их композиция образует правый обратный.

LaTeX

$$$\operatorname{RightInverse}(f,g) \Rightarrow \operatorname{RightInverse}(h\circ f,\ g\circ i).$$$

Lean4

theorem comp {f : α → β} {g : β → α} {h : β → γ} {i : γ → β} (hf : RightInverse f g) (hh : RightInverse h i) :
    RightInverse (h ∘ f) (g ∘ i) :=
  LeftInverse.comp hh hf

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