exists_lift_trans_eq — Mathlib

English

There exists a k and a lift such that the lifted map lands on the diagonal range in the pullback diagram.

Русский

Существуют k и подъем так, что поднятая карта попадает в диагональный диапазон в диаграмме тяготы.

LaTeX

$$$\exists k\exists h_{k i}\exists h_{k j}\exists y: (pullback.lift(h_{k i}, h_{k j})).base(y)=x$$$

Lean4

theorem exists_lift_trans_eq {i j : 𝒰.I₀} (x : (pullback (𝒰.f i) (𝒰.f j)).carrier) :
    ∃ (k : 𝒰.I₀) (hki : k ⟶ i) (hkj : k ⟶ j) (y : 𝒰.X k),
      (pullback.lift (𝒰.trans hki) (𝒰.trans hkj) (by simp)).base y = x :=
  LocallyDirected.directed x

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