Skip to content

[Merged by Bors] - feat(Data/Set/Card): a few missing lemmas - #22186

Closed
apnelson1 wants to merge 6 commits into
masterfrom
encard_lemmas
Closed

[Merged by Bors] - feat(Data/Set/Card): a few missing lemmas#22186
apnelson1 wants to merge 6 commits into
masterfrom
encard_lemmas

Conversation

@apnelson1

@apnelson1 apnelson1 commented Feb 22, 2025 •
edited
Loading

Copy link
Copy Markdown
Collaborator

We add two simp lemmas where the RHS is Set.encard s and the LHS is something uglier.

We also add two lemmas relating Set.Subsingleton and Set.Nontrivial with Set.encard.

Open in Gitpod

@github-actions github-actions Bot added the t-data Data (lists, quotients, numbers, etc) label Feb 22, 2025
@github-actions

github-actions Bot commented Feb 22, 2025 •
edited
Loading

Copy link
Copy Markdown

PR summary 9cf70dcadc

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ coe_fintypeCard
+ encard_le_one_iff_subsingleton
+ one_lt_encard_iff_nontrivial
+ toENat_cardinalMk

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).

@apnelson1 apnelson1 changed the title feat(Data/Set/Card): two missing simp lemmas feat(Data/Set/Card): a few missing lemmas Feb 22, 2025
eric-wieser
eric-wieser reviewed Feb 22, 2025
View reviewed changes
Comment thread Mathlib/Algebra/Group/Pointwise/Set/Card.lean
eric-wieser
eric-wieser reviewed Feb 22, 2025
View reviewed changes
Comment thread Mathlib/Data/Set/Card.lean Outdated
Ruben-VandeVelde
Ruben-VandeVelde reviewed Feb 22, 2025
View reviewed changes

@Ruben-VandeVelde Ruben-VandeVelde left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Thanks!

Comment thread Mathlib/Data/Set/Card.lean Outdated
Comment thread Mathlib/Data/Set/Card.lean Outdated
Comment thread Mathlib/Data/Set/Card.lean Outdated
madvorak
madvorak approved these changes Feb 23, 2025
View reviewed changes
Comment thread Mathlib/Data/Set/Card.lean Outdated
jcommelin
jcommelin reviewed Feb 24, 2025
View reviewed changes

@jcommelin jcommelin left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Feb 24, 2025
mathlib-bors Bot pushed a commit that referenced this pull request Feb 24, 2025
@apnelson1
feat(Data/Set/Card): a few missing lemmas (#22186)
709c428 
We add two simp lemmas where the RHS is `Set.encard s` and the LHS is something uglier.

We also add two lemmas relating `Set.Subsingleton`  and `Set.Nontrivial` with `Set.encard`.
@mathlib-bors

mathlib-bors Bot commented Feb 24, 2025

Copy link
Copy Markdown
Contributor

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title feat(Data/Set/Card): a few missing lemmas [Merged by Bors] - feat(Data/Set/Card): a few missing lemmas Feb 24, 2025
@mathlib-bors mathlib-bors Bot closed this Feb 24, 2025
@mathlib-bors
mathlib-bors Bot deleted the encard_lemmas branch February 24, 2025 10:06
Julian added a commit that referenced this pull request Feb 24, 2025
@Julian
Merge remote-tracking branch 'origin/master' into bhargava-factorial
3dec536 
* origin/master:
  feat(Polynomial): polynomial sequences are bases for R[X] (#20846)
  feat: monoidal structure on Hopf algebras (#12011)
  feat(DiscreteValuationRing): addVal_eq_zero_iff (#21154)
  refactor(Cache): refactor getPackageDir to not use manually provided package directories (#21817)
  feat(CategoryTheory): categories of homological complexes have a separator (#20229)
  chore(Data/Complex): deprecate `Complex.abs` (#21995)
  feat: uncountable instances for `Ordinal` and isomorphic types (#18547)
  feat(Data/Set/Card): a few missing lemmas (#22186)
  feat: discrete topological spaces are 0-manifolds (#22105)
  feat(Data/Matroid/Loop): matroid loops (#22045)
  feat(SetTheory/Ordinal/Nimber/Field): Nimber division (#19066)
  feat(LinearAlgebra/Pi): add `pi_proj` and `pi_proj_comp` (#22162)
  feat(Data/Matroid/Circuit): matroid cocircuits (#21692)
  feat(Topology/Compactification/OnePoint): generalize instance (#22179)
  feat(Combinatorics/SimpleGraph): takeUntil properties (#21250)
  feat(Tactic): `pnat_to_nat` and `enat_to_nat` tactics (#21602)
  refactor: move `Polynomial.coeffs` and related results (#22225)
  chore: add AlgHom.ker_coe_equiv, resolve porting notes and erws (#22019)
  refactor(Order/Category): `ConcreteCategory` instance for `\omegaCPO` (#21478)
  feat(CategoryTheory): Grothendieck categories have a coseparator (#22224)
  feat: tweak calc widget (#22170)
  feat(CategoryTheory): the Freyd-Mitchell embedding theorem (#22222)
  chore(CategoryTheory): turn more `simp` into `simps!` (#22223)
  feat(CategoryTheory): the category of ind-objects is Grothendieck abelian (#21606)
  feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono): epi-mono factorisation in `SimplexCategoryGenRel` (#21743)
  chore(CategoryTheory/DiscreteCategory): turn `simp` to `simps!` (#22217)
  feat(Analysis/Asymptotics): exponential growth of a sequence (#21178)
  feat(CategoryTheory): sigmaConst preserves monomorphisms (#21599)
  feat(RingTheory/Cotangent): `liftBaseChange` is injective for localizations (#21037)
  chore(CategoryTheory): fix incorrect name (#22210)
  feat(CategoryTheory): `IsPullback` version of 'pullback of iso is iso' (#22211)
  feat(CategoryTheory): pullbacks in functor categories (#22209)
  feat(CategoryTheory): detecting limit cones over connected diagrams (#22192)
  feat(LinearAlgebra): add theorems for injective/surjective/bijective compositions of bilinear maps (#21491)
Champitoad pushed a commit that referenced this pull request Feb 25, 2025
@apnelson1 @Champitoad
feat(Data/Set/Card): a few missing lemmas (#22186)
5aabe4d 
We add two simp lemmas where the RHS is `Set.encard s` and the LHS is something uglier.

We also add two lemmas relating `Set.Subsingleton`  and `Set.Nontrivial` with `Set.encard`.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@eric-wieser eric-wieser eric-wieser left review comments
@jcommelin jcommelin jcommelin left review comments
@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde left review comments
+1 more reviewer
@madvorak madvorak madvorak approved these changes
Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-data Data (lists, quotients, numbers, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@apnelson1 @eric-wieser @jcommelin @madvorak @Ruben-VandeVelde