Basic

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

Statistics

Metric	Count
Definitions AnalyticSet, MeasurablySeparable, measurableEquiv, borelSchroederBernstein, measurableEquivNatBoolOfNotCountable, measurableEquivOfNotCountable, StandardBorelSpace, UpgradedStandardBorel, toMeasurableSpace, toTopologicalSpace, upgradeStandardBorel	11
Theorems borelSpace, map_borel_eq, map_eq_borel, measurableEmbedding, measurableEmbedding, borelSpace, analyticSet, measurableSet_image_of_continuousOn_injOn, analyticSet_image, borelSpace_codomain, exists_continuous, map_measurableSpace_eq, map_measurableSpace_eq_borel, measurableEmbedding, measurableSet_preimage_iff_inter_range, measurableSet_preimage_iff_of_surjective, measurableSet_preimage_iff_preimage_val, measurable_comp_iff_of_surjective, measurable_comp_iff_restrict, analyticSet, analyticSet_image, image_of_antitoneOn, image_of_continuousOn_injOn, image_of_measurable_injOn, image_of_monotoneOn, image_of_monotoneOn_of_continuousOn, isClopenable, isClopenable', standardBorel, iInter, iUnion, image_of_continuous, image_of_continuousOn, measurableSet_of_compl, measurablySeparable, preimage, AnalyticSet_def, iUnion, analyticSet_empty, analyticSet_iff_exists_polishSpace_range, analyticSet_range_of_polishSpace, borel_eq_borel_of_le, isClopenable_iff_measurableSet, measurableSet_exists_tendsto, measurableSet_range_of_continuous_injective, measurableSet_tendsto_fun, measurablySeparable_range_of_disjoint, borelSpace, borelSpace, borelSpace, pi_countable, polish, prod, toBorelSpace, toPolishSpace, countablyGenerated_of_standardBorel, eq_borel_upgradeStandardBorel, measurableSingleton_of_standardBorel, standardBorelSpace_of_discreteMeasurableSpace, standardBorel_of_polish	60
Total	71

AddCosetSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
borelSpace 📖	mathematical	—	BorelSpace HasQuotient.Quotient AddSubgroup QuotientAddGroup.instHasQuotientAddSubgroup QuotientAddGroup.instTopologicalSpace QuotientAddGroup.measurableSpace	—	Quotient.borelSpace T1Space.t0Space T2Space.t1Space

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_borel_eq 📖	mathematical	Continuous	MeasurableSpace.map borel	—	map_eq_borel
map_eq_borel 📖	mathematical	Continuous	MeasurableSpace.map borel	—	Measurable.map_measurableSpace_eq standardBorel_of_polish MeasurableSpace.countablySeparated_of_separatesPoints BorelSpace.countablyGenerated separatesPointsOfOpensMeasurableSpaceOfT0Space BorelSpace.opensMeasurable measurable
measurableEmbedding 📖	mathematical	Continuous	MeasurableEmbedding	—	measurable BorelSpace.opensMeasurable MeasurableSet.image_of_continuousOn_injOn continuousOn Function.Injective.injOn

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurableEmbedding 📖	mathematical	MeasurableSet ContinuousOn Set.InjOn	MeasurableEmbedding Set.Elem Subtype.instMeasurableSpace Set Set.instMembership Set.restrict	—	Set.injOn_iff_injective Continuous.measurable Subtype.opensMeasurableSpace BorelSpace.opensMeasurable continuousOn_iff_continuous_restrict MeasurableEmbedding.measurableSet_image MeasurableEmbedding.subtype_coe MeasurableSet.image_of_continuousOn_injOn mono Subtype.coe_image_subset Set.InjOn.mono Set.image_comp

CosetSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
borelSpace 📖	mathematical	—	BorelSpace HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup QuotientGroup.instTopologicalSpace QuotientGroup.measurableSpace	—	Quotient.borelSpace T1Space.t0Space T2Space.t1Space

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
analyticSet 📖	mathematical	—	MeasureTheory.AnalyticSet	—	Subtype.range_val MeasureTheory.analyticSet_range_of_polishSpace polishSpace continuous_subtype_val
measurableSet_image_of_continuousOn_injOn 📖	mathematical	ContinuousOn Set.InjOn	MeasurableSet Set.image	—	Set.image_eq_range MeasureTheory.measurableSet_range_of_continuous_injective polishSpace continuousOn_iff_continuous_restrict Set.injOn_iff_injective

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
analyticSet_image 📖	mathematical	IsOpen Continuous	MeasureTheory.AnalyticSet Set.image	—	Set.image_eq_range MeasureTheory.analyticSet_range_of_polishSpace polishSpace Continuous.comp continuous_subtype_val

Measurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
borelSpace_codomain 📖	mathematical	Measurable	BorelSpace	—	map_measurableSpace_eq MeasurableSpace.countablySeparated_of_hasCountableSeparatingOn MeasurableSpace.hasCountableSeparatingOn_of_countablySeparated_subtype instCountablySeparatedElemOfHasCountableSeparatingOnIsOpen instHasCountableSeparatingOnIsOpenOfT0SpaceOfSecondCountableTopologyElem Subtype.t0Space TopologicalSpace.Subtype.secondCountableTopology map_measurableSpace_eq_borel
exists_continuous 📖	mathematical	Measurable	TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder Continuous PolishSpace	—	TopologicalSpace.exists_countable_basis MeasurableSet.isClopenable Set.mem_range_self IsOpen.measurableSet Subtype.opensMeasurableSpace TopologicalSpace.IsTopologicalBasis.isOpen PolishSpace.exists_polishSpace_forall_le Set.Countable.to_subtype TopologicalSpace.IsTopologicalBasis.continuous_iff Continuous.comp continuous_subtype_val
map_measurableSpace_eq 📖	mathematical	Measurable	MeasurableSpace.map	—	MeasurableSpace.ext measurableSet_preimage_iff_of_surjective
map_measurableSpace_eq_borel 📖	mathematical	Measurable	MeasurableSpace.map borel	—	mono le_rfl OpensMeasurableSpace.borel_le map_measurableSpace_eq MeasurableSpace.countablySeparated_of_separatesPoints BorelSpace.countablyGenerated separatesPointsOfOpensMeasurableSpaceOfT0Space BorelSpace.opensMeasurable
measurableEmbedding 📖	mathematical	Measurable	MeasurableEmbedding	—	MeasurableSet.image_of_measurable_injOn Function.Injective.injOn
measurableSet_preimage_iff_inter_range 📖	mathematical	Measurable MeasurableSet Set.range	Set.preimage Set Set.instInter	—	measurableSet_preimage_iff_preimage_val Set.inter_comm MeasurableEmbedding.measurableSet_image MeasurableEmbedding.subtype_coe Subtype.image_preimage_coe
measurableSet_preimage_iff_of_surjective 📖	mathematical	Measurable	MeasurableSet Set.preimage	—	exists_opensMeasurableSpace_of_countablySeparated MeasureTheory.AnalyticSet.measurableSet_of_compl T25Space.t2Space T3Space.t25Space T4Space.t3Space Set.image_preimage_eq MeasurableSet.analyticSet_image TopologicalSpace.Subtype.secondCountableTopology MeasurableSet.compl
measurableSet_preimage_iff_preimage_val 📖	mathematical	Measurable	MeasurableSet Set.preimage Set.Elem Set.range Subtype.instMeasurableSpace Set Set.instMembership	—	Set.mem_range_self measurableSet_preimage_iff_of_surjective Set.rangeFactorization_surjective
measurable_comp_iff_of_surjective 📖	—	Measurable	—	—	measurableSet_preimage_iff_of_surjective
measurable_comp_iff_restrict 📖	mathematical	Measurable	Set.Elem Set.range Subtype.instMeasurableSpace Set Set.instMembership Set.restrict	—	measurableSet_preimage_iff_preimage_val

MeasurableSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
analyticSet 📖	mathematical	MeasurableSet	MeasureTheory.AnalyticSet	—	isClopenable IsClosed.analyticSet Set.image_congr Set.image_id' MeasureTheory.AnalyticSet.image_of_continuous continuous_id_of_le
analyticSet_image 📖	mathematical	MeasurableSet Measurable	MeasureTheory.AnalyticSet Set.image	—	Measurable.exists_continuous UpgradedStandardBorel.toPolishSpace UpgradedStandardBorel.toBorelSpace borel_anti MeasureTheory.AnalyticSet.image_of_continuous analyticSet eq_borel_upgradeStandardBorel
image_of_antitoneOn 📖	mathematical	MeasurableSet AntitoneOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set.image	—	image_of_monotoneOn OrderDual.borelSpace instOrderTopologyOrderDual instSecondCountableTopologyOrderDual AntitoneOn.dual_right
image_of_continuousOn_injOn 📖	mathematical	MeasurableSet ContinuousOn Set.InjOn	Set.image	—	isClopenable IsClosed.measurableSet_image_of_continuousOn_injOn ContinuousOn.mono_dom
image_of_measurable_injOn 📖	mathematical	MeasurableSet Measurable Set.InjOn	Set.image	—	exists_opensMeasurableSpace_of_countablySeparated Measurable.exists_continuous UpgradedStandardBorel.toPolishSpace UpgradedStandardBorel.toBorelSpace TopologicalSpace.Subtype.secondCountableTopology Continuous.measurable BorelSpace.opensMeasurable continuous_id_of_le image_of_continuousOn_injOn T25Space.t2Space T3Space.t25Space T4Space.t3Space Continuous.continuousOn
image_of_monotoneOn 📖	mathematical	MeasurableSet MonotoneOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set.image	—	MonotoneOn.countable_not_continuousWithinAt Set.image_union Set.ext Set.sdiff_sep_self union image_of_monotoneOn_of_continuousOn diff Set.Countable.measurableSet instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable PolishSpace.toSecondCountableTopology TopologicalSpace.t2Space_of_metrizableSpace TopologicalSpace.PseudoMetrizableSpace.toMetrizableSpace T3Space.toT0Space T4Space.t3Space T5Space.toT4Space OrderTopology.t5Space TopologicalSpace.IsCompletelyPseudoMetrizableSpace.PseudoMetrizableSpace TopologicalSpace.IsCompletelyMetrizableSpace.toIsCompletelyPseudoMetrizableSpace PolishSpace.toIsCompletelyMetrizableSpace MonotoneOn.mono Set.diff_subset ContinuousWithinAt.mono T25Space.t2Space T3Space.t25Space Set.Countable.image
image_of_monotoneOn_of_continuousOn 📖	mathematical	MeasurableSet MonotoneOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder ContinuousOn	Set.image	—	MonotoneOn.countable_setOf_two_preimages PolishSpace.toSecondCountableTopology Set.ext biUnion Set.OrdConnected.preimage_monotoneOn Set.ordConnected_singleton inter Set.OrdConnected.measurableSet BorelSpace.opensMeasurable OrderTopology.to_orderClosedTopology Set.diff_self_inter Set.diff_union_inter union image_of_continuousOn_injOn T25Space.t2Space T3Space.t25Space T4Space.t3Space T5Space.toT4Space OrderTopology.t5Space diff ContinuousOn.mono Set.diff_subset Mathlib.Tactic.Contrapose.contrapose₁ lt_of_le_of_ne Set.Countable.measurableSet OpensMeasurableSpace.toMeasurableSingletonClass T5Space.toT1Space Set.Countable.mono
isClopenable 📖	mathematical	MeasurableSet	PolishSpace.IsClopenable	—	induction_on_open IsOpen.isClopenable PolishSpace.IsClopenable.compl PolishSpace.IsClopenable.iUnion
isClopenable' 📖	mathematical	MeasurableSet	BorelSpace PolishSpace IsClosed IsOpen	—	isClopenable UpgradedStandardBorel.toPolishSpace UpgradedStandardBorel.toBorelSpace eq_borel_upgradeStandardBorel MeasureTheory.borel_eq_borel_of_le
standardBorel 📖	mathematical	MeasurableSet	StandardBorelSpace Set.Elem Subtype.instMeasurableSpace Set Set.instMembership	—	isClopenable' standardBorel_of_polish Subtype.borelSpace IsClosed.polishSpace

