instIsMultiplicativeFibrations — Mathlib

English

The class of fibrations is closed under products, under the structure provided by a weak factorization system.

Русский

Класс фибраций замыкается на произведения; это следует из структуры слабой факторизационной системы.

LaTeX

$$$\operatorname{IsMultiplicative}(\operatorname{fibrations}C)$$$

Lean4

instance : (fibrations C).IsMultiplicative :=
  by
  rw [← trivialCofibrations_rlp]
  infer_instance

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