equalizerCondition_w — Mathlib

English

A streamlined equalizer condition for pullbacks in a regular topology setting.

Русский

Упрощённое условие равнителя для пулбеков в контексте регуларной топологии.

LaTeX

$$$EqualizerCondition_w := \dots$$$

Lean4

theorem equalizerCondition_w (P : Cᵒᵖ ⥤ D) {X B : C} {π : X ⟶ B} (c : PullbackCone π π) :
    P.map π.op ≫ P.map c.fst.op = P.map π.op ≫ P.map c.snd.op := by
  simp only [← Functor.map_comp, ← op_comp, c.condition]

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