piecewise_cases — Mathlib

English

A variant of piecewise_insert with similar equality; the inserted case reduces to an update of the previous piecewise definition.

Русский

Вариант утверждения про вставку, аналогично piecewise_insert, где вставленный элемент сводится к обновлению предыдущего определения.

LaTeX

$$Same form as piecewise_insert: $(\\mathrm{insert}\\ j\\ s).\\text{piecewise } f g = \\mathrm{update} (s.\\text{piecewise } f g) j (f j).$$$

Lean4

theorem piecewise_cases {i} (p : π i → Prop) (hf : p (f i)) (hg : p (g i)) : p (s.piecewise f g i) := by
  by_cases hi : i ∈ s <;> simpa [hi]

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