Commit 2024-11-19 15:27 e948d859

View on Github →

chore: further renames (#19243) Similar to #19209: bring more lemma names in line with the naming convention.

Estimated changes

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

Modified Mathlib/AlgebraicGeometry/Properties.lean

Modified Mathlib/Dynamics/Minimal.lean

deleted theorem isMinimal_iff_closed_smul_invariant

added theorem isMinimal_iff_isClosed_smul_invariant

Modified Mathlib/MeasureTheory/Group/Action.lean

Modified Mathlib/MeasureTheory/Group/Measure.lean

Modified Mathlib/MeasureTheory/Measure/Regular.lean

deleted theorem MeasureTheory.Measure.InnerRegular.exists_compact_not_null

added theorem MeasureTheory.Measure.InnerRegular.exists_isCompact_not_null

deleted theorem MeasureTheory.Measure.Regular.exists_compact_not_null

added theorem MeasureTheory.Measure.Regular.exists_isCompact_not_null

Modified Mathlib/Topology/ContinuousMap/Algebra.lean

Modified Mathlib/Topology/Irreducible.lean

deleted theorem isIrreducible_iff_sUnion_closed

added theorem isIrreducible_iff_sUnion_isClosed

deleted theorem isPreirreducible_iff_closed_union_closed

added theorem isPreirreducible_iff_isClosed_union_isClosed

Modified Mathlib/Topology/Maps/Basic.lean

deleted theorem Topology.IsInducing.isQuotientMap_iff_closed

added theorem Topology.IsInducing.isQuotientMap_iff_isClosed

Modified Mathlib/Topology/NoetherianSpace.lean

Modified Mathlib/Topology/UniformSpace/CompactConvergence.lean

deleted theorem ContinuousMap.tendsto_iff_forall_compact_tendstoUniformlyOn

added theorem ContinuousMap.tendsto_iff_forall_isCompact_tendstoUniformlyOn