Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-07 16:57 7428bd9b

View on Github →

refactor(data/finite/set,data/set/finite): move most contents of one file to another (#15166)

  • move most content of data.finite.set to data.set.finite;
  • use casesI nonempty_fintype _ instead of letI := fintype.of_finite; sometimes it lets us avoid classical.choice;
  • merge set.finite.of_fintype, set.finite_of_fintype, and set.finite_of_finite into set.to_finite;
  • rewrite set.finite_univ_iff and finite.of_finite_univ in terms of set.finite;
  • replace some assumptions [fintype (plift _)] with [finite _];
  • generalize set.cod_restrict and some lemmas to allow domain in Sort*, use it for finite.of_injective_finite.range.

Estimated changes

modified def fintype.of_finite
added theorem nonempty_fintype
deleted theorem finite.of_finite_univ
deleted theorem finite.set.finite_bUnion
deleted theorem set.finite_iff_finite
deleted theorem set.finite_of_finite
deleted theorem set.finite_univ_iff
modified theorem finset.finite_to_set
deleted theorem set.finite.of_fintype
modified theorem set.finite.of_subsingleton
modified theorem set.finite_Union
added theorem set.finite_coe_iff
modified theorem set.finite_empty
modified theorem set.finite_le_nat
modified theorem set.finite_lt_nat
modified theorem set.finite_mem_finset
deleted theorem set.finite_of_fintype
modified theorem set.finite_pure
modified theorem set.finite_range
modified theorem set.finite_singleton
modified theorem set.finite_univ
added theorem set.finite_univ_iff
added theorem set.to_finite
modified def set.cod_restrict
modified theorem set.coe_cod_restrict_apply
modified theorem set.injective_cod_restrict
modified theorem set.finite_Icc
modified theorem set.finite_Ici
modified theorem set.finite_Ico
modified theorem set.finite_Iic
modified theorem set.finite_Iio
modified theorem set.finite_Ioc
modified theorem set.finite_Ioi
modified theorem set.finite_Ioo
modified theorem set.fintype.is_pwo