piecewise_eq_of_notMem

Mathlib.Data.Set.Piecewise

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

English

If i ∉ s, then (s.piecewise f g)(i) = g(i).

Русский

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

LaTeX

$$$i \\notin s \\Rightarrow (s.\\mathrm{piecewise} f g)(i) = g(i)$$$

Lean4

@[simp]
theorem piecewise_eq_of_notMem {i : α} (hi : i ∉ s) : s.piecewise f g i = g i :=
  if_neg hi

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

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

Разделы

Аффилиация

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