CountablyGenerated

📁 Source: Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean

Statistics

Metric	Count
Definitions `CountableOrCountablyGenerated`, `CountablyGenerated`, `CountablySeparated`, `SeparatesPoints`, `countableGeneratingSet`, `countablePartition`, `countablePartitionSet`, `mapNatBool`, `natGeneratingSequence`	9
Theorems `countableOrCountablyGenerated`, `comap`, `isCountablyGenerated`, `sup`, `countably_separated`, `mono`, `subtype_iff`, `of_separatesPoints`, `mono`, `separates`, `countablySeparated`, `separatesPoints`, `countableOrCountablyGenerated_left_of_prod_left_of_nonempty`, `countableOrCountablyGenerated_prod_left_swap`, `countableOrCountablyGenerated_right_of_prod_left_of_nonempty`, `countablePartitionSet_eq_iff`, `countablePartitionSet_mem`, `countablePartitionSet_of_mem`, `countable_countableGeneratingSet`, `countablySeparated_def`, `countablySeparated_of_hasCountableSeparatingOn`, `countablySeparated_of_separatesPoints`, `countablySeparated_subtype_of_hasCountableSeparatingOn`, `disjoint_countablePartition`, `empty_mem_countableGeneratingSet`, `exists_countablyGenerated_le_of_countablySeparated`, `exists_measurableSet_of_ne`, `finite_countablePartition`, `generateFrom_countableGeneratingSet`, `generateFrom_countablePartition_le`, `generateFrom_countablePartition_le_succ`, `generateFrom_iUnion_countablePartition`, `generateFrom_iUnion_memPartition`, `generateFrom_iUnion_memPartition_le`, `generateFrom_memPartition_le`, `generateFrom_memPartition_le_range`, `generateFrom_memPartition_le_succ`, `generateFrom_natGeneratingSequence`, `hasCountableSeparatingOn_of_countablySeparated`, `hasCountableSeparatingOn_of_countablySeparated_subtype`, `injective_mapNatBool`, `instCountableOrCountablyGeneratedOfCountable`, `instCountableOrCountablyGeneratedOfCountablyGenerated`, `instCountableOrCountablyGeneratedProd`, `instCountablyGeneratedOfCountable`, `instCountablyGeneratedProd`, `instCountablyGeneratedSubtype`, `instFinite_countablePartition`, `measurableEquiv_nat_bool_of_countablyGenerated`, `measurableSet_countableGeneratingSet`, `measurableSet_countablePartition`, `measurableSet_countablePartitionSet`, `measurableSet_enumerateCountable_countableGeneratingSet`, `measurableSet_generateFrom_countablePartition_iff`, `measurableSet_generateFrom_memPartition`, `measurableSet_generateFrom_memPartition_iff`, `measurableSet_memPartition`, `measurableSet_memPartitionSet`, `measurableSet_natGeneratingSequence`, `measurableSet_succ_countablePartition`, `measurableSet_succ_memPartition`, `measurableSingletonClass_of_countablySeparated`, `measurable_injection_nat_bool_of_countablySeparated`, `measurable_mapNatBool`, `mem_countablePartitionSet`, `nonempty_countableGeneratingSet`, `sUnion_countablePartition`, `separatesPoints_def`, `separatesPoints_iff`, `separatesPoints_of_measurableSingletonClass`, `separating_of_generateFrom`, `eq_const_of_measurable_bot`	72
Total	81

MeasurableSpace

Definitions

