Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-19 12:41 697c8dd9

View on Github →

refactor(topology/basic): use dot notation in is_open.union and friends (#7647) The fact that the union of two open sets is open is called is_open_union. We rename it to is_open.union to enable dot notation. Same with is_open_inter, is_closed_union and is_closed_inter and is_clopen_union and is_clopen_inter and is_clopen_diff.

Estimated changes

added theorem is_closed.inter
added theorem is_closed.not
added theorem is_closed.union
deleted theorem is_closed_inter
deleted theorem is_closed_union
added theorem is_open.and
added theorem is_open.inter
added theorem is_open.sdiff
added theorem is_open.union
deleted theorem is_open_and
deleted theorem is_open_diff
deleted theorem is_open_inter
deleted theorem is_open_neg
deleted theorem is_open_union
added theorem Scott.is_open.inter
deleted theorem Scott.is_open_inter
added theorem is_clopen.compl
added theorem is_clopen.diff
added theorem is_clopen.inter
added theorem is_clopen.union
deleted theorem is_clopen_compl
deleted theorem is_clopen_diff
deleted theorem is_clopen_inter
deleted theorem is_clopen_union