lift₂_def₂ — Mathlib

English

The value of lift₂ at a pair x,y from index i is ih i (f₁ i j h x) and (f₂ i j h y) projected in the limit.

Русский

Значение lift₂ на пару x,y из индекса i равно ih i (f₁ i j h x) и ih i (f₂ i j h y) после отображения в предел.

LaTeX

$$$\\mathrm{lift\\_2\\_def}\\;(x,y,i,h\\xi,h\\yi) : \\mathrm{DirectLimit.lift\\_2}\\; f_1\\; f_2\\; ih\\; compat \\; (⟦x⟧, ⟦y⟧) = ih(i, f_1 x, f_2 y)$$$

Lean4

theorem lift₂_def₂ (x : Σ i, F₁ i) (y : Σ i, F₂ i) (i) (hxi : x.1 ≤ i) (hyi : y.1 ≤ i) :
    DirectLimit.lift₂ f₁ f₂ ih compat ⟦x⟧ ⟦y⟧ = ih i (f₁ _ _ hxi x.2) (f₂ _ _ hyi y.2) :=
  (lift₂Aux _ _ _ compat _ _).2 ..

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