instInvOfContinuousInv — Mathlib

English

If β has an inverse and the inversion is continuous, then the space of continuous maps α → β has an inverse operation defined pointwise: for f ∈ C(α,β), f⁻¹ is the map x ↦ (f(x))⁻¹.

Русский

Если β обладает обратной, и обратная операция непрерывна, то множество непрерывных отображений α → β имеет операцию обратного поэтапно: для f ∈ C(α,β) получаем f⁻¹, определённое как x ↦ (f(x))⁻¹.

LaTeX

$$$\forall f:\ C(\alpha,\beta),\ (f)^{-1} = x \mapsto (f(x))^{-1}.$$$

Lean4

@[to_additive]
instance [Inv β] [ContinuousInv β] : Inv C(α, β) where inv f := ⟨f⁻¹, f.continuous.inv⟩

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