Commit 2024-05-01 07:53 8390a316

View on Github →

chore(CategoryTheory/MorphismProperty): Use le instead of subset (#12520)

Estimated changes

Modified Mathlib/Algebra/Homology/Localization.lean

Modified Mathlib/Algebra/Homology/QuasiIso.lean

added theorem homotopyEquivalences_le_quasiIso

deleted theorem homotopyEquivalences_subset_quasiIso

Modified Mathlib/CategoryTheory/Localization/Composition.lean

Modified Mathlib/CategoryTheory/Localization/Equivalence.lean

Modified Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean

Modified Mathlib/CategoryTheory/Localization/Pi.lean

Modified Mathlib/CategoryTheory/Localization/Predicate.lean

modified theorem CategoryTheory.Functor.IsLocalization.for_id

modified def CategoryTheory.Localization.strictUniversalPropertyFixedTargetId

Modified Mathlib/CategoryTheory/MorphismProperty/Basic.lean

added theorem CategoryTheory.MorphismProperty.isoClosure_eq_iff

added theorem CategoryTheory.MorphismProperty.isoClosure_le_iff

deleted theorem CategoryTheory.MorphismProperty.isoClosure_subset_iff

added theorem CategoryTheory.MorphismProperty.le_def

added theorem CategoryTheory.MorphismProperty.le_isoClosure

added theorem CategoryTheory.MorphismProperty.map_inverseImage_le

deleted theorem CategoryTheory.MorphismProperty.map_inverseImage_subset

added theorem CategoryTheory.MorphismProperty.map_le_iff

deleted theorem CategoryTheory.MorphismProperty.map_subset_iff

modified theorem CategoryTheory.MorphismProperty.monotone_isoClosure

modified theorem CategoryTheory.MorphismProperty.monotone_map

deleted theorem CategoryTheory.MorphismProperty.subset_iff_le

deleted theorem CategoryTheory.MorphismProperty.subset_isoClosure

Modified Mathlib/CategoryTheory/MorphismProperty/Composition.lean

Modified Mathlib/CategoryTheory/MorphismProperty/IsInvertedBy.lean

added theorem CategoryTheory.MorphismProperty.IsInvertedBy.iff_le_inverseImage_isomorphisms

added theorem CategoryTheory.MorphismProperty.IsInvertedBy.iff_map_le_isomorphisms

deleted theorem CategoryTheory.MorphismProperty.IsInvertedBy.iff_map_subset_isomorphisms

added theorem CategoryTheory.MorphismProperty.IsInvertedBy.of_le

deleted theorem CategoryTheory.MorphismProperty.IsInvertedBy.of_subset

Modified Mathlib/CategoryTheory/MorphismProperty/Limits.lean

added theorem CategoryTheory.MorphismProperty.universally_eq_iff