piecewise_insert_self

Mathlib.Data.Finset.Piecewise

URI: https://scilib.ai/kg/mathlib#Finset.piecewise_insert_self

← MathLib Explorer

English

If s ⊆ t, then s.piecewise (t.piecewise f1 f2) g = s.piecewise f1 g.

Русский

Если s ⊆ t, то s.piecewise (t.piecewise f1 f2) g = s.piecewise f1 g.

LaTeX

$$$s\\mathrm{.piecewise}(t\\mathrm{.piecewise} f_1 f_2)\\; g = s\\mathrm{.piecewise} f_1 g$$$

Lean4

theorem piecewise_insert_self [DecidableEq ι] {j : ι} [∀ i, Decidable (i ∈ insert j s)] :
    (insert j s).piecewise f g j = f j := by simp [piecewise]

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

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

Разделы

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

Аффилиация

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