map_resLE — Mathlib

English

If U = U' and V = V', restricting f along e gives the same morphism as restricting f along e' with the corresponding equality corrections.

Русский

Если U = U' и V = V', ограничение f вдоль e даёт тот же морфизм, что и ограничение вдоль e' с учётом соответствующих равенств.

LaTeX

$$$\forall (e:equality),\; P(f.resLE U V e) \Rightarrow P(f.resLE U' V' (e'\,\text{via}\, e))$$$

Lean4

@[reassoc (attr := simp)]
theorem map_resLE (i : V' ≤ V) : X.homOfLE i ≫ f.resLE U V e = f.resLE U V' (i.trans e) := by
  simp_rw [← resLE_id, resLE_comp_resLE, Category.id_comp]

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