Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat(Data/Set): add result that shows a set is even iff it splits into two sets of equal cardinality #18878

Open
wants to merge 13 commits into
base: master
Choose a base branch
from
Open

feat(Data/Set): add result that shows a set is even iff it splits into two sets of equal cardinality #18878

wants to merge 13 commits into from
+57 −2

Conversation

pimotte
Copy link
Collaborator

@pimotte pimotte commented Nov 11, 2024 •
edited
Loading

These results make use of the fact that Set.ncard is defined to be 0, therefore
in the infinite case the cardinality is also considered even, in which case the set
also cleanly splits in two.

Open in Gitpod

In preparation for Tutte's theorem. Zulip thread

@pimotte pimotte added the t-logic Logic (model theory, etc) label Nov 11, 2024
@github-actions github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Nov 11, 2024
@github-actions GitHub Actions
Copy link

github-actions bot commented Nov 11, 2024 •
edited
Loading

PR summary a9e39caab3

Import changes exceeding 2%

% File
+13.32% Mathlib.Data.Set.Card

Import changes for modified files

Dependency changes

File Base Count Head Count Change
Mathlib.Data.Set.Card 683 774 +91 (+13.32%)
Import changes for all files
Files Import difference
Mathlib.SetTheory.Nimber.Field 8
659 files Mathlib.Topology.Category.Stonean.Adjunctions Mathlib.Data.Real.Hyperreal Mathlib.Analysis.MeanInequalitiesPow Mathlib.Analysis.Asymptotics.SpecificAsymptotics Mathlib.Combinatorics.SimpleGraph.Triangle.Removal Mathlib.Combinatorics.SimpleGraph.UniversalVerts Mathlib.Analysis.Calculus.Deriv.Pi Mathlib.Analysis.Calculus.Deriv.Inv Mathlib.Topology.Category.LightProfinite.EffectiveEpi Mathlib.Algebra.Periodic Mathlib.Dynamics.TopologicalEntropy.NetEntropy Mathlib.MeasureTheory.Constructions.BorelSpace.Metric Mathlib.NumberTheory.Padics.MahlerBasis Mathlib.Probability.Kernel.Defs Mathlib.Topology.Category.Stonean.EffectiveEpi Mathlib.Geometry.Manifold.LocalInvariantProperties Mathlib.Analysis.NormedSpace.OperatorNorm.Basic Mathlib.Topology.MetricSpace.Thickening Mathlib.Probability.Distributions.Geometric Mathlib.Topology.UniformSpace.Dini Mathlib.NumberTheory.Padics.PadicIntegers Mathlib.Analysis.Subadditive Mathlib.NumberTheory.MulChar.Lemmas Mathlib.Analysis.Analytic.OfScalars Mathlib.MeasureTheory.Integral.Marginal Mathlib.Analysis.Analytic.IteratedFDeriv Mathlib.Topology.Category.CompHaus.EffectiveEpi Mathlib.Topology.ContinuousMap.Bounded.Basic Mathlib.Analysis.CStarAlgebra.Multiplier Mathlib.Analysis.SpecialFunctions.Pow.Complex Mathlib.Analysis.Calculus.Deriv.Star Mathlib.MeasureTheory.Function.SpecialFunctions.Basic Mathlib.Analysis.Normed.Lp.PiLp Mathlib.Topology.Homotopy.Contractible Mathlib.Analysis.Calculus.Deriv.Add Mathlib.Analysis.SpecialFunctions.CompareExp Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit Mathlib.Algebra.Homology.DerivedCategory.HomologySequence Mathlib.Analysis.Convex.Birkhoff Mathlib.Topology.Algebra.Module.UniformConvergence Mathlib.Combinatorics.Derangements.Exponential Mathlib.Combinatorics.Additive.Corner.Roth Mathlib.MeasureTheory.Function.LpSeminorm.Basic Mathlib.Topology.Category.Profinite.CofilteredLimit Mathlib.Condensed.Limits Mathlib.MeasureTheory.OuterMeasure.Caratheodory Mathlib.Analysis.SpecialFunctions.Complex.Log Mathlib.MeasureTheory.Constructions.BorelSpace.Basic Mathlib.Probability.ProbabilityMassFunction.Monad Mathlib.MeasureTheory.OuterMeasure.Induced Mathlib.MeasureTheory.Measure.Regular Mathlib.Analysis.Asymptotics.AsymptoticEquivalent Mathlib.Topology.ContinuousMap.Polynomial Mathlib.MeasureTheory.Group.MeasurableEquiv Mathlib.Analysis.Calculus.FDeriv.WithLp Mathlib.RingTheory.Flat.Basic Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter Mathlib.MeasureTheory.Order.Lattice Mathlib.Condensed.TopComparison Mathlib.Analysis.Hofer Mathlib.Analysis.CStarAlgebra.ContinuousMap Mathlib.Analysis.Normed.Algebra.Ultra Mathlib.Analysis.Convex.Topology Mathlib.Condensed.Discrete.Basic Mathlib.Algebra.Homology.TotalComplexSymmetry Mathlib.Geometry.Manifold.ChartedSpace Mathlib.Geometry.Manifold.Sheaf.Basic Mathlib.Analysis.Calculus.FDeriv.Linear Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital Mathlib.RingTheory.TensorProduct.Nontrivial Mathlib.Analysis.Complex.HalfPlane Mathlib.Analysis.LocallyConvex.Bounded Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots Mathlib.Analysis.Seminorm Mathlib.MeasureTheory.Measure.AEDisjoint Mathlib.Topology.Separation.CompletelyRegular Mathlib.Topology.VectorBundle.Hom Mathlib.Analysis.Complex.UnitDisc.Basic Mathlib.CategoryTheory.Sites.SheafCohomology.Basic Mathlib.Topology.Instances.CantorSet Mathlib.Analysis.SpecialFunctions.Exp Mathlib.RingTheory.AdicCompletion.Functoriality Mathlib.Topology.Bornology.BoundedOperation Mathlib.Analysis.Normed.Algebra.Norm Mathlib.Computability.AkraBazzi.GrowsPolynomially Mathlib.Analysis.Convex.Body Mathlib.Analysis.NormedSpace.RCLike Mathlib.Condensed.Light.Explicit Mathlib.Data.Real.Sqrt Mathlib.Topology.Category.LightProfinite.Extend Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev Mathlib.NumberTheory.FLT.Four Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated Mathlib.Topology.Instances.ZMultiples Mathlib.Analysis.Calculus.FormalMultilinearSeries Mathlib.MeasureTheory.Order.Group.Lattice Mathlib.Topology.Germ Mathlib.Analysis.Calculus.AddTorsor.AffineMap Mathlib.Topology.Algebra.InfiniteSum.ENNReal Mathlib.CategoryTheory.Triangulated.Pretriangulated Mathlib.MeasureTheory.Group.Measure Mathlib.NumberTheory.Zsqrtd.ToReal Mathlib.Condensed.AB Mathlib.Condensed.Explicit Mathlib.Topology.ContinuousMap.Periodic Mathlib.NumberTheory.MulChar.Basic Mathlib.Condensed.Module Mathlib.Condensed.Discrete.Characterization Mathlib.Analysis.Calculus.FDeriv.Analytic Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic Mathlib.RingTheory.Polynomial.Dickson Mathlib.Analysis.Calculus.FDeriv.Star Mathlib.Condensed.Light.CartesianClosed Mathlib.Analysis.NormedSpace.RieszLemma Mathlib.Analysis.Calculus.FDeriv.Bilinear Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift Mathlib.Analysis.Complex.Circle Mathlib.Data.ZMod.Quotient Mathlib.MeasureTheory.OuterMeasure.OfFunction Mathlib.Algebra.Homology.HomotopyCategory.MappingCone Mathlib.Topology.MetricSpace.PartitionOfUnity Mathlib.Analysis.SpecialFunctions.PolynomialExp Mathlib.MeasureTheory.Covering.VitaliFamily Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary Mathlib.Analysis.LocallyConvex.Barrelled Mathlib.Analysis.Calculus.Deriv.Linear Mathlib.NumberTheory.Padics.PadicNumbers Mathlib.NumberTheory.SumPrimeReciprocals Mathlib.LinearAlgebra.Matrix.Determinant.Misc Mathlib.MeasureTheory.Measure.ContinuousPreimage Mathlib.RingTheory.RingHom.Flat Mathlib.MeasureTheory.Function.LpSeminorm.Trim Mathlib.Analysis.PSeries Mathlib.Algebra.Homology.BifunctorFlip Mathlib.MeasureTheory.Function.LpSpace Mathlib.MeasureTheory.Group.Arithmetic Mathlib.Probability.Kernel.Composition.ParallelComp Mathlib.Algebra.Homology.TotalComplexShift Mathlib.Dynamics.Ergodic.MeasurePreserving Mathlib.GroupTheory.Nilpotent Mathlib.RingTheory.WittVector.WittPolynomial Mathlib.GroupTheory.CommutingProbability Mathlib.Analysis.Calculus.FDeriv.Add Mathlib.Analysis.Complex.Basic Mathlib.MeasureTheory.Function.AEMeasurableOrder Mathlib.Analysis.Calculus.Deriv.Polynomial Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries Mathlib.MeasureTheory.Category.MeasCat Mathlib.Analysis.Calculus.TangentCone Mathlib.Algebra.Order.ToIntervalMod Mathlib.Topology.Category.Profinite.EffectiveEpi Mathlib.Data.Nat.Periodic Mathlib.RingTheory.Regular.IsSMulRegular Mathlib.MeasureTheory.Constructions.Pi Mathlib.Analysis.Normed.Order.UpperLower Mathlib.Topology.MetricSpace.GromovHausdorffRealized Mathlib.NumberTheory.EulerProduct.Basic Mathlib.Topology.ContinuousMap.Bounded.Star Mathlib.RingTheory.Flat.Localization Mathlib.Topology.ContinuousMap.Compact Mathlib.MeasureTheory.Decomposition.UnsignedHahn Mathlib.Analysis.Normed.Algebra.Unitization Mathlib.Analysis.SpecialFunctions.Pow.Continuity Mathlib.GroupTheory.SchurZassenhaus Mathlib.LinearAlgebra.Matrix.Polynomial Mathlib.Analysis.Calculus.FDeriv.Basic Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality Mathlib.Analysis.Calculus.FDeriv.Pi Mathlib.Topology.UniformSpace.CompareReals Mathlib.Dynamics.Ergodic.Conservative Mathlib.CategoryTheory.Triangulated.Triangulated Mathlib.Analysis.BoxIntegral.Box.SubboxInduction Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow Mathlib.Topology.Instances.AddCircle Mathlib.Analysis.Normed.Affine.Isometry Mathlib.Topology.Category.Profinite.AsLimit Mathlib.Analysis.Calculus.Deriv.Pow Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp Mathlib.Topology.Order.Bounded Mathlib.Topology.Homotopy.Path Mathlib.CategoryTheory.Triangulated.Opposite.Functor Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable Mathlib.Algebra.Category.Grp.EnoughInjectives Mathlib.Data.ZMod.Coprime Mathlib.NumberTheory.DirichletCharacter.Basic Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree Mathlib.Combinatorics.SimpleGraph.Regularity.Increment Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv Mathlib.Data.Complex.Exponential Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected Mathlib.Condensed.Basic Mathlib.MeasureTheory.Measure.NullMeasurable Mathlib.Topology.ContinuousMap.BoundedCompactlySupported Mathlib.Analysis.Normed.Operator.BanachSteinhaus Mathlib.AlgebraicTopology.FundamentalGroupoid.Product Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict Mathlib.Condensed.Light.TopComparison Mathlib.Condensed.Light.TopCatAdjunction Mathlib.Analysis.SpecificLimits.FloorPow Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear Mathlib.Condensed.Discrete.LocallyConstant Mathlib.Algebra.Order.AbsoluteValue.Equivalence Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated Mathlib.Analysis.LocallyConvex.Basic Mathlib.Analysis.Normed.Ring.WithAbs Mathlib.Analysis.LocallyConvex.WeakDual Mathlib.Analysis.Normed.Module.Span Mathlib.Analysis.Normed.Affine.MazurUlam Mathlib.CategoryTheory.Triangulated.HomologicalFunctor Mathlib.MeasureTheory.Measure.Content Mathlib.Analysis.Normed.Lp.ProdLp Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor Mathlib.Topology.Homotopy.Basic Mathlib.Analysis.LocallyConvex.AbsConvex Mathlib.Analysis.Normed.Ring.SeminormFromConst Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels Mathlib.Topology.UrysohnsBounded Mathlib.MeasureTheory.Decomposition.Exhaustion Mathlib.Data.ZMod.IntUnitsPower Mathlib.Analysis.Analytic.ChangeOrigin Mathlib.MeasureTheory.Measure.Sub Mathlib.Topology.Homotopy.Product Mathlib.Topology.Instances.Real Mathlib.Topology.Metrizable.Urysohn Mathlib.MeasureTheory.Measure.HasOuterApproxClosed Mathlib.Analysis.Normed.Group.Tannery Mathlib.Analysis.Calculus.ContDiff.Defs Mathlib.MeasureTheory.Measure.GiryMonad Mathlib.Probability.ProbabilityMassFunction.Constructions Mathlib.Probability.Kernel.Composition.Basic Mathlib.RingTheory.Flat.CategoryTheory Mathlib.Analysis.SpecialFunctions.Log.Base Mathlib.Condensed.Solid Mathlib.Analysis.Convex.SpecificFunctions.Pow Mathlib.Analysis.Normed.Lp.lpSpace Mathlib.Algebra.Homology.HomotopyCategory.Triangulated Mathlib.Algebra.Category.ModuleCat.EnoughInjectives Mathlib.Topology.Category.LightProfinite.AsLimit Mathlib.Condensed.Discrete.Module Mathlib.Topology.Category.LightProfinite.Limits Mathlib.Analysis.NormedSpace.OperatorNorm.Mul Mathlib.Analysis.Normed.Group.Quotient Mathlib.Topology.Category.CompHaus.Basic Mathlib.Analysis.Normed.Ring.Seminorm Mathlib.Algebra.Category.Ring.LinearAlgebra Mathlib.Order.Filter.ZeroAndBoundedAtFilter Mathlib.AlgebraicTopology.SingularSet Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov Mathlib.Analysis.Asymptotics.TVS Mathlib.Topology.Compactness.DeltaGeneratedSpace Mathlib.Analysis.Calculus.Deriv.ZPow Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic Mathlib.Probability.Kernel.Proper Mathlib.Topology.Algebra.Module.Alternating.Topology Mathlib.Topology.Category.CompHaus.Projective Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace Mathlib.Algebra.Homology.BifunctorAssociator Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors Mathlib.MeasureTheory.Measure.Trim Mathlib.Analysis.Normed.Group.Completeness Mathlib.Analysis.CStarAlgebra.Classes Mathlib.Analysis.Normed.Group.ZeroAtInfty Mathlib.Analysis.LocallyConvex.StrongTopology Mathlib.NumberTheory.PythagoreanTriples Mathlib.Analysis.NormedSpace.ConformalLinearMap Mathlib.MeasureTheory.Decomposition.Jordan Mathlib.Condensed.Light.Epi Mathlib.Analysis.BoxIntegral.Partition.Additive Mathlib.Analysis.Complex.ReImTopology Mathlib.RingTheory.ZMod Mathlib.Analysis.Calculus.Deriv.Basic Mathlib.Analysis.NormedSpace.OperatorNorm.Asymptotics Mathlib.Analysis.Calculus.DiffContOnCl Mathlib.Analysis.SpecialFunctions.Complex.Arg Mathlib.Topology.Category.Profinite.Projective Mathlib.Topology.PartitionOfUnity Mathlib.Analysis.NormedSpace.Multilinear.Curry Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences Mathlib.Analysis.SumOverResidueClass Mathlib.Topology.TietzeExtension Mathlib.Topology.MetricSpace.Polish Mathlib.Analysis.CStarAlgebra.Unitization Mathlib.Topology.Category.Profinite.Basic Mathlib.Topology.ContinuousMap.Units Mathlib.MeasureTheory.Group.LIntegral Mathlib.Topology.Instances.Rat Mathlib.Algebra.Homology.HomotopyCategory.HomComplex Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital Mathlib.Probability.Kernel.Invariance Mathlib.AlgebraicTopology.TopologicalSimplex Mathlib.MeasureTheory.Integral.LebesgueNormedSpace Mathlib.Probability.ProbabilityMassFunction.Binomial Mathlib.Topology.ContinuousMap.StarOrdered Mathlib.Analysis.Analytic.RadiusLiminf Mathlib.GroupTheory.Torsion Mathlib.Data.Real.CompleteField Mathlib.MeasureTheory.Group.Pointwise Mathlib.Analysis.Calculus.ContDiff.Bounds Mathlib.Analysis.Normed.Group.HomCompletion Mathlib.NumberTheory.Ostrowski Mathlib.Topology.Category.CompHaus.Limits Mathlib.Topology.Algebra.Module.LocallyConvex Mathlib.MeasureTheory.Measure.Doubling Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle Mathlib.Analysis.MeanInequalities Mathlib.Algebra.Star.CHSH Mathlib.Probability.Distributions.Poisson Mathlib.RingTheory.Polynomial.Chebyshev Mathlib.Analysis.Normed.Ring.SeminormFromBounded Mathlib.Geometry.Manifold.ConformalGroupoid Mathlib.Algebra.Homology.DerivedCategory.ShortExact Mathlib.Condensed.TopCatAdjunction Mathlib.RingTheory.Flat.FaithfullyFlat Mathlib.Algebra.Homology.HomotopyCategory.Shift Mathlib.Data.ZMod.Basic Mathlib.NumberTheory.LegendreSymbol.ZModChar Mathlib.Algebra.Homology.Monoidal Mathlib.Analysis.Calculus.Deriv.Prod Mathlib.Analysis.Calculus.ContDiff.Basic Mathlib.Analysis.Calculus.DSlope Mathlib.Analysis.Complex.Asymptotics Mathlib.Probability.ConditionalProbability Mathlib.Order.Filter.ENNReal Mathlib.Analysis.Normed.Field.UnitBall Mathlib.Analysis.Calculus.Deriv.Mul Mathlib.Analysis.Calculus.Conformal.NormedSpace Mathlib.Analysis.Normed.Group.Completion Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes Mathlib.Analysis.SpecialFunctions.Bernstein Mathlib.Analysis.Normed.Algebra.Exponential Mathlib.MeasureTheory.Integral.RieszMarkovKakutani Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex Mathlib.Analysis.Calculus.FDeriv.RestrictScalars Mathlib.Analysis.SpecialFunctions.Exponential Mathlib.Analysis.Analytic.Meromorphic Mathlib.Analysis.NormedSpace.Extr Mathlib.Topology.MetricSpace.GromovHausdorff Mathlib.Analysis.InnerProductSpace.Defs Mathlib.Topology.UnitInterval Mathlib.Topology.UrysohnsLemma Mathlib.Topology.Category.CompactlyGenerated Mathlib.NumberTheory.Harmonic.Int Mathlib.Analysis.Calculus.LocalExtr.Polynomial Mathlib.Analysis.Calculus.IteratedDeriv.Defs Mathlib.MeasureTheory.Constructions.BorelSpace.Complex Mathlib.Topology.Homotopy.HomotopyGroup Mathlib.Data.Real.StarOrdered Mathlib.Analysis.Normed.Order.Basic Mathlib.MeasureTheory.Measure.Count Mathlib.Analysis.Calculus.Deriv.Shift Mathlib.Probability.Kernel.Basic Mathlib.Analysis.Calculus.Deriv.Inverse Mathlib.MeasureTheory.Group.AEStabilizer Mathlib.GroupTheory.SpecificGroups.Quaternion Mathlib.Topology.Algebra.Module.StrongTopology Mathlib.Analysis.Convex.EGauge Mathlib.CategoryTheory.Localization.Triangulated Mathlib.Analysis.NormedSpace.ENormedSpace Mathlib.Topology.MetricSpace.ThickenedIndicator Mathlib.Topology.Algebra.Polynomial Mathlib.Algebra.Homology.ComplexShapeSigns Mathlib.Data.ZMod.Units Mathlib.Analysis.Calculus.Darboux Mathlib.MeasureTheory.Measure.Comap Mathlib.Probability.ProbabilityMassFunction.Basic Mathlib.LinearAlgebra.TensorProduct.Graded.External Mathlib.Topology.MetricSpace.Contracting Mathlib.MeasureTheory.Function.LpOrder Mathlib.Topology.Baire.BaireMeasurable Mathlib.Algebra.Homology.BifunctorHomotopy Mathlib.Analysis.Analytic.Linear Mathlib.Analysis.NormedSpace.Int Mathlib.Analysis.Normed.Lp.LpEquiv Mathlib.Analysis.RCLike.Basic Mathlib.Analysis.Normed.Operator.Banach Mathlib.Algebra.Module.CharacterModule Mathlib.Analysis.Calculus.LineDeriv.Basic Mathlib.Algebra.Module.Torsion Mathlib.Analysis.Normed.Group.AddCircle Mathlib.Analysis.Convex.Contractible Mathlib.MeasureTheory.Group.Convolution Mathlib.RingTheory.RootsOfUnity.Complex Mathlib.Analysis.Normed.Ring.Units Mathlib.NumberTheory.Padics.RingHoms Mathlib.Topology.ContinuousMap.Weierstrass Mathlib.Analysis.SpecialFunctions.Log.Monotone Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics Mathlib.Data.ZMod.Factorial Mathlib.Analysis.BoxIntegral.Partition.Filter Mathlib.Topology.MetricSpace.Perfect Mathlib.Condensed.Light.AB Mathlib.Topology.Connected.PathConnected Mathlib.Dynamics.Ergodic.Ergodic Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric Mathlib.Topology.EMetricSpace.BoundedVariation Mathlib.Algebra.Category.Ring.Under.Limits Mathlib.Analysis.Normed.Field.ProperSpace Mathlib.Analysis.CStarAlgebra.Basic Mathlib.MeasureTheory.Measure.OpenPos Mathlib.Topology.Algebra.PontryaginDual Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity Mathlib.Analysis.Analytic.Constructions Mathlib.Topology.MetricSpace.Holder Mathlib.MeasureTheory.Measure.Dirac Mathlib.Analysis.SpecificLimits.Normed Mathlib.Analysis.Calculus.FDeriv.Prod Mathlib.MeasureTheory.Decomposition.SignedHahn Mathlib.Topology.Category.Compactum Mathlib.Analysis.Normed.Group.InfiniteSum Mathlib.Analysis.NormedSpace.DualNumber Mathlib.Analysis.Calculus.Deriv.Comp Mathlib.CategoryTheory.Triangulated.TriangleShift Mathlib.Analysis.Normed.Affine.AddTorsor Mathlib.Condensed.Light.Limits Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps Mathlib.Algebra.Homology.TotalComplex Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk Mathlib.MeasureTheory.Integral.MeanInequalities Mathlib.Topology.VectorBundle.Constructions Mathlib.GroupTheory.Transfer Mathlib.Condensed.Discrete.Colimit Mathlib.Topology.MetricSpace.PiNat Mathlib.Analysis.NormedSpace.HomeomorphBall Mathlib.Topology.Category.Profinite.Extend Mathlib.Analysis.Normed.Group.Lemmas Mathlib.GroupTheory.Coxeter.Inversion Mathlib.Analysis.SpecialFunctions.Log.Basic Mathlib.MeasureTheory.Measure.Stieltjes Mathlib.Condensed.CartesianClosed Mathlib.Analysis.Analytic.Composition Mathlib.Topology.VectorBundle.Basic Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn Mathlib.Dynamics.Ergodic.Action.Regular Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic Mathlib.Analysis.Calculus.FDeriv.Mul Mathlib.Topology.Compactness.CompactlyGeneratedSpace Mathlib.Analysis.ConstantSpeed Mathlib.Topology.Category.Stonean.Basic Mathlib.Topology.ContinuousMap.ContinuousMapZero Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm Mathlib.Topology.Instances.EReal Mathlib.Topology.Algebra.Module.Multilinear.Bounded Mathlib.Topology.MetricSpace.HausdorffDistance Mathlib.Analysis.Convex.TotallyBounded Mathlib.Data.Complex.Order Mathlib.Analysis.Calculus.Deriv.AffineMap Mathlib.Topology.Algebra.ProperAction.ProperlyDiscontinuous Mathlib.GroupTheory.Sylow Mathlib.Analysis.NormedSpace.Extend Mathlib.NumberTheory.VonMangoldt Mathlib.Analysis.Asymptotics.Theta Mathlib.Combinatorics.SimpleGraph.DegreeSum Mathlib.MeasureTheory.Function.Egorov Mathlib.Probability.Independence.Basic Mathlib.Topology.Category.LightProfinite.Basic Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction Mathlib.Analysis.CStarAlgebra.Exponential Mathlib.Topology.MetricSpace.HolderNorm Mathlib.MeasureTheory.Function.ConvergenceInMeasure Mathlib.Analysis.Normed.Operator.BoundedLinearMaps Mathlib.Topology.MetricSpace.CantorScheme Mathlib.MeasureTheory.Function.AEEqOfLIntegral Mathlib.Analysis.SpecialFunctions.Pow.Real Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion Mathlib.Algebra.CharP.Quotient Mathlib.Dynamics.TopologicalEntropy.Semiconj Mathlib.Topology.ContinuousMap.StoneWeierstrass Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm Mathlib.MeasureTheory.Covering.Vitali Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle Mathlib.Analysis.Convex.Gauge Mathlib.MeasureTheory.VectorMeasure.Basic Mathlib.NumberTheory.LucasPrimality Mathlib.Topology.Category.LightProfinite.Sequence Mathlib.Analysis.Analytic.Basic Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness Mathlib.Analysis.Analytic.Uniqueness Mathlib.Condensed.Light.Basic Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp Mathlib.Topology.Algebra.ClopenNhdofOne Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence Mathlib.Analysis.Calculus.Deriv.Support Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv Mathlib.MeasureTheory.Constructions.Polish.Basic Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber Mathlib.Topology.MetricSpace.Kuratowski Mathlib.NumberTheory.LucasLehmer Mathlib.Condensed.Light.Module Mathlib.RingTheory.AdicCompletion.Algebra Mathlib.Dynamics.Ergodic.Function Mathlib.Analysis.Normed.Module.Basic Mathlib.Algebra.Algebra.ZMod Mathlib.Analysis.Complex.Convex Mathlib.Topology.Category.Locale Mathlib.NumberTheory.PrimeCounting Mathlib.Analysis.Normed.Group.Pointwise Mathlib.MeasureTheory.OuterMeasure.Defs Mathlib.Analysis.Normed.Ring.IsPowMulFaithful Mathlib.NumberTheory.Padics.Hensel Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic Mathlib.Algebra.Module.ZMod Mathlib.Analysis.Calculus.FDeriv.Comp Mathlib.Topology.Instances.RealVectorSpace Mathlib.Analysis.LocallyConvex.ContinuousOfBounded Mathlib.RingTheory.Fintype Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm Mathlib.Analysis.Analytic.CPolynomial Mathlib.Combinatorics.SimpleGraph.Regularity.Bound Mathlib.Algebra.Homology.HomotopyCategory.ShortExact Mathlib.CategoryTheory.Triangulated.Subcategory Mathlib.MeasureTheory.Measure.Restrict Mathlib.CategoryTheory.Triangulated.Functor Mathlib.Analysis.LocallyConvex.WithSeminorms Mathlib.Analysis.Asymptotics.SuperpolynomialDecay Mathlib.Analysis.Calculus.ContDiff.CPolynomial Mathlib.Analysis.Calculus.LocalExtr.Basic Mathlib.CategoryTheory.Triangulated.TStructure.Basic Mathlib.Analysis.Normed.Order.Lattice Mathlib.Analysis.Normed.Module.Ray Mathlib.MeasureTheory.Measure.MutuallySingular Mathlib.Analysis.Analytic.Within Mathlib.Probability.Independence.Kernel Mathlib.Analysis.Calculus.FDeriv.Equiv Mathlib.MeasureTheory.Group.Prod Mathlib.Order.Category.Frm Mathlib.Analysis.NormedSpace.OperatorNorm.Prod Mathlib.Topology.ContinuousMap.CompactlySupported Mathlib.GroupTheory.SpecificGroups.Cyclic Mathlib.Dynamics.TopologicalEntropy.CoverEntropy Mathlib.Analysis.CStarAlgebra.lpSpace Mathlib.Condensed.Epi Mathlib.GroupTheory.Coxeter.Length Mathlib.Topology.Maps.Proper.CompactlyGenerated Mathlib.MeasureTheory.Measure.Typeclasses Mathlib.RingTheory.Flat.Equalizer Mathlib.Analysis.NormedSpace.Real Mathlib.Analysis.Analytic.IsolatedZeros Mathlib.MeasureTheory.OuterMeasure.Operations Mathlib.MeasureTheory.Measure.Prod Mathlib.Analysis.Normed.Field.Lemmas Mathlib.Analysis.Normed.Field.InfiniteSum Mathlib.Topology.Algebra.Module.Multilinear.Topology Mathlib.Analysis.Normed.Group.ControlledClosure Mathlib.Condensed.Light.Functors Mathlib.GroupTheory.Order.Min Mathlib.MeasureTheory.Measure.AEMeasurable Mathlib.Analysis.Asymptotics.Asymptotics Mathlib.MeasureTheory.Measure.WithDensity Mathlib.MeasureTheory.Function.AEEqFun Mathlib.Algebra.CharP.Two Mathlib.MeasureTheory.Function.SimpleFuncDense Mathlib.Data.Complex.Abs Mathlib.Probability.Kernel.MeasurableLIntegral Mathlib.Analysis.SpecialFunctions.Complex.Circle Mathlib.Algebra.Homology.Bifunctor Mathlib.Analysis.Analytic.Inverse Mathlib.Topology.ContinuousMap.ZeroAtInfty Mathlib.Analysis.NormedSpace.FunctionSeries Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma Mathlib.Analysis.Normed.Operator.Compact Mathlib.GroupTheory.SpecificGroups.KleinFour Mathlib.Dynamics.Ergodic.Action.Basic Mathlib.RingTheory.Flat.Stability Mathlib.Condensed.Functors Mathlib.MeasureTheory.Constructions.Projective Mathlib.Analysis.NormedSpace.BallAction Mathlib.MeasureTheory.Measure.MeasureSpace Mathlib.MeasureTheory.Measure.MeasureSpaceDef Mathlib.NumberTheory.Padics.ProperSpace Mathlib.MeasureTheory.Group.Action Mathlib.Dynamics.BirkhoffSum.NormedSpace Mathlib.Analysis.Complex.RealDeriv Mathlib.MeasureTheory.OuterMeasure.Basic Mathlib.MeasureTheory.Function.AEMeasurableSequence Mathlib.Condensed.Equivalence Mathlib.Topology.Homotopy.Equiv Mathlib.Topology.Category.Profinite.Product Mathlib.RingTheory.IntegralDomain Mathlib.Topology.Homotopy.HSpaces Mathlib.Topology.Category.Profinite.Limits Mathlib.Topology.MetricSpace.Completion Mathlib.GroupTheory.SpecificGroups.Dihedral Mathlib.Topology.Instances.NNReal Mathlib.Analysis.Calculus.LogDeriv Mathlib.MeasureTheory.Measure.Haar.Basic Mathlib.Analysis.Calculus.Deriv.Slope Mathlib.Analysis.SpecificLimits.RCLike Mathlib.GroupTheory.Frattini Mathlib.Analysis.NormedSpace.Multilinear.Basic Mathlib.Algebra.CharP.CharAndCard Mathlib.MeasureTheory.Constructions.BorelSpace.Real Mathlib.GroupTheory.PGroup Mathlib.Analysis.Polynomial.Basic Mathlib.LinearAlgebra.TensorProduct.Graded.Internal Mathlib.Analysis.LocallyConvex.BalancedCoreHull Mathlib.Analysis.SpecialFunctions.Pow.NNReal Mathlib.Algebra.Category.Grp.Injective Mathlib.MeasureTheory.Constructions.BorelSpace.Order Mathlib.MeasureTheory.Integral.Indicator Mathlib.Topology.Algebra.InfiniteSum.Real Mathlib.Analysis.Normed.Group.Rat Mathlib.Analysis.Convex.SpecificFunctions.Basic Mathlib.Topology.MetricSpace.Closeds Mathlib.Analysis.Normed.Affine.ContinuousAffineMap Mathlib.Topology.Semicontinuous Mathlib.MeasureTheory.Measure.EverywherePos Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic Mathlib.Analysis.SpecificLimits.Basic Mathlib.MeasureTheory.Function.EssSup Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit Mathlib.Analysis.Calculus.LocalExtr.Rolle Mathlib.MeasureTheory.OuterMeasure.AE Mathlib.GroupTheory.Schreier Mathlib.MeasureTheory.Measure.Complex Mathlib.Combinatorics.Additive.CauchyDavenport Mathlib.CategoryTheory.Triangulated.Yoneda Mathlib.MeasureTheory.Function.Floor Mathlib.Algebra.Ring.NegOnePow Mathlib.Analysis.Calculus.LocalExtr.LineDeriv Mathlib.Algebra.Homology.BifunctorShift Mathlib.Analysis.NormedSpace.SphereNormEquiv Mathlib.Topology.Order.Category.FrameAdjunction Mathlib.Topology.ContinuousMap.Ideals Mathlib.RingTheory.RootsOfUnity.Basic Mathlib.Probability.UniformOn Mathlib.Analysis.SpecialFunctions.Trigonometric.Series Mathlib.Analysis.Convex.PartitionOfUnity Mathlib.Combinatorics.SimpleGraph.Matching Mathlib.Analysis.Complex.AbelLimit Mathlib.Analysis.SpecialFunctions.Sqrt Mathlib.Analysis.NormedSpace.Pointwise Mathlib.MeasureTheory.Integral.Lebesgue Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog Mathlib.Algebra.Homology.DerivedCategory.Basic Mathlib.Analysis.SpecialFunctions.Log.ERealExp Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt Mathlib.Topology.Baire.CompleteMetrizable Mathlib.MeasureTheory.Function.SimpleFunc Mathlib.Data.Nat.Totient Mathlib.MeasureTheory.Group.Defs Mathlib.Data.ZMod.Aut Mathlib.Topology.Algebra.ClosedSubgroup Mathlib.Analysis.Normed.Module.Completion Mathlib.MeasureTheory.Function.StronglyMeasurable.ENNReal Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps Mathlib.GroupTheory.SpecificGroups.ZGroup Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor Mathlib.Topology.Instances.ENNReal Mathlib.Topology.Category.Stonean.Limits Mathlib.Analysis.Calculus.ContDiff.WithLp Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass Mathlib.MeasureTheory.OuterMeasure.BorelCantelli Mathlib.Analysis.Normed.Algebra.UnitizationL1
 12
