piecewise_range_comp — Mathlib

English

For a function f:ι→α, the piecewise construction on range f satisfies: (range f).piecewise g1 g2 ∘ f = g1 ∘ f.

Русский

Для функции f:ι→α конструкция piecewise на диапазоне range(f) удовлетворяет: (range f).piecewise g1 g2 ∘ f = g1 ∘ f.

LaTeX

$$$\\bigl((\\mathrm{range}\\,f).\\mathrm{piecewise} g_1 g_2\\bigr) \\circ f = g_1 \\circ f$$$

Lean4

@[simp]
theorem piecewise_range_comp {ι : Sort*} (f : ι → α) [∀ j, Decidable (j ∈ range f)] (g₁ g₂ : α → β) :
    (range f).piecewise g₁ g₂ ∘ f = g₁ ∘ f :=
  (piecewise_eqOn ..).comp_eq

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