English
Left idempotence: applying piecewise twice on the left with the same s gives the same as a single application.
Русский
Левоидемпотентность: повторное применение piecewise слева с тем же s даёт такое же, как и одно применение.
LaTeX
$$$s.\\text{piecewise}(s.\\text{piecewise} f_1 f_2) g = s.\\text{piecewise} f_1 g.$$$
Lean4
@[simp]
theorem piecewise_idem_left (f₁ f₂ g : ∀ a, π a) : s.piecewise (s.piecewise f₁ f₂) g = s.piecewise f₁ g :=
piecewise_piecewise_of_subset_left (Subset.refl _) _ _ _