Commit 2024-02-06 07:47 a76d5c1c

View on Github →

feat(Topology/Bases): review IsSeparable API (#10286)

  • upgrade isSeparable_iUnion to an Iff lemma, restore the original version as IsSeparable.iUnion;
  • add isSeparable_union and isSeparable_closure;
  • upgrade isSeparable_pi from [Finite ι] to [Countable ι], add IsSeparable.univ_pi version;
  • add Dense.isSeparable_iff and isSeparable_range;
  • rename isSeparable_of_separableSpace_subtype to IsSeparable.of_subtype;
  • rename isSeparable_of_separableSpace to IsSeparable.of_separableSpace.

Estimated changes

added theorem Dense.isSeparable_iff