resLE_map — Mathlib

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]

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