range_toPullbackDiag

Mathlib.Data.Set.Prod

URI: https://scilib.ai/kg/mathlib#range_toPullbackDiag

← MathLib Explorer

English

The range of toPullbackDiag f is the pullback diagonal Δ(f).

Русский

Область значений toPullbackDiag f равна диагонали pullback Δ(f).

LaTeX

$$$\\operatorname{range}(\\text{toPullbackDiag } f) = \\text{pullbackDiagonal}(f)$$$

Lean4

theorem range_toPullbackDiag (f : X → Y) : range (toPullbackDiag f) = pullbackDiagonal f := by
  rw [← image_univ, image_toPullbackDiag, univ_prod_univ, preimage_univ, inter_univ]

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

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

Разделы

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

Аффилиация

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