10 files Mathlib.LinearAlgebra.Matrix.MvPolynomial Mathlib.Data.Matrix.DoublyStochastic Mathlib.LinearAlgebra.Matrix.Reindex Mathlib.LinearAlgebra.CrossProduct Mathlib.LinearAlgebra.Matrix.Permutation Mathlib.LinearAlgebra.Matrix.AbsoluteValue Mathlib.LinearAlgebra.Matrix.Basis Mathlib.LinearAlgebra.Matrix.Transvection Mathlib.LinearAlgebra.Matrix.Determinant.Basic Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
 28
9 files Mathlib.GroupTheory.Perm.Cycle.PossibleTypes Mathlib.GroupTheory.Exponent Mathlib.GroupTheory.Perm.Fin Mathlib.GroupTheory.GroupAction.Period Mathlib.GroupTheory.FixedPointFree Mathlib.GroupTheory.Perm.Cycle.Concrete Mathlib.GroupTheory.GroupAction.Blocks Mathlib.GroupTheory.SpecificGroups.Alternating Mathlib.GroupTheory.Perm.Cycle.Type
 29
6 files Mathlib.GroupTheory.Perm.Cycle.Basic Mathlib.GroupTheory.Perm.Closure Mathlib.GroupTheory.Perm.Cycle.Factors Mathlib.Algebra.Order.Chebyshev Mathlib.GroupTheory.Perm.Finite Mathlib.GroupTheory.Perm.ConjAct
 34