Name	Category	Theorems
`CountableOrCountablyGenerated` 📖	CompData	6 math math: `countableOrCountablyGenerated_left_of_prod_left_of_nonempty`, `countableOrCountablyGenerated_right_of_prod_left_of_nonempty`, `instCountableOrCountablyGeneratedOfCountablyGenerated`, `instCountableOrCountablyGeneratedProd`, `countableOrCountablyGenerated_prod_left_swap`, `instCountableOrCountablyGeneratedOfCountable`
`CountablyGenerated` 📖	CompData	9 math math: `CountablyGenerated.comap`, `exists_countablyGenerated_le_of_countablySeparated`, `instCountablyGeneratedProd`, `instCountablyGeneratedOfCountable`, `countablyGenerated_of_standardBorel`, `CountablyGenerated.sup`, `instCountablyGeneratedSubtype`, `CountableOrCountablyGenerated.countableOrCountablyGenerated`, `BorelSpace.countablyGenerated`
`CountablySeparated` 📖	CompData	8 math math: `countablySeparated_of_separatesPoints`, `CountablySeparated.mono`, `countablySeparated_def`, `Subtype.countablySeparated`, `CountablySeparated.subtype_iff`, `countablySeparated_of_hasCountableSeparatingOn`, `countablySeparated_subtype_of_hasCountableSeparatingOn`, `instCountablySeparatedElemOfHasCountableSeparatingOnIsOpen`
`SeparatesPoints` 📖	CompData	7 math math: `Subtype.separatesPoints`, `exists_countablyGenerated_le_of_countablySeparated`, `separatesPoints_iff`, `OpensMeasurableSpace.separatesPoints`, `separatesPointsOfOpensMeasurableSpaceOfT0Space`, `separatesPoints_of_measurableSingletonClass`, `SeparatesPoints.mono`
`countableGeneratingSet` 📖	CompOp	5 math math: `measurableSet_enumerateCountable_countableGeneratingSet`, `nonempty_countableGeneratingSet`, `empty_mem_countableGeneratingSet`, `generateFrom_countableGeneratingSet`, `countable_countableGeneratingSet`
`countablePartition` 📖	CompOp	9 math math: `instFinite_countablePartition`, `sUnion_countablePartition`, `ProbabilityTheory.measurable_countablePartitionSet_subtype`, `finite_countablePartition`, `measurableSet_generateFrom_countablePartition_iff`, `generateFrom_iUnion_countablePartition`, `countablePartitionSet_mem`, `generateFrom_countablePartition_le`, `generateFrom_countablePartition_le_succ`
`countablePartitionSet` 📖	CompOp	14 math math: `ProbabilityTheory.Kernel.measurable_densityProcess_countableFiltration_aux`, `mem_countablePartitionSet`, `measurableSet_countablePartitionSet`, `ProbabilityTheory.Kernel.meas_countablePartitionSet_le_of_fst_le`, `ProbabilityTheory.measurable_countablePartitionSet_subtype`, `ProbabilityTheory.measurable_countablePartitionSet`, `ProbabilityTheory.measurableSet_countableFiltration_countablePartitionSet`, `ProbabilityTheory.Kernel.measurable_densityProcess_aux`, `countablePartitionSet_mem`, `ProbabilityTheory.Kernel.densityProcess_fst_univ`, `countablePartitionSet_eq_iff`, `ProbabilityTheory.Kernel.densityProcess_def`, `countablePartitionSet_of_mem`, `ProbabilityTheory.measurable_countableFiltration_countablePartitionSet`
`mapNatBool` 📖	CompOp	2 math math: `measurable_mapNatBool`, `injective_mapNatBool`
`natGeneratingSequence` 📖	CompOp	2 math math: `generateFrom_natGeneratingSequence`, `measurableSet_natGeneratingSequence`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`countableOrCountablyGenerated_left_of_prod_left_of_nonempty` 📖	mathematical	—	`CountableOrCountablyGenerated`	—	`CountableOrCountablyGenerated.countableOrCountablyGenerated` `countable_left_of_prod_of_nonempty` `instCountableOrCountablyGeneratedOfCountable` `instCountableOrCountablyGeneratedOfCountablyGenerated`
`countableOrCountablyGenerated_prod_left_swap` 📖	mathematical	—	`CountableOrCountablyGenerated`	—	`countable_prod_swap`
`countableOrCountablyGenerated_right_of_prod_left_of_nonempty` 📖	mathematical	—	`CountableOrCountablyGenerated`	—	`CountableOrCountablyGenerated.countableOrCountablyGenerated` `countable_right_of_prod_of_nonempty` `instCountableOrCountablyGeneratedOfCountable` `instCountableOrCountablyGeneratedOfCountablyGenerated`
`countablePartitionSet_eq_iff` 📖	mathematical	`Set` `Set.instMembership` `countablePartition`	`countablePartitionSet`	—	`memPartitionSet_eq_iff` `countable_countableGeneratingSet`
`countablePartitionSet_mem` 📖	mathematical	—	`Set` `Set.instMembership` `countablePartition` `countablePartitionSet`	—	`memPartitionSet_mem` `countable_countableGeneratingSet`
`countablePartitionSet_of_mem` 📖	mathematical	`Set` `Set.instMembership` `countablePartition`	`countablePartitionSet`	—	`memPartitionSet_of_mem` `countable_countableGeneratingSet`
`countable_countableGeneratingSet` 📖	mathematical	—	`Set.Countable` `Set` `countableGeneratingSet`	—	`Set.Countable.insert` `CountablyGenerated.isCountablyGenerated`
`countablySeparated_def` 📖	mathematical	—	`CountablySeparated` `HasCountableSeparatingOn` `MeasurableSet` `Set.univ`	—	`CountablySeparated.countably_separated`
`countablySeparated_of_hasCountableSeparatingOn` 📖	mathematical	—	`CountablySeparated`	—	—
`countablySeparated_of_separatesPoints` 📖	mathematical	—	`CountablySeparated`	—	`separating_of_generateFrom`
`countablySeparated_subtype_of_hasCountableSeparatingOn` 📖	mathematical	—	`CountablySeparated` `Set.Elem` `Subtype.instMeasurableSpace` `Set` `Set.instMembership`	—	`CountablySeparated.subtype_iff`
`disjoint_countablePartition` 📖	mathematical	`Set` `Set.instMembership` `countablePartition`	`Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`disjoint_memPartition` `countable_countableGeneratingSet`
`empty_mem_countableGeneratingSet` 📖	mathematical	—	`Set` `Set.instMembership` `countableGeneratingSet` `Set.instEmptyCollection`	—	`Set.mem_insert` `CountablyGenerated.isCountablyGenerated`
`exists_countablyGenerated_le_of_countablySeparated` 📖	mathematical	—	`CountablyGenerated` `SeparatesPoints` `MeasurableSpace` `instLE`	—	`separatesPoints_iff` `measurableSet_generateFrom` `generateFrom_le`
`exists_measurableSet_of_ne` 📖	mathematical	—	`MeasurableSet` `Set` `Set.instMembership`	—	`Mathlib.Tactic.Contrapose.contrapose₂` `Mathlib.Tactic.Push.not_and_eq` `separatesPoints_def`
`finite_countablePartition` 📖	mathematical	—	`Set.Finite` `Set` `countablePartition`	—	`finite_memPartition` `countable_countableGeneratingSet`
`generateFrom_countableGeneratingSet` 📖	mathematical	—	`generateFrom` `countableGeneratingSet`	—	`CountablyGenerated.isCountablyGenerated` `generateFrom_insert_empty`
`generateFrom_countablePartition_le` 📖	mathematical	—	`MeasurableSpace` `instLE` `generateFrom` `countablePartition`	—	`generateFrom_memPartition_le` `countable_countableGeneratingSet` `measurableSet_enumerateCountable_countableGeneratingSet`
`generateFrom_countablePartition_le_succ` 📖	mathematical	—	`MeasurableSpace` `instLE` `generateFrom` `countablePartition`	—	`generateFrom_memPartition_le_succ` `countable_countableGeneratingSet`
`generateFrom_iUnion_countablePartition` 📖	mathematical	—	`generateFrom` `Set.iUnion` `Set` `countablePartition`	—	`countable_countableGeneratingSet` `countablePartition.eq_1` `generateFrom_iUnion_memPartition` `Set.range_enumerateCountable_of_mem` `empty_mem_countableGeneratingSet` `generateFrom_countableGeneratingSet`
`generateFrom_iUnion_memPartition` 📖	mathematical	—	`generateFrom` `Set.iUnion` `Set` `memPartition` `Set.range`	—	`le_antisymm` `generateFrom_le` `MeasurableSet.univ` `MeasurableSet.inter` `measurableSet_generateFrom` `MeasurableSet.diff` `generateFrom_mono` `Set.subset_iUnion` `measurableSet_generateFrom_memPartition`
`generateFrom_iUnion_memPartition_le` 📖	mathematical	`MeasurableSet`	`MeasurableSpace` `instLE` `generateFrom` `Set.iUnion` `Set` `memPartition`	—	`Eq.trans_le` `generateFrom_iUnion_memPartition` `generateFrom_le`
`generateFrom_memPartition_le` 📖	mathematical	`MeasurableSet`	`MeasurableSpace` `instLE` `generateFrom` `memPartition`	—	`LE.le.trans` `generateFrom_mono` `Set.subset_iUnion` `generateFrom_iUnion_memPartition_le`
`generateFrom_memPartition_le_range` 📖	mathematical	—	`MeasurableSpace` `instLE` `generateFrom` `memPartition` `Set.range` `Set`	—	`generateFrom_iUnion_memPartition` `generateFrom_mono` `Set.subset_iUnion`
`generateFrom_memPartition_le_succ` 📖	mathematical	—	`MeasurableSpace` `instLE` `generateFrom` `memPartition`	—	`generateFrom_le` `measurableSet_succ_memPartition`
`generateFrom_natGeneratingSequence` 📖	mathematical	—	`generateFrom` `Set.range` `Set` `natGeneratingSequence`	—	`countable_countableGeneratingSet` `natGeneratingSequence.eq_1` `Set.range_enumerateCountable_of_mem` `empty_mem_countableGeneratingSet` `generateFrom_countableGeneratingSet`
`hasCountableSeparatingOn_of_countablySeparated` 📖	mathematical	—	`HasCountableSeparatingOn` `MeasurableSet` `Set.univ`	—	`CountablySeparated.countably_separated`
`hasCountableSeparatingOn_of_countablySeparated_subtype` 📖	mathematical	—	`HasCountableSeparatingOn` `MeasurableSet`	—	`CountablySeparated.subtype_iff`
`injective_mapNatBool` 📖	mathematical	—	`mapNatBool`	—	`separating_of_generateFrom` `generateFrom_natGeneratingSequence`
`instCountableOrCountablyGeneratedOfCountable` 📖	mathematical	—	`CountableOrCountablyGenerated`	—	—
`instCountableOrCountablyGeneratedOfCountablyGenerated` 📖	mathematical	—	`CountableOrCountablyGenerated`	—	—
`instCountableOrCountablyGeneratedProd` 📖	mathematical	—	`CountableOrCountablyGenerated`	—	`instCountableOrCountablyGeneratedOfCountable` `instCountableProd` `instCountableOrCountablyGeneratedOfCountablyGenerated`
`instCountablyGeneratedOfCountable` 📖	mathematical	—	`CountablyGenerated`	—	`Set.countable_iUnion` `Set.countable_singleton` `le_antisymm` `Set.Subset.antisymm` `measurableAtom_subset` `MeasurableSet.biUnion` `Set.to_countable` `SetCoe.countable` `measurableSet_generateFrom` `Set.iUnion_singleton_eq_range` `generateFrom_le`
`instCountablyGeneratedProd` 📖	mathematical	—	`CountablyGenerated` `Prod.instMeasurableSpace`	—	`CountablyGenerated.sup` `CountablyGenerated.comap`
`instCountablyGeneratedSubtype` 📖	mathematical	—	`CountablyGenerated` `Subtype.instMeasurableSpace`	—	`CountablyGenerated.comap`
`instFinite_countablePartition` 📖	mathematical	—	`Finite` `Set.Elem` `Set` `countablePartition`	—	`Set.finite_coe_iff` `finite_countablePartition`
`measurableEquiv_nat_bool_of_countablyGenerated` 📖	mathematical	—	`MeasurableEquiv` `Set.Elem` `Subtype.instMeasurableSpace` `Set` `Set.instMembership` `pi` `Bool.instMeasurableSpace`	—	`injective_mapNatBool` `measurable_mapNatBool` `generateFrom_natGeneratingSequence` `measurable_generateFrom` `Equiv.image_eq_preimage_symm` `Measurable.eq_const` `Bool.instMeasurableSingletonClass` `measurable_pi_apply` `Equiv.preimage_eq_iff_eq_image`
`measurableSet_countableGeneratingSet` 📖	mathematical	`Set` `Set.instMembership` `countableGeneratingSet`	`MeasurableSet`	—	`generateFrom_countableGeneratingSet` `measurableSet_generateFrom`
`measurableSet_countablePartition` 📖	mathematical	`Set` `Set.instMembership` `countablePartition`	`MeasurableSet`	—	`generateFrom_countablePartition_le` `measurableSet_generateFrom`
`measurableSet_countablePartitionSet` 📖	mathematical	—	`MeasurableSet` `countablePartitionSet`	—	`measurableSet_countablePartition` `countablePartitionSet_mem`
`measurableSet_enumerateCountable_countableGeneratingSet` 📖	mathematical	—	`MeasurableSet` `Set.enumerateCountable` `Set` `countableGeneratingSet` `countable_countableGeneratingSet` `Set.instEmptyCollection`	—	`measurableSet_countableGeneratingSet` `countable_countableGeneratingSet` `Set.enumerateCountable_mem` `empty_mem_countableGeneratingSet`
`measurableSet_generateFrom_countablePartition_iff` 📖	mathematical	—	`MeasurableSet` `generateFrom` `countablePartition` `Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `Set.sUnion`	—	`measurableSet_generateFrom_memPartition_iff` `countable_countableGeneratingSet`
`measurableSet_generateFrom_memPartition` 📖	mathematical	—	`MeasurableSet` `generateFrom` `memPartition`	—	`sUnion_memPartition` `Set.univ_inter` `MeasurableSet.biUnion` `Set.Finite.countable` `finite_memPartition` `measurableSet_generateFrom` `memPartition_succ`
`measurableSet_generateFrom_memPartition_iff` 📖	mathematical	—	`MeasurableSet` `generateFrom` `memPartition` `Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `Set.sUnion`	—	`generateFrom_induction` `Finset.coe_singleton` `Set.sUnion_singleton` `Finset.coe_empty` `Set.sUnion_empty` `Finset.coe_sdiff` `Set.coe_toFinset` `Set.diff_subset` `IsCompl.eq_compl` `Set.disjoint_sUnion_right` `Set.disjoint_sUnion_left` `disjoint_memPartition` `Set.mem_of_mem_diff` `Set.notMem_of_mem_diff` `codisjoint_iff` `sUnion_memPartition` `Set.union_comm` `Set.sUnion_union` `Set.union_diff_cancel` `Set.Finite.subset` `finite_memPartition` `Set.sUnion_iUnion` `Set.sUnion_eq_biUnion` `MeasurableSet.biUnion` `Finset.countable_toSet` `measurableSet_generateFrom`
`measurableSet_memPartition` 📖	—	`MeasurableSet` `Set` `Set.instMembership` `memPartition`	—	—	`generateFrom_memPartition_le` `measurableSet_generateFrom`
`measurableSet_memPartitionSet` 📖	mathematical	`MeasurableSet`	`memPartitionSet`	—	`measurableSet_memPartition` `memPartitionSet_mem`
`measurableSet_natGeneratingSequence` 📖	mathematical	—	`MeasurableSet` `natGeneratingSequence`	—	`measurableSet_countableGeneratingSet` `Set.enumerateCountable_mem` `countable_countableGeneratingSet` `empty_mem_countableGeneratingSet`
`measurableSet_succ_countablePartition` 📖	mathematical	`Set` `Set.instMembership` `countablePartition`	`MeasurableSet` `generateFrom`	—	`measurableSet_succ_memPartition` `countable_countableGeneratingSet`
`measurableSet_succ_memPartition` 📖	mathematical	`Set` `Set.instMembership` `memPartition`	`MeasurableSet` `generateFrom`	—	`Set.diff_union_inter` `MeasurableSet.union` `measurableSet_generateFrom` `memPartition_succ`
`measurableSingletonClass_of_countablySeparated` 📖	mathematical	—	`MeasurableSingletonClass`	—	`measurable_injection_nat_bool_of_countablySeparated` `Function.Injective.preimage_image` `Set.image_singleton` `MeasurableSet.singleton` `Pi.instMeasurableSingletonClass` `instCountableNat` `Bool.instMeasurableSingletonClass`
`measurable_injection_nat_bool_of_countablySeparated` 📖	mathematical	—	`Measurable` `pi` `Bool.instMeasurableSpace`	—	`exists_countablyGenerated_le_of_countablySeparated` `Measurable.mono` `measurable_mapNatBool` `le_rfl` `injective_mapNatBool`
`measurable_mapNatBool` 📖	mathematical	—	`Measurable` `pi` `Bool.instMeasurableSpace` `mapNatBool`	—	`measurable_pi_iff` `measurable_to_bool` `measurableSet_natGeneratingSequence`
`mem_countablePartitionSet` 📖	mathematical	—	`Set` `Set.instMembership` `countablePartitionSet`	—	`mem_memPartitionSet` `countable_countableGeneratingSet`
`nonempty_countableGeneratingSet` 📖	mathematical	—	`Set.Nonempty` `Set` `countableGeneratingSet`	—	`Set.mem_insert` `CountablyGenerated.isCountablyGenerated`
`sUnion_countablePartition` 📖	mathematical	—	`Set.sUnion` `countablePartition` `Set.univ`	—	`sUnion_memPartition` `countable_countableGeneratingSet`
`separatesPoints_def` 📖	—	`Set` `Set.instMembership`	—	—	`SeparatesPoints.separates`
`separatesPoints_iff` 📖	mathematical	—	`SeparatesPoints`	—	`SeparatesPoints.separates` `not_imp_not` `MeasurableSet.compl`
`separatesPoints_of_measurableSingletonClass` 📖	mathematical	—	`SeparatesPoints`	—	`MeasurableSet.singleton`
`separating_of_generateFrom` 📖	—	`Set` `Set.instMembership`	—	—	`separatesPoints_def` `forall_generateFrom_mem_iff_mem_iff`

MeasurableSpace.CountableOrCountablyGenerated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`countableOrCountablyGenerated` 📖	mathematical	—	`Countable` `MeasurableSpace.CountablyGenerated`	—	—

MeasurableSpace.CountablyGenerated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap` 📖	mathematical	—	`MeasurableSpace.CountablyGenerated` `MeasurableSpace.comap`	—	`MeasurableSpace.comap_generateFrom` `Set.Countable.image`
`isCountablyGenerated` 📖	mathematical	—	`Set.Countable` `Set` `MeasurableSpace.generateFrom`	—	—
`sup` 📖	mathematical	—	`MeasurableSpace.CountablyGenerated` `MeasurableSpace` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `MeasurableSpace.instCompleteLattice`	—	`Set.Countable.union` `MeasurableSpace.generateFrom_sup_generateFrom`

