comm — Mathlib

English

If χ' yields a pullback with m and χ₀, then χ' equals χ m.

Русский

Если χ' образует pullback с m и χ₀, то χ' = χ m.

LaTeX

$$∀ χ' (hχ' : IsPullback m (Classifier.χ₀ U) χ' (truth C)) → χ' = χ m$$

Lean4

/-- The diagram
```
      U ---------m----------> X
      |                       |
    χ₀ U                     χ m
      |                       |
      v                       v
      Ω₀ ------truth--------> Ω
```
commutes.
-/
@[reassoc]
theorem comm : m ≫ χ m = Classifier.χ₀ _ U ≫ truth C :=
  (isPullback_χ m).w

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