Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-18 10:59 4d4b501e

View on Github →

chore(data/set/finite): rename some lemmas (#7241)

Revert some name changes from #5813

  • set.fintype_set_bUnion → set.fintype_bUnion;
  • set.fintype_set_bUnion' → set.fintype_bUnion';
  • set.fintype_bUnion → set.fintype_bind;
  • set.fintype_bUnion' → set.fintype_bind';
  • set.finite_bUnion → set.finite.bind;

Add a few lemmas

  • set.finite_Union_Prop;
  • add set.seq versions of lemmas/defs about <*> (they work for α, β in different universes).

Estimated changes

added theorem set.finite.bind
added theorem set.finite.seq'
modified theorem set.finite.seq
added theorem set.finite_Union_Prop
deleted theorem set.finite_bUnion
modified def set.fintype_bUnion
added def set.fintype_bind