piecewise_idem_right — Mathlib

English

Right idempotence: applying piecewise on the right twice is the same as one application.

Русский

Правоидемпотентность: повторное применение справа даёт тот же результат, что и одно применение.

LaTeX

$$$s.\\text{piecewise} f (s.\\text{piecewise} g_1 g_2) = s.\\text{piecewise} f g_2.$$$

Lean4

@[simp]
theorem piecewise_idem_right (f g₁ g₂ : ∀ a, π a) : s.piecewise f (s.piecewise g₁ g₂) = s.piecewise f g₂ :=
  piecewise_piecewise_of_subset_right (Subset.refl _) f g₁ g₂

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