Theoremsapp_eq_appIso_inv_app_of_comp_eq, app_eq_invApp_app_of_comp_eq_aux, app_ΓIso_hom, app_ΓIso_hom_apply, app_ΓIso_hom_assoc, comp, comp_lift, comp_lift_assoc, hasLimit_cospan_forget_of_left, hasLimit_cospan_forget_of_left', hasLimit_cospan_forget_of_right, hasLimit_cospan_forget_of_right', hasPullback_of_left, hasPullback_of_right, iff_isIso_stalkMap, iff_stalk_iso, image_preimage_eq_preimage_image_of_isPullback, instFstScheme, instHasOfPostcompPropertyScheme, instIsIsoCommRingCatStalkMap, instIsOpenImmersionMapSchemeLocallyRingedSpaceForgetToLocallyRingedSpace, instLift, instPreservesLimitSchemeLocallyRingedSpaceWalkingCospanCospanForgetToLocallyRingedSpace, instPreservesLimitSchemeLocallyRingedSpaceWalkingCospanCospanForgetToLocallyRingedSpace_1, instPreservesLimitSchemeTopCatWalkingCospanCospanForgetToTop, instPreservesLimitSchemeTopCatWalkingCospanCospanForgetToTop_1, instPreservesLimitSchemeWalkingCospanCospanForget, instPreservesLimitSchemeWalkingCospanCospanForget_1, instSndScheme, instπWalkingCospanSchemeCospanOne, isIso, isOpen_range, isPullback, isPullback_lift_id, isoOfRangeEq_hom_fac, isoOfRangeEq_hom_fac_assoc, isoOfRangeEq_inv_fac, isoOfRangeEq_inv_fac_assoc, le_monomorphisms, lift_app, lift_fac, lift_fac_assoc, lift_uniq, map_ΓIso_hom, map_ΓIso_inv, map_ΓIso_inv_apply, map_ΓIso_inv_assoc, mono, ofRestrict, of_comp, of_isIso, of_isIso_stalkMap, of_isLocalization, of_stalk_iso, opensEquiv_apply_coe, opensEquiv_symm_apply, opensRange_pullback_fst_of_right, opensRange_pullback_snd_of_left, range_pullbackFst, range_pullbackSnd, range_pullback_fst_of_right, range_pullback_snd_of_left, range_pullback_to_base_of_left, range_pullback_to_base_of_right, to_iso, ΓIso_inv, scheme_eq_of_locallyRingedSpace_eq, scheme_toScheme, toSchemeHom_isOpenImmersion, toSchemeHom_toPshHom, toScheme_toLocallyRingedSpace, appIso_hom, appIso_hom', appIso_inv_app, appIso_inv_appLE, appIso_inv_appLE_assoc, appIso_inv_app_apply, appIso_inv_app_assoc, appIso_inv_app_presheafMap, appIso_inv_naturality, appIso_inv_naturality_assoc, appLE_appIso_inv, appLE_appIso_inv_apply, appLE_appIso_inv_assoc, app_appIso_inv, app_appIso_inv_assoc, app_invApp', app_invApp'_assoc, apply_mem_image_iff, coe_image, coe_opensRange, comp_appIso, comp_image, id_appIso, id_image, image_iSup, image_iSup₂, image_injective, image_le_image_iff, image_le_image_of_le, image_le_opensRange, image_mono, image_preimage_eq_opensRange_inf, image_preimage_eq_opensRange_inter, image_preimage_le, image_top_eq_opensRange, instIsContinuousOpensOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, instIsIsoCommRingCatAppObjOpensOpensFunctor, inv_image, isIso_app, isOpenEmbedding, map_mem_image_iff, mem_opensRange, opensFunctor_map_homOfLE, opensRange_comp, opensRange_comp_of_isIso, opensRange_of_isIso, opensRange_pullbackFst, opensRange_pullbackSnd, preimage_image_eq, preimage_opensRange, basic_open_isOpenImmersion, exists_affine_mem_range_and_range_subset, image_basicOpen, image_zeroLocus, instIsOpenImmersionMapOfHomAwayAlgebraMap, isOpenImmersion_SpecMap_localizationAway, ofRestrict_app, ofRestrict_appIso, ofRestrict_appLE, ofRestrict_toLRSHom_base, ofRestrict_toLRSHom_c_app, restrict_carrier, restrict_presheaf_map, restrict_presheaf_obj, restrict_toPresheafedSpace, isIso_iff_isIso_stalkMap, isIso_iff_isOpenImmersion, isIso_iff_isOpenImmersion_and_epi_base, isIso_iff_stalk_iso, isIso_of_isOpenImmersion_of_opensRange_eq_top, isOpenImmersion_isMultiplicative, isOpenImmersion_isStableUnderComposition, isOpenImmersion_respectsIso, isOpenImmersion_stableUnderBaseChange | 145 |