mathlib3
ea13c1cf - refactor(topology/subset_properties): reformulate `is_clopen_b{Union,Inter}` in terms of `set.finite` (#15272)

Commit

3 years ago

refactor(topology/subset_properties): reformulate `is_clopen_b{Union,Inter}` in terms of `set.finite` (#15272) This way it mirrors `is_open_bInter`/`is_closed_bUnion`. Also add `is_clopen.prod`.

Author

urkud

Parents

2a325960

mathlib3 ea13c1cf - refactor(topology/subset_properties): reformulate `is_clopen_b{Union,Inter}` in terms of `set.finite` (#15272)

mathlib3
ea13c1cf - refactor(topology/subset_properties): reformulate `is_clopen_b{Union,Inter}` in terms of `set.finite` (#15272)