Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-03-11 13:51
357276c9
View on Github →
chore: review porting notes in
Topology/
(
#22670
)
Estimated changes
Modified
Mathlib/Topology/Algebra/Affine.lean
Modified
Mathlib/Topology/Algebra/ConstMulAction.lean
Modified
Mathlib/Topology/Algebra/ContinuousAffineMap.lean
Modified
Mathlib/Topology/Algebra/Field.lean
Modified
Mathlib/Topology/Algebra/Group/Basic.lean
Modified
Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean
Modified
Mathlib/Topology/Algebra/InfiniteSum/Order.lean
Modified
Mathlib/Topology/Algebra/Module/CharacterSpace.lean
Modified
Mathlib/Topology/Algebra/Module/LinearMap.lean
Modified
Mathlib/Topology/Algebra/Module/StrongTopology.lean
Modified
Mathlib/Topology/Algebra/Module/WeakBilin.lean
Modified
Mathlib/Topology/Algebra/Module/WeakDual.lean
Modified
Mathlib/Topology/Algebra/MulAction.lean
Modified
Mathlib/Topology/Algebra/OpenSubgroup.lean
Modified
Mathlib/Topology/Algebra/Order/Field.lean
Modified
Mathlib/Topology/Algebra/PontryaginDual.lean
Modified
Mathlib/Topology/Algebra/StarSubalgebra.lean
Modified
Mathlib/Topology/Algebra/Support.lean
Modified
Mathlib/Topology/Algebra/Valued/ValuationTopology.lean
modified
theorem
Valued.hasBasis_uniformity
Modified
Mathlib/Topology/Algebra/Valued/ValuedField.lean
Modified
Mathlib/Topology/Bornology/Constructions.lean
Modified
Mathlib/Topology/Bornology/Hom.lean
Modified
Mathlib/Topology/Category/Compactum.lean
Modified
Mathlib/Topology/Category/TopCat/Limits/Products.lean
Modified
Mathlib/Topology/Category/TopCat/Opens.lean
Modified
Mathlib/Topology/Compactness/Compact.lean
Modified
Mathlib/Topology/Compactness/Paracompact.lean
Modified
Mathlib/Topology/Compactness/SigmaCompact.lean
Modified
Mathlib/Topology/Connected/Clopen.lean
Modified
Mathlib/Topology/Connected/TotallyDisconnected.lean
Modified
Mathlib/Topology/Constructions.lean
Modified
Mathlib/Topology/ContinuousMap/Basic.lean
Modified
Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
Modified
Mathlib/Topology/ContinuousMap/Defs.lean
Modified
Mathlib/Topology/ContinuousMap/Polynomial.lean
Modified
Mathlib/Topology/ContinuousMap/Units.lean
Modified
Mathlib/Topology/DiscreteQuotient.lean
Modified
Mathlib/Topology/EMetricSpace/Basic.lean
Modified
Mathlib/Topology/EMetricSpace/BoundedVariation.lean
Modified
Mathlib/Topology/EMetricSpace/Defs.lean
Modified
Mathlib/Topology/EMetricSpace/Paracompact.lean
Modified
Mathlib/Topology/EMetricSpace/Pi.lean
Modified
Mathlib/Topology/FiberBundle/Constructions.lean
Modified
Mathlib/Topology/FiberBundle/Trivialization.lean
Modified
Mathlib/Topology/Gluing.lean
Modified
Mathlib/Topology/Homeomorph/Defs.lean
Modified
Mathlib/Topology/Homeomorph/Lemmas.lean
modified
def
Homeomorph.ulift.{u,
Modified
Mathlib/Topology/Homotopy/Basic.lean
Modified
Mathlib/Topology/Homotopy/Contractible.lean
Modified
Mathlib/Topology/Homotopy/HSpaces.lean
Modified
Mathlib/Topology/Homotopy/HomotopyGroup.lean
Modified
Mathlib/Topology/Homotopy/Path.lean
Modified
Mathlib/Topology/Homotopy/Product.lean
Modified
Mathlib/Topology/Instances/AddCircle.lean
Modified
Mathlib/Topology/Instances/ENNReal/Lemmas.lean
Modified
Mathlib/Topology/Instances/Real/Lemmas.lean
Modified
Mathlib/Topology/List.lean
Modified
Mathlib/Topology/MetricSpace/Antilipschitz.lean
Modified
Mathlib/Topology/MetricSpace/Basic.lean
Modified
Mathlib/Topology/MetricSpace/Bounded.lean
Modified
Mathlib/Topology/MetricSpace/Cauchy.lean
Modified
Mathlib/Topology/MetricSpace/Closeds.lean
Modified
Mathlib/Topology/MetricSpace/Contracting.lean
Modified
Mathlib/Topology/MetricSpace/Dilation.lean
Modified
Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean
Modified
Mathlib/Topology/MetricSpace/Isometry.lean
Modified
Mathlib/Topology/MetricSpace/Polish.lean
Modified
Mathlib/Topology/MetricSpace/Pseudo/Basic.lean
Modified
Mathlib/Topology/MetricSpace/Pseudo/Constructions.lean
Modified
Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
Modified
Mathlib/Topology/Metrizable/Uniformity.lean
Modified
Mathlib/Topology/Order/Basic.lean
Modified
Mathlib/Topology/Order/Compact.lean
Modified
Mathlib/Topology/Order/Hom/Basic.lean
Modified
Mathlib/Topology/Order/LowerUpperTopology.lean
Modified
Mathlib/Topology/Order/MonotoneConvergence.lean
Modified
Mathlib/Topology/Order/OrderClosed.lean
Modified
Mathlib/Topology/PartialHomeomorph.lean
Modified
Mathlib/Topology/Path.lean
Modified
Mathlib/Topology/Separation/Basic.lean
Modified
Mathlib/Topology/Separation/Hausdorff.lean
Modified
Mathlib/Topology/Sets/Closeds.lean
Modified
Mathlib/Topology/Sets/Compacts.lean
Modified
Mathlib/Topology/Sets/Opens.lean
Modified
Mathlib/Topology/Sheaves/CommRingCat.lean
Modified
Mathlib/Topology/Sheaves/Sheaf.lean
Modified
Mathlib/Topology/Sheaves/SheafCondition/EqualizerProducts.lean
Modified
Mathlib/Topology/Sheaves/SheafCondition/OpensLeCover.lean
Modified
Mathlib/Topology/Sheaves/Skyscraper.lean
Modified
Mathlib/Topology/Sheaves/Stalks.lean
Modified
Mathlib/Topology/UniformSpace/Basic.lean
Modified
Mathlib/Topology/UniformSpace/Cauchy.lean
Modified
Mathlib/Topology/UniformSpace/Defs.lean
Modified
Mathlib/Topology/UniformSpace/Equiv.lean
Modified
Mathlib/Topology/UniformSpace/Pi.lean
Modified
Mathlib/Topology/UniformSpace/UniformConvergence.lean
Modified
Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
Modified
Mathlib/Topology/UnitInterval.lean
modified
theorem
unitInterval.continuous_symm
Modified
Mathlib/Topology/VectorBundle/Basic.lean
Modified
Mathlib/Topology/VectorBundle/Hom.lean