CountableSeparatingOn

Statistics

Metric	Count
Definitions	0
Theorems `instHasCountableSeparatingOnIsClosedOfIsOpen`, `instHasCountableSeparatingOnIsOpenOfT0SpaceOfSecondCountableTopologyElem`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`instHasCountableSeparatingOnIsClosedOfIsOpen` 📖	mathematical	—	`HasCountableSeparatingOn` `IsClosed`	—	`HasCountableSeparatingOn.exists_countable_separating` `Set.Countable.image` `Set.forall_mem_image` `IsOpen.isClosed_compl` `not_iff_not` `Set.mem_image_of_mem`
`instHasCountableSeparatingOnIsOpenOfT0SpaceOfSecondCountableTopologyElem` 📖	mathematical	—	`HasCountableSeparatingOn` `IsOpen`	—	`TopologicalSpace.countable_countableBasis` `TopologicalSpace.isOpen_of_mem_countableBasis` `Inseparable.eq` `TopologicalSpace.IsTopologicalBasis.inseparable_iff` `TopologicalSpace.isBasis_countableBasis` `HasCountableSeparatingOn.of_subtype` `isOpen_induced_iff`

---