3 files Mathlib.GroupTheory.OrderOfElement Mathlib.GroupTheory.NoncommPiCoprod Mathlib.LinearAlgebra.FiniteSpan
 36
Mathlib.GroupTheory.CosetCover 44
10 files Mathlib.GroupTheory.SemidirectProduct Mathlib.GroupTheory.GroupExtension.Defs Mathlib.GroupTheory.FreeGroup.NielsenSchreier Mathlib.CategoryTheory.Action Mathlib.GroupTheory.Perm.DomMulAct Mathlib.GroupTheory.Commensurable Mathlib.GroupTheory.Complement Mathlib.GroupTheory.Index Mathlib.GroupTheory.PushoutI Mathlib.GroupTheory.HNNExtension
 58
Mathlib.GroupTheory.ClassEquation 85
Mathlib.MeasureTheory.MeasurableSpace.NCard Mathlib.Data.Matroid.Closure 89
Mathlib.Algebra.Group.Pointwise.Set.Card 90
8 files Mathlib.Data.Matroid.Basic Mathlib.Data.Matroid.Map Mathlib.Data.Matroid.Dual Mathlib.Data.Matroid.Constructions Mathlib.Data.Matroid.IndepAxioms Mathlib.Data.Matroid.Restrict Mathlib.Data.Set.Card Mathlib.Data.Matroid.Sum
 91

