comp — Mathlib

English

If f has left inverse g and h has left inverse i, then h ∘ f has left inverse g ∘ i.

Русский

Если f имеет левый обратный g и h имеет левый обратный i, то h ∘ f имеет левый обратный g ∘ i.

LaTeX

$$$\text{If } \operatorname{LeftInverse}(f,g) \text{ and } \operatorname{LeftInverse}(h,i),\ \operatorname{LeftInverse}(h\circ f,\ g\circ i).$$$

Lean4

theorem comp {f : α → β} {g : β → α} {h : β → γ} {i : γ → β} (hf : LeftInverse f g) (hh : LeftInverse h i) :
    LeftInverse (h ∘ f) (g ∘ i) := fun a ↦ show h (f (g (i a))) = a by rw [hf (i a), hh a]

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