resLE_id — Mathlib

English

If i is an inclusion V ≤ V' between opens of X, restricting the identity morphism along i yields the canonical restriction X.homOfLE i.

Русский

При включении i: V ≤ V' между открытыми подмножствами X ограничение тождественного морфизма даёт каноническое ограничение X.homOfLE i.

LaTeX

$$$\mathrm{resLE}(\mathrm{id}_X)\;V'\;V\;i = X.homOfLE(i)$$$

Lean4

theorem resLE_id (i : V ≤ V') : resLE (𝟙 X) V' V i = X.homOfLE i :=
  by
  simp only [resLE, morphismRestrict_id]
  rfl

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