extendDomain_apply_subtype

Mathlib.Logic.Equiv.Basic

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

English

For b ∈ β′ with p b, e.extendDomain f b = f (e (f.symm ⟨b, h⟩)).

Русский

Для b ∈ β′ с p b выполняется e.extendDomain f b = f (e (f.symm ⟨b, h⟩)).

LaTeX

$$$\\text{If } h: p(b)\\text{ then } e.extendDomain f(b) = f(e(f^{-1}(b,h)))$$$

Lean4

theorem extendDomain_apply_subtype {b : β'} (h : p b) : e.extendDomain f b = f (e (f.symm ⟨b, h⟩)) := by
  simp [Perm.extendDomain, h]

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

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

Разделы

Аффилиация

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