coe_resLE_base — Mathlib

English

The app on global sections factors through resLE: the resLE map from functions on Y over U to X over V followed by the restriction to the top-level opens equals the app map after applying resLE.

Русский

Факторизация отображения app через ограничение: отображение appLE от секций над U в X над V затем ограничение равно отображению app после применения resLE.

LaTeX

$$$\mathrm{resLE}\,f\,U\,V\,e \;\gg\; \mathrm{appLE} = \mathrm{appLE}\,(f U V e)$$$

Lean4

@[simp]
theorem coe_resLE_base (x : V) : ((f.resLE U V e).base x).val = f.base x := by simp [resLE, morphismRestrict_base]

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