piecewise_insert_of_ne

Mathlib.Data.Set.Piecewise

URI: https://scilib.ai/kg/mathlib#Set.piecewise_insert_of_ne

← MathLib Explorer

English

If i ≠ j, then (insert j s).piecewise f g i = (s.piecewise f g i).

Русский

Если i ≠ j, то (insert j s).piecewise f g i = (s.piecewise f g i).

LaTeX

$$$i \\neq j \\Rightarrow (\\mathrm{piecewise}_{\\mathrm{insert}(j,s)} f g)(i) = (\\mathrm{piecewise}_{s} f g)(i)$$$

Lean4

@[simp]
theorem piecewise_insert_of_ne {i j : α} (h : i ≠ j) [∀ i, Decidable (i ∈ insert j s)] :
    (insert j s).piecewise f g i = s.piecewise f g i := by simp [piecewise, h]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru