locally_finite): add Ico_subset_Ico_union_Ico (#11710)

Commit

3 years ago

feat(data/finset/locally_finite): add Ico_subset_Ico_union_Ico (#11710) This lemma extends the result for `set`s to `finset`s.

Author

BoltonBailey

Parents