sumCompl_apply_inr

Mathlib.Logic.Equiv.Sum

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

English

Within sumCompl, taking inr x yields x.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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