right_apply

Mathlib.Logic.Equiv.Basic

URI: https://scilib.ai/kg/mathlib#Equiv.Perm.subtypeCongr.right_apply

English

If h is a proof that ¬p a, then ep.subtypeCongr en a = en ⟨a,h⟩.

Русский

Если доказано, что ¬p(a), то ep.subtypeCongr en a = en ⟨a,h⟩.

LaTeX

$$$ ep.subtypeCongr en a = en(\\langle a, h \\rangle) \\quad (\\text{when } ¬p(a)). $$$

Lean4

@[simp]
theorem right_apply {a : ε} (h : ¬p a) : ep.subtypeCongr en a = en ⟨a, h⟩ := by simp [Perm.subtypeCongr.apply, h]

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

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

Разделы

Аффилиация

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