piecewise_idem_left — Mathlib

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 _) _ _ _

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