piecewise_compl

Mathlib.Data.Set.Piecewise

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

← MathLib Explorer

English

Complementary piecewise relation: (sᶜ).piecewise f g = s.piecewise g f.

Русский

Отношение piecewise по дополнению: (sᶜ).piecewise f g = s.piecewise g f.

LaTeX

$$$\\text{piecewise}_{s^{\\complement}}(f,g) = \\text{piecewise}_{s}(g,f)$$$

Lean4

@[simp]
theorem piecewise_compl [∀ i, Decidable (i ∈ sᶜ)] : sᶜ.piecewise f g = s.piecewise g f :=
  funext fun x => if hx : x ∈ s then by simp [hx] else by simp [hx]

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

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

Разделы

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

Аффилиация

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