piecewise_inv — Mathlib

English

Taking inverses commutes with piecewise: the piecewise of f1^{-1} and g1^{-1} equals the inverse of the piecewise f1 g1.

Русский

Степень инверсий совместима с разбиением на куски: piecewise f1^{-1} g1^{-1} = (piecewise f1 g1)^{-1}.

LaTeX

$$$s.piecewise f_1^{-1} g_1^{-1} = (s.piecewise f_1 g_1)^{-1}$$$

Lean4

@[to_additive]
theorem piecewise_inv [∀ i, Inv (f i)] (s : Set I) [∀ i, Decidable (i ∈ s)] (f₁ g₁ : ∀ i, f i) :
    s.piecewise f₁⁻¹ g₁⁻¹ = (s.piecewise f₁ g₁)⁻¹ :=
  s.piecewise_op f₁ g₁ fun _ x => x⁻¹

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