left_apply_subtype

Mathlib.Logic.Equiv.Basic

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

English

For a ∈ {x | p x}, ep.subtypeCongr en a = ep a.

Русский

Для a ∈ {x | p x}, ep.subtypeCongr en a = ep a.

LaTeX

$$$ ep.subtypeCongr en a = ep(a) \\quad (a \\in {x \\mid p(x)}). $$$

Lean4

@[simp]
theorem left_apply_subtype (a : { a // p a }) : ep.subtypeCongr en a = ep a :=
  Perm.subtypeCongr.left_apply ep en a.property

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

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

Разделы

Аффилиация

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