isFibrant_of_fibration — Mathlib

English

If p: X→Y is a fibration and Y is fibrant, then X is fibrant.

Русский

Если p: X→Y является фибрацией, а Y — фибривант, то X является фибривантом.

LaTeX

$$$\forall p:\, X\to Y,\ [\text{Fibration}(p)] \land [\text{IsFibrant}(Y)] \Rightarrow \text{IsFibrant}(X)$$$

Lean4

theorem isFibrant_of_fibration [(fibrations C).IsStableUnderComposition] {X Y : C} (p : X ⟶ Y) [Fibration p]
    [hY : IsFibrant Y] : IsFibrant X := by
  rw [isFibrant_iff] at hY ⊢
  rw [Subsingleton.elim (terminal.from X) (p ≫ terminal.from Y)]
  infer_instance

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