range_fromSpec — Mathlib

English

As above, the image of the fromSpec map covers exactly U; reiterating the range equality with U.

Русский

Как выше, образ fromSpec точно покрывает U; повторяем равенство образа и U.

LaTeX

$$Set.range hU.fromSpec.base = (U : Set X)$$

Lean4

@[simp]
theorem range_fromSpec : Set.range hU.fromSpec.base = (U : Set X) :=
  by
  delta IsAffineOpen.fromSpec; dsimp [IsAffineOpen.isoSpec_inv]
  rw [Set.range_comp, Set.range_eq_univ.mpr, Set.image_univ]
  · exact Subtype.range_coe
  rw [← TopCat.coe_comp, ← TopCat.epi_iff_surjective]
  infer_instance

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