Theoremsof_basicOpenCover, respectsIso, to_basicOpen, mk, arrow_mk_iso_iff, cancel_left_of_respectsIso, cancel_right_of_respectsIso, ext, ext_iff, instIsLocalOfOfIsZariskiLocalAtTarget, respectsIso_mk, respectsIso_of, toProperty_apply, copy, eq_targetAffineLocally, eq_targetAffineLocally', iff, iff_of_iSup_eq_top, iff_of_isAffine, iff_of_openCover, instIsZariskiLocalAtTarget, instRespectsIsoScheme, instTargetAffineLocallyOfIsLocal, isLocal_affineProperty, isStableUnderBaseChange, isZariskiLocalAtSource, of_iSup_eq_top, of_isLocalAtTarget, of_isPullback, of_isZariskiLocalAtTarget, of_openCover, restrict, comp, iff_exists_resLE, iff_of_iSup_eq_top, iff_of_openCover, isLocalAtTarget, mk', of_iSup_eq_top, of_isOpenImmersion, of_openCover, resLE, respectsLeft_isOpenImmersion, sigmaDesc, iff_of_iSup_eq_top, iff_of_openCover, mk', of_iSup_eq_top, of_isPullback, of_openCover, of_range_subset_iSup, restrict, comp, iff_exists_resLE, iff_of_iSup_eq_top, iff_of_openCover, isZariskiLocalAtTarget, mk', of_iSup_eq_top, of_isOpenImmersion, of_openCover, resLE, respectsLeft_isOpenImmersion, sigmaDesc, coprodMap, iff_of_iSup_eq_top, iff_of_openCover, mk', of_forall_exists_morphismRestrict, of_forall_source_exists_preimage, of_iSup_eq_top, of_isPullback, of_openCover, of_range_subset_iSup, restrict, hasOfPostcompProperty_isOpenImmersion_of_morphismRestrict, instHasOfPostcompPropertySchemeIsOpenImmersionOfIsStableUnderBaseChange, instRespectsIsoSchemeTargetAffineLocallyOfToProperty, of_targetAffineLocally_of_isPullback | 79 |