piCongrLeft_symm_apply

Mathlib.Topology.Homeomorph.Lemmas

URI: https://scilib.ai/kg/mathlib#Homeomorph.piCongrLeft_symm_apply

← MathLib Explorer

English

The inverse of piCongrLeft e is piCongrLeft of the inverse bijection e^{-1}.

Русский

Обратное к piCongrLeft e — это piCongrLeft для биекции e^{-1}.

LaTeX

$$$ (\pi\!CongrLeft\ e)^{-1} = \pi\!CongrLeft\ (e^{-1}).$$$

Lean4

@[simp]
theorem piCongrLeft_symm_apply {ι ι' : Type*} {Y : ι' → Type*} [∀ j, TopologicalSpace (Y j)] (e : ι ≃ ι') :
    ⇑(piCongrLeft (Y := Y) e).symm = (· <| e ·) :=
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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