preimage_pullbackDiagonal

Mathlib.Data.Set.Prod

URI: https://scilib.ai/kg/mathlib#Function.Injective.preimage_pullbackDiagonal

← MathLib Explorer

English

The range of the map x ↦ (x, x) equals the diagonal Δ(α).

Русский

Область значений отображения x ↦ (x, x) равна диагонали Δ(α).

LaTeX

$$$\\operatorname{range}(\\lambda x. (x,x)) = \\Delta(\\alpha)$$$

Lean4

theorem preimage_pullbackDiagonal {f : X → Y} {g : Z → X} (inj : g.Injective) :
    mapPullback g id g (by rfl) (by rfl) ⁻¹' pullbackDiagonal f = pullbackDiagonal (f ∘ g) :=
  ext fun _ ↦ inj.eq_iff

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

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

Разделы

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

Аффилиация

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