case a
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
hf : IsUnit f
⊢ basicOpen X f ≤ U

case a
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
hf : IsUnit f
⊢ U ≤ basicOpen X f
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
hf : IsUnit f
⊢ basicOpen X f = U
apply le_antisymm
case a
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
hf : IsUnit f
x : ↑↑X.toPresheafedSpace
hx : x ∈ ↑U
⊢ x ∈ ↑(basicOpen X f)
case a
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
hf : IsUnit f
⊢ U ≤ basicOpen X f
intro x hx
case a
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
hf : IsUnit f
x : ↑↑X.toPresheafedSpace
hx : x ∈ ↑U
⊢ IsUnit (↑(germ X.presheaf { val := x, property := hx }) f)
case a
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
hf : IsUnit f
x : ↑↑X.toPresheafedSpace
hx : x ∈ ↑U
⊢ x ∈ ↑(basicOpen X f)
erw [X.mem_basicOpen f (⟨x, hx⟩ : U)]
no goals
case a
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
hf : IsUnit f
x : ↑↑X.toPresheafedSpace
hx : x ∈ ↑U
⊢ IsUnit (↑(germ X.presheaf { val := x, property := hx }) f)
exact RingHom.isUnit_map _ hf
no goals
case a
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
hf : IsUnit f
⊢ basicOpen X f ≤ U
exact X.basicOpen_le f