map₂_def₂ — Mathlib

English

For any i, if x,y come from F_i with hxi/hyi ≤ i, then map₂ f₁ f₂ f ih compat ⟦x⟧ ⟦y⟧ equals ⟦⟨i, ih i (f₁ i j hxi x) (f₂ i j hyi y)⟩⟧.

Русский

Для любых i, если x,y происходят из F_i и их индексы удовлетворяют неравенствам, тогда map₂_def₂ даёт нужное представление.

LaTeX

$$$\\mathrm{map\\_2\\_def\\_2}\\; (x,y,i,hxi,h yi) : \\mathrm{map\\_2}\\; f_1\\; f_2\\; f\\; ih\\; compat\\; ⟦x⟧ ⟦y⟧ = ⟦⟨i, ih i (f_1 \\_ \\_ hxi x) (f_2 \\_ \\_ hyi y)⟩⟧$$$

Lean4

theorem map₂_def₂ (x y) (i) (hxi : x.1 ≤ i) (hyi : y.1 ≤ i) :
    map₂ f₁ f₂ f ih compat ⟦x⟧ ⟦y⟧ = ⟦⟨i, ih i (f₁ _ _ hxi x.2) (f₂ _ _ hyi y.2)⟩⟧ :=
  lift₂_def₂ ..

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