Declarations diff

+ disjoint_insert_left
+ disjoint_insert_right
+ exists_disjoint_union_of_even_card
+ exists_union_disjoint_cardinal_eq_iff
+ exists_union_disjoint_cardinal_eq_of_even
+ exists_union_disjoint_cardinal_eq_of_infinite
+ exists_union_disjoint_ncard_eq_of_even

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@github-actions github-actions bot added the t-data Data (lists, quotients, numbers, etc) label Nov 11, 2024
b-mehta
b-mehta reviewed Nov 11, 2024
View reviewed changes
Mathlib/Data/Set/Card.lean Outdated Show resolved Hide resolved
@b-mehta b-mehta added the awaiting-author A reviewer has asked the author a question or requested changes label Nov 11, 2024
vihdzp
vihdzp reviewed Nov 11, 2024
View reviewed changes
Mathlib/Data/Set/Card.lean Show resolved Hide resolved
Mathlib/Data/Set/Card.lean Outdated Show resolved Hide resolved
Mathlib/Data/Set/Card.lean Outdated Show resolved Hide resolved
@pimotte pimotte removed the awaiting-author A reviewer has asked the author a question or requested changes label Nov 12, 2024
@pimotte pimotte mentioned this pull request Nov 12, 2024
Closed
1 task
vihdzp
vihdzp reviewed Nov 12, 2024
View reviewed changes
Mathlib/Data/Set/Card.lean Outdated Show resolved Hide resolved
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Nov 13, 2024
@vihdzp
Copy link
Collaborator

