Topology

Statistics

Metric	Count
Definitions	0
Theorems `ae_restrict_le_codiscreteWithin`	1
Total	1

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_restrict_le_codiscreteWithin` 📖	mathematical	`MeasurableSet`	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.restrict` `Filter.codiscreteWithin`	—	`isDiscrete_iff_discreteTopology` `isDiscrete_of_codiscreteWithin` `compl_compl` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.mem_ae_iff` `MeasureTheory.Measure.restrict_apply'` `Set.Countable.measure_zero` `TopologicalSpace.separableSpace_iff_countable` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.Subtype.secondCountableTopology`

---