pi_lift_π_apply — Mathlib

English

For β, f: β → Type(u), P and s, the Pi and lift interact as expected: (Pi.π g b) (Pi.map α x) equals α b (Pi.π f b x).

Русский

Для β, f: β → Type(u), P и s, Pi и lift взаимодействуют как ожидается: (Pi.π g b) (Pi.map α x) = α b (Pi.π f b x).

LaTeX

$$$(Pi.\\pi\ \ g\ b)\ (Pi.map\\ α\ x) = α.b\\ (Pi.\\pi\ f\ b\ x).$$$

Lean4

/-- A restatement of `Types.Limit.lift_π_apply` that uses `Pi.π` and `Pi.lift`. -/
-- The increased `@[simp]` priority here results in a minor speed up in
-- `Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean`.

@[simp 1001]
theorem pi_lift_π_apply {β : Type v} [Small.{u} β] (f : β → Type u) {P : Type u} (s : ∀ b, P ⟶ f b) (b : β) (x : P) :
    (Pi.π f b : (piObj f) → f b) (@Pi.lift β _ _ f _ P s x) = s b x :=
  congr_fun (limit.lift_π (Fan.mk P s) ⟨b⟩) x

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