trivialFibrations_sub_weakEquivalences

English

For any C with Fibrations and WeakEquivalences, trivialFibrations C is contained in weakEquivalences C.

Русский

Если заданы фибрации и слабые эквалентности, тривиальные фибрации лежат внутри слабых эквалентностей.

LaTeX

$$$\text{trivialFibrations } C \leq \text{weakEquivalences } C$$$

Lean4

theorem trivialFibrations_sub_weakEquivalences : trivialFibrations C ≤ weakEquivalences C := fun _ _ _ hf ↦ hf.2

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