MeasureTheory

Definitions

Name	Category	Theorems
AnalyticSet 📖	MathDef	8 math math: analyticSet_iff_exists_polishSpace_range, MeasurableSet.analyticSet, IsOpen.analyticSet_image, IsClosed.analyticSet, AnalyticSet_def, MeasurableSet.analyticSet_image, analyticSet_range_of_polishSpace, analyticSet_empty
MeasurablySeparable 📖	MathDef	2 math math: measurablySeparable_range_of_disjoint, AnalyticSet.measurablySeparable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
AnalyticSet_def 📖	mathematical	—	AnalyticSet Set Set.instEmptyCollection Continuous Pi.topologicalSpace instTopologicalSpaceNat Set.range	—	—
analyticSet_empty 📖	mathematical	—	AnalyticSet Set Set.instEmptyCollection	—	AnalyticSet_def
analyticSet_iff_exists_polishSpace_range 📖	mathematical	—	AnalyticSet Continuous Set.range	—	AnalyticSet_def instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace Encodable.countable Empty.instIsEmpty PseudoEMetricSpace.pseudoMetrizableSpace TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable DiscreteUniformity.instCompleteSpace DiscreteUniformity.inst EMetric.instIsCountablyGeneratedUniformity T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace continuous_bot Set.range_eq_empty TopologicalSpace.instSeparableSpaceForallOfCountable instCountableNat Pi.complete instIsCountablyGeneratedProdForallUniformityOfCountable Pi.instT0Space analyticSet_range_of_polishSpace
analyticSet_range_of_polishSpace 📖	mathematical	Continuous	AnalyticSet Set.range	—	isEmpty_or_nonempty Set.range_eq_empty analyticSet_empty AnalyticSet_def PolishSpace.exists_nat_nat_continuous_surjective Continuous.comp Function.Surjective.range_comp
borel_eq_borel_of_le 📖	mathematical	TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder	borel	—	le_antisymm Continuous.measurableEmbedding TopologicalSpace.t2Space_of_metrizableSpace TopologicalSpace.IsCompletelyMetrizableSpace.MetrizableSpace PolishSpace.toIsCompletelyMetrizableSpace continuous_id_of_le Set.image_congr Set.image_id' MeasurableEmbedding.measurableSet_image borel_anti
isClopenable_iff_measurableSet 📖	mathematical	—	PolishSpace.IsClopenable MeasurableSet	—	BorelSpace.measurable_eq borel_eq_borel_of_le MeasurableSpace.measurableSet_generateFrom MeasurableSet.isClopenable
measurableSet_exists_tendsto 📖	mathematical	Measurable	MeasurableSet setOf Filter.Tendsto nhds	—	Filter.eq_or_neBot Filter.exists_antitone_basis PolishSpace.toIsCompletelyMetrizableSpace TopologicalSpace.UpgradedIsCompletelyMetrizableSpace.toCompleteSpace Filter.HasAntitoneBasis.prod Filter.HasAntitoneBasis.map Filter.NeBot.map Filter.HasBasis.le_basis_iff Filter.HasAntitoneBasis.toHasBasis Metric.uniformity_basis_dist_inv_nat_succ Set.setOf_forall MeasurableSet.biInter Set.countable_univ instCountableNat Set.setOf_exists MeasurableSet.iUnion Set.prod_image_image_eq Set.iInter_congr_Prop Set.to_countable SetCoe.countable measurableSet_lt BorelSpace.opensMeasurable Real.borelSpace instSecondCountableTopologyReal OrderTopology.to_orderClosedTopology instOrderTopologyReal Measurable.dist PolishSpace.toSecondCountableTopology measurable_const
measurableSet_range_of_continuous_injective 📖	mathematical	Continuous	MeasurableSet Set.range	—	TopologicalSpace.exists_countable_basis PolishSpace.toSecondCountableTopology AnalyticSet.measurablySeparable IsOpen.analyticSet_image TopologicalSpace.IsTopologicalBasis.isOpen Disjoint.image Function.Injective.injOn Set.subset_univ Disjoint.symm exists_seq_strictAnti_tendsto instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace PolishSpace.toIsCompletelyMetrizableSpace Set.Subset.antisymm Set.mem_iInter Nat.instAtLeastTwoHAddOfNat TopologicalSpace.IsTopologicalBasis.mem_nhds_iff Metric.ball_mem_nhds half_pos LE.le.trans Metric.diam_mono Metric.isBounded_ball Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Metric.diam_ball LT.lt.le Set.mem_iUnion Bornology.IsBounded.subset Set.mem_inter subset_closure Set.mem_image_of_mem Set.disjoint_left Set.nonempty_iff_ne_empty Set.not_disjoint_iff_nonempty_inter MulZeroClass.mul_zero Filter.Tendsto.const_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal cauchySeq_of_le_tendsto_0' dist_triangle add_le_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Metric.dist_le_diam_of_mem le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Tactic.Linarith.sub_nonpos_of_le StrictAnti.antitone CauchySeq.tendsto_limUnder TopologicalSpace.UpgradedIsCompletelyMetrizableSpace.toCompleteSpace t2_separation Metric.mem_nhds_iff ContinuousAt.preimage_mem_nhds Continuous.continuousAt IsOpen.mem_nhds Filter.Eventually.exists Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat tendsto_order add_zero Filter.Tendsto.add IsTopologicalSemiring.toContinuousAdd tendsto_iff_dist_tendsto_zero Set.image_subset_iff Set.Subset.trans le_imp_le_of_le_of_le add_le_add_left le_refl closure_mono Disjoint.closure_left Set.mem_range_self MeasurableSet.inter IsClosed.measurableSet isClosed_closure MeasurableSet.iInter Encodable.countable Prop.countable MeasurableSet.diff MeasurableSet.iUnion instCountableNat
measurableSet_tendsto_fun 📖	mathematical	Measurable	MeasurableSet setOf Filter.Tendsto nhds	—	tendsto_iff_dist_tendsto_zero measurableSet_tendsto FirstCountableTopology.nhds_generated_countable TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace nhds_isMeasurablyGenerated BorelSpace.opensMeasurable Real.borelSpace Measurable.dist
measurablySeparable_range_of_disjoint 📖	mathematical	Continuous Pi.topologicalSpace instTopologicalSpaceNat Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.range	MeasurablySeparable	—	Mathlib.Tactic.Contrapose.contrapose₂ Mathlib.Tactic.Push.not_and_eq PiNat.iUnion_cylinder_update Set.image_iUnion MeasurablySeparable.iUnion instCountableNat PiNat.update_mem_cylinder PiNat.cylinder_zero Set.image_univ Function.iterate_succ' Nat.le_induction PiNat.mem_cylinder_iff_eq PiNat.mem_cylinder_iff t2_separation Set.disjoint_iff_forall_ne Set.mem_range_self Metric.mem_nhds_iff ContinuousAt.preimage_mem_nhds Continuous.continuousAt IsOpen.mem_nhds Nat.instAtLeastTwoHAddOfNat exists_pow_lt_of_lt_one Real.instIsStrictOrderedRing Real.instArchimedean AddGroup.existsAddOfLE lt_min Mathlib.Meta.NormNum.isNNRat_lt_true instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.instAtLeastTwo Set.image_subset_iff Set.Subset.trans LE.le.trans_lt PiNat.mem_cylinder_iff_dist_le LT.lt.trans_le min_le_left Disjoint.mono_left min_le_right Disjoint.symm IsOpen.measurableSet

