MorphismProperty

📁 Source: Mathlib/CategoryTheory/Sites/MorphismProperty.lean

Statistics

Metric	Count
Definitions MorphismProperty, coverage, grothendieckTopology, precoverage, pretopology	5
Theorems bot_mem_precoverage, comap_precoverage, coverage_eq_toCoverage_pretopology, coverage_toPrecoverage, grothendieckTopology_eq_toGrothendieck_pretopology, instHasIsosPrecoverageOfContainsIdentitiesOfRespectsIso, instIsStableUnderBaseChangePrecoverageOfIsStableUnderBaseChange, instIsStableUnderCompositionPrecoverageOfIsStableUnderComposition, instSmallPrecoverage, ofArrows_mem_precoverage, precoverage_inf, precoverage_monotone, pretopology_inf, pretopology_le, pretopology_monotone, pretopology_toPrecoverage	16
Total	21

CategoryTheory

Definitions

Name	Category	Theorems
MorphismProperty 📖	CompOp	282 math math: AlgebraicGeometry.descendsAlong_isOpenImmersion_surjective_inf_flat_inf_quasicompact', homotopyEquivalences_le_quasiIso, SimplexCategoryGenRel.multiplicativeClosure_isGenerator_eq_top, AlgebraicGeometry.descendsAlong_universallyClosed_surjective_inf_flat_inf_quasicompact, MorphismProperty.isomorphisms_le_of_containsIdentities, MorphismProperty.comp_eq_top_iff, MorphismProperty.isStableUnderLimitsOfShape_iff_limitsOfShape_le, MorphismProperty.hasOfPostcompProperty_iff_le_diagonal, MorphismProperty.universally_inf, SSet.modelCategoryQuillen.I_le_monomorphisms, AlgebraicGeometry.HasAffineProperty.affineAnd_le_affineAnd, IsCardinalFiltered.exists_cardinal_directed.D₁_W, MorphismProperty.DescendsAlong.top, MorphismProperty.Over.hasPullbacks, MorphismProperty.HasCardinalLT.iSup, MorphismProperty.Over.instHasTerminalTopOfContainsIdentities, MorphismProperty.ContainsIdentities.inf, MorphismProperty.Over.map_obj_left, MorphismProperty.Over.pullbackComp_hom_app_left, MorphismProperty.pushouts_le, MorphismProperty.Under.mk_hom, Localization.LeftBousfield.galoisConnection, ObjectProperty.isomorphisms_le_isoModSerre, AlgebraicGeometry.instIsOpenImmersionLeftSchemeDiscretePUnitMapWalkingSpanOverTopMorphismPropertySpan, AlgebraicGeometry.isImmersion_eq_inf, MorphismProperty.colimitsOfShape_le_coproducts, MorphismProperty.IsInvertedBy.iff_map_le_isomorphisms, AlgebraicGeometry.descendsAlong_isomorphisms_surjective_inf_flat_inf_quasicompact, MorphismProperty.Over.mapCongr_inv_app_left, MorphismProperty.monotone_map, MorphismProperty.transfiniteCompositionsOfShape_le_transfiniteCompositions, AlgebraicGeometry.IsSeparated.eq_valuativeCriterion, AlgebraicGeometry.IsClosedImmersion.eq_proper_inf_monomorphisms, MorphismProperty.IsMultiplicative.instTop, MorphismProperty.Over.pullbackMapHomPullback_app, MorphismProperty.IsMultiplicative.inf, MorphismProperty.colimitsOfShape_le, MorphismProperty.IsLocalAtSource.inf, MorphismProperty.Over.mk_hom, MorphismProperty.Over.pullback_obj_left, MorphismProperty.Over.map_map_left, SSet.Truncated.HomotopyCategory.multiplicativeClosure_morphismPropertyHomMk, IsGrothendieckAbelian.isomorphisms_le_pushouts_generatingMonomorphisms, MorphismProperty.transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone_ι_transitionMap, MorphismProperty.coproducts_monotone, Localization.Construction.morphismProperty_eq_top', MorphismProperty.Over.Hom.ext_iff, HomotopicalAlgebra.trivialCofibrations_sub_cofibrations, MorphismProperty.colimitsOfShape_discrete_le_llp_rlp, MorphismProperty.Over.pullbackCongr_hom_app_left_fst, MorphismProperty.Over.mapPullbackAdj_counit_app, MorphismProperty.isStableUnderRetracts_iff_retracts_le, MorphismProperty.multiplicativeClosure_monotone, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_f, Functor.relativelyRepresentable.isomorphisms_le, MorphismProperty.DescendsAlong.inf, MorphismProperty.CodescendsAlong.inf, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionCocone_pt, MorphismProperty.retracts_le, MorphismProperty.instRespectsIsoTop, MorphismProperty.IsStableUnderBaseChange.inf, MorphismProperty.instFaithfulOverTopOverForget, MorphismProperty.IsLocalAtSource.top, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap_id, MorphismProperty.Over.map_comp, AlgebraicGeometry.instDescendsAlongSchemeMinMorphismPropertySurjectiveFlatLocallyOfFinitePresentationOfQuasiCompactOfIsZariskiLocalAtTarget, MorphismProperty.Comma.instFullTopCommaForget, HomotopicalAlgebra.trivialCofibrations_sub_weakEquivalences, AlgebraicGeometry.HasAffineProperty.affineAnd_eq_of_propertyIsLocal, Localization.LeftBousfield.le_W_iff, MorphismProperty.le_ind, AlgebraicGeometry.Etale.instHasOfPostcompPropertySchemeMinMorphismPropertyLocallyOfFiniteTypeFormallyUnramified, MorphismProperty.transfiniteCompositionsOfShape_le, HomotopicalAlgebra.trivialFibrations_sub_fibrations, AlgebraicGeometry.IsFinite.eq_proper_inf_locallyQuasiFinite, IsGrothendieckAbelian.generatingMonomorphisms_le_monomorphisms, MorphismProperty.Over.instPreservesFiniteLimitsTopPullback, Cat.FreeRefl.multiplicativeClosure_morphismPropertyHomMk, MorphismProperty.transfiniteCompositionsOfShape_monotone, MorphismProperty.isStableUnderCobaseChange_iff_pushouts_le, MorphismProperty.Over.mapPullbackAdj_unit_app, MorphismProperty.universally_le, GrothendieckTopology.PreservesSheafification.le, AlgebraicGeometry.IsLocalIso.eq_iInf, AlgebraicGeometry.topologically_iso_le, MorphismProperty.Over.mapId_inv_app_left, SSet.Truncated.liftOfStrictSegal.naturalityProperty_eq_top, AlgebraicGeometry.instHasOfPostcompPropertySchemeQuasiSeparatedTopMorphismProperty, MorphismProperty.le_pushouts, IsCardinalFiltered.exists_cardinal_directed.Diagram.iSup_W, MorphismProperty.Over.mapCongr_hom_app_left, MorphismProperty.IsLocalAtTarget.top, MorphismProperty.strictMap_multiplicativeClosure_le, SmallObject.succStruct_prop_le_propArrow, MorphismProperty.isoClosure_le_iff, MorphismProperty.instIsStableUnderCobaseChangeTop, MorphismProperty.Over.forget_comp_forget_map, MorphismProperty.Over.pullbackComp_inv_app_left, MorphismProperty.coproducts_le_iff, MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionCocone_ι_app, ObjectProperty.galoisConnection_isColocal, MorphismProperty.map_inverseImage_le, MorphismProperty.le_isLocal_isLocal, MorphismProperty.gc_llp_rlp, SimplexCategory.Truncated.morphismProperty_eq_top, HomotopicalAlgebra.trivialFibrations_sub_weakEquivalences, MorphismProperty.instHasOfPrecompPropertyTop, MorphismProperty.HasCardinalLT.sup, MorphismProperty.instIsStableUnderRetractsMin, MorphismProperty.retracts_transfiniteComposition_pushouts_coproducts_le_llp_rlp, MorphismProperty.iSup_iff, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_X, MorphismProperty.map_le_iff, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_f, ObjectProperty.le_isLocal_iff, MorphismProperty.le_coproducts, MorphismProperty.RespectsLeft.inf, MorphismProperty.instFullUnderTopUnderForget, Paths.morphismProperty_eq_top', Localization.Construction.morphismProperty_is_top', MorphismProperty.instIsLeftAdjointOverTopMapOfHasPullbacksAlongOfIsStableUnderBaseChangeAlong, MorphismProperty.Over.mapComp_hom_app_left, MorphismProperty.le_pullbacks, ObjectProperty.epimorphisms_le_epiModSerre, MorphismProperty.antitone_rlp, MorphismProperty.bijective_eq_sup, MorphismProperty.IsStableUnderTransfiniteCompositionOfShape.le, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone_ι_transitionMap_assoc, MorphismProperty.instIsStableUnderBaseChangeTop, MorphismProperty.Over.w_assoc, MorphismProperty.le_llp_rlp, AlgebraicGeometry.HasRingHomProperty.inf, Localization.Construction.morphismProperty_eq_top, MorphismProperty.instHasOfPostcompPropertyTop, MorphismProperty.le_llp_iff_le_rlp, MorphismProperty.coproducts_le, ObjectProperty.le_isColocal_iff, MorphismProperty.instFaithfulCostructuredArrowTopOverToOver, AlgebraicGeometry.isOpenImmersion_eq_inf, MorphismProperty.CostructuredArrow.toOver_map, AlgebraicGeometry.instHasCoproductsOfShapeOverSchemeTopMorphismPropertyOfSmall, MorphismProperty.le_retracts, MorphismProperty.instHasOfPrecompPropertyMin, AlgebraicGeometry.IsClosedImmersion.eq_inf, ObjectProperty.monomorphisms_le_monoModSerre, MorphismProperty.CostructuredArrow.toOver_obj, MorphismProperty.Under.w, MorphismProperty.pretopology_inf, AlgebraicGeometry.targetAffineLocally_affineAnd_eq_affineLocally, MorphismProperty.inf, MorphismProperty.RespectsRight.inf, MorphismProperty.coproducts_le_llp_rlp, MorphismProperty.Over.mk_left, AlgebraicGeometry.isPreimmersion_eq_inf, MorphismProperty.CostructuredArrow.mk_left, AlgebraicGeometry.isProper_eq, MorphismProperty.Under.Hom.ext_iff, MorphismProperty.limitsOfShape_le, MorphismProperty.Under.mk_left, MorphismProperty.retracts_le_iff, AlgebraicGeometry.universallyClosed_eq_universallySpecializing, MorphismProperty.transfiniteCompositionsOfShape_le_llp_rlp, MorphismProperty.Over.instPreservesFiniteLimitsTopOverForget, AlgebraicGeometry.Flat.surjective_descendsAlong_surjective_inf_flat_inf_quasicompact, MorphismProperty.retracts_transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp, AlgebraicGeometry.IsProper.eq_valuativeCriterion, MorphismProperty.Under.forget_comp_forget_map, MorphismProperty.IsInvertedBy.iff_le_inverseImage_isomorphisms, AlgebraicGeometry.IsClosedImmersion.eq_isFinite_inf_mono, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_X, MorphismProperty.instFullOverTopOverForget, MorphismProperty.isomorphisms_le_pushouts, MorphismProperty.Comma.hasColimitsOfShape_of_closedUnderColimitsOfShape, MorphismProperty.Over.w, MorphismProperty.IsStableUnderComposition.inf, AlgebraicGeometry.UniversallyClosed.eq_valuativeCriterion, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.trans_app_left, MorphismProperty.le_leftBousfieldW_isLocal, AlgebraicGeometry.Scheme.instLocallyCoverDenseOverTopMorphismPropertyOverForgetOverGrothendieckTopology, MorphismProperty.CodescendsAlong.top, MorphismProperty.colimitsOfShape_le_of_final, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap_comp, LocalizerMorphism.map, AlgebraicGeometry.isomorphisms_eq_isOpenImmersion_inf_surjective, MorphismProperty.instHasOfPostcompPropertyMin, Cat.FreeRefl.morphismProperty_eq_top, Paths.morphismProperty_eq_top_of_isMultiplicative, MorphismProperty.transfiniteCompositions_le, AlgebraicGeometry.instHasOfPostcompPropertySchemeIsSeparatedTopMorphismProperty, MorphismProperty.Comma.hasColimit_of_closedUnderColimitsOfShape, AlgebraicGeometry.geometrically_inf, MorphismProperty.CostructuredArrow.Hom.ext_iff, AlgebraicGeometry.IsImmersion.instHasOfPostcompPropertySchemeTopMorphismProperty, MorphismProperty.retracts_le_llp_rlp, AlgebraicGeometry.Scheme.smallGrothendieckTopology_eq_toGrothendieck_smallPretopology, MorphismProperty.Over.pullback_map_left, AlgebraicGeometry.IsFinite.eq_isProper_inf_isAffineHom, MorphismProperty.antitone_llp, AlgebraicGeometry.targetAffineLocally_affineAnd_le, MorphismProperty.sSup_iff, AlgebraicGeometry.instIsLocallyDirectedCompSchemeOverOverTopMorphismPropertyForgetForgetForget, SSet.modelCategoryQuillen.J_le_monomorphisms, MorphismProperty.isStableUnderTransfiniteCompositionOfShape_iff, MorphismProperty.Over.pullback_obj_hom, FreeGroupoid.instIsLocalizationOfTopMorphismProperty, MorphismProperty.instHasTwoOutOfThreePropertyTop, MorphismProperty.le_isColocal_isColocal, MorphismProperty.Over.mapComp_inv_app_left, Localization.morphismProperty_eq_top, MorphismProperty.Under.w_assoc, MorphismProperty.instFullCostructuredArrowTopOverToOver, AlgebraicGeometry.Scheme.mem_smallGrothendieckTopology, MorphismProperty.map_top_eq_top_of_essSurj_of_full, MorphismProperty.instHasTwoOutOfThreePropertyMin, MorphismProperty.instHasPullbackSndHomDiscretePUnitOfHasPullbacksAlongOfIsStableUnderBaseChangeAlong, MorphismProperty.precoverage_inf, AlgebraicGeometry.HasAffineProperty.affineAnd_le_isAffineHom, MorphismProperty.IsStableUnderCobaseChange.inf, MorphismProperty.monotone_isoClosure, AlgebraicGeometry.isomorphisms_eq_stalkwise, MorphismProperty.transfiniteCompositions_pushouts_coproducts_le_llp_rlp, AlgebraicGeometry.IsOpenImmersion.le_monomorphisms, MorphismProperty.le_def, AlgebraicGeometry.IsFinite.eq_inf, MorphismProperty.pushouts_le_llp_rlp, AlgebraicGeometry.affineLocally_le, AlgebraicGeometry.GeometricallyIntegral.eq_geometricallyReduced_inf_geometricallyIrreducible, IsCardinalFiltered.exists_cardinal_directed.D₃_W, MorphismProperty.isStableUnderColimitsOfShape_iff_colimitsOfShape_le, MorphismProperty.toSet_max, MorphismProperty.le_isoClosure, ObjectProperty.galoisConnection_isLocal, AlgebraicGeometry.instMonoObjWalkingSpanCompOverSchemeTopMorphismPropertySpanOverForgetForgetForgetNoneWalkingPairSomeMapInitOfIsOpenImmersionLeftDiscretePUnit, MorphismProperty.pullbacks_monotone, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor_map, MorphismProperty.universally_mono, MorphismProperty.presheaf_monomorphisms_le_monomorphisms, MorphismProperty.pushouts_le_iff, MorphismProperty.isStableUnderBaseChange_iff_pullbacks_le, IsCardinalFiltered.exists_cardinal_directed.D₄_W, AlgebraicGeometry.IsIntegralHom.eq_universallyClosed_inf_isAffineHom, MorphismProperty.pullbacks_le, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor_obj, ConcreteCategory.injective_le_monomorphisms, MorphismProperty.pushouts_monotone, MorphismProperty.le_colimitsOfShape_punit, IsCardinalFiltered.exists_cardinal_directed.D₂_W, AlgebraicGeometry.Scheme.mem_toGrothendieck_smallPretopology, MorphismProperty.retracts_monotone, MorphismProperty.Over.mapId_hom_app_left, MorphismProperty.Over.pullbackComp_left_fst_fst, ConcreteCategory.surjective_le_epimorphisms, MorphismProperty.IsLocalAtTarget.inf, MorphismProperty.Comma.hasLimitsOfShape_of_closedUnderLimitsOfShape, isGroupoid_iff_isomorphisms_eq_top, MorphismProperty.le_multiplicativeClosure, Localization.instIsGroupoidLocalizationTopMorphismProperty, MorphismProperty.top_apply, AlgebraicGeometry.instHasFiniteCoproductsOverSchemeTopMorphismProperty, Localization.Construction.morphismProperty_is_top, AlgebraicGeometry.ValuativeCriterion.eq, SSet.Truncated.HomotopyCategory.morphismProperty_eq_top, MorphismProperty.transfiniteCompositions_monotone, MorphismProperty.top_eq, MorphismProperty.Over.pullbackCongr_hom_app_left_fst_assoc, IsCardinalFiltered.exists_cardinal_directed.Diagram.sup_W, MorphismProperty.transfiniteCompositions_le_llp_rlp, AlgebraicGeometry.descendsAlong_universallyOpen_surjective_inf_flat_inf_quasicompact, MorphismProperty.CostructuredArrow.mk_hom, Paths.morphismProperty_eq_top, MorphismProperty.Comma.hasLimit_of_closedUnderLimitsOfShape, AlgebraicGeometry.sourceLocalClosure.le, MorphismProperty.Over.map_obj_hom, AlgebraicGeometry.descendsAlong_universallyInjective_surjective_inf_flat_inf_quasicompact, MorphismProperty.instFaithfulUnderTopUnderForget, MorphismProperty.multiplicativeClosure_le_iff, MorphismProperty.le_transfiniteCompositions, MorphismProperty.toSet_iSup, MorphismProperty.transfiniteCompositions_le_iff, SimplexCategory.morphismProperty_eq_top

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
coverage 📖	CompOp	2 math math: coverage_toPrecoverage, coverage_eq_toCoverage_pretopology
grothendieckTopology 📖	CompOp	1 math math: grothendieckTopology_eq_toGrothendieck_pretopology
precoverage 📖	CompOp	11 math math: instSmallPrecoverage, ofArrows_mem_precoverage, coverage_toPrecoverage, precoverage_monotone, instHasIsosPrecoverageOfContainsIdentitiesOfRespectsIso, instIsStableUnderBaseChangePrecoverageOfIsStableUnderBaseChange, bot_mem_precoverage, comap_precoverage, pretopology_toPrecoverage, precoverage_inf, instIsStableUnderCompositionPrecoverageOfIsStableUnderComposition
pretopology 📖	CompOp	9 math math: coverage_eq_toCoverage_pretopology, pretopology_monotone, AlgebraicGeometry.Scheme.pretopology_le_inf, AlgebraicGeometry.Scheme.grothendieckTopology_eq_inf, grothendieckTopology_eq_toGrothendieck_pretopology, pretopology_toPrecoverage, pretopology_inf, AlgebraicGeometry.Scheme.pretopology_eq_inf, pretopology_le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_mem_precoverage 📖	mathematical	—	CategoryTheory.Presieve Set Set.instMembership CategoryTheory.Precoverage.coverings precoverage Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticePresieve BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	—
comap_precoverage 📖	mathematical	—	CategoryTheory.Precoverage.comap precoverage inverseImage	—	CategoryTheory.Precoverage.ext Set.ext CategoryTheory.Presieve.exists_eq_ofArrows CategoryTheory.Presieve.map_ofArrows
coverage_eq_toCoverage_pretopology 📖	mathematical	—	coverage instHasPullbacksOfHasPullbacks CategoryTheory.Pretopology.toCoverage pretopology	—	instHasPullbacksOfHasPullbacks
coverage_toPrecoverage 📖	mathematical	—	CategoryTheory.Coverage.toPrecoverage coverage precoverage	—	—
grothendieckTopology_eq_toGrothendieck_pretopology 📖	mathematical	—	grothendieckTopology instHasPullbacksOfHasPullbacks CategoryTheory.Pretopology.toGrothendieck pretopology	—	instHasPullbacksOfHasPullbacks grothendieckTopology.eq_1 coverage_eq_toCoverage_pretopology CategoryTheory.Pretopology.toGrothendieck_toCoverage
instHasIsosPrecoverageOfContainsIdentitiesOfRespectsIso 📖	mathematical	—	CategoryTheory.Precoverage.HasIsos precoverage	—	of_isIso
instIsStableUnderBaseChangePrecoverageOfIsStableUnderBaseChange 📖	mathematical	—	CategoryTheory.Precoverage.IsStableUnderBaseChange precoverage	—	of_isPullback CategoryTheory.IsPullback.flip
instIsStableUnderCompositionPrecoverageOfIsStableUnderComposition 📖	mathematical	—	CategoryTheory.Precoverage.IsStableUnderComposition precoverage	—	comp_mem
instSmallPrecoverage 📖	mathematical	—	CategoryTheory.Precoverage.Small precoverage	—	PEmpty.instIsEmpty
ofArrows_mem_precoverage 📖	mathematical	—	CategoryTheory.Presieve Set Set.instMembership CategoryTheory.Precoverage.coverings precoverage CategoryTheory.Presieve.ofArrows	—	—
precoverage_inf 📖	mathematical	—	precoverage CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra CategoryTheory.Precoverage CategoryTheory.Precoverage.instMin	—	CategoryTheory.Precoverage.ext Set.ext
precoverage_monotone 📖	mathematical	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra	CategoryTheory.Precoverage CategoryTheory.Precoverage.instPartialOrder precoverage	—	—
pretopology_inf 📖	mathematical	—	pretopology CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra IsMultiplicative.inf IsStableUnderBaseChange.inf CategoryTheory.Pretopology CategoryTheory.Pretopology.instCompleteLattice	—	CategoryTheory.Pretopology.ext IsMultiplicative.inf IsStableUnderBaseChange.inf precoverage_inf
pretopology_le 📖	mathematical	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra	CategoryTheory.Pretopology CategoryTheory.Pretopology.LE pretopology	—	pretopology_monotone
pretopology_monotone 📖	mathematical	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra	CategoryTheory.Pretopology CategoryTheory.Pretopology.LE pretopology	—	precoverage_monotone
pretopology_toPrecoverage 📖	mathematical	—	CategoryTheory.Pretopology.toPrecoverage pretopology precoverage	—	—

---

← Back to Index