Commit 2022-07-13 02:40 ea13c1cf

View on Github →

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.

Estimated changes

Modified src/topology/category/Profinite/cofiltered_limit.lean

Modified src/topology/separation.lean

Modified src/topology/subset_properties.lean

added theorem is_clopen.prod

modified theorem is_clopen_bInter

added theorem is_clopen_bInter_finset

modified theorem is_clopen_bUnion

added theorem is_clopen_bUnion_finset