coe_sumSet

Mathlib.Logic.Embedding.Set

URI: https://scilib.ai/kg/mathlib#Function.Embedding.coe_sumSet

English

The underlying function of sumSet is the standard Sum.elim when coercing to function.

Русский

Базовая функция sumSet при приводе к функции равна обычному Sum.elim.

LaTeX

$$$\\text{coe}(\\text{sumSet } h) = \\text{Sum.elim } (\\uparrow) (\\uparrow)$$$

Lean4

@[norm_cast]
theorem coe_sumSet (h : Disjoint s t) : (Function.Embedding.sumSet h : s ⊕ t → α) = Sum.elim (↑) (↑) :=
  rfl

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

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

Разделы

Аффилиация

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