piecewise_empty

Mathlib.Data.Set.Piecewise

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

English

The piecewise construction with the empty set yields the second function g.

Русский

Конструкция piecewise над пустым множеством даёт вторую функцию g.

LaTeX

$$$\\text{piecewise}_{\\emptyset}(f,g) = g$$$

Lean4

@[simp]
theorem piecewise_empty [∀ i : α, Decidable (i ∈ (∅ : Set α))] : piecewise ∅ f g = g :=
  by
  ext i
  simp [piecewise]

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

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

Разделы

Аффилиация

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