MeasureTheory.AnalyticSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iInter 📖	mathematical	MeasureTheory.AnalyticSet	Set.iInter	—	isClosed_iInter isClosed_eq Continuous.comp continuous_apply continuous_subtype_val Set.Subset.antisymm Set.mem_iInter Set.mem_range_self Set.mem_range MeasureTheory.analyticSet_range_of_polishSpace IsClosed.polishSpace instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.instSeparableSpaceForallOfCountable TopologicalSpace.SecondCountableTopology.to_separableSpace PolishSpace.toSecondCountableTopology TopologicalSpace.IsCompletelyMetrizableSpace.pi_countable PolishSpace.toIsCompletelyMetrizableSpace MeasureTheory.analyticSet_iff_exists_polishSpace_range
iUnion 📖	mathematical	MeasureTheory.AnalyticSet	Set.iUnion	—	continuous_sigma Set.range_sigma_eq_iUnion_range MeasureTheory.analyticSet_range_of_polishSpace instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace TopologicalSpace.instSecondCountableTopologySigmaOfCountable PolishSpace.toSecondCountableTopology TopologicalSpace.IsCompletelyMetrizableSpace.sigma PolishSpace.toIsCompletelyMetrizableSpace MeasureTheory.analyticSet_iff_exists_polishSpace_range
image_of_continuous 📖	mathematical	MeasureTheory.AnalyticSet Continuous	Set.image	—	image_of_continuousOn Continuous.continuousOn
image_of_continuousOn 📖	mathematical	MeasureTheory.AnalyticSet ContinuousOn	Set.image	—	MeasureTheory.analyticSet_iff_exists_polishSpace_range Set.range_comp MeasureTheory.analyticSet_range_of_polishSpace ContinuousOn.comp_continuous Set.mem_range_self
measurableSet_of_compl 📖	mathematical	MeasureTheory.AnalyticSet Compl.compl Set Set.instCompl	MeasurableSet	—	measurablySeparable disjoint_compl_right HasSubset.Subset.antisymm Set.instAntisymmSubset Set.disjoint_compl_left_iff_subset
measurablySeparable 📖	mathematical	MeasureTheory.AnalyticSet Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	MeasureTheory.MeasurablySeparable	—	MeasureTheory.AnalyticSet_def Set.Subset.refl MeasurableSet.empty Set.subset_univ MeasurableSet.univ MeasureTheory.measurablySeparable_range_of_disjoint
preimage 📖	mathematical	MeasureTheory.AnalyticSet Continuous	Set.preimage	—	MeasureTheory.analyticSet_iff_exists_polishSpace_range isClosed_eq Continuous.fst' Continuous.snd' Set.ext image_of_continuous IsClosed.analyticSet instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.instSeparableSpaceProd TopologicalSpace.SecondCountableTopology.to_separableSpace PolishSpace.toSecondCountableTopology TopologicalSpace.IsCompletelyMetrizableSpace.prod PolishSpace.toIsCompletelyMetrizableSpace continuous_fst

