Commit 2024-03-19 18:17 75784e0d

View on Github →

chore: rename open_range to isOpen_range, closed_range to isClosed_range (#11438) All these lemmas refer to the range of some function being open/range (i.e. isOpen or isClosed).

Estimated changes

Modified Mathlib/AlgebraicGeometry/FunctionField.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Basic.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

added theorem AlgebraicGeometry.IsOpenImmersion.isOpen_range

deleted theorem AlgebraicGeometry.IsOpenImmersion.open_range

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

Modified Mathlib/AlgebraicGeometry/Properties.lean

Modified Mathlib/Analysis/InnerProductSpace/LaxMilgram.lean

deleted theorem IsCoercive.closed_range

added theorem IsCoercive.isClosed_range

Modified Mathlib/Analysis/NormedSpace/Star/GelfandDuality.lean

Modified Mathlib/Analysis/NormedSpace/Units.lean

Modified Mathlib/CategoryTheory/Extensive.lean

Modified Mathlib/Geometry/Manifold/BumpFunction.lean

Modified Mathlib/Geometry/Manifold/InteriorBoundary.lean

Modified Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean

deleted theorem ModelWithCorners.closed_range

added theorem ModelWithCorners.isClosed_range

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

Modified Mathlib/MeasureTheory/Constructions/Polish.lean

Modified Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

Modified Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

Modified Mathlib/Topology/Algebra/Module/FiniteDimension.lean

Modified Mathlib/Topology/Algebra/StarSubalgebra.lean

Modified Mathlib/Topology/Category/Profinite/Nobeling.lean

Modified Mathlib/Topology/Category/Stonean/Limits.lean

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

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

Modified Mathlib/Topology/Clopen.lean

Modified Mathlib/Topology/Compactification/OnePoint.lean

Modified Mathlib/Topology/Compactness/Compact.lean

Modified Mathlib/Topology/Compactness/Lindelof.lean

Modified Mathlib/Topology/Compactness/LocallyCompact.lean

Modified Mathlib/Topology/Compactness/Paracompact.lean

Modified Mathlib/Topology/Connected/LocallyConnected.lean

Modified Mathlib/Topology/Constructions.lean

Modified Mathlib/Topology/ContinuousFunction/ZeroAtInfty.lean

deleted theorem ZeroAtInftyContinuousMap.closed_range_toBCF

added theorem ZeroAtInftyContinuousMap.isClosed_range_toBCF

Modified Mathlib/Topology/ContinuousOn.lean

Modified Mathlib/Topology/Defs/Induced.lean

Modified Mathlib/Topology/Instances/ENNReal.lean

Modified Mathlib/Topology/Instances/Irrational.lean

Modified Mathlib/Topology/IsLocalHomeomorph.lean

Modified Mathlib/Topology/LocalAtTarget.lean

Modified Mathlib/Topology/Maps.lean

deleted theorem IsClosedMap.closed_range

added theorem IsClosedMap.isClosed_range

Modified Mathlib/Topology/MetricSpace/Antilipschitz.lean

Modified Mathlib/Topology/MetricSpace/Polish.lean

Modified Mathlib/Topology/SeparatedMap.lean

Modified Mathlib/Topology/Separation.lean

deleted theorem Function.LeftInverse.closed_range

added theorem Function.LeftInverse.isClosed_range

Modified Mathlib/Topology/Sets/Opens.lean

Modified Mathlib/Topology/Sober.lean

Modified Mathlib/Topology/TietzeExtension.lean

Modified Mathlib/Topology/UniformSpace/UniformEmbedding.lean