sumCompl_apply_inl

Mathlib.Logic.Equiv.Sum

URI: https://scilib.ai/kg/mathlib#Equiv.sumCompl_apply_inl

English

Within sumCompl, taking inl x yields x.

Русский

Внутри sumCompl, применение inl к x даёт x.

LaTeX

$$$$\mathrm{sumCompl}(p)(\mathrm{inl}(x)) = x.$$$$

Lean4

@[simp]
theorem sumCompl_apply_inl {α} (p : α → Prop) [DecidablePred p] (x : { a // p a }) : sumCompl p (Sum.inl x) = x :=
  rfl

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

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

Разделы

Аффилиация

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