basicOpen_res_eq — Mathlib

English

A high-priority simplification equates a basicOpen with a standard basicOpen under isomorphism.

Русский

Высокий приоритет упрощения эквивалентен базовому открытому через изоморфизм.

LaTeX

$$$@basicOpen_eq X f = @RingedSpace.basicOpen X f$$$

Lean4

/-- High priority: This should fire before `basicOpen_res`. -/
@[simp (high)]
theorem basicOpen_res_eq {U V : (Opens X)ᵒᵖ} (i : U ⟶ V) [IsIso i] (f : X.presheaf.obj U) :
    @basicOpen X (unop V) (X.presheaf.map i f) = @RingedSpace.basicOpen X (unop U) f :=
  by
  apply le_antisymm
  · rw [X.basicOpen_res i f]; exact inf_le_right
  · have := X.basicOpen_res (inv i) (X.presheaf.map i f)
    rw [← CommRingCat.comp_apply, ← X.presheaf.map_comp, IsIso.hom_inv_id, X.presheaf.map_id,
      CommRingCat.id_apply] at this
    rw [this]
    exact inf_le_right

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