MeasurableSpace.CountablySeparated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`countably_separated` 📖	mathematical	—	`HasCountableSeparatingOn` `MeasurableSet` `Set.univ`	—	—
`mono` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE`	`MeasurableSpace.CountablySeparated`	—	—
`subtype_iff` 📖	mathematical	—	`MeasurableSpace.CountablySeparated` `Set.Elem` `Subtype.instMeasurableSpace` `Set` `Set.instMembership` `HasCountableSeparatingOn` `MeasurableSet`	—	`MeasurableSpace.countablySeparated_def` `HasCountableSeparatingOn.subtype_iff`

MeasurableSpace.MeasurableSingletonClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_separatesPoints` 📖	mathematical	—	`MeasurableSingletonClass`	—	`Set.ext` `eq_or_ne` `MeasurableSet.iInter` `Prop.countable` `MeasurableSpace.exists_measurableSet_of_ne`

MeasurableSpace.SeparatesPoints

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mono` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE`	`MeasurableSpace.SeparatesPoints`	—	`separates`
`separates` 📖	—	`Set` `Set.instMembership`	—	—	—

MeasurableSpace.Subtype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`countablySeparated` 📖	mathematical	—	`MeasurableSpace.CountablySeparated` `Set.Elem` `Subtype.instMeasurableSpace` `Set` `Set.instMembership`	—	`MeasurableSpace.CountablySeparated.subtype_iff` `HasCountableSeparatingOn.mono` `MeasurableSpace.CountablySeparated.countably_separated` `Set.subset_univ`
`separatesPoints` 📖	mathematical	—	`MeasurableSpace.SeparatesPoints` `Set.Elem` `Subtype.instMeasurableSpace` `Set` `Set.instMembership`	—	`Subtype.val_injective` `MeasurableSpace.SeparatesPoints.separates` `measurable_subtype_coe`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_const_of_measurable_bot` 📖	—	`Measurable` `Bot.bot` `MeasurableSpace` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `MeasurableSpace.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	—	`MeasurableSpace.exists_measurableSet_of_ne` `MeasurableSpace.measurableSet_bot_iff` `isEmpty_or_nonempty`

---

← Back to Index