English
If i is an inclusion V ≤ V' of opens in X, then pushing i through the left side corresponds to refining the open set on the target: X.homOfLE i ≫ f.resLE U V e = f.resLE U V' (i.trans e).
Русский
Если i — вложение V ≤ V' открытых подмножеств X, то слева композиция с i равна ограничению после уточнения открытого множества на цели: X.homOfLE i ≫ f.resLE U V e = f.resLE U V' (i.trans e).
LaTeX
$$$X.homOfLE(i) \;\gg\; f.resLE\;U\;V\;e = f.resLE\;U\;V'\;(i.trans\;e)$$$
Lean4
@[reassoc (attr := simp)]
theorem resLE_map (i : U ≤ U') :
f.resLE U V e ≫ Y.homOfLE i = f.resLE U' V (e.trans ((Opens.map f.base).map i.hom).le) := by
simp_rw [← resLE_id, resLE_comp_resLE, Category.comp_id]