MeasureTheory.MeasurablySeparable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iUnion 📖	mathematical	MeasureTheory.MeasurablySeparable	Set.iUnion	—	Set.iUnion_subset Set.subset_iUnion_of_subset Set.subset_iInter Disjoint.mono_right Set.iInter_subset MeasurableSet.iUnion MeasurableSet.iInter

PolishSpace

Definitions

Name	Category	Theorems
borelSchroederBernstein 📖	CompOp	—
measurableEquivNatBoolOfNotCountable 📖	CompOp	—
measurableEquivOfNotCountable 📖	CompOp	—

PolishSpace.Equiv

Definitions

Name	Category	Theorems
measurableEquiv 📖	CompOp	—

Quotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
borelSpace 📖	mathematical	—	BorelSpace instTopologicalSpaceQuotient instMeasurableSpace	—	Continuous.map_eq_borel continuous_quotient_mk' mk'_surjective

QuotientAddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
borelSpace 📖	mathematical	—	BorelSpace HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup instTopologicalSpace measurableSpace	—	Continuous.map_eq_borel T3Space.toT0Space instT3Space instSecondCountableTopology IsTopologicalAddGroup.toContinuousAdd PolishSpace.toSecondCountableTopology mk_surjective

QuotientGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
borelSpace 📖	mathematical	—	BorelSpace HasQuotient.Quotient Subgroup instHasQuotientSubgroup instTopologicalSpace measurableSpace	—	Continuous.map_eq_borel T3Space.toT0Space instT3Space instSecondCountableTopology IsTopologicalGroup.toContinuousMul PolishSpace.toSecondCountableTopology mk_surjective

StandardBorelSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pi_countable 📖	mathematical	StandardBorelSpace	MeasurableSpace.pi	—	standardBorel_of_polish Pi.borelSpace PolishSpace.toSecondCountableTopology UpgradedStandardBorel.toPolishSpace UpgradedStandardBorel.toBorelSpace instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.instSeparableSpaceForallOfCountable TopologicalSpace.SecondCountableTopology.to_separableSpace TopologicalSpace.IsCompletelyMetrizableSpace.pi_countable PolishSpace.toIsCompletelyMetrizableSpace
polish 📖	mathematical	—	BorelSpace PolishSpace	—	—
prod 📖	mathematical	—	StandardBorelSpace Prod.instMeasurableSpace	—	standardBorel_of_polish Prod.borelSpace UpgradedStandardBorel.toBorelSpace secondCountableTopologyEither_of_right PolishSpace.toSecondCountableTopology UpgradedStandardBorel.toPolishSpace instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.instSeparableSpaceProd TopologicalSpace.SecondCountableTopology.to_separableSpace TopologicalSpace.IsCompletelyMetrizableSpace.prod PolishSpace.toIsCompletelyMetrizableSpace

UpgradedStandardBorel

Definitions

Name	Category	Theorems
toMeasurableSpace 📖	CompOp	1 math math: toBorelSpace
toTopologicalSpace 📖	CompOp	3 math math: toBorelSpace, toPolishSpace, eq_borel_upgradeStandardBorel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toBorelSpace 📖	mathematical	—	BorelSpace toTopologicalSpace toMeasurableSpace	—	—
toPolishSpace 📖	mathematical	—	PolishSpace toTopologicalSpace	—	—

(root)

Definitions

Name	Category	Theorems
StandardBorelSpace 📖	CompData	4 math math: MeasurableSet.standardBorel, standardBorelSpace_of_discreteMeasurableSpace, StandardBorelSpace.prod, standardBorel_of_polish
UpgradedStandardBorel 📖	CompData	—
upgradeStandardBorel 📖	CompOp	1 math math: eq_borel_upgradeStandardBorel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
countablyGenerated_of_standardBorel 📖	mathematical	—	MeasurableSpace.CountablyGenerated	—	BorelSpace.countablyGenerated UpgradedStandardBorel.toBorelSpace PolishSpace.toSecondCountableTopology UpgradedStandardBorel.toPolishSpace
eq_borel_upgradeStandardBorel 📖	mathematical	—	borel UpgradedStandardBorel.toTopologicalSpace upgradeStandardBorel	—	BorelSpace.measurable_eq UpgradedStandardBorel.toBorelSpace
measurableSingleton_of_standardBorel 📖	mathematical	—	MeasurableSingletonClass	—	instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable UpgradedStandardBorel.toBorelSpace PolishSpace.toSecondCountableTopology UpgradedStandardBorel.toPolishSpace TopologicalSpace.t2Space_of_metrizableSpace TopologicalSpace.IsCompletelyMetrizableSpace.MetrizableSpace PolishSpace.toIsCompletelyMetrizableSpace
standardBorelSpace_of_discreteMeasurableSpace 📖	mathematical	—	StandardBorelSpace	—	standardBorel_of_polish DiscreteMeasurableSpace.toBorelSpace instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace TopologicalSpace.DiscreteTopology.metrizableSpace TopologicalSpace.IsCompletelyMetrizableSpace.discrete
standardBorel_of_polish 📖	mathematical	—	StandardBorelSpace	—	—

---

← Back to Index