piCongrLeft_apply_apply

Mathlib.Topology.Homeomorph.Lemmas

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

← MathLib Explorer

English

For any e, x, and i, piCongrLeft e x (e i) = x i.

Русский

Для любого e, x и i выполняется piCongrLeft e x (e i) = x i.

LaTeX

$$$\pi\!CongrLeft\ e\ x\ (e\ i) = x\ i.$$$

Lean4

@[simp]
theorem piCongrLeft_apply_apply {ι ι' : Type*} {Y : ι' → Type*} [∀ j, TopologicalSpace (Y j)] (e : ι ≃ ι')
    (x : ∀ i, Y (e i)) (i : ι) : piCongrLeft e x (e i) = x i :=
  Equiv.piCongrLeft_apply_apply ..

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

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

Разделы

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

Аффилиация

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