pullback_comm_sq

Mathlib.Data.Set.Prod

URI: https://scilib.ai/kg/mathlib#Function.pullback_comm_sq

English

The pullback diagonal Δ(f) is defined as the set { p in f.Pullback f | p.fst = p.snd }.

Русский

Диагональ в pullback определяется как множество { p ∈ f.Pullback f | p.fst = p.snd }.

LaTeX

$$$\\text{pullbackDiagonal}(f) = \\{ p \\in f\\text{.Pullback } f \\mid p.fst = p.snd \\}$$$

Lean4

theorem pullback_comm_sq (f : X → Y) (g : Z → Y) : f ∘ @fst X Y Z f g = g ∘ @snd X Y Z f g :=
  funext fun p ↦ p.2

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

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

Разделы

Аффилиация

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