right_apply_subtype

Mathlib.Logic.Equiv.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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