isPullback_χ — Mathlib

English

The square with m, χ₀, χ, truth is a pullback.

Русский

Квадрат с m, χ₀, χ, truth является обязательной диаграммой притягивания (pullback).

LaTeX

$$IsPullback m (Classifier.χ₀ U) χ m.truth C$$

Lean4

/-- The diagram
```
      U ---------m----------> X
      |                       |
    χ₀ U                     χ m
      |                       |
      v                       v
      Ω₀ ------truth--------> Ω
```
is a pullback square.
-/
theorem isPullback_χ : IsPullback m (Classifier.χ₀ _ U) (χ m) (truth C) :=
  Classifier.isPullback _ m

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