pullbacks_monotone — Mathlib

English

If P ≤ Q then P.pullbacks ≤ Q.pullbacks. In words, forming pullbacks is monotone with respect to the morphism-property order.

Русский

Если P ≤ Q, то P.pullbacks ≤ Q.pullbacks. Иными словами, построение пулбэков монотонно по отношению свойств морфизмов.

LaTeX

$$P \le Q \Rightarrow P.pullbacks \le Q.pullbacks$$

Lean4

theorem pullbacks_monotone : Monotone (pullbacks (C := C)) :=
  by
  rintro _ _ h _ _ _ ⟨_, _, _, _, _, hp, sq⟩
  exact ⟨_, _, _, _, _, h _ hp, sq⟩

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