Mathlib Changelog
v4
Changelog
About
Github
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