Documentation Verification Report

EmbeddingReal

📁 Source: Mathlib/MeasureTheory/Constructions/Polish/EmbeddingReal.lean

Statistics

Metric	Count
Definitions `embeddingReal`	1
Theorems `exists_measurableEmbedding_real`, `exists_nat_measurableEquiv_range_coe_fin_of_finite`, `exists_subset_real_measurableEquiv`, `measurableEmbedding_embeddingReal`, `measurableEquiv_range_coe_nat_of_infinite_of_countable`, `measurable_embeddingReal`	6
Total	7

MeasureTheory

Definitions

Name	Category	Theorems
`embeddingReal` 📖	CompOp	5 math math: `ProbabilityTheory.Kernel.borelMarkovFromReal_apply'`, `measurableEmbedding_embeddingReal`, `measurableEmbedding_sigmoid_comp_embeddingReal`, `ProbabilityTheory.Kernel.borelMarkovFromReal_apply`, `measurable_embeddingReal`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_measurableEmbedding_real` 📖	mathematical	—	`MeasurableEmbedding` `Real` `Real.measurableSpace`	—	`exists_subset_real_measurableEquiv` `MeasurableEmbedding.comp` `MeasurableEmbedding.subtype_coe` `MeasurableEquiv.measurableEmbedding`
`exists_nat_measurableEquiv_range_coe_fin_of_finite` 📖	mathematical	—	`MeasurableEquiv` `Set.Elem` `Real` `Set.range` `Real.instNatCast` `Subtype.instMeasurableSpace` `Set` `Set.instMembership` `Real.measurableSpace`	—	`Finite.exists_equiv_fin` `standardBorelSpace_of_discreteMeasurableSpace` `MeasurableSingletonClass.toDiscreteMeasurableSpace` `Subtype.instMeasurableSingletonClass` `instMeasurableSingletonClassOfMeasurableEq` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `BorelSpace.opensMeasurable` `Real.borelSpace` `instSecondCountableTopologyReal` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Finite.to_countable` `Finite.Set.finite_range` `Finite.of_fintype` `Nat.cast_injective` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Fin.val_injective`
`exists_subset_real_measurableEquiv` 📖	mathematical	—	`MeasurableSet` `Real` `Real.measurableSpace` `MeasurableEquiv` `Set.Elem` `Subtype.instMeasurableSpace` `Set` `Set.instMembership`	—	`finite_or_infinite` `exists_nat_measurableEquiv_range_coe_fin_of_finite` `MeasurableEmbedding.measurableSet_range` `Continuous.measurableEmbedding` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Real.borelSpace` `instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `Countable.LindelofSpace` `instCountableFin` `TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace` `TopologicalSpace.DiscreteTopology.metrizableSpace` `instDiscreteTopologyFin` `TopologicalSpace.IsCompletelyMetrizableSpace.discrete` `continuous_of_discreteTopology` `Nat.cast_injective` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Fin.val_injective` `instCountableNat` `PseudoEMetricSpace.pseudoMetrizableSpace` `TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable` `DiscreteUniformity.instCompleteSpace` `DiscreteUniformity.inst` `EMetric.instIsCountablyGeneratedUniformity` `T6Space.toT0Space` `instT6SpaceOfMetrizableSpace` `Nat.borelSpace` `instDiscreteTopologyNat` `measurableEquiv_range_coe_nat_of_infinite_of_countable` `MeasurableSet.univ` `standardBorel_of_polish` `Subtype.borelSpace` `separableSpace_univ` `instSecondCountableTopologyReal` `TopologicalSpace.IsCompletelyMetrizableSpace.univ` `Real.instCompleteSpace` `Set.countable_coe_iff` `Cardinal.not_countable_real`
`measurableEmbedding_embeddingReal` 📖	mathematical	—	`MeasurableEmbedding` `Real` `Real.measurableSpace` `embeddingReal`	—	`exists_measurableEmbedding_real`
`measurableEquiv_range_coe_nat_of_infinite_of_countable` 📖	mathematical	—	`MeasurableEquiv` `Set.Elem` `Real` `Set.range` `Real.instNatCast` `Subtype.instMeasurableSpace` `Set` `Set.instMembership` `Real.measurableSpace`	—	`IsClosed.polishSpace` `instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instSecondCountableTopologyReal` `TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable` `Real.instCompleteSpace` `EMetric.instIsCountablyGeneratedUniformity` `T6Space.toT0Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `IsClosedMap.isClosed_range` `Topology.IsClosedEmbedding.isClosedMap` `Nat.isClosedEmbedding_coe_real` `standardBorel_of_polish` `Subtype.borelSpace` `Real.borelSpace` `nonempty_equiv_of_countable` `instCountableNat` `instInfiniteNat` `Nat.cast_injective` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing`
`measurable_embeddingReal` 📖	mathematical	—	`Measurable` `Real` `Real.measurableSpace` `embeddingReal`	—	`MeasurableEmbedding.measurable` `measurableEmbedding_embeddingReal`

---

← Back to Index