inv_comp — Mathlib

English

If f: β → γ and g: α → β are continuous and γ has a continuous inverse, then the inverse of the composition satisfies (f⁻¹) ∘ g = (f ∘ g)⁻¹.

Русский

Пусть f: β → γ и g: α → β непрерывны, и γ имеет непрерывное обратное. Тогда (f⁻¹) ∘ g = (f ∘ g)⁻¹.

LaTeX

$$$\forall f:\ C(β,γ),\ \forall g:\ C(α,β): (f^{-1}).\,comp\,g = (f.\,comp\,g)^{-1}.$$$

Lean4

@[to_additive (attr := simp)]
theorem inv_comp [Inv γ] [ContinuousInv γ] (f : C(β, γ)) (g : C(α, β)) : f⁻¹.comp g = (f.comp g)⁻¹ :=
  rfl

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