Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_clopen_bUnion_finset

Modification history

2022-07-13 02:40

src/topology/subset_properties.lean

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

Added is_clopen_bUnion_finset View on Github →