lift_snd — Mathlib

English

In the relative representability setup, lift i h hi on the right yields h when composed with hf.snd g.

Русский

В контексте относительной представительности подъём вправо даёт h при компоновке с hf.snd g.

LaTeX

$$$$ hf.lift i h hi \\;\\circ\\; hf.snd g = h $$$$

Lean4

@[reassoc (attr := simp)]
theorem lift_snd [Full F] [Faithful F] : hf.lift i h hi ≫ hf.snd g = h :=
  F.map_injective <| by simpa [lift] using PullbackCone.IsLimit.lift_snd _ _ _ _

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