restrict_restrict — Mathlib

English

Restricting a section along a chain of inclusions is the same as restricting directly along the composed inclusion.

Русский

Ограничение секции по цепочке вложений эквивалентно ограничению по композиции вложений.

LaTeX

$$restrictOpen (restrictOpen x V e2) U e1 = restrictOpen x U h$$

Lean4

theorem restrict_restrict {F : X.Presheaf C} {U V W : Opens X} (e₁ : U ≤ V) (e₂ : V ≤ W) (x : ToType (F.obj (op W))) :
    x |_ V |_ U = x |_ U := by
  delta restrictOpen restrict
  rw [← ConcreteCategory.comp_apply, ← Functor.map_comp]
  rfl

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