single_apply_mem

Mathlib.Data.Finsupp.Single

URI: https://scilib.ai/kg/mathlib#Finsupp.single_apply_mem

English

For DecidableEq α, the function single a b equals Pi.single a b.

Русский

При DecidableEq для α, single a b равен Pi.single a b.

LaTeX

$$$$\\text{If } [\\text{DecidableEq } \\alpha],\\; \\text{single } a\\, b = \\Pi.single\\, a\\, b.$$$$

Lean4

theorem single_apply_mem (x) : single a b x ∈ ({0, b} : Set M) := by
  rcases em (x = a) with (rfl | hx) <;> [simp; simp [hx]]

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

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

Разделы

Аффилиация

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