pi_lift_π_apply' — Mathlib

English

Specialized universe version of pi_lift_π_apply; equality holds in the specialized universes.

Русский

Специализированная версия universes для pi_lift_π_apply, равенство выполняется в конкретных вселенных.

LaTeX

$$$\forall \beta\ (f: \beta \to Type v)\ (P: Type v)\ (s: \beta \to P \to f b)\ (b: \beta)\ (x: P),\; (Pi.π f b) (Pi.lift \beta _ _ f _ P s x) = s b x.$$$

Lean4

/-- A restatement of `Types.Limit.lift_π_apply` that uses `Pi.π` and `Pi.lift`,
with specialized universes. -/
theorem pi_lift_π_apply' {β : Type v} (f : β → Type v) {P : Type v} (s : ∀ b, P ⟶ f b) (b : β) (x : P) :
    (Pi.π f b : (piObj f) → f b) (@Pi.lift β _ _ f _ P s x) = s b x := by simp

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