vihdzp commented Nov 13, 2024

By the way, would it be cleaner to implement these results in terms of IsCompl?

@pimotte
Copy link
Collaborator Author

pimotte commented Nov 14, 2024

By the way, would it be cleaner to implement these results in terms of IsCompl?

I'm not sure, this would entail casting t and u to Set s, right? I'm happy to defer to your expertise here. (I'm going to refactor once your PR is merged).

@vihdzp
Copy link
Collaborator

vihdzp commented Nov 14, 2024

Oh you're right, the assumption here is t ∪ u = s instead of t ∪ u = univ. So I think it's fine as is.

@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Jan 5, 2025
@mathlib4-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

@vihdzp
Copy link
Collaborator

vihdzp commented Jan 5, 2025

I'm really sorry for the delay on my PR! You should now be able to implement my suggestions.

tb65536
tb65536 reviewed Jan 5, 2025
View reviewed changes
Copy link
Collaborator

@tb65536 tb65536 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I might suggest proving the infinite version first. Then you can drop the finiteness assumption from the ncard version and golf the iff version. Something like this:

open Cardinal

theorem exists_union_disjoint_cardinal_eq_of_infinite (h : s.Infinite) : ∃ (t u : Set α),
    t ∪ u = s ∧ Disjoint t u ∧ #t = #u := by
  have := h.to_subtype
  have f : s ≃ s ⊕ s := by
    apply Classical.choice
    rw [← Cardinal.eq, ← add_def, add_mk_eq_self]
  refine ⟨Subtype.val '' (f ⁻¹' (range .inl)), Subtype.val '' (f ⁻¹' (range .inr)), ?_, ?_, ?_⟩
  · rw [← image_union, ← preimage_union]
    simp
  · exact disjoint_image_of_injective Subtype.val_injective
      (isCompl_range_inl_range_inr.disjoint.preimage f)
  · simp [mk_image_eq Subtype.val_injective]

theorem exists_union_disjoint_cardinal_eq_of_even (he : Even s.ncard) : ∃ (t u : Set α),
    t ∪ u = s ∧ Disjoint t u ∧ #t = #u := by
  obtain hs | hs := s.infinite_or_finite
  · exact exists_union_disjoint_cardinal_eq_of_infinite hs
  classical
  rw [ncard_eq_toFinset_card s hs] at he
  obtain ⟨t, u, hutu, hdtu, hctu⟩ := Finset.exists_disjoint_union_of_even_card he
  use t.toSet, u.toSet
  simp [← Finset.coe_union, *]

theorem exists_union_disjoint_ncard_eq_of_even (he : Even s.ncard) : ∃ (t u : Set α),
    t ∪ u = s ∧ Disjoint t u ∧ t.ncard = u.ncard := by
  obtain ⟨t, u, hutu, hdtu, hctu⟩ := exists_union_disjoint_cardinal_eq_of_even he
  exact ⟨t, u, hutu, hdtu, congrArg Cardinal.toNat hctu⟩

theorem exists_union_disjoint_cardinal_eq_iff (s : Set α) :
    Even (s.ncard) ↔ ∃ (t u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #t = #u := by
  use exists_union_disjoint_cardinal_eq_of_even
  rintro ⟨t, u, rfl, hdtu, hctu⟩
  obtain hfin | hnfin := (t ∪ u).finite_or_infinite
  · rw [finite_union] at hfin
    have hn : t.ncard = u.ncard := congrArg Cardinal.toNat hctu
    rw [ncard_union_eq hdtu hfin.1 hfin.2, hn]
    exact Even.add_self u.ncard
  · simp only [hnfin.ncard, even_zero]

Mathlib/Data/Set/Basic.lean Outdated Show resolved Hide resolved
@pimotte
Copy link
Collaborator Author

pimotte commented Jan 6, 2025

I might suggest proving the infinite version first. Then you can drop the finiteness assumption from the ncard version and golf the iff version. Something like this:

open Cardinal

theorem exists_union_disjoint_cardinal_eq_of_infinite (h : s.Infinite) : ∃ (t u : Set α),
    t ∪ u = s ∧ Disjoint t u ∧ #t = #u := by
  have := h.to_subtype
  have f : s ≃ s ⊕ s := by
    apply Classical.choice
    rw [← Cardinal.eq, ← add_def, add_mk_eq_self]
  refine ⟨Subtype.val '' (f ⁻¹' (range .inl)), Subtype.val '' (f ⁻¹' (range .inr)), ?_, ?_, ?_⟩
  · rw [← image_union, ← preimage_union]
    simp
  · exact disjoint_image_of_injective Subtype.val_injective
      (isCompl_range_inl_range_inr.disjoint.preimage f)
  · simp [mk_image_eq Subtype.val_injective]

theorem exists_union_disjoint_cardinal_eq_of_even (he : Even s.ncard) : ∃ (t u : Set α),
    t ∪ u = s ∧ Disjoint t u ∧ #t = #u := by
  obtain hs | hs := s.infinite_or_finite
  · exact exists_union_disjoint_cardinal_eq_of_infinite hs
  classical
  rw [ncard_eq_toFinset_card s hs] at he
  obtain ⟨t, u, hutu, hdtu, hctu⟩ := Finset.exists_disjoint_union_of_even_card he
  use t.toSet, u.toSet
  simp [← Finset.coe_union, *]

theorem exists_union_disjoint_ncard_eq_of_even (he : Even s.ncard) : ∃ (t u : Set α),
    t ∪ u = s ∧ Disjoint t u ∧ t.ncard = u.ncard := by
  obtain ⟨t, u, hutu, hdtu, hctu⟩ := exists_union_disjoint_cardinal_eq_of_even he
  exact ⟨t, u, hutu, hdtu, congrArg Cardinal.toNat hctu⟩

theorem exists_union_disjoint_cardinal_eq_iff (s : Set α) :
    Even (s.ncard) ↔ ∃ (t u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #t = #u := by
  use exists_union_disjoint_cardinal_eq_of_even
  rintro ⟨t, u, rfl, hdtu, hctu⟩
  obtain hfin | hnfin := (t ∪ u).finite_or_infinite
  · rw [finite_union] at hfin
    have hn : t.ncard = u.ncard := congrArg Cardinal.toNat hctu
    rw [ncard_union_eq hdtu hfin.1 hfin.2, hn]
    exact Even.add_self u.ncard
  · simp only [hnfin.ncard, even_zero]

Adopted your suggestions, thanks!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@vihdzp vihdzp vihdzp left review comments

@b-mehta b-mehta b-mehta left review comments

@tb65536 tb65536 tb65536 left review comments

Assignees
No one assigned
Labels
large-import Automatically added label for PRs with a significant increase in transitive imports t-data Data (lists, quotients, numbers, etc) t-logic Logic (model theory, etc)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@pimotte @vihdzp @mathlib4-dependent-issues-bot @tb65536 @b-mehta