Commit 2023-12-01 16:02 8b8aaa21

View on Github →

chore: rename lemmas containing "of_open" to match the naming convention (#8229) Mostly, this means replacing "of_open" by "of_isOpen". A few lemmas names were misleading and are corrected differently. Zulip discussion.

Estimated changes

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean

Modified Mathlib/Analysis/Calculus/ContDiff/Basic.lean

added theorem ContDiffOn.continuousOn_deriv_of_isOpen

deleted theorem ContDiffOn.continuousOn_deriv_of_open

added theorem ContDiffOn.deriv_of_isOpen

deleted theorem ContDiffOn.deriv_of_open

added theorem contDiffOn_succ_iff_deriv_of_isOpen

deleted theorem contDiffOn_succ_iff_deriv_of_open

added theorem contDiffOn_top_iff_deriv_of_isOpen

deleted theorem contDiffOn_top_iff_deriv_of_open

Modified Mathlib/Analysis/Calculus/ContDiff/Defs.lean

added theorem ContDiffOn.continuousOn_fderiv_of_isOpen

deleted theorem ContDiffOn.continuousOn_fderiv_of_open

added theorem ContDiffOn.fderiv_of_isOpen

deleted theorem ContDiffOn.fderiv_of_open

added theorem contDiffOn_succ_iff_fderiv_of_isOpen

deleted theorem contDiffOn_succ_iff_fderiv_of_open

added theorem contDiffOn_top_iff_fderiv_of_isOpen

deleted theorem contDiffOn_top_iff_fderiv_of_open

Modified Mathlib/Analysis/Calculus/Deriv/Basic.lean

added theorem derivWithin_of_isOpen

deleted theorem derivWithin_of_open

Modified Mathlib/Analysis/Calculus/LineDeriv/Basic.lean

added theorem lineDerivWithin_of_isOpen

deleted theorem lineDerivWithin_of_open

Modified Mathlib/Analysis/Complex/AbsMax.lean

Modified Mathlib/Analysis/Convex/Gauge.lean

added theorem gaugeSeminorm_lt_one_of_isOpen

deleted theorem gaugeSeminorm_lt_one_of_open

added theorem gauge_lt_one_eq_self_of_isOpen

deleted theorem gauge_lt_one_eq_self_of_open

added theorem gauge_lt_one_of_mem_of_isOpen

deleted theorem gauge_lt_one_of_mem_of_open

Modified Mathlib/Analysis/Convex/Strict.lean

Modified Mathlib/Analysis/Convolution.lean

Modified Mathlib/Analysis/LocallyConvex/AbsConvex.lean

Modified Mathlib/Analysis/NormedSpace/Basic.lean

Modified Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean

Modified Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean

Modified Mathlib/Geometry/Manifold/ChartedSpace.lean

Modified Mathlib/Geometry/Manifold/Complex.lean

Modified Mathlib/Geometry/Manifold/PartitionOfUnity.lean

Modified Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean

Modified Mathlib/MeasureTheory/Measure/Regular.lean

added theorem MeasureTheory.Measure.InnerRegularWRT.measurableSet_of_isOpen

deleted theorem MeasureTheory.Measure.InnerRegularWRT.measurableSet_of_open

Modified Mathlib/MeasureTheory/Measure/Typeclasses.lean

Modified Mathlib/NumberTheory/NumberField/Units.lean

Modified Mathlib/Topology/Algebra/Group/Basic.lean

added theorem discreteTopology_iff_isOpen_singleton_one

deleted theorem discreteTopology_iff_open_singleton_one

added theorem discreteTopology_of_isOpen_singleton_one

deleted theorem discreteTopology_of_open_singleton_one

Modified Mathlib/Topology/Algebra/Nonarchimedean/AdicTopology.lean

Modified Mathlib/Topology/Algebra/OpenSubgroup.lean

added theorem Ideal.isOpen_of_isOpen_subideal

deleted theorem Ideal.isOpen_of_open_subideal

Modified Mathlib/Topology/Bases.lean

added theorem TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds

deleted theorem TopologicalSpace.isTopologicalBasis_of_open_of_nhds

Modified Mathlib/Topology/Basic.lean

added theorem Dense.inter_of_isOpen_left

added theorem Dense.inter_of_isOpen_right

deleted theorem Dense.inter_of_open_left

deleted theorem Dense.inter_of_open_right

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

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

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

Modified Mathlib/Topology/Clopen.lean

Modified Mathlib/Topology/Connected/Basic.lean

added theorem IsConnected.preimage_of_isOpenMap

deleted theorem IsConnected.preimage_of_openMap

added theorem IsPreconnected.preimage_of_isOpenMap

deleted theorem IsPreconnected.preimage_of_open_map

Modified Mathlib/Topology/Connected/LocallyConnected.lean

Modified Mathlib/Topology/ContinuousOn.lean

added theorem ContinuousOn.isOpen_inter_preimage

deleted theorem ContinuousOn.preimage_open_of_open

added theorem continuousOn_isOpen_of_generateFrom

deleted theorem continuousOn_open_of_generateFrom

Modified Mathlib/Topology/Covering.lean

Modified Mathlib/Topology/FiberBundle/Basic.lean

Modified Mathlib/Topology/GDelta.lean

added theorem isGδ_biInter_of_isOpen

deleted theorem isGδ_biInter_of_open

added theorem isGδ_iInter_of_isOpen

deleted theorem isGδ_iInter_of_open

Modified Mathlib/Topology/Instances/Real.lean

Modified Mathlib/Topology/IsLocallyHomeomorph.lean

Modified Mathlib/Topology/LocalHomeomorph.lean

added theorem LocalHomeomorph.image_isOpen_of_isOpen'

added theorem LocalHomeomorph.image_isOpen_of_isOpen

deleted theorem LocalHomeomorph.image_open_of_open'

deleted theorem LocalHomeomorph.image_open_of_open

added theorem LocalHomeomorph.isOpen_inter_preimage

added theorem LocalHomeomorph.isOpen_inter_preimage_symm

deleted theorem LocalHomeomorph.preimage_open_of_open

deleted theorem LocalHomeomorph.preimage_open_of_open_symm

Modified Mathlib/Topology/MetricSpace/Baire.lean

added theorem dense_biInter_of_isOpen

deleted theorem dense_biInter_of_open

added theorem dense_iInter_of_isOpen

added theorem dense_iInter_of_isOpen_nat

deleted theorem dense_iInter_of_open

deleted theorem dense_iInter_of_open_nat

added theorem dense_sInter_of_isOpen

deleted theorem dense_sInter_of_open

Modified Mathlib/Topology/MetricSpace/PiNat.lean

Modified Mathlib/Topology/Separation.lean

deleted theorem compact_exists_clopen_in_open

added theorem compact_exists_isClopen_in_isOpen

added theorem exists_isOpen_singleton_of_isOpen_finite

deleted theorem exists_open_singleton_of_open_finite

deleted theorem isTopologicalBasis_clopen

added theorem isTopologicalBasis_isClopen

Modified Mathlib/Topology/Sets/Opens.lean

Modified Mathlib/Topology/UniformSpace/Basic.lean

added theorem isOpen_of_uniformity_sum_aux

deleted theorem open_of_uniformity_sum_aux

added theorem uniformity_sum_of_isOpen_aux

deleted theorem uniformity_sum_of_open_aux

Modified Mathlib/Topology/UniformSpace/Cauchy.lean

Modified docs/overview.yaml