extendDomain_apply_not_subtype

Mathlib.Logic.Equiv.Basic

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

English

If b ∈ β′ and ¬p(b), then e.extendDomain f(b) = b.

Русский

Если b ∈ β′ и не выполняется p(b), то e.extendDomain f(b) = b.

LaTeX

$$$\\text{If } \\neg p(b)\\text{ then } e.extendDomain f(b) = b$$$

Lean4

theorem extendDomain_apply_not_subtype {b : β'} (h : ¬p b) : e.extendDomain f b = b := by simp [Perm.extendDomain, h]

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

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

Разделы

Аффилиация

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