basicOpen_res — Mathlib

English

The basicOpen construction is functorial with respect to restriction of opens.

Русский

Конструкция basicOpen относимa к ограничениям открытых множеств по отношению к отображениям.

LaTeX

$$$\text{basicOpen}_{X}(f)|_{i} = \text{basicOpen}_{X}(f|_{i})$$$

Lean4

@[simp]
theorem basicOpen_res {U V : (Opens X)ᵒᵖ} (i : U ⟶ V) (f : X.presheaf.obj U) :
    @basicOpen X (unop V) (X.presheaf.map i f) = unop V ⊓ @basicOpen X (unop U) f :=
  by
  ext x; constructor
  · rintro ⟨hxV, hx⟩
    rw [germ_res_apply' X.presheaf] at hx
    exact ⟨hxV, i.unop.le hxV, hx⟩
  · rintro ⟨hxV, _, hx⟩
    refine ⟨hxV, ?_⟩
    rw [germ_res_apply' X.presheaf]
    exact hx

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