Commit 2024-02-15 20:01 a39f83f3

View on Github →

refactor(Set/Finite): redefine using _root_.Finite (#10542)

Estimated changes

modified theorem Set.Finite.diff
modified theorem Set.Finite.finite_subsets
modified theorem Set.Finite.inter_of_left
modified theorem Set.Finite.inter_of_right
modified theorem Set.Finite.sep
deleted inductive Set.Finite
modified theorem Set.finite_coe_iff
modified theorem Set.finite_iUnion
modified theorem Set.finite_univ_iff
modified theorem Set.toFinite