Commit 2024-08-07 06:03 c0d0e84f

View on Github →

chore: backports for leanprover/lean4#4814 (part 18) (#15431) see https://github.com/leanprover-community/mathlib4/pull/15245

Estimated changes

Modified Mathlib/Algebra/Homology/ShortComplex/ConcreteCategory.lean

modified theorem CategoryTheory.ShortComplex.ShortExact.injective_f

modified theorem CategoryTheory.ShortComplex.ShortExact.surjective_g

Modified Mathlib/CategoryTheory/Galois/Prorepresentability.lean

modified theorem CategoryTheory.PreGaloisCategory.AutGalois.π_surjective

Modified Mathlib/CategoryTheory/Triangulated/HomologicalFunctor.lean

Modified Mathlib/Geometry/Manifold/LocalInvariantProperties.lean

Modified Mathlib/RingTheory/FractionalIdeal/Basic.lean

Modified Mathlib/RingTheory/Ideal/Maps.lean

modified theorem Ideal.comap_le_map_of_inv_on

modified theorem Ideal.map_le_comap_of_inv_on

modified theorem Ideal.map_le_comap_of_inverse

Modified Mathlib/Topology/Category/TopCat/Limits/Cofiltered.lean

modified theorem TopCat.isTopologicalBasis_cofiltered_limit

Modified Mathlib/Topology/Covering.lean

modified theorem IsCoveringMap.constOn_of_comp

modified theorem IsCoveringMap.eqOn_of_comp_eqOn

Modified Mathlib/Topology/Sets/Closeds.lean

Modified Mathlib/Topology/StoneCech.lean

Modified Mathlib/Topology/UniformSpace/Cauchy.lean

modified theorem SequentiallyComplete.le_nhds_of_seq_tendsto_nhds

modified theorem SequentiallyComplete.seq_is_cauchySeq

modified theorem cauchy_comap_uniformSpace