Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-02 17:31 ae025835

View on Github →

refactor(data/set/finite): protect set.finite (#14344) This change will make it so that it does not conflict with a top-level finite that will be added to complement infinite.

Estimated changes

modified theorem mul_finprod_cond_ne
modified theorem set.finite.star
modified theorem set.finite.convex_hull_eq
modified theorem set.finite.countable
modified theorem set.exists_max_image
modified theorem set.exists_min_image
modified theorem set.finite.bdd_above_bUnion
modified theorem set.finite.bdd_below_bUnion
modified theorem set.finite.fin_embedding
modified theorem set.finite.finite_subsets
modified theorem set.finite.inf_of_left
modified theorem set.finite.inf_of_right
modified theorem set.finite.map
modified theorem set.finite.of_diff
modified theorem set.finite.sUnion
modified theorem set.finite.sup
modified inductive set.finite
modified theorem set.finite_is_bot
modified theorem set.finite_is_top
modified theorem set.finite_le_nat
modified theorem set.finite_lt_nat
modified theorem set.finite_mem_finset
modified theorem set.finite_option
modified theorem set.finite_range_const
modified theorem set.finite_range_ite
modified theorem set.finite_subset_Union
modified theorem set.subsingleton.finite
modified theorem set.finite.inv
modified theorem set.finite.mul
modified theorem set.finite.smul
modified theorem set.finite.smul_set
modified theorem set.finite.vsub
modified theorem finrank_span_le_card
modified theorem finrank_span_set_eq_card
modified theorem set.finite.measurable_set
modified theorem set.finite.cSup_lt_iff
modified theorem set.finite.lt_cInf_iff
modified theorem set.nonempty.cInf_mem
modified theorem set.nonempty.cSup_mem
modified theorem filter.bInter_mem
modified theorem filter.mem_infi_of_Inter
modified theorem filter.sInter_mem
modified theorem filter.mem_cofinite
modified theorem filter.pi_mem_pi
modified theorem filter.pi_mem_pi_iff
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 submodule.fg_span
modified theorem set.finite.is_Gδ
modified theorem set.finite.is_Gδ_compl
modified theorem set.finite.is_separable
modified theorem is_closed_bUnion
modified theorem is_open_bInter
modified theorem is_open_sInter
modified theorem bornology.is_bounded_bUnion
modified theorem bornology.is_bounded_sUnion
modified theorem metric.bounded_bUnion
modified theorem metric.bounded_of_finite
modified theorem dimH_finite
modified theorem set.finite.compact_bUnion
modified theorem set.finite.is_compact