lift₂_def — Mathlib

English

There is a map between two direct limits built from ih and compat, sending ⟦⟨i,x⟩⟧ to ⟦⟨i, ih i x⟩⟧.

Русский

Существует отображение между пределами, построенное из ih и совместимости; отправляет ⟦⟨i,x⟩⟧ в ⟦⟨i, ih i x⟩⟧.

LaTeX

$$$\\mathrm{DirectLimit.map}\\; f_1\\; f_2\\; ih\\; compat : \\mathrm{DirectLimit}(F_1,f_1) \\to \\mathrm{DirectLimit}(F_2,f_2)$ with $\\mathrm{map}(z) = z.lift\\_2\\; w$$$

Lean4

theorem lift₂_def (i x y) : DirectLimit.lift₂ f₁ f₂ ih compat ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧ = ih i x y := by
  rw [lift₂_def₂ _ _ _ _ _ _ i le_rfl le_rfl, map_self', map_self']

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