Commit 2025-05-25 12:30 401dce0e

View on Github →

chore(*): not_mem/nmem -> notMem (#25159)

Estimated changes

Modified Archive/Imo/Imo2015Q6.lean

added theorem Imo2015Q6.notMem_pool_self

deleted theorem Imo2015Q6.not_mem_pool_self

Modified Archive/Imo/Imo2019Q2.lean

added theorem Imo2019Q2.Imo2019q2Cfg.Q_notMem_CB

deleted theorem Imo2019Q2.Imo2019q2Cfg.Q_not_mem_CB

Modified Archive/Imo/Imo2021Q1.lean

Modified Archive/Imo/Imo2024Q3.lean

Modified Archive/Imo/Imo2024Q5.lean

added theorem Imo2024Q5.MonsterData.notMem_monsterCells_of_fst_eq_zero

deleted theorem Imo2024Q5.MonsterData.not_mem_monsterCells_of_fst_eq_zero

Modified Archive/MiuLanguage/DecisionNec.lean

Modified Archive/Wiedijk100Theorems/AbelRuffini.lean

Modified Archive/Wiedijk100Theorems/AscendingDescendingSequences.lean

Modified Archive/Wiedijk100Theorems/BallotProblem.lean

Modified Archive/Wiedijk100Theorems/BuffonsNeedle.lean

Modified Archive/Wiedijk100Theorems/Partition.lean

Modified Counterexamples/CliffordAlgebraNotInjective.lean

added theorem Q60596.X0_X1_X2_notMem_kIdeal

deleted theorem Q60596.X0_X1_X2_not_mem_kIdeal

Modified Mathlib/Algebra/Algebra/Spectrum/Basic.lean

added theorem Units.zero_notMem_spectrum

deleted theorem Units.zero_not_mem_spectrum

added theorem spectrum.notMem_iff

deleted theorem spectrum.not_mem_iff

added theorem spectrum.zero_notMem_iff

deleted theorem spectrum.zero_not_mem_iff

Modified Mathlib/Algebra/BigOperators/Finprod.lean

added theorem finprod_mem_insert_of_eq_one_if_notMem

deleted theorem finprod_mem_insert_of_eq_one_if_not_mem

Modified Mathlib/Algebra/BigOperators/Finsupp/Basic.lean

added theorem Nat.prod_pow_pos_of_zero_notMem_support

deleted theorem Nat.prod_pow_pos_of_zero_not_mem_support

Modified Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean

added theorem Finset.prod_insert_of_eq_one_if_notMem

deleted theorem Finset.prod_insert_of_eq_one_if_not_mem

Modified Mathlib/Algebra/BigOperators/Group/Finset/Indicator.lean

Modified Mathlib/Algebra/BigOperators/Group/Finset/Lemmas.lean

Modified Mathlib/Algebra/BigOperators/Group/Finset/Piecewise.lean

added theorem Finset.prod_update_of_notMem

deleted theorem Finset.prod_update_of_not_mem

Modified Mathlib/Algebra/BigOperators/Group/Finset/Powerset.lean

Modified Mathlib/Algebra/BigOperators/Group/List/Lemmas.lean

Modified Mathlib/Algebra/BigOperators/Intervals.lean

Modified Mathlib/Algebra/BigOperators/Pi.lean

Modified Mathlib/Algebra/DirectSum/Basic.lean

added theorem DirectSum.mk_apply_of_notMem

deleted theorem DirectSum.mk_apply_of_not_mem

Modified Mathlib/Algebra/DirectSum/Internal.lean

Modified Mathlib/Algebra/Field/Subfield/Basic.lean

added theorem Subfield.notMem_of_notMem_closure

deleted theorem Subfield.not_mem_of_not_mem_closure

Modified Mathlib/Algebra/FreeAbelianGroup/Finsupp.lean

added theorem FreeAbelianGroup.notMem_support_iff

deleted theorem FreeAbelianGroup.not_mem_support_iff

Modified Mathlib/Algebra/FreeMonoid/Basic.lean

added theorem FreeMonoid.notMem_one

deleted theorem FreeMonoid.not_mem_one

Modified Mathlib/Algebra/GCDMonoid/Multiset.lean

Modified Mathlib/Algebra/Group/Indicator.lean

added theorem Set.mulIndicator_of_notMem

deleted theorem Set.mulIndicator_of_not_mem

added theorem Set.mulIndicator_preimage_of_notMem

deleted theorem Set.mulIndicator_preimage_of_not_mem

added theorem Set.mulIndicator_union_of_notMem_inter

deleted theorem Set.mulIndicator_union_of_not_mem_inter

Modified Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean

deleted theorem Finset.not_one_mem_div_iff

deleted theorem Finset.not_one_mem_inv_mul_iff

added theorem Finset.one_notMem_div_iff

added theorem Finset.one_notMem_inv_mul_iff

Modified Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

deleted theorem Set.not_one_mem_div_iff

deleted theorem Set.not_one_mem_inv_mul_iff

added theorem Set.one_notMem_div_iff

added theorem Set.one_notMem_inv_mul_iff

Modified Mathlib/Algebra/Group/Pointwise/Set/BigOperators.lean

Modified Mathlib/Algebra/Group/Subgroup/Finite.lean

Modified Mathlib/Algebra/Group/Subgroup/Lattice.lean

added theorem Subgroup.notMem_of_notMem_closure

deleted theorem Subgroup.not_mem_of_not_mem_closure

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

added theorem Submonoid.notMem_of_notMem_closure

deleted theorem Submonoid.not_mem_of_not_mem_closure

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

added theorem Subsemigroup.notMem_of_notMem_closure

deleted theorem Subsemigroup.not_mem_of_not_mem_closure

Modified Mathlib/Algebra/Group/Subsemigroup/Defs.lean

added theorem Subsemigroup.notMem_bot

deleted theorem Subsemigroup.not_mem_bot

Modified Mathlib/Algebra/Group/Support.lean

deleted theorem Function.nmem_mulSupport

added theorem Function.notMem_mulSupport

Modified Mathlib/Algebra/GroupWithZero/Indicator.lean

added theorem Set.indicator_eq_zero_iff_notMem

deleted theorem Set.indicator_eq_zero_iff_not_mem

Modified Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean

deleted theorem nmem_nonZeroDivisorsLeft_iff

deleted theorem nmem_nonZeroDivisorsRight_iff

deleted theorem nmem_nonZeroDivisors_iff

added theorem notMem_nonZeroDivisorsLeft_iff

added theorem notMem_nonZeroDivisorsRight_iff

added theorem notMem_nonZeroDivisors_iff

added theorem zero_notMem_nonZeroDivisors

deleted theorem zero_not_mem_nonZeroDivisors

Modified Mathlib/Algebra/Homology/Embedding/Basic.lean

added theorem ComplexShape.notMem_range_embeddingUpIntGE_iff

added theorem ComplexShape.notMem_range_embeddingUpIntLE_iff

deleted theorem ComplexShape.not_mem_range_embeddingUpIntGE_iff

deleted theorem ComplexShape.not_mem_range_embeddingUpIntLE_iff

Modified Mathlib/Algebra/Homology/Embedding/Boundary.lean

added theorem ComplexShape.Embedding.BoundaryGE.notMem

deleted theorem ComplexShape.Embedding.BoundaryGE.not_mem

added theorem ComplexShape.Embedding.BoundaryLE.notMem

deleted theorem ComplexShape.Embedding.BoundaryLE.not_mem

Modified Mathlib/Algebra/Homology/Embedding/CochainComplex.lean

Modified Mathlib/Algebra/Homology/Embedding/HomEquiv.lean

Modified Mathlib/Algebra/Lie/LieTheorem.lean

Modified Mathlib/Algebra/Lie/Semisimple/Basic.lean

Modified Mathlib/Algebra/Lie/Weights/RootSystem.lean

Modified Mathlib/Algebra/Module/LocalizedModule/Int.lean

Modified Mathlib/Algebra/Module/Submodule/Basic.lean

added theorem Submodule.notMem_of_ortho

deleted theorem Submodule.not_mem_of_ortho

Modified Mathlib/Algebra/Module/ZLattice/Basic.lean

Modified Mathlib/Algebra/MonoidAlgebra/Degree.lean

Modified Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean

Modified Mathlib/Algebra/MvPolynomial/Basic.lean

added theorem MvPolynomial.notMem_support_iff

deleted theorem MvPolynomial.not_mem_support_iff

added theorem MvPolynomial.zero_notMem_coeffs

deleted theorem MvPolynomial.zero_not_mem_coeffs

Modified Mathlib/Algebra/MvPolynomial/Degrees.lean

Modified Mathlib/Algebra/MvPolynomial/Equiv.lean

Modified Mathlib/Algebra/MvPolynomial/Eval.lean

Modified Mathlib/Algebra/MvPolynomial/PDeriv.lean

added theorem MvPolynomial.pderiv_eq_zero_of_notMem_vars

deleted theorem MvPolynomial.pderiv_eq_zero_of_not_mem_vars

Modified Mathlib/Algebra/MvPolynomial/Rename.lean

Modified Mathlib/Algebra/MvPolynomial/Variables.lean

added theorem MvPolynomial.mem_support_notMem_vars_zero

deleted theorem MvPolynomial.mem_support_not_mem_vars_zero

Modified Mathlib/Algebra/Order/Antidiag/Finsupp.lean

Modified Mathlib/Algebra/Order/Antidiag/Nat.lean

Modified Mathlib/Algebra/Order/Antidiag/Pi.lean

Modified Mathlib/Algebra/Order/Archimedean/IndicatorCard.lean

Modified Mathlib/Algebra/Order/BigOperators/Group/Finset.lean

Modified Mathlib/Algebra/Order/BigOperators/Group/LocallyFinite.lean

Modified Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean

Modified Mathlib/Algebra/Order/Floor/Ring.lean

added theorem Int.ceil_eq_floor_add_one_iff_notMem

deleted theorem Int.ceil_eq_floor_add_one_iff_not_mem

Modified Mathlib/Algebra/Order/Group/Finset.lean

Modified Mathlib/Algebra/Order/Group/Indicator.lean

Modified Mathlib/Algebra/Order/Group/Multiset.lean

Modified Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean

added theorem one_notMem_iff

deleted theorem one_not_mem_iff

Modified Mathlib/Algebra/Order/ToIntervalMod.lean

added theorem AddCommGroup.modEq_iff_forall_notMem_Ioo_mod

deleted theorem AddCommGroup.modEq_iff_not_forall_mem_Ioo_mod

Modified Mathlib/Algebra/Polynomial/AlgebraMap.lean

deleted theorem Polynomial.nmem_nonZeroDivisors_iff

added theorem Polynomial.notMem_nonZeroDivisors_iff

Modified Mathlib/Algebra/Polynomial/Basic.lean

added theorem Polynomial.notMem_support_iff

deleted theorem Polynomial.not_mem_support_iff

Modified Mathlib/Algebra/Polynomial/Coeff.lean

Modified Mathlib/Algebra/Polynomial/Degree/Definitions.lean

Modified Mathlib/Algebra/Polynomial/Degree/Operations.lean

deleted theorem Polynomial.zero_nmem_multiset_map_X_add_C

deleted theorem Polynomial.zero_nmem_multiset_map_X_sub_C

added theorem Polynomial.zero_notMem_multiset_map_X_add_C

added theorem Polynomial.zero_notMem_multiset_map_X_sub_C

Modified Mathlib/Algebra/Polynomial/EraseLead.lean

added theorem Polynomial.natDegree_notMem_eraseLead_support

deleted theorem Polynomial.natDegree_not_mem_eraseLead_support

Modified Mathlib/Algebra/Polynomial/Expand.lean

Modified Mathlib/Algebra/Polynomial/HasseDeriv.lean

Modified Mathlib/Algebra/Polynomial/Laurent.lean

Modified Mathlib/Algebra/Polynomial/Monic.lean

Modified Mathlib/Algebra/Polynomial/Monomial.lean

Modified Mathlib/Algebra/Polynomial/Reverse.lean

Modified Mathlib/Algebra/Polynomial/Roots.lean

Modified Mathlib/Algebra/Polynomial/SpecificDegree.lean

Modified Mathlib/Algebra/Polynomial/Splits.lean

Modified Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean

Modified Mathlib/Algebra/Ring/Subring/Basic.lean

added theorem Subring.notMem_of_notMem_closure

deleted theorem Subring.not_mem_of_not_mem_closure

Modified Mathlib/Algebra/Ring/Subsemiring/Basic.lean

added theorem Subsemiring.notMem_of_notMem_closure

deleted theorem Subsemiring.not_mem_of_not_mem_closure

Modified Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean

added theorem SkewMonoidAlgebra.notMem_support_iff

deleted theorem SkewMonoidAlgebra.not_mem_support_iff

Modified Mathlib/Algebra/Squarefree/Basic.lean

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

Modified Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

added theorem AlgebraicGeometry.LocallyRingedSpace.notMem_prime_iff_unit_in_stalk

deleted theorem AlgebraicGeometry.LocallyRingedSpace.not_mem_prime_iff_unit_in_stalk

Modified Mathlib/AlgebraicGeometry/Modules/Tilde.lean

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

added theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.denom_notMem

deleted theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.denom_not_mem

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean

added theorem ProjectiveSpectrum.mem_compl_zeroLocus_iff_notMem

deleted theorem ProjectiveSpectrum.mem_compl_zeroLocus_iff_not_mem

Modified Mathlib/AlgebraicGeometry/ResidueField.lean

added theorem AlgebraicGeometry.Scheme.evaluation_eq_zero_iff_notMem_basicOpen

deleted theorem AlgebraicGeometry.Scheme.evaluation_eq_zero_iff_not_mem_basicOpen

Modified Mathlib/AlgebraicGeometry/StructureSheaf.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/Degenerate.lean

added theorem SSet.mem_degenerate_iff_notMem_nonDegenerate

deleted theorem SSet.mem_degenerate_iff_not_mem_nonDegenerate

added theorem SSet.mem_nonDegenerate_iff_notMem_degenerate

deleted theorem SSet.mem_nonDegenerate_iff_not_mem_degenerate

Modified Mathlib/Analysis/Analytic/Composition.lean

Modified Mathlib/Analysis/Analytic/Order.lean

Modified Mathlib/Analysis/BoxIntegral/Basic.lean

Modified Mathlib/Analysis/BoxIntegral/Integrability.lean

Modified Mathlib/Analysis/BoxIntegral/Partition/Additive.lean

Modified Mathlib/Analysis/BoxIntegral/Partition/Basic.lean

added theorem BoxIntegral.Prepartition.notMem_bot

deleted theorem BoxIntegral.Prepartition.not_mem_bot

Modified Mathlib/Analysis/BoxIntegral/Partition/Split.lean

added theorem BoxIntegral.Prepartition.split_of_notMem_Ioo

deleted theorem BoxIntegral.Prepartition.split_of_not_mem_Ioo

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean

Modified Mathlib/Analysis/CStarAlgebra/Spectrum.lean

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

Modified Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean

added theorem ExistsContDiffBumpBase.y_eq_zero_of_notMem_ball

deleted theorem ExistsContDiffBumpBase.y_eq_zero_of_not_mem_ball

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

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

Modified Mathlib/Analysis/Calculus/DSlope.lean

deleted theorem differentiableOn_dslope_of_nmem

added theorem differentiableOn_dslope_of_notMem

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

deleted theorem derivWithin_zero_of_nmem_closure

added theorem derivWithin_zero_of_notMem_closure

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

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

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

deleted theorem HasFDerivAt.of_nmem_tsupport

added theorem HasFDerivAt.of_notMem_tsupport

added theorem HasFDerivWithinAt.of_notMem_closure

added theorem HasFDerivWithinAt.of_notMem_tsupport

deleted theorem HasFDerivWithinAt.of_not_mem_closure

deleted theorem HasFDerivWithinAt.of_not_mem_tsupport

deleted theorem HasStrictFDerivAt.of_nmem_tsupport

added theorem HasStrictFDerivAt.of_notMem_tsupport

deleted theorem fderivWithin_zero_of_nmem_closure

added theorem fderivWithin_zero_of_notMem_closure

added theorem fderiv_of_notMem_tsupport

deleted theorem fderiv_of_not_mem_tsupport

Modified Mathlib/Analysis/Calculus/FDeriv/Extend.lean

Modified Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean

Modified Mathlib/Analysis/Calculus/Monotone.lean

Modified Mathlib/Analysis/Calculus/Rademacher.lean

Modified Mathlib/Analysis/Complex/Basic.lean

added theorem Complex.zero_notMem_slitPlane

deleted theorem Complex.zero_not_mem_slitPlane

Modified Mathlib/Analysis/Complex/RemovableSingularity.lean

Modified Mathlib/Analysis/Complex/Tietze.lean

Modified Mathlib/Analysis/Convex/Basic.lean

Modified Mathlib/Analysis/Convex/Caratheodory.lean

Modified Mathlib/Analysis/Convex/Combination.lean

Modified Mathlib/Analysis/Convex/Cone/InnerDual.lean

deleted theorem ConvexCone.hyperplane_separation_of_nonempty_of_isClosed_of_nmem

added theorem ConvexCone.hyperplane_separation_of_nonempty_of_isClosed_of_notMem

Modified Mathlib/Analysis/Convex/Cone/Proper.lean

deleted theorem ProperCone.hyperplane_separation_of_nmem

added theorem ProperCone.hyperplane_separation_of_notMem

Modified Mathlib/Analysis/Convex/Deriv.lean

Modified Mathlib/Analysis/Convex/Exposed.lean

Modified Mathlib/Analysis/Convex/Extreme.lean

Modified Mathlib/Analysis/Convex/Gauge.lean

added theorem le_gauge_of_notMem

deleted theorem le_gauge_of_not_mem

added theorem one_le_gauge_of_notMem

deleted theorem one_le_gauge_of_not_mem

Modified Mathlib/Analysis/Convex/Hull.lean

added theorem Convex.convex_remove_iff_notMem_convexHull_remove

deleted theorem Convex.convex_remove_iff_not_mem_convexHull_remove

Modified Mathlib/Analysis/Convex/Independent.lean

added theorem convexIndependent_iff_notMem_convexHull_diff

deleted theorem convexIndependent_iff_not_mem_convexHull_diff

added theorem convexIndependent_set_iff_notMem_convexHull_diff

deleted theorem convexIndependent_set_iff_not_mem_convexHull_diff

Modified Mathlib/Analysis/Convex/Piecewise.lean

Modified Mathlib/Analysis/Convex/Side.lean

added theorem AffineSubspace.SOppSide.left_notMem

deleted theorem AffineSubspace.SOppSide.left_not_mem

added theorem AffineSubspace.SOppSide.right_notMem

deleted theorem AffineSubspace.SOppSide.right_not_mem

added theorem AffineSubspace.SSameSide.left_notMem

deleted theorem AffineSubspace.SSameSide.left_not_mem

added theorem AffineSubspace.SSameSide.right_notMem

deleted theorem AffineSubspace.SSameSide.right_not_mem

added theorem Sbtw.sOppSide_of_notMem_of_mem

deleted theorem Sbtw.sOppSide_of_not_mem_of_mem

Modified Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean

Modified Mathlib/Analysis/Convolution.lean

Modified Mathlib/Analysis/Distribution/AEEqOfIntegralContDiff.lean

Modified Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean

Modified Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean

Modified Mathlib/Analysis/InnerProductSpace/Projection.lean

Modified Mathlib/Analysis/InnerProductSpace/StarOrder.lean

Modified Mathlib/Analysis/LocallyConvex/BalancedCoreHull.lean

Modified Mathlib/Analysis/MellinTransform.lean

Modified Mathlib/Analysis/Normed/Algebra/Exponential.lean

Modified Mathlib/Analysis/Normed/Algebra/Spectrum.lean

Modified Mathlib/Analysis/Normed/Group/AddCircle.lean

Modified Mathlib/Analysis/Normed/Ring/Units.lean

Modified Mathlib/Analysis/NormedSpace/FunctionSeries.lean

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

Modified Mathlib/Analysis/NormedSpace/OperatorNorm/NNNorm.lean

Modified Mathlib/Analysis/SpecialFunctions/Complex/CircleMap.lean

added theorem circleMap_notMem_ball

deleted theorem circleMap_not_mem_ball

Modified Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean

Modified Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean

Modified Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean

Modified Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean

Modified Mathlib/Analysis/SpecialFunctions/Integrals.lean

Modified Mathlib/Combinatorics/Additive/Dissociation.lean

Modified Mathlib/Combinatorics/Additive/FreimanHom.lean

Modified Mathlib/Combinatorics/Colex.lean

Modified Mathlib/Combinatorics/Configuration.lean

Modified Mathlib/Combinatorics/Derangements/Basic.lean

Modified Mathlib/Combinatorics/Enumerative/Bell.lean

Modified Mathlib/Combinatorics/Enumerative/Partition.lean

Modified Mathlib/Combinatorics/HalesJewett.lean

Modified Mathlib/Combinatorics/Hall/Finite.lean

Modified Mathlib/Combinatorics/Schnirelmann.lean

added theorem schnirelmannDensity_eq_zero_of_one_notMem

deleted theorem schnirelmannDensity_eq_zero_of_one_not_mem

added theorem schnirelmannDensity_le_of_notMem

deleted theorem schnirelmannDensity_le_of_not_mem

Modified Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean

deleted theorem AhlswedeZhang.supSum_of_not_univ_mem

added theorem AhlswedeZhang.supSum_of_univ_notMem

modified theorem Finset.truncatedInf_empty

added theorem Finset.truncatedInf_of_notMem

deleted theorem Finset.truncatedInf_of_not_mem

added theorem Finset.truncatedInf_sups_of_notMem

deleted theorem Finset.truncatedInf_sups_of_not_mem

added theorem Finset.truncatedInf_union_of_notMem

deleted theorem Finset.truncatedInf_union_of_not_mem

modified theorem Finset.truncatedSup_empty

added theorem Finset.truncatedSup_infs_of_notMem

deleted theorem Finset.truncatedSup_infs_of_not_mem

added theorem Finset.truncatedSup_of_notMem

deleted theorem Finset.truncatedSup_of_not_mem

added theorem Finset.truncatedSup_union_of_notMem

deleted theorem Finset.truncatedSup_union_of_not_mem

Modified Mathlib/Combinatorics/SetFamily/Compression/Down.lean

Modified Mathlib/Combinatorics/SetFamily/Compression/UV.lean

added theorem UV.disjoint_of_mem_compression_of_notMem

deleted theorem UV.disjoint_of_mem_compression_of_not_mem

added theorem UV.le_of_mem_compression_of_notMem

deleted theorem UV.le_of_mem_compression_of_not_mem

added theorem UV.sup_sdiff_mem_of_mem_compression_of_notMem

deleted theorem UV.sup_sdiff_mem_of_mem_compression_of_not_mem

Modified Mathlib/Combinatorics/SetFamily/FourFunctions.lean

Modified Mathlib/Combinatorics/SetFamily/HarrisKleitman.lean

Modified Mathlib/Combinatorics/SetFamily/Intersecting.lean

added theorem Set.Intersecting.bot_notMem

added theorem Set.Intersecting.compl_notMem

added theorem Set.Intersecting.notMem

deleted theorem Set.Intersecting.not_bot_mem

deleted theorem Set.Intersecting.not_compl_mem

deleted theorem Set.Intersecting.not_mem

Modified Mathlib/Combinatorics/SetFamily/Kleitman.lean

Modified Mathlib/Combinatorics/SetFamily/KruskalKatona.lean

Modified Mathlib/Combinatorics/SetFamily/LYM.lean

Modified Mathlib/Combinatorics/SetFamily/Shadow.lean

Modified Mathlib/Combinatorics/SetFamily/Shatter.lean

Modified Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

Modified Mathlib/Combinatorics/SimpleGraph/Basic.lean

added theorem SimpleGraph.notMem_commonNeighbors_left

added theorem SimpleGraph.notMem_commonNeighbors_right

added theorem SimpleGraph.notMem_neighborSet_self

deleted theorem SimpleGraph.not_mem_commonNeighbors_left

deleted theorem SimpleGraph.not_mem_commonNeighbors_right

deleted theorem SimpleGraph.not_mem_neighborSet_self

Modified Mathlib/Combinatorics/SimpleGraph/Bipartite.lean

Modified Mathlib/Combinatorics/SimpleGraph/Clique.lean

added theorem SimpleGraph.isClique_insert_of_notMem

deleted theorem SimpleGraph.isClique_insert_of_not_mem

Modified Mathlib/Combinatorics/SimpleGraph/Coloring.lean

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/Represents.lean

added theorem SimpleGraph.ConnectedComponent.Represents.disjoint_supp_of_notMem

deleted theorem SimpleGraph.ConnectedComponent.Represents.disjoint_supp_of_not_mem

added theorem SimpleGraph.ConnectedComponent.Represents.ncard_sdiff_of_notMem

deleted theorem SimpleGraph.ConnectedComponent.Represents.ncard_sdiff_of_not_mem

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean

added theorem SimpleGraph.Walk.notMem_support_takeUntil_support_takeUntil_subset

deleted theorem SimpleGraph.Walk.not_mem_support_takeUntil_support_takeUntil_subset

Modified Mathlib/Combinatorics/SimpleGraph/Copy.lean

Modified Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean

Modified Mathlib/Combinatorics/SimpleGraph/DeleteEdges.lean

modified theorem SimpleGraph.deleteEdges_adj

added theorem SimpleGraph.induce_deleteIncidenceSet_of_notMem

deleted theorem SimpleGraph.induce_deleteIncidenceSet_of_not_mem

Modified Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean

added theorem SimpleGraph.ComponentCompl.notMem_of_mem

deleted theorem SimpleGraph.ComponentCompl.not_mem_of_mem

Modified Mathlib/Combinatorics/SimpleGraph/Finite.lean

added theorem SimpleGraph.degree_eq_zero_iff_notMem_support

deleted theorem SimpleGraph.degree_eq_zero_iff_not_mem_support

added theorem SimpleGraph.notMem_neighborFinset_self

deleted theorem SimpleGraph.not_mem_neighborFinset_self

Modified Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean

added theorem SimpleGraph.incMatrix_of_notMem_incidenceSet

deleted theorem SimpleGraph.incMatrix_of_not_mem_incidenceSet

added theorem SimpleGraph.sum_incMatrix_apply_of_notMem_edgeSet

deleted theorem SimpleGraph.sum_incMatrix_apply_of_not_mem_edgeSet

Modified Mathlib/Combinatorics/SimpleGraph/Matching.lean

Modified Mathlib/Combinatorics/SimpleGraph/Path.lean

added theorem SimpleGraph.Path.notMem_edges_of_loop

deleted theorem SimpleGraph.Path.not_mem_edges_of_loop

added theorem SimpleGraph.Walk.endpoint_notMem_support_takeUntil

deleted theorem SimpleGraph.Walk.endpoint_not_mem_support_takeUntil

added theorem SimpleGraph.isBridge_iff_adj_and_forall_cycle_notMem

deleted theorem SimpleGraph.isBridge_iff_adj_and_forall_cycle_not_mem

added theorem SimpleGraph.isBridge_iff_mem_and_forall_cycle_notMem

deleted theorem SimpleGraph.isBridge_iff_mem_and_forall_cycle_not_mem

Modified Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean

Modified Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean

Modified Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean

Modified Mathlib/Combinatorics/SimpleGraph/Subgraph.lean

modified theorem SimpleGraph.Subgraph.deleteEdges_adj

Modified Mathlib/Combinatorics/SimpleGraph/Walk.lean

Modified Mathlib/Combinatorics/Young/YoungDiagram.lean

added theorem YoungDiagram.notMem_bot

deleted theorem YoungDiagram.not_mem_bot

Modified Mathlib/Computability/EpsilonNFA.lean

Modified Mathlib/Computability/Language.lean

added theorem Language.notMem_zero

deleted theorem Language.not_mem_zero

Modified Mathlib/Computability/PostTuringMachine.lean

Modified Mathlib/Computability/TuringMachine.lean

Modified Mathlib/Control/LawfulFix.lean

Modified Mathlib/Data/DFinsupp/Defs.lean

added theorem DFinsupp.mk_of_notMem

deleted theorem DFinsupp.mk_of_not_mem

added theorem DFinsupp.notMem_support_iff

deleted theorem DFinsupp.not_mem_support_iff

Modified Mathlib/Data/DFinsupp/Interval.lean

Modified Mathlib/Data/DFinsupp/Lex.lean

Modified Mathlib/Data/DFinsupp/Multiset.lean

Modified Mathlib/Data/DFinsupp/NeLocus.lean

added theorem DFinsupp.notMem_neLocus

deleted theorem DFinsupp.not_mem_neLocus

Modified Mathlib/Data/DFinsupp/Order.lean

Modified Mathlib/Data/DFinsupp/WellFounded.lean

Modified Mathlib/Data/FinEnum.lean

Modified Mathlib/Data/Finmap.lean

added theorem Finmap.entries_insert_of_notMem

deleted theorem Finmap.entries_insert_of_not_mem

added theorem Finmap.notMem_empty

added theorem Finmap.notMem_erase_self

deleted theorem Finmap.not_mem_empty

deleted theorem Finmap.not_mem_erase_self

Modified Mathlib/Data/Finset/Basic.lean

added theorem Finset.sdiff_insert_insert_of_mem_of_notMem

deleted theorem Finset.sdiff_insert_insert_of_mem_of_not_mem

added theorem Finset.subset_insert_iff_of_notMem

deleted theorem Finset.subset_insert_iff_of_not_mem

Modified Mathlib/Data/Finset/BooleanAlgebra.lean

added theorem Finset.notMem_compl

deleted theorem Finset.not_mem_compl

Modified Mathlib/Data/Finset/Card.lean

added theorem Finset.card_insert_of_notMem

deleted theorem Finset.card_insert_of_not_mem

added theorem Finset.exists_mem_notMem_of_card_lt_card

deleted theorem Finset.exists_mem_not_mem_of_card_lt_card

Modified Mathlib/Data/Finset/Defs.lean

added theorem Finset.notMem_mono

deleted theorem Finset.not_mem_mono

Modified Mathlib/Data/Finset/Disjoint.lean

Modified Mathlib/Data/Finset/Empty.lean

added theorem Finset.eq_empty_iff_forall_notMem

deleted theorem Finset.eq_empty_iff_forall_not_mem

added theorem Finset.eq_empty_of_forall_notMem

deleted theorem Finset.eq_empty_of_forall_not_mem

added theorem Finset.notMem_empty

deleted theorem Finset.not_mem_empty

modified theorem Finset.not_nonempty_empty

Modified Mathlib/Data/Finset/Erase.lean

added theorem Finset.eq_of_mem_of_notMem_erase

deleted theorem Finset.eq_of_mem_of_not_mem_erase

added theorem Finset.erase_eq_of_notMem

deleted theorem Finset.erase_eq_of_not_mem

added theorem Finset.notMem_erase

deleted theorem Finset.not_mem_erase

Modified Mathlib/Data/Finset/Finsupp.lean

Modified Mathlib/Data/Finset/Fold.lean

Modified Mathlib/Data/Finset/Image.lean

added theorem Finset.notMem_map_subtype_of_not_property

deleted theorem Finset.not_mem_map_subtype_of_not_property

Modified Mathlib/Data/Finset/Insert.lean

modified theorem Finset.cons_empty

added theorem Finset.eq_of_mem_cons_of_notMem

deleted theorem Finset.eq_of_mem_cons_of_not_mem

added theorem Finset.eq_of_mem_insert_of_notMem

deleted theorem Finset.eq_of_mem_insert_of_not_mem

added theorem Finset.insert_val_of_notMem

deleted theorem Finset.insert_val_of_not_mem

added theorem Finset.ne_insert_of_notMem

deleted theorem Finset.ne_insert_of_not_mem

added theorem Finset.notMem_singleton

deleted theorem Finset.not_mem_singleton

Modified Mathlib/Data/Finset/Lattice/Basic.lean

added theorem Finset.notMem_union

deleted theorem Finset.not_mem_union

Modified Mathlib/Data/Finset/Lattice/Fold.lean

Modified Mathlib/Data/Finset/Lattice/Lemmas.lean

added theorem Finset.insert_inter_of_notMem

deleted theorem Finset.insert_inter_of_not_mem

added theorem Finset.inter_insert_of_notMem

deleted theorem Finset.inter_insert_of_not_mem

added theorem Finset.inter_singleton_of_notMem

deleted theorem Finset.inter_singleton_of_not_mem

added theorem Finset.singleton_inter_of_notMem

deleted theorem Finset.singleton_inter_of_not_mem

Modified Mathlib/Data/Finset/Max.lean

added theorem Finset.notMem_of_coe_lt_min

added theorem Finset.notMem_of_lt_min

added theorem Finset.notMem_of_max_lt

added theorem Finset.notMem_of_max_lt_coe

deleted theorem Finset.not_mem_of_coe_lt_min

deleted theorem Finset.not_mem_of_lt_min

deleted theorem Finset.not_mem_of_max_lt

deleted theorem Finset.not_mem_of_max_lt_coe

Modified Mathlib/Data/Finset/NoncommProd.lean

added theorem Finset.noncommProd_insert_of_notMem'

added theorem Finset.noncommProd_insert_of_notMem

deleted theorem Finset.noncommProd_insert_of_not_mem'

deleted theorem Finset.noncommProd_insert_of_not_mem

Modified Mathlib/Data/Finset/Pi.lean

Modified Mathlib/Data/Finset/PiInduction.lean

Modified Mathlib/Data/Finset/Piecewise.lean

added theorem Finset.piecewise_eq_of_notMem

deleted theorem Finset.piecewise_eq_of_not_mem

added theorem Finset.update_piecewise_of_notMem

deleted theorem Finset.update_piecewise_of_not_mem

Modified Mathlib/Data/Finset/Powerset.lean

added theorem Finset.notMem_of_mem_powerset_of_notMem

deleted theorem Finset.not_mem_of_mem_powerset_of_not_mem

Modified Mathlib/Data/Finset/Prod.lean

Modified Mathlib/Data/Finset/Range.lean

added theorem Finset.notMem_range_self

deleted theorem Finset.not_mem_range_self

Modified Mathlib/Data/Finset/SDiff.lean

added theorem Finset.insert_sdiff_of_notMem

deleted theorem Finset.insert_sdiff_of_not_mem

added theorem Finset.notMem_sdiff_of_mem_right

added theorem Finset.notMem_sdiff_of_notMem_left

deleted theorem Finset.not_mem_sdiff_of_mem_right

deleted theorem Finset.not_mem_sdiff_of_not_mem_left

added theorem Finset.sdiff_insert_of_notMem

deleted theorem Finset.sdiff_insert_of_not_mem

Modified Mathlib/Data/Finset/Sigma.lean

added theorem Finset.notMem_sigmaLift_of_ne_left

added theorem Finset.notMem_sigmaLift_of_ne_right

deleted theorem Finset.not_mem_sigmaLift_of_ne_left

deleted theorem Finset.not_mem_sigmaLift_of_ne_right

Modified Mathlib/Data/Finset/Sym.lean

Modified Mathlib/Data/Finsupp/Basic.lean

added theorem Finsupp.notMem_graph_snd_zero

deleted theorem Finsupp.not_mem_graph_snd_zero

added theorem Finsupp.zero_notMem_frange

deleted theorem Finsupp.zero_not_mem_frange

Modified Mathlib/Data/Finsupp/Defs.lean

added theorem Finsupp.notMem_support_iff

deleted theorem Finsupp.not_mem_support_iff

Modified Mathlib/Data/Finsupp/Indicator.lean

added theorem Finsupp.indicator_of_notMem

deleted theorem Finsupp.indicator_of_not_mem

Modified Mathlib/Data/Finsupp/Interval.lean

Modified Mathlib/Data/Finsupp/NeLocus.lean

added theorem Finsupp.notMem_neLocus

deleted theorem Finsupp.not_mem_neLocus

Modified Mathlib/Data/Finsupp/Order.lean

Modified Mathlib/Data/Finsupp/Single.lean

added theorem Finsupp.erase_of_notMem_support

deleted theorem Finsupp.erase_of_not_mem_support

Modified Mathlib/Data/Finsupp/Weight.lean

Modified Mathlib/Data/Fintype/BigOperators.lean

Modified Mathlib/Data/Fintype/Card.lean

added theorem Finset.card_lt_univ_of_notMem

deleted theorem Finset.card_lt_univ_of_not_mem

added theorem Fintype.card_lt_of_injective_of_notMem

deleted theorem Fintype.card_lt_of_injective_of_not_mem

Modified Mathlib/Data/Fintype/EquivFin.lean

added theorem Infinite.exists_notMem_finset

deleted theorem Infinite.exists_not_mem_finset

Modified Mathlib/Data/Fintype/Pi.lean

added theorem Fintype.filter_piFinset_of_notMem

deleted theorem Fintype.filter_piFinset_of_not_mem

Modified Mathlib/Data/Holor.lean

Modified Mathlib/Data/List/AList.lean

added theorem AList.entries_insert_of_notMem

deleted theorem AList.entries_insert_of_not_mem

added theorem AList.insert_of_notMem

deleted theorem AList.insert_of_not_mem

added theorem AList.notMem_empty

deleted theorem AList.not_mem_empty

Modified Mathlib/Data/List/Basic.lean

added theorem List.append_cons_inj_of_notMem

deleted theorem List.append_cons_inj_of_not_mem

added theorem List.idxOf_append_of_notMem

deleted theorem List.idxOf_append_of_not_mem

added theorem List.idxOf_of_notMem

deleted theorem List.idxOf_of_not_mem

Modified Mathlib/Data/List/Cycle.lean

added theorem Cycle.notMem_nil

deleted theorem Cycle.not_mem_nil

Modified Mathlib/Data/List/Dedup.lean

added theorem List.dedup_cons_of_notMem'

added theorem List.dedup_cons_of_notMem

deleted theorem List.dedup_cons_of_not_mem'

deleted theorem List.dedup_cons_of_not_mem

Modified Mathlib/Data/List/Intervals.lean

added theorem List.Ico.notMem_top

deleted theorem List.Ico.not_mem_top

Modified Mathlib/Data/List/Lattice.lean

added theorem List.inter_cons_of_notMem

deleted theorem List.inter_cons_of_not_mem

Modified Mathlib/Data/List/Lemmas.lean

added theorem List.injOn_insertIdx_index_of_notMem

deleted theorem List.injOn_insertIdx_index_of_not_mem

Modified Mathlib/Data/List/Nodup.lean

added theorem List.Nodup.notMem

deleted theorem List.Nodup.not_mem

Modified Mathlib/Data/List/Perm/Lattice.lean

Modified Mathlib/Data/List/Permutation.lean

added theorem List.nodup_permutations'Aux_of_notMem

deleted theorem List.nodup_permutations'Aux_of_not_mem

Modified Mathlib/Data/List/Sigma.lean

added theorem List.kerase_of_notMem_keys

deleted theorem List.kerase_of_not_mem_keys

added theorem List.notMem_keys

added theorem List.notMem_keys_kerase

added theorem List.notMem_keys_of_nodupKeys_cons

deleted theorem List.not_mem_keys

deleted theorem List.not_mem_keys_kerase

deleted theorem List.not_mem_keys_of_nodupKeys_cons

Modified Mathlib/Data/List/Sort.lean

added theorem List.erase_orderedInsert_of_notMem

deleted theorem List.erase_orderedInsert_of_not_mem

Modified Mathlib/Data/List/SplitBy.lean

added theorem List.nil_notMem_splitBy

deleted theorem List.nil_not_mem_splitBy

Modified Mathlib/Data/List/Sym.lean

Modified Mathlib/Data/Matroid/Basic.lean

Modified Mathlib/Data/Matroid/Circuit.lean

added theorem Matroid.fundCircuit_eq_of_notMem_ground

deleted theorem Matroid.fundCircuit_eq_of_not_mem_ground

added theorem Matroid.fundCocircuit_eq_of_notMem

added theorem Matroid.fundCocircuit_eq_of_notMem_ground

deleted theorem Matroid.fundCocircuit_eq_of_not_mem

deleted theorem Matroid.fundCocircuit_eq_of_not_mem_ground

Modified Mathlib/Data/Matroid/Closure.lean

added theorem Matroid.Indep.insert_indep_iff_of_notMem

deleted theorem Matroid.Indep.insert_indep_iff_of_not_mem

added theorem Matroid.Indep.mem_closure_iff_of_notMem

deleted theorem Matroid.Indep.mem_closure_iff_of_not_mem

added theorem Matroid.Indep.notMem_closure_diff_of_mem

added theorem Matroid.Indep.notMem_closure_iff

added theorem Matroid.Indep.notMem_closure_iff_of_notMem

deleted theorem Matroid.Indep.not_mem_closure_diff_of_mem

deleted theorem Matroid.Indep.not_mem_closure_iff

deleted theorem Matroid.Indep.not_mem_closure_iff_of_not_mem

added theorem Matroid.Indep.union_indep_iff_forall_notMem_closure_left

added theorem Matroid.Indep.union_indep_iff_forall_notMem_closure_right

deleted theorem Matroid.Indep.union_indep_iff_forall_not_mem_closure_left

deleted theorem Matroid.Indep.union_indep_iff_forall_not_mem_closure_right

added theorem Matroid.IsBase.exchange_base_of_notMem_closure

deleted theorem Matroid.IsBase.exchange_base_of_not_mem_closure

added theorem Matroid.IsBasis.insert_isBasis_insert_of_notMem_closure

deleted theorem Matroid.IsBasis.insert_isBasis_insert_of_not_mem_closure

added theorem Matroid.indep_iff_forall_notMem_closure_diff'

added theorem Matroid.indep_iff_forall_notMem_closure_diff

deleted theorem Matroid.indep_iff_forall_not_mem_closure_diff'

deleted theorem Matroid.indep_iff_forall_not_mem_closure_diff

added theorem Matroid.notMem_of_mem_diff_closure

deleted theorem Matroid.not_mem_of_mem_diff_closure

Modified Mathlib/Data/Matroid/IndepAxioms.lean

Modified Mathlib/Data/Matroid/Loop.lean

added theorem Matroid.IsBase.isColoop_iff_forall_notMem_fundCircuit

deleted theorem Matroid.IsBase.isColoop_iff_forall_not_mem_fundCircuit

added theorem Matroid.IsColoop.notMem_closure_of_notMem

added theorem Matroid.IsColoop.notMem_isCircuit

deleted theorem Matroid.IsColoop.not_mem_closure_of_not_mem

deleted theorem Matroid.IsColoop.not_mem_isCircuit

added theorem Matroid.IsLoop.notMem_of_indep

deleted theorem Matroid.IsLoop.not_mem_of_indep

added theorem Matroid.isColoop_iff_forall_notMem_isCircuit

deleted theorem Matroid.isColoop_iff_forall_not_mem_isCircuit

added theorem Matroid.isColoop_iff_notMem_closure_compl

deleted theorem Matroid.isColoop_iff_not_mem_closure_compl

added theorem Matroid.isLoop_iff_forall_notMem_isBase

deleted theorem Matroid.isLoop_iff_forall_not_mem_isBase

added theorem Matroid.isNonloop_iff_notMem_loops

deleted theorem Matroid.isNonloop_iff_not_mem_loops

added theorem Matroid.isNonloop_of_notMem_closure

deleted theorem Matroid.isNonloop_of_not_mem_closure

Modified Mathlib/Data/Matroid/Minor/Delete.lean

added theorem Matroid.isNonloop_iff_delete_of_notMem

deleted theorem Matroid.isNonloop_iff_delete_of_not_mem

Modified Mathlib/Data/Matroid/Rank/ENat.lean

added theorem Matroid.eRk_insert_of_notMem_ground

deleted theorem Matroid.eRk_insert_of_not_mem_ground

Modified Mathlib/Data/Multiset/AddSub.lean

added theorem Multiset.erase_of_notMem

deleted theorem Multiset.erase_of_not_mem

Modified Mathlib/Data/Multiset/Count.lean

added theorem Multiset.count_eq_zero_of_notMem

deleted theorem Multiset.count_eq_zero_of_not_mem

Modified Mathlib/Data/Multiset/Dedup.lean

added theorem Multiset.dedup_cons_of_notMem

deleted theorem Multiset.dedup_cons_of_not_mem

Modified Mathlib/Data/Multiset/Defs.lean

added theorem Multiset.notMem_mono

deleted theorem Multiset.not_mem_mono

Modified Mathlib/Data/Multiset/DershowitzManna.lean

Modified Mathlib/Data/Multiset/Filter.lean

added theorem Multiset.Nodup.notMem_erase

deleted theorem Multiset.Nodup.not_mem_erase

Modified Mathlib/Data/Multiset/FinsetOps.lean

added theorem Multiset.length_ndinsert_of_notMem

deleted theorem Multiset.length_ndinsert_of_not_mem

added theorem Multiset.ndinsert_of_notMem

deleted theorem Multiset.ndinsert_of_not_mem

added theorem Multiset.ndinter_cons_of_notMem

deleted theorem Multiset.ndinter_cons_of_not_mem

Modified Mathlib/Data/Multiset/Pi.lean

Modified Mathlib/Data/Multiset/Range.lean

added theorem Multiset.notMem_range_self

deleted theorem Multiset.not_mem_range_self

Modified Mathlib/Data/Multiset/UnionInter.lean

Modified Mathlib/Data/Multiset/ZeroCons.lean

added theorem Multiset.Nodup.notMem

deleted theorem Multiset.Nodup.not_mem

added theorem Multiset.cons_le_of_notMem

deleted theorem Multiset.cons_le_of_not_mem

added theorem Multiset.eq_zero_iff_forall_notMem

deleted theorem Multiset.eq_zero_iff_forall_not_mem

added theorem Multiset.eq_zero_of_forall_notMem

deleted theorem Multiset.eq_zero_of_forall_not_mem

added theorem Multiset.le_cons_of_notMem

deleted theorem Multiset.le_cons_of_not_mem

added theorem Multiset.notMem_zero

deleted theorem Multiset.not_mem_zero

Modified Mathlib/Data/Nat/BitIndices.lean

added theorem Nat.notMem_bitIndices_self

deleted theorem Nat.not_mem_bitIndices_self

Modified Mathlib/Data/Nat/Choose/Multinomial.lean

added theorem Sym.multinomial_coe_fill_of_notMem

deleted theorem Sym.multinomial_coe_fill_of_not_mem

Modified Mathlib/Data/Nat/Factorization/Basic.lean

Modified Mathlib/Data/Nat/Factorization/Defs.lean

Modified Mathlib/Data/Nat/Factorization/PrimePow.lean

Modified Mathlib/Data/Nat/Lattice.lean

added theorem Nat.notMem_of_lt_sInf

deleted theorem Nat.not_mem_of_lt_sInf

Modified Mathlib/Data/Nat/Nth.lean

Modified Mathlib/Data/Part.lean

added theorem Part.notMem_none

deleted theorem Part.not_mem_none

Modified Mathlib/Data/Prod/TProd.lean

Modified Mathlib/Data/Real/Hyperreal.lean

Modified Mathlib/Data/Rel.lean

Modified Mathlib/Data/Seq/Computation.lean

modified theorem Computation.empty_promises

added theorem Computation.notMem_empty

deleted theorem Computation.not_mem_empty

modified theorem Computation.not_terminates_empty

Modified Mathlib/Data/Seq/Parallel.lean

Modified Mathlib/Data/Seq/Seq.lean

added theorem Stream'.Seq.notMem_nil

deleted theorem Stream'.Seq.not_mem_nil

Modified Mathlib/Data/Set/Basic.lean

added theorem Set.eq_empty_iff_forall_notMem

deleted theorem Set.eq_empty_iff_forall_not_mem

added theorem Set.eq_empty_of_forall_notMem

deleted theorem Set.eq_empty_of_forall_not_mem

added theorem Set.ne_univ_iff_exists_notMem

deleted theorem Set.ne_univ_iff_exists_not_mem

deleted theorem Set.nmem_setOf_iff

added theorem Set.notMem_compl_iff

added theorem Set.notMem_diff_of_mem

added theorem Set.notMem_empty

added theorem Set.notMem_of_mem_compl

added theorem Set.notMem_of_mem_diff

added theorem Set.notMem_setOf_iff

added theorem Set.notMem_subset

deleted theorem Set.not_mem_compl_iff

deleted theorem Set.not_mem_diff_of_mem

deleted theorem Set.not_mem_empty

deleted theorem Set.not_mem_of_mem_compl

deleted theorem Set.not_mem_of_mem_diff

deleted theorem Set.not_mem_subset

added theorem Set.not_notMem

deleted theorem Set.not_not_mem

added theorem Set.not_subset_iff_exists_mem_notMem

deleted theorem Set.not_subset_iff_exists_mem_not_mem

Modified Mathlib/Data/Set/BoolIndicator.lean

added theorem Set.notMem_iff_boolIndicator

deleted theorem Set.not_mem_iff_boolIndicator

Modified Mathlib/Data/Set/Card.lean

added theorem Set.encard_insert_of_notMem

deleted theorem Set.encard_insert_of_not_mem

added theorem Set.exists_mem_notMem_of_ncard_lt_ncard

deleted theorem Set.exists_mem_not_mem_of_ncard_lt_ncard

added theorem Set.ncard_insert_of_notMem

deleted theorem Set.ncard_insert_of_not_mem

Modified Mathlib/Data/Set/Disjoint.lean

Modified Mathlib/Data/Set/Equitable.lean

Modified Mathlib/Data/Set/Finite/Basic.lean

added theorem Finset.exists_notMem

deleted theorem Finset.exists_not_mem

added theorem Set.Finite.exists_notMem

deleted theorem Set.Finite.exists_not_mem

added theorem Set.Infinite.exists_notMem_finite

added theorem Set.Infinite.exists_notMem_finset

deleted theorem Set.Infinite.exists_not_mem_finite

deleted theorem Set.Infinite.exists_not_mem_finset

Modified Mathlib/Data/Set/Function.lean

added theorem Function.update_comp_eq_of_notMem_range'

added theorem Function.update_comp_eq_of_notMem_range

deleted theorem Function.update_comp_eq_of_not_mem_range'

deleted theorem Function.update_comp_eq_of_not_mem_range

added theorem Set.preimage_invFun_of_notMem

deleted theorem Set.preimage_invFun_of_not_mem

Modified Mathlib/Data/Set/Image.lean

added theorem Set.preimage_const_of_notMem

deleted theorem Set.preimage_const_of_not_mem

Modified Mathlib/Data/Set/Insert.lean

added theorem HasSubset.Subset.ssubset_of_mem_notMem

deleted theorem HasSubset.Subset.ssubset_of_mem_not_mem

added theorem Set.diff_insert_of_notMem

deleted theorem Set.diff_insert_of_not_mem

added theorem Set.eq_of_mem_insert_of_notMem

deleted theorem Set.eq_of_not_mem_of_mem_insert

added theorem Set.insert_diff_of_notMem

deleted theorem Set.insert_diff_of_not_mem

added theorem Set.insert_diff_self_of_notMem

deleted theorem Set.insert_diff_self_of_not_mem

added theorem Set.insert_inter_of_notMem

deleted theorem Set.insert_inter_of_not_mem

added theorem Set.inter_insert_of_notMem

deleted theorem Set.inter_insert_of_not_mem

added theorem Set.ne_insert_of_notMem

deleted theorem Set.ne_insert_of_not_mem

deleted theorem Set.nmem_singleton_empty

added theorem Set.notMem_singleton_empty

added theorem Set.notMem_singleton_iff

deleted theorem Set.not_mem_singleton_iff

added theorem Set.subset_insert_iff_of_notMem

deleted theorem Set.subset_insert_iff_of_not_mem

Modified Mathlib/Data/Set/Lattice.lean

added theorem Set.notMem_of_notMem_sUnion

deleted theorem Set.not_mem_of_not_mem_sUnion

Modified Mathlib/Data/Set/Pairwise/Basic.lean

added theorem Set.Pairwise.insert_of_notMem

deleted theorem Set.Pairwise.insert_of_not_mem

added theorem Set.Pairwise.insert_of_symmetric_of_notMem

deleted theorem Set.Pairwise.insert_of_symmetric_of_not_mem

added theorem Set.PairwiseDisjoint.insert_of_notMem

deleted theorem Set.PairwiseDisjoint.insert_of_not_mem

added theorem Set.pairwiseDisjoint_insert_of_notMem

deleted theorem Set.pairwiseDisjoint_insert_of_not_mem

added theorem Set.pairwise_insert_of_notMem

deleted theorem Set.pairwise_insert_of_not_mem

added theorem Set.pairwise_insert_of_symmetric_of_notMem

deleted theorem Set.pairwise_insert_of_symmetric_of_not_mem

Modified Mathlib/Data/Set/Pairwise/Lattice.lean

Modified Mathlib/Data/Set/Piecewise.lean

added theorem Set.piecewise_eq_of_notMem

deleted theorem Set.piecewise_eq_of_not_mem

Modified Mathlib/Data/Set/Prod.lean

added theorem Set.eval_image_pi_of_notMem

deleted theorem Set.eval_image_pi_of_not_mem

added theorem Set.pi_update_of_notMem

deleted theorem Set.pi_update_of_not_mem

Modified Mathlib/Data/Setoid/Partition.lean

added theorem Setoid.empty_notMem_classes

deleted theorem Setoid.empty_not_mem_classes

Modified Mathlib/Data/Sum/Interval.lean

Modified Mathlib/Data/Sym/Basic.lean

added theorem Sym.count_coe_fill_self_of_notMem

deleted theorem Sym.count_coe_fill_self_of_not_mem

added theorem Sym.notMem_nil

deleted theorem Sym.not_mem_nil

added theorem SymOptionSuccEquiv.encode_of_none_notMem

deleted theorem SymOptionSuccEquiv.encode_of_not_none_mem

Modified Mathlib/Data/Sym/Card.lean

Modified Mathlib/Data/Sym/Sym2.lean

Modified Mathlib/Data/Vector/Mem.lean

added theorem List.Vector.notMem_map_zero

added theorem List.Vector.notMem_nil

added theorem List.Vector.notMem_zero

deleted theorem List.Vector.not_mem_map_zero

deleted theorem List.Vector.not_mem_nil

deleted theorem List.Vector.not_mem_zero

Modified Mathlib/Data/WSeq/Basic.lean

added theorem Stream'.WSeq.notMem_nil

deleted theorem Stream'.WSeq.not_mem_nil

Modified Mathlib/Dynamics/Ergodic/Conservative.lean

added theorem MeasureTheory.Conservative.measure_mem_forall_ge_image_notMem_eq_zero

deleted theorem MeasureTheory.Conservative.measure_mem_forall_ge_image_not_mem_eq_zero

Modified Mathlib/Dynamics/Ergodic/Ergodic.lean

deleted theorem PreErgodic.ae_mem_or_ae_nmem

added theorem PreErgodic.ae_mem_or_ae_notMem

deleted theorem QuasiErgodic.ae_mem_or_ae_nmem₀

added theorem QuasiErgodic.ae_mem_or_ae_notMem₀

Modified Mathlib/Dynamics/Ergodic/Function.lean

Modified Mathlib/Dynamics/PeriodicPts/Defs.lean

deleted theorem Function.minimalPeriod_eq_zero_iff_nmem_periodicPts

added theorem Function.minimalPeriod_eq_zero_iff_notMem_periodicPts

deleted theorem Function.minimalPeriod_eq_zero_of_nmem_periodicPts

added theorem Function.minimalPeriod_eq_zero_of_notMem_periodicPts

Modified Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean

Modified Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean

Modified Mathlib/FieldTheory/Finite/Basic.lean

Modified Mathlib/FieldTheory/Galois/Basic.lean

Modified Mathlib/FieldTheory/Minpoly/IsConjRoot.lean

added theorem notMem_iff_exists_ne_and_isConjRoot

deleted theorem not_mem_iff_exists_ne_and_isConjRoot

Modified Mathlib/FieldTheory/PrimitiveElement.lean

Modified Mathlib/FieldTheory/PurelyInseparable/Tower.lean

Modified Mathlib/FieldTheory/Separable.lean

Modified Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean

Modified Mathlib/Geometry/Euclidean/Circumcenter.lean

Modified Mathlib/Geometry/Euclidean/MongePoint.lean

Modified Mathlib/Geometry/Euclidean/Projection.lean

added theorem EuclideanGeometry.dist_orthogonalProjection_ne_zero_of_notMem

deleted theorem EuclideanGeometry.dist_orthogonalProjection_ne_zero_of_not_mem

Modified Mathlib/Geometry/Manifold/ContMDiff/Basic.lean

added theorem contMDiffAt_of_notMem_mulTSupport

deleted theorem contMDiffAt_of_not_mem_mulTSupport

added theorem contMDiffWithinAt_of_notMem_mulTSupport

deleted theorem contMDiffWithinAt_of_not_mem_mulTSupport

Modified Mathlib/Geometry/Manifold/PartitionOfUnity.lean

Modified Mathlib/Geometry/RingedSpace/LocallyRingedSpace/ResidueField.lean

added theorem AlgebraicGeometry.LocallyRingedSpace.evaluation_eq_zero_iff_notMem_basicOpen

deleted theorem AlgebraicGeometry.LocallyRingedSpace.evaluation_eq_zero_iff_not_mem_basicOpen

added theorem AlgebraicGeometry.LocallyRingedSpace.Γevaluation_eq_zero_iff_notMem_basicOpen

deleted theorem AlgebraicGeometry.LocallyRingedSpace.Γevaluation_eq_zero_iff_not_mem_basicOpen

Modified Mathlib/GroupTheory/Archimedean.lean

Modified Mathlib/GroupTheory/CosetCover.lean

deleted theorem Subspace.biUnion_ne_univ_of_top_nmem

added theorem Subspace.biUnion_ne_univ_of_top_notMem

Modified Mathlib/GroupTheory/Exponent.lean

added theorem mul_notMem_of_exponent_two

added theorem mul_notMem_of_orderOf_eq_two

deleted theorem mul_not_mem_of_exponent_two

deleted theorem mul_not_mem_of_orderOf_eq_two

Modified Mathlib/GroupTheory/GroupAction/Primitive.lean

added theorem MulAction.IsPreprimitive.exists_mem_smul_and_notMem_smul

deleted theorem MulAction.IsPreprimitive.exists_mem_smul_and_not_mem_smul

added theorem MulAction.IsPreprimitive.of_isTrivialBlock_of_notMem_fixedPoints

deleted theorem MulAction.IsPreprimitive.of_isTrivialBlock_of_not_mem_fixedPoints

Modified Mathlib/GroupTheory/GroupAction/SubMulAction.lean

Modified Mathlib/GroupTheory/NoncommPiCoprod.lean

Modified Mathlib/GroupTheory/Perm/Centralizer.lean

Modified Mathlib/GroupTheory/Perm/ClosureSwap.lean

added theorem exists_smul_notMem_of_subset_orbit_closure

deleted theorem exists_smul_not_mem_of_subset_orbit_closure

Modified Mathlib/GroupTheory/Perm/Cycle/Basic.lean

Modified Mathlib/GroupTheory/Perm/Cycle/Concrete.lean

added theorem Cycle.formPerm_eq_self_of_notMem

deleted theorem Cycle.formPerm_eq_self_of_not_mem

Modified Mathlib/GroupTheory/Perm/Cycle/Factors.lean

Modified Mathlib/GroupTheory/Perm/Cycle/Type.lean

Modified Mathlib/GroupTheory/Perm/Fin.lean

Modified Mathlib/GroupTheory/Perm/List.lean

added theorem List.formPerm_apply_of_notMem

deleted theorem List.formPerm_apply_of_not_mem

added theorem List.formPerm_eq_self_of_notMem

deleted theorem List.formPerm_eq_self_of_not_mem

Modified Mathlib/GroupTheory/Perm/Sign.lean

Modified Mathlib/GroupTheory/Perm/Support.lean

added theorem Equiv.Perm.notMem_support

deleted theorem Equiv.Perm.not_mem_support

Modified Mathlib/GroupTheory/Perm/ViaEmbedding.lean

added theorem Equiv.Perm.viaEmbedding_apply_of_notMem

deleted theorem Equiv.Perm.viaEmbedding_apply_of_not_mem

Modified Mathlib/GroupTheory/SpecificGroups/Alternating/Centralizer.lean

Modified Mathlib/GroupTheory/SpecificGroups/KleinFour.lean

Modified Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean

added theorem AffineSubspace.notMem_bot

deleted theorem AffineSubspace.not_mem_bot

Modified Mathlib/LinearAlgebra/AffineSpace/Basis.lean

added theorem AffineBasis.coord_apply_combination_of_notMem

deleted theorem AffineBasis.coord_apply_combination_of_not_mem

Modified Mathlib/LinearAlgebra/AffineSpace/Combination.lean

Modified Mathlib/LinearAlgebra/AffineSpace/Independent.lean

added theorem AffineIndependent.affineIndependent_of_notMem_span

deleted theorem AffineIndependent.affineIndependent_of_not_mem_span

added theorem AffineIndependent.notMem_affineSpan_diff

deleted theorem AffineIndependent.not_mem_affineSpan_diff

added theorem affineIndependent_of_ne_of_mem_of_mem_of_notMem

deleted theorem affineIndependent_of_ne_of_mem_of_mem_of_not_mem

added theorem affineIndependent_of_ne_of_mem_of_notMem_of_mem

deleted theorem affineIndependent_of_ne_of_mem_of_not_mem_of_mem

added theorem affineIndependent_of_ne_of_notMem_of_mem_of_mem

deleted theorem affineIndependent_of_ne_of_not_mem_of_mem_of_mem

Modified Mathlib/LinearAlgebra/Alternating/Basic.lean

Modified Mathlib/LinearAlgebra/Basis/Basic.lean

Modified Mathlib/LinearAlgebra/Basis/Cardinality.lean

Modified Mathlib/LinearAlgebra/Basis/VectorSpace.lean

added theorem LinearMap.exists_extend_of_notMem

deleted theorem LinearMap.exists_extend_of_not_mem

added theorem Submodule.exists_le_ker_of_notMem

deleted theorem Submodule.exists_le_ker_of_not_mem

Modified Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean

Modified Mathlib/LinearAlgebra/DFinsupp.lean

Modified Mathlib/LinearAlgebra/Dimension/DivisionRing.lean

Modified Mathlib/LinearAlgebra/Dimension/RankNullity.lean

added theorem Submodule.exists_smul_notMem_of_rank_lt

deleted theorem Submodule.exists_smul_not_mem_of_rank_lt

Modified Mathlib/LinearAlgebra/Dual/Basis.lean

Modified Mathlib/LinearAlgebra/Dual/Lemmas.lean

deleted theorem Submodule.exists_dual_map_eq_bot_of_nmem

added theorem Submodule.exists_dual_map_eq_bot_of_notMem

Modified Mathlib/LinearAlgebra/Eigenspace/Basic.lean

Modified Mathlib/LinearAlgebra/Eigenspace/Matrix.lean

Modified Mathlib/LinearAlgebra/Eigenspace/Pi.lean

Modified Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean

Modified Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean

Modified Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean

Modified Mathlib/LinearAlgebra/FreeModule/PID.lean

deleted theorem Basis.SmithNormalForm.le_ker_coord_of_nmem_range

added theorem Basis.SmithNormalForm.le_ker_coord_of_notMem_range

deleted theorem Basis.SmithNormalForm.repr_eq_zero_of_nmem_range

added theorem Basis.SmithNormalForm.repr_eq_zero_of_notMem_range

Modified Mathlib/LinearAlgebra/Lagrange.lean

Modified Mathlib/LinearAlgebra/LinearIndependent/Basic.lean

added theorem LinearIndependent.linearCombination_ne_of_notMem_support

deleted theorem LinearIndependent.linearCombination_ne_of_not_mem_support

added theorem LinearIndependent.notMem_span_image

deleted theorem LinearIndependent.not_mem_span_image

Modified Mathlib/LinearAlgebra/LinearIndependent/Defs.lean

added theorem LinearIndepOn.notMem_span

added theorem LinearIndepOn.notMem_span_of_insert

deleted theorem LinearIndepOn.not_mem_span

deleted theorem LinearIndepOn.not_mem_span_of_insert

added theorem LinearIndepOn.zero_notMem_image

deleted theorem LinearIndepOn.zero_not_mem_image

added theorem LinearIndependent.notMem_span

deleted theorem LinearIndependent.not_mem_span

added theorem linearIndepOn_iff_notMem_span

deleted theorem linearIndepOn_iff_not_mem_span

added theorem linearIndependent_iff_notMem_span

deleted theorem linearIndependent_iff_not_mem_span

Modified Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean

added theorem LinearIndepOn.notMem_span_iff

added theorem LinearIndepOn.notMem_span_iff_id

deleted theorem LinearIndepOn.not_mem_span_iff

deleted theorem LinearIndepOn.not_mem_span_iff_id

Modified Mathlib/LinearAlgebra/Matrix/Block.lean

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean

Modified Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean

Modified Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean

Modified Mathlib/LinearAlgebra/Matrix/SemiringInverse.lean

Modified Mathlib/LinearAlgebra/Multilinear/Basic.lean

Modified Mathlib/LinearAlgebra/Multilinear/Curry.lean

Modified Mathlib/LinearAlgebra/PID.lean

Modified Mathlib/LinearAlgebra/Quotient/Basic.lean

Modified Mathlib/LinearAlgebra/RootSystem/Base.lean

deleted theorem RootPairing.Base.sub_nmem_range_coroot

deleted theorem RootPairing.Base.sub_nmem_range_root

added theorem RootPairing.Base.sub_notMem_range_coroot

added theorem RootPairing.Base.sub_notMem_range_root

Modified Mathlib/LinearAlgebra/RootSystem/Chain.lean

Modified Mathlib/LinearAlgebra/RootSystem/Defs.lean

deleted theorem RootPairing.zero_nmem_range_coroot

deleted theorem RootPairing.zero_nmem_range_root

added theorem RootPairing.zero_notMem_range_coroot

added theorem RootPairing.zero_notMem_range_root

Modified Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean

deleted theorem RootPairing.RootPositiveForm.rootLength_lt_of_pairingIn_nmem

added theorem RootPairing.RootPositiveForm.rootLength_lt_of_pairingIn_notMem

Modified Mathlib/LinearAlgebra/RootSystem/Reduced.lean

deleted theorem RootPairing.two_smul_nmem_range_root

added theorem RootPairing.two_smul_notMem_range_root

Modified Mathlib/LinearAlgebra/SesquilinearForm.lean

Modified Mathlib/LinearAlgebra/Span/Basic.lean

added theorem Submodule.disjoint_span_singleton_of_notMem

deleted theorem Submodule.disjoint_span_singleton_of_not_mem

added theorem Submodule.isCompl_span_singleton_of_isCoatom_of_notMem

deleted theorem Submodule.isCompl_span_singleton_of_isCoatom_of_not_mem

added theorem Submodule.notMem_span_of_apply_notMem_span_image

deleted theorem Submodule.not_mem_span_of_apply_not_mem_span_image

Modified Mathlib/LinearAlgebra/Span/Defs.lean

added theorem Submodule.lt_sup_iff_notMem

deleted theorem Submodule.lt_sup_iff_not_mem

Modified Mathlib/Logic/Basic.lean

Modified Mathlib/Logic/Denumerable.lean

Modified Mathlib/Logic/Equiv/Fintype.lean

added theorem Equiv.Perm.viaFintypeEmbedding_apply_notMem_range

deleted theorem Equiv.Perm.viaFintypeEmbedding_apply_not_mem_range

Modified Mathlib/Logic/Equiv/PartialEquiv.lean

Modified Mathlib/Logic/Equiv/Set.lean

added theorem Equiv.Set.sumCompl_symm_apply_of_notMem

deleted theorem Equiv.Set.sumCompl_symm_apply_of_not_mem

added theorem Equiv.Set.sumDiffSubset_symm_apply_of_notMem

deleted theorem Equiv.Set.sumDiffSubset_symm_apply_of_not_mem

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

Modified Mathlib/MeasureTheory/Constructions/Cylinders.lean

Modified Mathlib/MeasureTheory/Covering/Besicovitch.lean

Modified Mathlib/MeasureTheory/Function/AEEqOfLIntegral.lean

Modified Mathlib/MeasureTheory/Function/AEMeasurableOrder.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/Indicator.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean

Modified Mathlib/MeasureTheory/Function/ContinuousMapDense.lean

Modified Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean

Modified Mathlib/MeasureTheory/Function/EssSup.lean

Modified Mathlib/MeasureTheory/Function/Intersectivity.lean

Modified Mathlib/MeasureTheory/Function/L2Space.lean

Modified Mathlib/MeasureTheory/Function/LocallyIntegrable.lean

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

Modified Mathlib/MeasureTheory/Function/LpSpace/Indicator.lean

deleted theorem MeasureTheory.indicatorConstLp_coeFn_nmem

added theorem MeasureTheory.indicatorConstLp_coeFn_notMem

Modified Mathlib/MeasureTheory/Function/SimpleFunc.lean

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

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

Modified Mathlib/MeasureTheory/Function/UniformIntegrable.lean

Modified Mathlib/MeasureTheory/Integral/Average.lean

added theorem MeasureTheory.exists_notMem_null_average_le

added theorem MeasureTheory.exists_notMem_null_integral_le

added theorem MeasureTheory.exists_notMem_null_laverage_le

added theorem MeasureTheory.exists_notMem_null_le_average

added theorem MeasureTheory.exists_notMem_null_le_integral

added theorem MeasureTheory.exists_notMem_null_le_laverage

added theorem MeasureTheory.exists_notMem_null_le_lintegral

added theorem MeasureTheory.exists_notMem_null_lintegral_le

deleted theorem MeasureTheory.exists_not_mem_null_average_le

deleted theorem MeasureTheory.exists_not_mem_null_integral_le

deleted theorem MeasureTheory.exists_not_mem_null_laverage_le

deleted theorem MeasureTheory.exists_not_mem_null_le_average

deleted theorem MeasureTheory.exists_not_mem_null_le_integral

deleted theorem MeasureTheory.exists_not_mem_null_le_laverage

deleted theorem MeasureTheory.exists_not_mem_null_le_lintegral

deleted theorem MeasureTheory.exists_not_mem_null_lintegral_le

Modified Mathlib/MeasureTheory/Integral/Bochner/L1.lean

Modified Mathlib/MeasureTheory/Integral/Bochner/Set.lean

Modified Mathlib/MeasureTheory/Integral/CircleIntegral.lean

Modified Mathlib/MeasureTheory/Integral/DominatedConvergence.lean

Modified Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean

Modified Mathlib/MeasureTheory/Integral/IntegrableOn.lean

added theorem MeasureTheory.IntegrableOn.integrable_of_ae_notMem_eq_zero

deleted theorem MeasureTheory.IntegrableOn.integrable_of_ae_not_mem_eq_zero

added theorem MeasureTheory.IntegrableOn.integrable_of_forall_notMem_eq_zero

deleted theorem MeasureTheory.IntegrableOn.integrable_of_forall_not_mem_eq_zero

Modified Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral/FundThmCalculus.lean

Modified Mathlib/MeasureTheory/Integral/Layercake.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue/Add.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean

Modified Mathlib/MeasureTheory/Integral/Marginal.lean

added theorem MeasureTheory.lmarginal_update_of_notMem

deleted theorem MeasureTheory.lmarginal_update_of_not_mem

Modified Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Basic.lean

Modified Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Real.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean

added theorem measurableSet_notMem

deleted theorem measurableSet_not_mem

added theorem measurable_set_notMem

deleted theorem measurable_set_not_mem

Modified Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Defs.lean

Modified Mathlib/MeasureTheory/Measure/AEMeasurable.lean

Modified Mathlib/MeasureTheory/Measure/AbsolutelyContinuous.lean

Modified Mathlib/MeasureTheory/Measure/AddContent.lean

Modified Mathlib/MeasureTheory/Measure/Count.lean

Modified Mathlib/MeasureTheory/Measure/Decomposition/Exhaustion.lean

Modified Mathlib/MeasureTheory/Measure/Dirac.lean

Modified Mathlib/MeasureTheory/Measure/DiracProba.lean

Modified Mathlib/MeasureTheory/Measure/Haar/Basic.lean

Modified Mathlib/MeasureTheory/Measure/Haar/Unique.lean

Modified Mathlib/MeasureTheory/Measure/HasOuterApproxClosed.lean

Modified Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean

Modified Mathlib/MeasureTheory/Measure/Restrict.lean

deleted theorem mem_map_indicator_ae_iff_of_zero_nmem

added theorem mem_map_indicator_ae_iff_of_zero_notMem

Modified Mathlib/MeasureTheory/Measure/Stieltjes.lean

Modified Mathlib/MeasureTheory/Measure/Typeclasses/NoAtoms.lean

added theorem Set.Countable.ae_notMem

deleted theorem Set.Countable.ae_not_mem

Modified Mathlib/MeasureTheory/Measure/WithDensity.lean

Modified Mathlib/MeasureTheory/Order/UpperLower.lean

Modified Mathlib/MeasureTheory/OuterMeasure/AE.lean

deleted theorem MeasureTheory.measure_zero_iff_ae_nmem

added theorem MeasureTheory.measure_zero_iff_ae_notMem

Modified Mathlib/MeasureTheory/OuterMeasure/BorelCantelli.lean

added theorem MeasureTheory.ae_eventually_notMem

deleted theorem MeasureTheory.ae_eventually_not_mem

Modified Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean

Modified Mathlib/MeasureTheory/PiSystem.lean

Modified Mathlib/MeasureTheory/SetAlgebra.lean

Modified Mathlib/MeasureTheory/SetSemiring.lean

deleted theorem MeasureTheory.IsSetSemiring.empty_nmem_disjointOfDiff

deleted theorem MeasureTheory.IsSetSemiring.empty_nmem_disjointOfDiffUnion

deleted theorem MeasureTheory.IsSetSemiring.empty_nmem_disjointOfUnion

added theorem MeasureTheory.IsSetSemiring.empty_notMem_disjointOfDiff

added theorem MeasureTheory.IsSetSemiring.empty_notMem_disjointOfDiffUnion

added theorem MeasureTheory.IsSetSemiring.empty_notMem_disjointOfUnion

deleted theorem MeasureTheory.IsSetSemiring.nmem_disjointOfDiff

added theorem MeasureTheory.IsSetSemiring.notMem_disjointOfDiff

Modified Mathlib/MeasureTheory/VectorMeasure/Decomposition/Hahn.lean

Modified Mathlib/ModelTheory/Definability.lean

modified theorem FirstOrder.Language.DefinableSet.mem_compl

modified theorem FirstOrder.Language.DefinableSet.mem_sdiff

added theorem FirstOrder.Language.DefinableSet.notMem_bot

deleted theorem FirstOrder.Language.DefinableSet.not_mem_bot

Modified Mathlib/ModelTheory/Semantics.lean

Modified Mathlib/ModelTheory/Substructures.lean

added theorem FirstOrder.Language.Substructure.notMem_of_notMem_closure

deleted theorem FirstOrder.Language.Substructure.not_mem_of_not_mem_closure

Modified Mathlib/ModelTheory/Types.lean

modified theorem FirstOrder.Language.Theory.CompleteType.not_mem_iff

Modified Mathlib/NumberTheory/ArithmeticFunction.lean

Modified Mathlib/NumberTheory/BernoulliPolynomials.lean

Modified Mathlib/NumberTheory/ClassNumber/Finite.lean

added theorem ClassGroup.finsetApprox.zero_notMem

deleted theorem ClassGroup.finsetApprox.zero_not_mem

Modified Mathlib/NumberTheory/Cyclotomic/Basic.lean

Modified Mathlib/NumberTheory/Divisors.lean

deleted theorem Nat.properDivisors.not_self_mem

added theorem Nat.self_notMem_properDivisors

Modified Mathlib/NumberTheory/EulerProduct/Basic.lean

Modified Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean

Modified Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean

Modified Mathlib/NumberTheory/LSeries/PrimesInAP.lean

Modified Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean

added theorem NumberField.mixedEmbedding.negAt_apply_isReal_and_notMem

deleted theorem NumberField.mixedEmbedding.negAt_apply_isReal_and_not_mem

added theorem NumberField.mixedEmbedding.pos_of_notMem_negAt_plusPart

deleted theorem NumberField.mixedEmbedding.pos_of_not_mem_negAt_plusPart

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean

Modified Mathlib/NumberTheory/NumberField/FinitePlaces.lean

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.norm_eq_one_iff_notMem

deleted theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.norm_eq_one_iff_not_mem

Modified Mathlib/NumberTheory/NumberField/ProductFormula.lean

Modified Mathlib/NumberTheory/RamificationInertia/Basic.lean

Modified Mathlib/NumberTheory/Rayleigh.lean

Modified Mathlib/NumberTheory/SmoothNumbers.lean

added theorem Nat.notMem_primesBelow

deleted theorem Nat.not_mem_primesBelow

Modified Mathlib/Order/BoundedOrder/Basic.lean

added theorem bot_notMem_iff

deleted theorem bot_not_mem_iff

added theorem top_notMem_iff

deleted theorem top_not_mem_iff

Modified Mathlib/Order/Closure.lean

added theorem LowerAdjoint.notMem_of_notMem_closure

deleted theorem LowerAdjoint.not_mem_of_not_mem_closure

Modified Mathlib/Order/CompactlyGenerated/Basic.lean

Modified Mathlib/Order/CompleteLattice/Chain.lean

Modified Mathlib/Order/CompleteLattice/SetLike.lean

added theorem CompleteSublattice.notMem_bot

deleted theorem CompleteSublattice.not_mem_bot

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

added theorem notMem_of_csSup_lt

added theorem notMem_of_lt_csInf'

added theorem notMem_of_lt_csInf

deleted theorem not_mem_of_csSup_lt

deleted theorem not_mem_of_lt_csInf'

deleted theorem not_mem_of_lt_csInf

Modified Mathlib/Order/CountableDenseLinearOrder.lean

Modified Mathlib/Order/Cover.lean

Modified Mathlib/Order/Filter/AtTopBot/Basic.lean

Modified Mathlib/Order/Filter/AtTopBot/CountablyGenerated.lean

Modified Mathlib/Order/Filter/AtTopBot/Defs.lean

Modified Mathlib/Order/Filter/Bases/Basic.lean

added theorem Filter.notMem_iff_inf_principal_compl

deleted theorem Filter.not_mem_iff_inf_principal_compl

Modified Mathlib/Order/Filter/Basic.lean

added theorem Filter.compl_notMem

deleted theorem Filter.compl_not_mem

added theorem Filter.empty_notMem

deleted theorem Filter.empty_not_mem

Modified Mathlib/Order/Filter/Cocardinal.lean

deleted theorem Filter.eventually_cocardinal_nmem_of_card_lt

added theorem Filter.eventually_cocardinal_notMem_of_card_lt

deleted theorem Finset.eventually_cocardinal_nmem

added theorem Finset.eventually_cocardinal_notMem

Modified Mathlib/Order/Filter/Cofinite.lean

deleted theorem Finset.eventually_cofinite_nmem

added theorem Finset.eventually_cofinite_notMem

deleted theorem Set.Finite.eventually_cofinite_nmem

added theorem Set.Finite.eventually_cofinite_notMem

Modified Mathlib/Order/Filter/ENNReal.lean

Modified Mathlib/Order/Filter/IndicatorFunction.lean

Modified Mathlib/Order/Filter/Map.lean

added theorem Filter.comap_const_of_notMem

deleted theorem Filter.comap_const_of_not_mem

Modified Mathlib/Order/Filter/Tendsto.lean

deleted theorem Filter.not_tendsto_iff_exists_frequently_nmem

added theorem Filter.not_tendsto_iff_exists_frequently_notMem

Modified Mathlib/Order/Filter/Ultrafilter/Basic.lean

deleted theorem Filter.nmem_hyperfilter_of_finite

added theorem Filter.notMem_hyperfilter_of_finite

Modified Mathlib/Order/Filter/Ultrafilter/Defs.lean

added theorem Ultrafilter.compl_mem_iff_notMem

deleted theorem Ultrafilter.compl_mem_iff_not_mem

added theorem Ultrafilter.compl_notMem_iff

deleted theorem Ultrafilter.compl_not_mem_iff

added theorem Ultrafilter.empty_notMem

deleted theorem Ultrafilter.empty_not_mem

Modified Mathlib/Order/Fin/Tuple.lean

added theorem Fin.preimage_insertNth_Icc_of_notMem

deleted theorem Fin.preimage_insertNth_Icc_of_not_mem

Modified Mathlib/Order/Ideal.lean

added theorem Order.Ideal.IsProper.notMem_of_compl_mem

added theorem Order.Ideal.IsProper.notMem_or_compl_notMem

deleted theorem Order.Ideal.IsProper.not_mem_of_compl_mem

deleted theorem Order.Ideal.IsProper.not_mem_or_compl_not_mem

added theorem Order.Ideal.IsProper.top_notMem

deleted theorem Order.Ideal.IsProper.top_not_mem

added theorem Order.Ideal.isProper_of_notMem

deleted theorem Order.Ideal.isProper_of_not_mem

added theorem Order.Ideal.lt_sup_principal_of_notMem

deleted theorem Order.Ideal.lt_sup_principal_of_not_mem

Modified Mathlib/Order/Interval/Finset/Basic.lean

modified theorem Finset.Icc_eq_cons_Ico

modified theorem Finset.Icc_eq_cons_Ioc

modified theorem Finset.Ici_eq_cons_Ioi

modified theorem Finset.Ico_eq_cons_Ioo

modified theorem Finset.Iic_eq_cons_Iio

modified theorem Finset.Ioc_eq_cons_Ioo

added theorem Finset.left_notMem_Ioc

added theorem Finset.left_notMem_Ioo

deleted theorem Finset.left_not_mem_Ioc

deleted theorem Finset.left_not_mem_Ioo

added theorem Finset.notMem_Iio_self

added theorem Finset.notMem_Ioi_self

added theorem Finset.notMem_uIcc_of_gt

added theorem Finset.notMem_uIcc_of_lt

deleted theorem Finset.not_mem_Iio_self

deleted theorem Finset.not_mem_Ioi_self

deleted theorem Finset.not_mem_uIcc_of_gt

deleted theorem Finset.not_mem_uIcc_of_lt

added theorem Finset.right_notMem_Ico

added theorem Finset.right_notMem_Ioo

deleted theorem Finset.right_not_mem_Ico

deleted theorem Finset.right_not_mem_Ioo

Modified Mathlib/Order/Interval/Multiset.lean

added theorem Multiset.left_notMem_Ioc

added theorem Multiset.left_notMem_Ioo

deleted theorem Multiset.left_not_mem_Ioc

deleted theorem Multiset.left_not_mem_Ioo

added theorem Multiset.right_notMem_Ico

added theorem Multiset.right_notMem_Ioo

deleted theorem Multiset.right_not_mem_Ico

deleted theorem Multiset.right_not_mem_Ioo

Modified Mathlib/Order/Interval/Set/Basic.lean

added theorem Set.notMem_Icc_of_gt

added theorem Set.notMem_Icc_of_lt

added theorem Set.notMem_Ico_of_ge

added theorem Set.notMem_Ico_of_lt

added theorem Set.notMem_Iio_self

added theorem Set.notMem_Ioc_of_gt

added theorem Set.notMem_Ioc_of_le

added theorem Set.notMem_Ioi_self

added theorem Set.notMem_Ioo_of_ge

added theorem Set.notMem_Ioo_of_le

deleted theorem Set.not_mem_Icc_of_gt

deleted theorem Set.not_mem_Icc_of_lt

deleted theorem Set.not_mem_Ico_of_ge

deleted theorem Set.not_mem_Ico_of_lt

deleted theorem Set.not_mem_Iio_self

deleted theorem Set.not_mem_Ioc_of_gt

deleted theorem Set.not_mem_Ioc_of_le

deleted theorem Set.not_mem_Ioi_self

deleted theorem Set.not_mem_Ioo_of_ge

deleted theorem Set.not_mem_Ioo_of_le

Modified Mathlib/Order/Interval/Set/Disjoint.lean

modified theorem IsGLB.biUnion_Ici_eq_Ioi

modified theorem IsLUB.biUnion_Iic_eq_Iio

Modified Mathlib/Order/Interval/Set/LinearOrder.lean

added theorem Set.notMem_Ici

added theorem Set.notMem_Iic

added theorem Set.notMem_Iio

added theorem Set.notMem_Ioi

deleted theorem Set.not_mem_Ici

deleted theorem Set.not_mem_Iic

deleted theorem Set.not_mem_Iio

deleted theorem Set.not_mem_Ioi

Modified Mathlib/Order/Interval/Set/OrdConnectedComponent.lean

Modified Mathlib/Order/Interval/Set/OrdConnectedLinear.lean

Modified Mathlib/Order/Interval/Set/UnorderedInterval.lean

added theorem Set.eq_of_notMem_uIoc_of_notMem_uIoc

deleted theorem Set.eq_of_not_mem_uIoc_of_not_mem_uIoc

added theorem Set.notMem_uIcc_of_gt

added theorem Set.notMem_uIcc_of_lt

added theorem Set.notMem_uIoc

deleted theorem Set.not_mem_uIcc_of_gt

deleted theorem Set.not_mem_uIcc_of_lt

deleted theorem Set.not_mem_uIoc

Modified Mathlib/Order/IsNormal.lean

Modified Mathlib/Order/Minimal.lean

added theorem Minimal.notMem_of_prop_diff_singleton

deleted theorem Minimal.not_mem_of_prop_diff_singleton

Modified Mathlib/Order/OrderIsoNat.lean

Modified Mathlib/Order/Partition/Basic.lean

added theorem Partition.bot_notMem

deleted theorem Partition.bot_not_mem

Modified Mathlib/Order/Partition/Finpartition.lean

added theorem Finpartition.empty_notMem_parts

deleted theorem Finpartition.not_empty_mem_parts

Modified Mathlib/Order/Preorder/Chain.lean

Modified Mathlib/Order/PrimeIdeal.lean

added theorem Order.Ideal.IsPrime.compl_mem_of_notMem

deleted theorem Order.Ideal.IsPrime.mem_compl_of_not_mem

Modified Mathlib/Order/PrimeSeparator.lean

Modified Mathlib/Order/Sublattice.lean

added theorem Sublattice.notMem_bot

deleted theorem Sublattice.not_mem_bot

Modified Mathlib/Order/SuccPred/Basic.lean

deleted theorem isMax_of_not_succ_mem

added theorem isMax_of_succ_notMem

deleted theorem isMin_of_not_pred_mem

added theorem isMin_of_pred_notMem

deleted theorem not_pred_mem_iff_isMin

deleted theorem not_succ_mem_iff_isMax

added theorem pred_notMem_iff_isMin

added theorem succ_notMem_iff_isMax

Modified Mathlib/Order/SuccPred/Limit.lean

added theorem IsGLB.isPredLimit_of_notMem

deleted theorem IsGLB.isPredLimit_of_not_mem

added theorem IsGLB.isPredPrelimit_of_notMem

deleted theorem IsGLB.isPredPrelimit_of_not_mem

added theorem IsLUB.isSuccLimit_of_notMem

deleted theorem IsLUB.isSuccLimit_of_not_mem

added theorem IsLUB.isSuccPrelimit_of_notMem

deleted theorem IsLUB.isSuccPrelimit_of_not_mem

Modified Mathlib/Order/SupIndep.lean

Modified Mathlib/Order/UpperLower/Basic.lean

added theorem IsLowerSet.bot_notMem

deleted theorem IsLowerSet.not_bot_mem

deleted theorem IsUpperSet.not_top_mem

added theorem IsUpperSet.top_notMem

Modified Mathlib/Order/UpperLower/CompleteLattice.lean

added theorem LowerSet.notMem_bot

deleted theorem LowerSet.not_mem_bot

added theorem UpperSet.notMem_top

deleted theorem UpperSet.not_mem_top

Modified Mathlib/Order/WellFoundedSet.lean

added theorem Set.PartiallyWellOrderedOn.exists_notMem_of_gt

deleted theorem Set.PartiallyWellOrderedOn.exists_not_mem_of_gt

Modified Mathlib/Probability/Distributions/Uniform.lean

added theorem PMF.ofMultiset_apply_of_notMem

deleted theorem PMF.ofMultiset_apply_of_not_mem

added theorem PMF.uniformOfFinset_apply_of_notMem

deleted theorem PMF.uniformOfFinset_apply_of_not_mem

Modified Mathlib/Probability/Independence/Basic.lean

added theorem ProbabilityTheory.iIndepFun.indepFun_finset_prod_of_notMem

added theorem ProbabilityTheory.iIndepFun.indepFun_finset_prod_of_notMem₀

deleted theorem ProbabilityTheory.iIndepFun.indepFun_finset_prod_of_not_mem

deleted theorem ProbabilityTheory.iIndepFun.indepFun_finset_prod_of_not_mem₀

added theorem ProbabilityTheory.iIndepSets.piiUnionInter_of_notMem

deleted theorem ProbabilityTheory.iIndepSets.piiUnionInter_of_not_mem

Modified Mathlib/Probability/Independence/Conditional.lean

added theorem ProbabilityTheory.iCondIndepFun.condIndepFun_finset_prod_of_notMem

deleted theorem ProbabilityTheory.iCondIndepFun.condIndepFun_finset_prod_of_not_mem

added theorem ProbabilityTheory.iCondIndepSets.piiUnionInter_of_notMem

deleted theorem ProbabilityTheory.iCondIndepSets.piiUnionInter_of_not_mem

Modified Mathlib/Probability/Independence/Kernel.lean

added theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_finset_prod_of_notMem

added theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_finset_prod_of_notMem₀

deleted theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_finset_prod_of_not_mem

deleted theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_finset_prod_of_not_mem₀

added theorem ProbabilityTheory.Kernel.iIndepSets.piiUnionInter_of_notMem

deleted theorem ProbabilityTheory.Kernel.iIndepSets.piiUnionInter_of_not_mem

Modified Mathlib/Probability/Integration.lean

Modified Mathlib/Probability/Kernel/Basic.lean

Modified Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean

Modified Mathlib/Probability/Kernel/Defs.lean

Modified Mathlib/Probability/Kernel/Disintegration/Basic.lean

Modified Mathlib/Probability/Kernel/RadonNikodym.lean

added theorem ProbabilityTheory.Kernel.notMem_mutuallySingularSetSlice

deleted theorem ProbabilityTheory.Kernel.not_mem_mutuallySingularSetSlice

Modified Mathlib/Probability/Kernel/WithDensity.lean

Modified Mathlib/Probability/Martingale/BorelCantelli.lean

Modified Mathlib/Probability/Martingale/OptionalSampling.lean

Modified Mathlib/Probability/Martingale/Upcrossing.lean

Modified Mathlib/Probability/Moments/Basic.lean

Modified Mathlib/Probability/Moments/SubGaussian.lean

Modified Mathlib/Probability/ProbabilityMassFunction/Basic.lean

Modified Mathlib/Probability/ProbabilityMassFunction/Constructions.lean

added theorem PMF.filter_apply_eq_zero_of_notMem

deleted theorem PMF.filter_apply_eq_zero_of_not_mem

added theorem PMF.ofFinset_apply_of_notMem

deleted theorem PMF.ofFinset_apply_of_not_mem

Modified Mathlib/Probability/Process/HittingTime.lean

added theorem MeasureTheory.notMem_of_lt_hitting

deleted theorem MeasureTheory.not_mem_of_lt_hitting

Modified Mathlib/Probability/Process/Stopping.lean

Modified Mathlib/Probability/StrongLaw.lean

Modified Mathlib/RingTheory/AdicCompletion/LocalRing.lean

deleted theorem isUnit_iff_nmem_of_isAdicComplete_maximal

added theorem isUnit_iff_notMem_of_isAdicComplete_maximal

Modified Mathlib/RingTheory/Algebraic/MvPolynomial.lean

Modified Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

added theorem IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers

deleted theorem IsDedekindDomain.HeightOneSpectrum.not_mem_adicCompletionIntegers

Modified Mathlib/RingTheory/DedekindDomain/Factorization.lean

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

added theorem FractionalIdeal.exists_notMem_one_of_ne_bot

deleted theorem FractionalIdeal.exists_not_mem_one_of_ne_bot

added theorem Ideal.exist_integer_multiples_notMem

deleted theorem Ideal.exist_integer_multiples_not_mem

added theorem Ideal.exists_mem_pow_notMem_pow_succ

deleted theorem Ideal.exists_mem_pow_not_mem_pow_succ

Modified Mathlib/RingTheory/DedekindDomain/PID.lean

added theorem Ideal.eq_span_singleton_of_mem_of_notMem_sq_of_notMem_prime_ne

deleted theorem Ideal.eq_span_singleton_of_mem_of_not_mem_sq_of_not_mem_prime_ne

Modified Mathlib/RingTheory/DedekindDomain/SelmerGroup.lean

Modified Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean

Modified Mathlib/RingTheory/Fintype.lean

Modified Mathlib/RingTheory/FractionalIdeal/Norm.lean

Modified Mathlib/RingTheory/FractionalIdeal/Operations.lean

Modified Mathlib/RingTheory/GradedAlgebra/Radical.lean

Modified Mathlib/RingTheory/HahnSeries/Multiplication.lean

Modified Mathlib/RingTheory/Ideal/Maps.lean

deleted theorem RingHom.not_one_mem_ker

added theorem RingHom.one_notMem_ker

Modified Mathlib/RingTheory/Ideal/Maximal.lean

deleted theorem Ideal.exists_le_prime_nmem_of_isIdempotentElem

added theorem Ideal.exists_le_prime_notMem_of_isIdempotentElem

Modified Mathlib/RingTheory/Ideal/MinimalPrime/Basic.lean

Modified Mathlib/RingTheory/Ideal/Nonunits.lean

added theorem one_notMem_nonunits

deleted theorem one_not_mem_nonunits

Modified Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean

Modified Mathlib/RingTheory/Ideal/Operations.lean

added theorem Ideal.disjoint_powers_iff_notMem

deleted theorem Ideal.disjoint_powers_iff_not_mem

Modified Mathlib/RingTheory/Ideal/Prime.lean

added theorem Ideal.IsPrime.mul_notMem

deleted theorem Ideal.IsPrime.mul_not_mem

Modified Mathlib/RingTheory/Idempotents.lean

added theorem OrthogonalIdempotents.mul_sum_of_notMem

deleted theorem OrthogonalIdempotents.mul_sum_of_not_mem

Modified Mathlib/RingTheory/IntegralDomain.lean

Modified Mathlib/RingTheory/Jacobson/Ideal.lean

added theorem Ideal.eq_jacobson_iff_notMem

deleted theorem Ideal.eq_jacobson_iff_not_mem

Modified Mathlib/RingTheory/Jacobson/Ring.lean

Modified Mathlib/RingTheory/KrullDimension/Zero.lean

added theorem le_isUnit_iff_zero_notMem

deleted theorem le_isUnit_iff_zero_not_mem

Modified Mathlib/RingTheory/LaurentSeries.lean

Modified Mathlib/RingTheory/LittleWedderburn.lean

Modified Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean

added theorem IsLocalRing.notMem_maximalIdeal

deleted theorem IsLocalRing.not_mem_maximalIdeal

Modified Mathlib/RingTheory/LocalRing/Module.lean

Modified Mathlib/RingTheory/Localization/Integer.lean

Modified Mathlib/RingTheory/Localization/Integral.lean

added theorem IsLocalization.coeffIntegerNormalization_of_coeff_zero

deleted theorem IsLocalization.coeffIntegerNormalization_of_not_mem_support

Modified Mathlib/RingTheory/MatrixPolynomialAlgebra.lean

Modified Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean

Modified Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean

Modified Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean

added theorem MvPolynomial.weightedHomogeneousComponent_eq_zero_of_notMem

deleted theorem MvPolynomial.weightedHomogeneousComponent_eq_zero_of_not_mem

Modified Mathlib/RingTheory/MvPowerSeries/Inverse.lean

Modified Mathlib/RingTheory/MvPowerSeries/NoZeroDivisors.lean

Modified Mathlib/RingTheory/NonUnitalSubring/Basic.lean

added theorem NonUnitalSubring.notMem_of_notMem_closure

deleted theorem NonUnitalSubring.not_mem_of_not_mem_closure

Modified Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean

added theorem NonUnitalSubsemiring.notMem_of_notMem_closure

deleted theorem NonUnitalSubsemiring.not_mem_of_not_mem_closure

Modified Mathlib/RingTheory/Nullstellensatz.lean

Modified Mathlib/RingTheory/Polynomial/Basic.lean

added theorem exists_C_coeff_notMem

deleted theorem exists_C_coeff_not_mem

Modified Mathlib/RingTheory/Polynomial/Bernstein.lean

Modified Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean

Modified Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean

added theorem Polynomial.Monic.isEisensteinAt_of_mem_of_notMem

deleted theorem Polynomial.Monic.isEisensteinAt_of_mem_of_not_mem

added theorem Polynomial.Monic.leadingCoeff_notMem

deleted theorem Polynomial.Monic.leadingCoeff_not_mem

Modified Mathlib/RingTheory/Polynomial/Eisenstein/Distinguished.lean

Modified Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean

Modified Mathlib/RingTheory/PowerBasis.lean

Modified Mathlib/RingTheory/PowerSeries/WeierstrassPreparation.lean

Modified Mathlib/RingTheory/PrincipalIdealDomain.lean

Modified Mathlib/RingTheory/PrincipalIdealDomainOfPrime.lean

Modified Mathlib/RingTheory/Radical.lean

Modified Mathlib/RingTheory/Regular/RegularSequence.lean

Modified Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean

Modified Mathlib/RingTheory/Smooth/Locus.lean

Modified Mathlib/RingTheory/Smooth/StandardSmooth.lean

Modified Mathlib/RingTheory/Smooth/StandardSmoothCotangent.lean

added theorem Algebra.SubmersivePresentation.sectionCotangent_zero_of_notMem_range

deleted theorem Algebra.SubmersivePresentation.sectionCotangent_zero_of_not_mem_range

Modified Mathlib/RingTheory/Spectrum/Maximal/Localization.lean

Modified Mathlib/RingTheory/Spectrum/Prime/Basic.lean

added theorem PrimeSpectrum.mem_compl_zeroLocus_iff_notMem

deleted theorem PrimeSpectrum.mem_compl_zeroLocus_iff_not_mem

Modified Mathlib/RingTheory/Spectrum/Prime/IsOpenComapC.lean

Modified Mathlib/RingTheory/Spectrum/Prime/Jacobson.lean

Modified Mathlib/RingTheory/Spectrum/Prime/RingHom.lean

deleted theorem PrimeSpectrum.exists_maximal_nmem_range_sigmaToPi_of_infinite

added theorem PrimeSpectrum.exists_maximal_notMem_range_sigmaToPi_of_infinite

Modified Mathlib/RingTheory/Spectrum/Prime/Topology.lean

Modified Mathlib/RingTheory/Support.lean

added theorem Module.notMem_support_iff'

added theorem Module.notMem_support_iff

deleted theorem Module.not_mem_support_iff'

deleted theorem Module.not_mem_support_iff

Modified Mathlib/RingTheory/TensorProduct/Finite.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain/Defs.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean

added theorem Associates.reducible_notMem_factorSet

deleted theorem Associates.reducible_not_mem_factorSet

Modified Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicity.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean

added theorem UniqueFactorizationMonoid.zero_notMem_normalizedFactors

deleted theorem UniqueFactorizationMonoid.zero_not_mem_normalizedFactors

Modified Mathlib/RingTheory/Unramified/Finite.lean

Modified Mathlib/RingTheory/Unramified/Locus.lean

Modified Mathlib/RingTheory/Valuation/LocalSubring.lean

Modified Mathlib/SetTheory/Cardinal/Basic.lean

added theorem Cardinal.exists_notMem_of_length_lt

deleted theorem Cardinal.exists_not_mem_of_length_lt

Modified Mathlib/SetTheory/Nimber/Basic.lean

Modified Mathlib/SetTheory/Nimber/Field.lean

added theorem Nimber.invAux_notMem_invSet

deleted theorem Nimber.invAux_not_mem_invSet

Modified Mathlib/SetTheory/Ordinal/Family.lean

added theorem Ordinal.lsub_notMem_range

deleted theorem Ordinal.lsub_not_mem_range

Modified Mathlib/SetTheory/Ordinal/NaturalOps.lean

Modified Mathlib/SetTheory/ZFC/Basic.lean

added theorem ZFSet.notMem_empty

added theorem ZFSet.notMem_of_subset

added theorem ZFSet.notMem_sInter_of_notMem

deleted theorem ZFSet.not_mem_empty

deleted theorem ZFSet.not_mem_of_subset

deleted theorem ZFSet.not_mem_sInter_of_not_mem

Modified Mathlib/SetTheory/ZFC/Class.lean

added theorem Class.notMem_empty

deleted theorem Class.not_mem_empty

added theorem Class.univ_notMem_univ

deleted theorem Class.univ_not_mem_univ

added theorem ZFSet.isOrdinal_notMem_univ

deleted theorem ZFSet.isOrdinal_not_mem_univ

Modified Mathlib/SetTheory/ZFC/Ordinal.lean

added theorem ZFSet.IsOrdinal.notMem_iff_subset

deleted theorem ZFSet.IsOrdinal.not_mem_iff_subset

modified theorem ZFSet.isTransitive_empty

Modified Mathlib/SetTheory/ZFC/PSet.lean

added theorem PSet.notMem_empty

added theorem PSet.notMem_of_subset

deleted theorem PSet.not_mem_empty

deleted theorem PSet.not_mem_of_subset

Modified Mathlib/Tactic/NormNum/BigOperators.lean

Modified Mathlib/Tactic/Push.lean

Modified Mathlib/Topology/Algebra/ConstMulAction.lean

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

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

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

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

added theorem exists_open_convex_of_notMem

deleted theorem exists_open_convex_of_not_mem

Modified Mathlib/Topology/Algebra/Support.lean

deleted theorem image_eq_one_of_nmem_mulTSupport

added theorem image_eq_one_of_notMem_mulTSupport

added theorem notMem_mulTSupport_iff_eventuallyEq

deleted theorem not_mem_mulTSupport_iff_eventuallyEq

Modified Mathlib/Topology/Bases.lean

deleted theorem TopologicalSpace.empty_nmem_countableBasis

added theorem TopologicalSpace.empty_notMem_countableBasis

Modified Mathlib/Topology/Category/Compactum.lean

Modified Mathlib/Topology/Clopen.lean

Modified Mathlib/Topology/Closure.lean

added theorem notMem_of_notMem_closure

deleted theorem not_mem_of_not_mem_closure

Modified Mathlib/Topology/ClusterPt.lean

added theorem notMem_closure_iff_nhdsWithin_eq_bot

deleted theorem not_mem_closure_iff_nhdsWithin_eq_bot

Modified Mathlib/Topology/Compactification/OnePoint.lean

added theorem OnePoint.infty_notMem_image_coe

added theorem OnePoint.infty_notMem_range_coe

deleted theorem OnePoint.infty_not_mem_image_coe

deleted theorem OnePoint.infty_not_mem_range_coe

added theorem OnePoint.isClosed_iff_of_notMem

deleted theorem OnePoint.isClosed_iff_of_not_mem

added theorem OnePoint.isOpen_iff_of_notMem

deleted theorem OnePoint.isOpen_iff_of_not_mem

added theorem OnePoint.notMem_range_coe_iff

deleted theorem OnePoint.not_mem_range_coe_iff

Modified Mathlib/Topology/Compactness/Compact.lean

Modified Mathlib/Topology/Compactness/Lindelof.lean

Modified Mathlib/Topology/Compactness/SigmaCompact.lean

Modified Mathlib/Topology/Connected/Clopen.lean

Modified Mathlib/Topology/ContinuousMap/BoundedCompactlySupported.lean

Modified Mathlib/Topology/ContinuousMap/Ideals.lean

added theorem ContinuousMap.notMem_idealOfSet

added theorem ContinuousMap.notMem_setOfIdeal

deleted theorem ContinuousMap.not_mem_idealOfSet

deleted theorem ContinuousMap.not_mem_setOfIdeal

Modified Mathlib/Topology/ContinuousOn.lean

added theorem continuousWithinAt_of_notMem_closure

deleted theorem continuousWithinAt_of_not_mem_closure

Modified Mathlib/Topology/DenseEmbedding.lean

Modified Mathlib/Topology/DiscreteSubset.lean

Modified Mathlib/Topology/EMetricSpace/Defs.lean

Modified Mathlib/Topology/EMetricSpace/Paracompact.lean

Modified Mathlib/Topology/FiberBundle/Trivialization.lean

added theorem Pretrivialization.coe_symm_of_notMem

deleted theorem Pretrivialization.coe_symm_of_not_mem

added theorem Pretrivialization.symm_apply_of_notMem

deleted theorem Pretrivialization.symm_apply_of_not_mem

added theorem Trivialization.symm_apply_of_notMem

deleted theorem Trivialization.symm_apply_of_not_mem

Modified Mathlib/Topology/GDelta/MetrizableSpace.lean

Modified Mathlib/Topology/JacobsonSpace.lean

Modified Mathlib/Topology/LocallyConstant/Algebra.lean

Modified Mathlib/Topology/LocallyConstant/Basic.lean

added theorem LocallyConstant.mulIndicator_of_notMem

deleted theorem LocallyConstant.mulIndicator_of_not_mem

Modified Mathlib/Topology/LocallyFinsupp.lean

added theorem Function.locallyFinsuppWithin.apply_eq_zero_of_notMem

deleted theorem Function.locallyFinsuppWithin.apply_eq_zero_of_not_mem

Modified Mathlib/Topology/Maps/Proper/Basic.lean

Modified Mathlib/Topology/Maps/Proper/UniversallyClosed.lean

Modified Mathlib/Topology/MetricSpace/GromovHausdorff.lean

Modified Mathlib/Topology/MetricSpace/HausdorffDistance.lean

added theorem EMetric.exists_real_pos_lt_infEdist_of_notMem_closure

deleted theorem EMetric.exists_real_pos_lt_infEdist_of_not_mem_closure

added theorem EMetric.infEdist_closure_pos_iff_notMem_closure

deleted theorem EMetric.infEdist_closure_pos_iff_not_mem_closure

added theorem EMetric.infEdist_pos_iff_notMem_closure

deleted theorem EMetric.infEdist_pos_iff_not_mem_closure

added theorem IsClosed.notMem_iff_infDist_pos

deleted theorem IsClosed.not_mem_iff_infDist_pos

added theorem Metric.infDist_pos_iff_notMem_closure

deleted theorem Metric.infDist_pos_iff_not_mem_closure

added theorem Metric.notMem_of_dist_lt_infDist

deleted theorem Metric.not_mem_of_dist_lt_infDist

Modified Mathlib/Topology/MetricSpace/MetricSeparated.lean

added theorem Metric.isSeparated_insert_of_notMem

deleted theorem Metric.isSeparated_insert_of_not_mem

Modified Mathlib/Topology/MetricSpace/PiNat.lean

Modified Mathlib/Topology/MetricSpace/Polish.lean

Modified Mathlib/Topology/MetricSpace/Pseudo/Defs.lean

Modified Mathlib/Topology/MetricSpace/ThickenedIndicator.lean

Modified Mathlib/Topology/MetricSpace/Thickening.lean

added theorem Metric.eventually_notMem_cthickening_of_infEdist_pos

added theorem Metric.eventually_notMem_thickening_of_infEdist_pos

deleted theorem Metric.eventually_not_mem_cthickening_of_infEdist_pos

deleted theorem Metric.eventually_not_mem_thickening_of_infEdist_pos

Modified Mathlib/Topology/Order/Basic.lean

Modified Mathlib/Topology/Order/Compact.lean

Modified Mathlib/Topology/Order/IsLUB.lean

added theorem IsGLB.exists_seq_strictAnti_tendsto_of_notMem

deleted theorem IsGLB.exists_seq_strictAnti_tendsto_of_not_mem

added theorem IsLUB.exists_seq_strictMono_tendsto_of_notMem

deleted theorem IsLUB.exists_seq_strictMono_tendsto_of_not_mem

Modified Mathlib/Topology/Order/LeftRight.lean

Modified Mathlib/Topology/Order/LowerUpperTopology.lean

Modified Mathlib/Topology/Piecewise.lean

Modified Mathlib/Topology/Separation/Basic.lean

added theorem t0Space_iff_or_notMem_closure

deleted theorem t0Space_iff_or_not_mem_closure

Modified Mathlib/Topology/Separation/DisjointCover.lean

Modified Mathlib/Topology/Separation/Hausdorff.lean

added theorem IsCompact.separation_of_notMem

deleted theorem IsCompact.separation_of_not_mem

Modified Mathlib/Topology/Separation/Regular.lean

Modified Mathlib/Topology/Sheaves/Skyscraper.lean

Modified Mathlib/Topology/ShrinkingLemma.lean

Modified Mathlib/Topology/StoneCech.lean

Modified Mathlib/Topology/UniformSpace/OfCompactT2.lean

Modified Mathlib/Topology/UrysohnsLemma.lean

deleted theorem Urysohns.CU.approx_of_nmem_U

added theorem Urysohns.CU.approx_of_notMem_U

deleted theorem Urysohns.CU.lim_of_nmem_U

added theorem Urysohns.CU.lim_of_notMem_U

Modified Mathlib/Topology/VectorBundle/Basic.lean

added theorem Pretrivialization.linearMapAt_def_of_notMem

deleted theorem Pretrivialization.linearMapAt_def_of_not_mem

added theorem Trivialization.linearMapAt_def_of_notMem

deleted theorem Trivialization.linearMapAt_def_of_not_mem

Modified MathlibTest/norm_num_ext.lean