instHasLiftingPropertyιHornHAddNatOfNatOfFibration

English

For a morphism f with a fibration structure, the horn inclusion (horn ⟨n⟩ i).ι has the lifting property with respect to f for each i.

Русский

Для морфизма f с фибрацией: включение рога (horn ⟨n⟩ i).ι обладает свойством подстановки по отношению к f для каждого i.

LaTeX

$$$ [\\text{Fibration}(f)] \\Rightarrow \\mathrm{HasLiftingProperty}((\\mathrm{horn}(n+1,i)).\\iota, f)$$$

Lean4

instance [hf : Fibration f] {n : ℕ} (i : Fin (n + 2)) : HasLiftingProperty (horn (n + 1) i).ι f :=
  by
  rw [fibration_iff] at hf
  exact hf _ (horn_ι_mem_J _ _)

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