le_pullbacks — Mathlib

English

For any morphism q, if q has property P, then the pullbacks involving q satisfy the corresponding pullback property.

Русский

Для любого морфизма q, если q удовлетворяет P, то соответствующие пуллбэки удовлетворяют свойству pullbacks.

LaTeX

$$P(q) \Rightarrow P.pullbacks(q)$$

Lean4

theorem le_pullbacks : P ≤ P.pullbacks := by
  intro A B q hq
  exact P.pullbacks_mk IsPullback.of_id_fst hq

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