left_apply

Mathlib.Logic.Equiv.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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