pi_map_π_apply — Mathlib

English

A restatement of Limit.map_π_apply using Pi.π and Pi.map: the equality holds for Pi objects.

Русский

Переформулирование Limit.map_π_apply через Pi.π и Pi.map: равенство сохраняется.

LaTeX

$$$\forall {\beta : Type v} [Small.{u} {\beta}] {f g : (\beta \to Type u)} (\alpha : \forall j, f j \to g j) (b : \beta) (x : \text{Limit}.\pi f b)\; ,\; \text{Eq}(\text{Pi}.π g b (\text{Pi}.map α x), \alpha b (\text{Pi}.π f b x)).$$$

Lean4

/-- A restatement of `Types.Limit.map_π_apply` that uses `Pi.π` and `Pi.map`. -/
-- Not `@[simp]` since `simp` can prove it.

theorem pi_map_π_apply {β : Type v} [Small.{u} β] {f g : β → Type u} (α : ∀ j, f j ⟶ g j) (b : β) (x) :
    (Pi.π g b : ∏ᶜ g → g b) (Pi.map α x) = α b ((Pi.π f b : ∏ᶜ f → f b) x) :=
  Limit.map_π_apply.{v, u} _ _ _

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