Basic

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

Statistics

Metric	Count
Definitions BorelSpace, measurableSpace, measurableSpace, toMeasurableEquiv, addBorelInstance, borelToRefl, tacticBorelize___, measurableSpace, OpensMeasurableSpace, measurableSpace, SecondCountableTopologyEither, borel	12
Theorems borelSpace, countablyGenerated, measurable_eq, opensMeasurable, aemeasurable, aemeasurable2, borel_measurable, measurable, measurable2, measurableAdd, measurableMul₂, toMeasurableConstSMul, toMeasurableConstVAdd, measurableInv, measurableInv, measurable, measurableMul, measurableMul₂, measurableNeg, measurable_piecewise, measurableSMul₂, toMeasurableSMul, measurableSub, measurableSub₂, toMeasurableVAdd, instBorelSpace, toBorelSpace, borelSpace, borelSpace, borelSpace, measurableInv, measurable, measurableEmbedding, toMeasurableEquiv_coe, toMeasurableEquiv_symm_coe, mem_measurableSet_iff, borelSpace, measurableSet, nullMeasurableSet, measurable, closure_subset_measurableSet, measurableSet, measure_closure, nullMeasurableSet, measurableSet, measurableSet, nullMeasurableSet, borelSpace, induction_on_open, nhdsWithin_isMeasurablyGenerated, comap, map, borelSpace, borelSpace, borel_le, separatesPoints, toMeasurableSingletonClass, borelSpace, opensMeasurableSpace, borelSpace, borelSpace_of_subsingleton, opensMeasurableSpace, opensMeasurableSpace_of_subsingleton, borelSpace, opensMeasurableSpace, borelSpace, borelSpace, out, borelSpace, opensMeasurableSpace, borel_eq_generateFrom, measurableEmbedding, measurableEmbedding, measurableEmbedding, instBorelSpace, borelSpace, borel_anti, borel_comap, borel_eq_generateFrom_isClosed, borel_eq_generateFrom_of_subbasis, borel_eq_top_of_countable, borel_eq_top_of_discrete, closure_ae_eq_of_null_frontier, instCountablySeparatedElemOfHasCountableSeparatingOnIsOpen, instMeasurableEqOfSecondCountableTopologyOfT2Space, interior_ae_eq_of_null_frontier, isPiSystem_isClosed, isPiSystem_isOpen, measurableSet_closure, measurableSet_frontier, measurableSet_interior, measurableSet_of_continuousAt, measurable_of_continuousOn_compl_singleton, measurable_of_isClosed, measurable_of_isClosed', measurable_of_isOpen, measure_closure_of_null_frontier, measure_interior_of_null_frontier, nhds_isMeasurablyGenerated, nullMeasurableSet_of_null_frontier, null_frontier_inter, opensMeasurableSpace_iff_forall_measurableSet, pi_le_borel_pi, prod_le_borel_prod, secondCountableTopologyEither_of_left, secondCountableTopologyEither_of_right, separatesPointsOfOpensMeasurableSpaceOfT0Space	107
Total	119

Bool

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
borelSpace 📖	mathematical	—	BorelSpace instTopologicalSpaceBool instMeasurableSpace	—	borel_eq_top_of_discrete instDiscreteTopologyBool

BorelSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
countablyGenerated 📖	mathematical	—	MeasurableSpace.CountablyGenerated	—	TopologicalSpace.exists_countable_basis measurable_eq TopologicalSpace.IsTopologicalBasis.borel_eq_generateFrom
measurable_eq 📖	mathematical	—	borel	—	—
opensMeasurable 📖	mathematical	—	OpensMeasurableSpace	—	ge_of_eq measurable_eq

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aemeasurable 📖	mathematical	Continuous	AEMeasurable	—	Measurable.aemeasurable measurable
aemeasurable2 📖	—	Continuous instTopologicalSpaceProd AEMeasurable	—	—	Measurable.comp_aemeasurable measurable Prod.opensMeasurableSpace AEMeasurable.prodMk
borel_measurable 📖	mathematical	Continuous	Measurable borel	—	Measurable.of_le_map MeasurableSpace.generateFrom_le IsOpen.preimage
measurable 📖	mathematical	Continuous	Measurable	—	Measurable.mono borel_measurable OpensMeasurableSpace.borel_le le_of_eq BorelSpace.measurable_eq
measurable2 📖	—	Continuous instTopologicalSpaceProd Measurable	—	—	Measurable.comp measurable Prod.opensMeasurableSpace Measurable.prodMk

ContinuousAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurableAdd 📖	mathematical	—	MeasurableAdd	—	Continuous.measurable BorelSpace.opensMeasurable Continuous.comp' Continuous.fun_add Continuous.fst continuous_id' Continuous.snd Continuous.prodMk continuous_const
measurableMul₂ 📖	mathematical	—	MeasurableAdd₂	—	Continuous.measurable Prod.opensMeasurableSpace BorelSpace.opensMeasurable secondCountableTopologyEither_of_right continuous_add

ContinuousConstSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toMeasurableConstSMul 📖	mathematical	—	MeasurableConstSMul	—	Continuous.measurable BorelSpace.opensMeasurable Continuous.const_smul continuous_id'

ContinuousConstVAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toMeasurableConstVAdd 📖	mathematical	—	MeasurableConstVAdd	—	Continuous.measurable BorelSpace.opensMeasurable Continuous.const_vadd continuous_id'

ContinuousInv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurableInv 📖	mathematical	—	MeasurableInv	—	Continuous.measurable BorelSpace.opensMeasurable continuous_inv

ContinuousInv₀

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurableInv 📖	mathematical	—	MeasurableInv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	measurable_of_continuousOn_compl_singleton BorelSpace.opensMeasurable continuousOn_inv₀

ContinuousMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurable 📖	mathematical	—	Measurable DFunLike.coe ContinuousMap instFunLike	—	Continuous.measurable continuous

ContinuousMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurableMul 📖	mathematical	—	MeasurableMul	—	Continuous.measurable BorelSpace.opensMeasurable Continuous.comp' Continuous.fun_mul Continuous.fst continuous_id' Continuous.snd Continuous.prodMk continuous_const
measurableMul₂ 📖	mathematical	—	MeasurableMul₂	—	Continuous.measurable Prod.opensMeasurableSpace BorelSpace.opensMeasurable secondCountableTopologyEither_of_right continuous_mul

ContinuousNeg

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurableNeg 📖	mathematical	—	MeasurableNeg	—	Continuous.measurable BorelSpace.opensMeasurable continuous_neg

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurable_piecewise 📖	mathematical	ContinuousOn Compl.compl Set Set.instCompl MeasurableSet	Measurable Set.piecewise	—	measurable_of_isOpen Set.piecewise_preimage Set.ite.eq_1 MeasurableSet.union continuousOn_iff' MeasurableSet.inter IsOpen.measurableSet Set.diff_eq_compl_inter Set.inter_comm MeasurableSet.compl

ContinuousSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurableSMul₂ 📖	mathematical	—	MeasurableSMul₂	—	Continuous.measurable Prod.opensMeasurableSpace BorelSpace.opensMeasurable continuous_smul
toMeasurableSMul 📖	mathematical	—	MeasurableSMul	—	ContinuousConstSMul.toMeasurableConstSMul continuousConstSMul Continuous.measurable Continuous.smul continuous_id' continuous_const

ContinuousSub

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurableSub 📖	mathematical	—	MeasurableSub	—	Continuous.measurable BorelSpace.opensMeasurable Continuous.sub continuous_const continuous_id'
measurableSub₂ 📖	mathematical	—	MeasurableSub₂	—	Continuous.measurable Prod.opensMeasurableSpace BorelSpace.opensMeasurable secondCountableTopologyEither_of_right continuous_sub

ContinuousVAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toMeasurableVAdd 📖	mathematical	—	MeasurableVAdd	—	ContinuousConstVAdd.toMeasurableConstVAdd continuousConstVAdd Continuous.measurable Continuous.vadd continuous_id' continuous_const

Countable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instBorelSpace 📖	mathematical	—	BorelSpace	—	Set.Countable.measurableSet Set.to_countable SetCoe.countable MeasurableSpace.measurableSet_generateFrom isOpen_discrete MeasurableSpace.ext

DiscreteMeasurableSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toBorelSpace 📖	mathematical	—	BorelSpace	—	MeasurableSpace.ext

ENNReal

Definitions

Name	Category	Theorems
measurableSpace 📖	CompOp	91 math math: MeasureTheory.aemeasurable_withDensity_ennreal_iff', measurable_ereal_toENNReal, EReal.measurable_exp, MeasureTheory.Measure.measurable_measure, Measurable.ennreal_ofReal, MeasureTheory.Measure.measurable_coe, hasMeasurablePow, MeasureTheory.measurable_measure_add_right, AEMeasurable.enorm, ProbabilityTheory.Kernel.measurable_densityProcess_countableFiltration_aux, ProbabilityTheory.Kernel.measurable_singularPart_fun_right, measurable_edist_right, measurable_toNNReal, Measurable.coe_nnreal_ennreal, ProbabilityTheory.measurable_condDistrib, MeasureTheory.measurable_measure_mul_right, instMeasurableInv, measurable_infEDist, MeasureTheory.Measure.singularPart_def, ProbabilityTheory.IdentDistrib.coe_nnreal_ennreal, MeasureTheory.StronglyMeasurable.enorm, measurable_toReal, Measurable.infEdist, ProbabilityTheory.measurable_gaussianPDF, MeasureTheory.aemeasurable_ofReal_abs_det_fderivWithin, MeasureTheory.measurable_pdf, MeasureTheory.exists_measurable_le_forall_setLIntegral_eq, ProbabilityTheory.Kernel.measurable_rnDeriv, measurable_infEdist, AEMeasurable.edist, instMeasurableMul₂, AEMeasurable.coe_nnreal_ennreal, MeasureTheory.StronglyAdapted.measurable_upcrossings, ProbabilityTheory.IsKolmogorovProcess.measurable_edist, MeasureTheory.iSup_lintegral_measurable_le_eq_lintegral, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left', ProbabilityTheory.measurable_preCDF, ProbabilityTheory.Kernel.measurable_lintegral_indicator_const, ProbabilityTheory.Kernel.measurable_singularPart_fun, measurable_measure_prodMk_left_finite, MeasureTheory.Measure.HaveLebesgueDecomposition.lebesgue_decomposition, VitaliFamily.limRatioMeas_measurable, measurable_of_measurable_nnreal_prod, measurable_of_measurable_nnreal_nnreal, ProbabilityTheory.Kernel.measurable_rnDeriv_right, measurable_coe_ennreal_ereal, aemeasurable_of_exist_almost_disjoint_supersets, Measurable.enorm, MeasureTheory.Measure.rnDeriv_def, ProbabilityTheory.Kernel.measurable_densityProcess_aux, measurable_edist_left, measurable_measure_prodMk_left, AEMeasurable.ereal_toENNReal, NNReal.instMeasurableSMul₂ENNReal, ProbabilityTheory.measurable_condExpKernel, measurable_log, measurable_enorm, instMeasurableSub₂, MeasureTheory.measurable_condLExp', MeasureTheory.measurable_condLExp, measurable_measure_prodMk_right, MeasureTheory.aemeasurable_withDensity_ennreal_iff, measurable_ofReal, measurable_of_measurable_nnreal, borelSpace, Measurable.edist, MeasureTheory.AEStronglyMeasurable.enorm, BoundedContinuousFunction.measurable_coe_ennreal_comp, ProbabilityTheory.Kernel.measurable_coe, AEMeasurable.ennreal_ofReal, MeasureTheory.exists_measurable_le_lintegral_eq, MeasureTheory.condLExp_def, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left_of_finite, ProbabilityTheory.IsAEKolmogorovProcess.aemeasurable_edist, MeasureTheory.exists_measurable_le_setLIntegral_eq_of_integrable, measurable_edist, ProbabilityTheory.Kernel.measurable_kernel_prodMk_right, MeasureTheory.Measure.measurable_rnDeriv, instMeasurableSMulNNReal, MeasureTheory.exists_measurable_le_withDensity_eq, Probability.measurable_cauchyPDF, measurable_coe_nnreal_ennreal, aemeasurable_coe_nnreal_ennreal_iff, MeasureTheory.AEStronglyMeasurable.edist, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left, MeasureTheory.Measure.haveLebesgueDecomposition_spec, Measurable.infEDist, VitaliFamily.aemeasurable_limRatio, measurable_coe_nnreal_ennreal_iff, Measurable.ereal_toENNReal, Measurable.ereal_exp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
borelSpace 📖	mathematical	—	BorelSpace ENNReal instTopologicalSpace measurableSpace	—	—

EReal

Definitions

Name	Category	Theorems
measurableSpace 📖	CompOp	18 math math: instMeasurableMul₂, measurable_ereal_toENNReal, measurable_exp, measurable_ereal_toReal, instMeasurableAdd₂, measurable_of_measurable_real, Measurable.coe_ereal_ennreal, Measurable.ennreal_log, measurable_coe_ennreal_ereal, measurable_of_real_prod, borelSpace, ENNReal.measurable_log, measurable_coe_real_ereal, AEMeasurable.coe_ereal_ennreal, measurableEmbedding_coe, Measurable.coe_real_ereal, AEMeasurable.coe_real_ereal, measurable_of_real_real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
borelSpace 📖	mathematical	—	BorelSpace EReal instTopologicalSpace measurableSpace	—	—

Empty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
borelSpace 📖	mathematical	—	BorelSpace instTopologicalSpaceEmpty instMeasurableSpace	—	borel_eq_top_of_discrete instDiscreteTopologyEmpty

HasContinuousInv₀

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurableInv 📖	mathematical	—	MeasurableInv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	ContinuousInv₀.measurableInv

Homeomorph

Definitions

Name	Category	Theorems
toMeasurableEquiv 📖	CompOp	2 math math: toMeasurableEquiv_symm_coe, toMeasurableEquiv_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurable 📖	mathematical	—	Measurable DFunLike.coe Homeomorph EquivLike.toFunLike instEquivLike	—	Continuous.measurable continuous
measurableEmbedding 📖	mathematical	—	MeasurableEmbedding DFunLike.coe Homeomorph EquivLike.toFunLike instEquivLike	—	MeasurableEquiv.measurableEmbedding
toMeasurableEquiv_coe 📖	mathematical	—	DFunLike.coe MeasurableEquiv EquivLike.toFunLike MeasurableEquiv.instEquivLike toMeasurableEquiv Homeomorph instEquivLike	—	—
toMeasurableEquiv_symm_coe 📖	mathematical	—	DFunLike.coe MeasurableEquiv EquivLike.toFunLike MeasurableEquiv.instEquivLike MeasurableEquiv.symm toMeasurableEquiv Homeomorph instEquivLike symm	—	—

Inseparable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_measurableSet_iff 📖	mathematical	Inseparable MeasurableSet	Set Set.instMembership	—	MeasurableSet.induction_on_open mem_open_iff Iff.not

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
borelSpace 📖	mathematical	—	BorelSpace instTopologicalSpaceInt instMeasurableSpace	—	borel_eq_top_of_discrete instDiscreteTopologyInt

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurableSet 📖	mathematical	—	MeasurableSet	—	MeasurableSet.of_compl IsOpen.measurableSet isOpen_compl
nullMeasurableSet 📖	mathematical	—	MeasureTheory.NullMeasurableSet	—	MeasurableSet.nullMeasurableSet measurableSet

IsClosedEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurable 📖	mathematical	Topology.IsClosedEmbedding	Measurable	—	Continuous.measurable Topology.IsClosedEmbedding.continuous

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_subset_measurableSet 📖	mathematical	IsCompact MeasurableSet Set Set.instHasSubset	closure	—	closure_eq_biUnion_inseparable Set.iUnion₂_subset_iff Inseparable.mem_measurableSet_iff
measurableSet 📖	mathematical	IsCompact	MeasurableSet	—	IsClosed.measurableSet isClosed
measure_closure 📖	mathematical	IsCompact	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike closure	—	le_antisymm MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass closure_subset_measurableSet MeasureTheory.measurableSet_toMeasurable MeasureTheory.subset_toMeasurable MeasureTheory.measure_toMeasurable subset_closure
nullMeasurableSet 📖	mathematical	IsCompact	MeasureTheory.NullMeasurableSet	—	IsClosed.nullMeasurableSet isClosed

IsGδ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurableSet 📖	mathematical	IsGδ	MeasurableSet	—	MeasurableSet.sInter IsOpen.measurableSet

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurableSet 📖	mathematical	IsOpen	MeasurableSet	—	OpensMeasurableSpace.borel_le
nullMeasurableSet 📖	mathematical	IsOpen	MeasureTheory.NullMeasurableSet	—	MeasurableSet.nullMeasurableSet measurableSet

Mathlib.Tactic.Borelize

Definitions

Name	Category	Theorems
addBorelInstance 📖	CompOp	—
borelToRefl 📖	CompOp	—
tacticBorelize___ 📖	CompOp	—

MeasurableEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
borelSpace 📖	mathematical	MeasurableEmbedding Topology.IsInducing	BorelSpace	—	BorelSpace.measurable_eq comap_eq borel_comap Topology.IsInducing.eq_induced

MeasurableSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
induction_on_open 📖	—	IsOpen.measurableSet BorelSpace.opensMeasurable Compl.compl Set Set.instCompl compl Set.iUnion iUnion instCountableNat MeasurableSet	—	—	IsOpen.measurableSet BorelSpace.opensMeasurable compl iUnion instCountableNat MeasurableSpace.induction_on_inter BorelSpace.measurable_eq isPiSystem_isOpen isOpen_empty
nhdsWithin_isMeasurablyGenerated 📖	mathematical	MeasurableSet	Filter.IsMeasurablyGenerated nhdsWithin	—	Filter.inf_isMeasurablyGenerated nhds_isMeasurablyGenerated principal_isMeasurablyGenerated

MeasureTheory.Measure.IsFiniteMeasureOnCompacts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap 📖	mathematical	—	MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.Measure.comap DFunLike.coe Homeomorph EquivLike.toFunLike Homeomorph.instEquivLike	—	MeasureTheory.IsFiniteMeasureOnCompacts.comap' Homeomorph.continuous Homeomorph.measurableEmbedding
map 📖	mathematical	—	MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.Measure.map DFunLike.coe Homeomorph EquivLike.toFunLike Homeomorph.instEquivLike	—	Homeomorph.toMeasurableEquiv_coe MeasurableEquiv.map_apply IsCompact.measure_lt_top Homeomorph.isCompact_preimage

NNReal

Definitions

Name	Category	Theorems
measurableSpace 📖	CompOp	26 math math: AEMeasurable.ennreal_toNNReal, Measurable.ennreal_toNNReal, aemeasurable_coe_nnreal_real_iff, ENNReal.measurable_toNNReal, AEMeasurable.real_toNNReal, measurable_real_toNNReal, ProbabilityTheory.IdentDistrib.nnnorm, Measurable.nnnorm, Measurable.real_toNNReal, instMeasurableSMul₂ENNReal, measurable_coe_nnreal_real, AEMeasurable.nnnorm, hasMeasurablePow, borelSpace, MeasureTheory.aemeasurable_toNNReal_abs_det_fderivWithin, measurable_nndist, measurable_infNndist, ENNReal.instMeasurableSMulNNReal, Measurable.nndist, measurable_coe_nnreal_ennreal, aemeasurable_coe_nnreal_ennreal_iff, measurable_coe_nnreal_real_iff, measurable_coe_nnreal_ennreal_iff, Measurable.infNndist, MeasureTheory.exists_pos_lintegral_lt_of_sigmaFinite, measurable_nnnorm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
borelSpace 📖	mathematical	—	BorelSpace NNReal instTopologicalSpace measurableSpace	—	Subtype.borelSpace Real.borelSpace

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
borelSpace 📖	mathematical	—	BorelSpace instTopologicalSpaceNat instMeasurableSpace	—	borel_eq_top_of_discrete instDiscreteTopologyNat

OpensMeasurableSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
borel_le 📖	mathematical	—	MeasurableSpace MeasurableSpace.instLE borel	—	—
separatesPoints 📖	mathematical	—	MeasurableSpace.SeparatesPoints	—	MeasurableSpace.separatesPoints_iff Inseparable.eq inseparable_iff_forall_isOpen IsOpen.measurableSet
toMeasurableSingletonClass 📖	mathematical	—	MeasurableSingletonClass	—	IsClosed.measurableSet isClosed_singleton

OrderDual

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
borelSpace 📖	mathematical	—	BorelSpace OrderDual instTopologicalSpace instMeasurableSpaceOrderDual	—	—
opensMeasurableSpace 📖	mathematical	—	OpensMeasurableSpace OrderDual instTopologicalSpace instMeasurableSpaceOrderDual	—	—

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
borelSpace 📖	mathematical	SecondCountableTopology BorelSpace	topologicalSpace MeasurableSpace.pi	—	le_antisymm pi_le_borel_pi OpensMeasurableSpace.borel_le opensMeasurableSpace BorelSpace.opensMeasurable
borelSpace_of_subsingleton 📖	mathematical	BorelSpace	topologicalSpace MeasurableSpace.pi	—	le_antisymm pi_le_borel_pi OpensMeasurableSpace.borel_le opensMeasurableSpace_of_subsingleton BorelSpace.opensMeasurable
opensMeasurableSpace 📖	mathematical	SecondCountableTopology OpensMeasurableSpace	topologicalSpace MeasurableSpace.pi	—	TopologicalSpace.eq_generateFrom_countableBasis pi_generateFrom_eq borel_eq_generateFrom_of_subbasis TopologicalSpace.instSecondCountableTopologyForallOfCountable MeasurableSpace.generateFrom_le MeasurableSet.pi Finset.countable_toSet IsOpen.measurableSet
opensMeasurableSpace_of_subsingleton 📖	mathematical	OpensMeasurableSpace	topologicalSpace MeasurableSpace.pi	—	isEmpty_or_nonempty Subsingleton.set_cases Unique.instSubsingleton MeasurableSet.empty MeasurableSet.univ nonempty_unique borel.eq_1 MeasurableSpace.pi.eq_1 ciSup_unique MeasurableSpace.generateFrom_le MeasurableSpace.measurableSet_comap ciInf_unique IsOpen.measurableSet

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
borelSpace 📖	mathematical	—	BorelSpace instTopologicalSpaceProd instMeasurableSpace	—	le_antisymm prod_le_borel_prod OpensMeasurableSpace.borel_le opensMeasurableSpace BorelSpace.opensMeasurable
opensMeasurableSpace 📖	mathematical	—	OpensMeasurableSpace instTopologicalSpaceProd instMeasurableSpace	—	opensMeasurableSpace_iff_forall_measurableSet SecondCountableTopologyEither.out isOpen_iff_forall_mem_open Set.Subset.antisymm isOpen_prod_iff TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open TopologicalSpace.isBasis_countableBasis HasSubset.Subset.trans Set.instIsTransSubset Set.prod_mono_left Set.mem_prod MeasurableSet.biUnion TopologicalSpace.countable_countableBasis MeasurableSet.prod IsOpen.measurableSet TopologicalSpace.isOpen_of_mem_countableBasis Set.prod_mono_right

Rat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
borelSpace 📖	mathematical	—	BorelSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace instMetricSpace instMeasurableSpace	—	borel_eq_top_of_countable T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace Encodable.countable

Real

Definitions

Name	Category	Theorems
measurableSpace 📖	CompOp	440 math, 2 bridge math: Measurable.ereal_toReal, ProbabilityTheory.Kernel.measurable_rnDerivAux, hasDerivAt_fourier, NumberField.mixedEmbedding.fundamentalDomain_integerLattice, RCLike.measurable_ofReal, ProbabilityTheory.cdf_measure_stieltjesFunction, ProbabilityTheory.condCDF_ae_eq, ProbabilityTheory.gaussianReal_map_const_mul, ProbabilityTheory.lintegral_condCDF, mellin_eq_fourier, hasMeasurablePow, BoxIntegral.Prepartition.measure_iUnion_toReal, NumberField.mixedEmbedding.measurable_polarCoordReal_symm, fourierCoeff_tsum_comp_add, ProbabilityTheory.IsCondKernelCDF.toKernel_Iic, smul_map_volume_mul_right, ProbabilityTheory.lintegral_toKernel_univ, RightDerivMeasurableAux.measurableSet_B, intervalIntegrable_iff', measurable_sinh, ProbabilityTheory.variance_fun_id_gaussianReal, ProbabilityTheory.Kernel.borelMarkovFromReal_apply', ProbabilityTheory.setLIntegral_preCDF_fst, intervalIntegrable_iff, Polynomial.Chebyshev.integral_measureT_eq_integral_cos, ProbabilityTheory.unitInterval.cdf_eq_real, ProbabilityTheory.gaussianReal_map_neg, intervalIntegral.intervalIntegral_eq_integral_uIoc, AddCircle.volume_eq_smul_haarAddCircle, ZLattice.covolume_eq_det_inv, ProbabilityTheory.isProbabilityMeasure_paretoMeasure, ProbabilityTheory.IsGaussian.map_eq_gaussianReal, WeakFEPair.hf_modif_int, measurable_norm, ProbabilityTheory.integrable_preCDF, ProbabilityTheory.rnDeriv_gaussianReal, Complex.measurable_arg, ProbabilityTheory.aemeasurable_of_mem_interior_integrableExpSet, BoxIntegral.Box.measurableSet_Icc, indicator_indepFun_pi_of_prod_bcf, intervalIntegrable_iff_integrableOn_Icc_of_le, GaussianFourier.integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace, MeasureTheory.measurableEmbedding_embeddingReal, ProbabilityTheory.setIntegral_condCDF, ProbabilityTheory.integral_gaussianReal_eq_integral_smul, unitInterval.coe_symmMeasurableEquiv, fourier_gaussian_pi', ProbabilityTheory.integral_continuousLinearMap_gaussianReal, exists_eq_interval_average_of_noAtoms, AddCircle.isAddFundamentalDomain_of_ae_ball, measurable_ereal_toReal, intervalIntegrable_iff_integrableOn_Ico_of_le, fourier_real_eq_integral_exp_smul, ProbabilityTheory.setLIntegral_stieltjesOfMeasurableRat_rat, stronglyMeasurable_derivWithin_Ioi, ProbabilityTheory.gaussianReal_zero_var, ProbabilityTheory.isProbabilityMeasure_expMeasure, Probability.measurable_cauchyPDFReal, ProbabilityTheory.IsRatCondKernelCDF.setIntegral, AddCircle.integral_haarAddCircle, AEMeasurable.norm, fourier_deriv, ProbabilityTheory.IsCondKernelCDF.integral, smul_map_diagonal_volume_pi, BoxIntegral.Box.measurableSet_coe, volume_val, Polynomial.Chebyshev.integral_T_real_mul_self_measureT_of_ne_zero, ENNReal.hasMeasurablePow, Polynomial.Chebyshev.integral_measureT, aestronglyMeasurable_rpowIntegrand₀₁, OrthonormalBasis.measurePreserving_repr, AEMeasurable.im, ProbabilityTheory.Kernel.isCondKernelCDF_condKernelCDF, Icc_mem_vitaliFamily_at_left, aemeasurable_coe_nnreal_real_iff, Polynomial.Chebyshev.integral_measureT_eq_integral_cos_of_continuous, Complex.measurableEquivPi_apply, MeasureTheory.charFunDual_eq_charFun_map_one, unitInterval.symmMeasurableEquiv_apply, Set.OrdConnected.nullMeasurableSet, ProbabilityTheory.integral_stieltjesOfMeasurableRat, ProbabilityTheory.IsRatCondKernelCDFAux.measurable, intervalIntegral.FTCFilter.finiteAt_inner, BoxIntegral.unitPartition.integralSum_eq_tsum_div, ProbabilityTheory.covarianceBilin_apply_basisFun_self, MeasureTheory.charFun_apply_real, GaussianFourier.integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace, ProbabilityTheory.integrable_condCDF, InformationTheory.measurable_klFun, UnitAddTorus.mFourierCoeff_toLp, ProbabilityTheory.gaussianReal_map_continuousLinearMap, EuclideanSpace.volume_closedBall_fin_three, ProbabilityTheory.Kernel.instIsMarkovKernelCondKernelUnitReal, Complex.measurableEquivRealProd_apply, ProbabilityTheory.cdf_eq_real, map_matrix_volume_pi_eq_smul_volume_pi, measurable_circleMap, ProbabilityTheory.IsMeasurableRatCDF.instIsProbabilityMeasure_stieltjesFunction, orthonormal_fourier, intervalIntegral.abs_intervalIntegral_eq, MeasureTheory.memLp_haarAddCircle_iff, ProbabilityTheory.noAtoms_gaussianReal, ProbabilityTheory.isProbabilityMeasure_gammaMeasure, fourierIntegral_gaussian_pi, volume_eq_stieltjes_id, measurable_sinc, smul_map_volume_mul_left, ENNReal.measurable_toReal, mellinInv_eq_fourierIntegralInv, PiLp.volume_preserving_toLp, measurableEmbedding_sigmoid, Complex.measurable_re, BoxIntegral.Box.measure_coe_lt_top, MeasureTheory.posConvolution_eq_convolution_indicator, ProbabilityTheory.Kernel.measurable_density, NumberField.mixedEmbedding.fundamentalDomain_idealLattice, measurable_cos, BoxIntegral.Box.measure_Icc_lt_top, ZLattice.covolume_div_covolume_eq_relIndex, Polynomial.toAddCircle.integrable, AddCircle.instHasAddFundamentalDomainSubtypeAddOppositeRealMemAddSubgroupOpZmultiples, isAddFundamentalDomain_Ioc, measurableEmbedding_sigmoid_comp_embeddingReal, MeasureTheory.exists_subset_real_measurableEquiv, mellinInv_eq_fourierInv, ProbabilityTheory.isRatCondKernelCDF_preCDF, fourier_real_eq, ProbabilityTheory.ofReal_condCDF_ae_eq, ProbabilityTheory.IsMeasurableRatCDF.measure_stieltjesFunction_univ, hasSum_fourier_series_L2, measurable_arctan, ProbabilityTheory.integral_truncation_eq_intervalIntegral, MeasureTheory.hausdorffMeasure_pi_real, Monotone.ae_hasDerivAt, ProbabilityTheory.IsCondKernelCDF.setIntegral, IntervalIntegrable.aestronglyMeasurable', integrable_sinc, EuclideanSpace.volume_closedBall_fin_two, intervalIntegrable_iff_integrableOn_Ioc_of_le, ProbabilityTheory.measurable_gaussianPDF, ProbabilityTheory.gaussianReal_map_linearMap, tendsto_measure_Icc, aestronglyMeasurable_derivWithin_Ioi, ProbabilityTheory.integrableExpSet_id_gaussianReal, intervalIntegral.integral_cases, measurable_real_toNNReal, ProbabilityTheory.complexMGF_id_mul_I, ProbabilityTheory.Kernel.measurable_densityProcess, ProbabilityTheory.IsCondKernelCDF.setLIntegral, unitInterval.measurable_symm, ProbabilityTheory.instIsProbabilityMeasureGaussianReal, measurableSet_pi_polarCoord_target, ProbabilityTheory.integrableExpSet_fun_id_gaussianReal, ProbabilityTheory.measurable_paretoPDFReal, RCLike.measurable_re, ProbabilityTheory.preCDF_le_one, zero_at_infty_fourierIntegral, ProbabilityTheory.Kernel.measurable_densityProcess_left, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed, ProbabilityTheory.measurable_gammaPDFReal, ProbabilityTheory.memLp_id_gaussianReal', fourierIntegral_real_eq_integral_exp_smul, deriv_fourierIntegral, NumberField.mixedEmbedding.covolume_idealLattice, NumberField.mixedEmbedding.volume_preserving_negAt, AddCircle.instIsProbabilityMeasureRealHaarAddCircle, ProbabilityTheory.integral_truncation_eq_intervalIntegral_of_nonneg, ProbabilityTheory.Kernel.measurable_countableFiltration_densityProcess, ProbabilityTheory.setIntegral_stieltjesOfMeasurableRat, MeasureTheory.hausdorffMeasure_prod_real, ProbabilityTheory.mgf_fun_id_gaussianReal, MeasureTheory.hausdorffMeasure_lineMap_image, intervalIntegral.integral_smul_measure, intervalIntegral.FTCFilter.meas_gen, ProbabilityTheory.gaussianReal_apply, NumberField.Units.regOfFamily_of_isMaxRank, ProbabilityTheory.gaussianReal_conv_gaussianReal, PiLp.volume_preserving_ofLp, measurableSet_of_differentiableWithinAt_Ici_of_isComplete, ProbabilityTheory.isGaussian_gaussianReal, Polynomial.Chebyshev.integrable_measureT, ProbabilityTheory.monotone_preCDF, MeasureTheory.integral_charFun_Icc, ProbabilityTheory.moment_truncation_eq_intervalIntegral_of_nonneg, intervalIntegral.norm_intervalIntegral_eq, measurable_cosh, indicator_indepFun_pi_of_bcf, fourierCoeff_toLp, coe_fourierBasis, ProbabilityTheory.variance_continuousLinearMap_gaussianReal, tendsto_measure_Icc_nhdsWithin_right, ProbabilityTheory.Kernel.compProd_fst_condKernelReal, unitInterval.symmMeasurableEquiv_symm_apply, Probability.stronglyMeasurable_cauchyPDF, ProbabilityTheory.aemeasurable_of_integrable_exp_mul, NumberField.mixedEmbedding.volume_preserving_mixedSpaceToRealMixedSpace_symm, aestronglyMeasurable_derivWithin_Ici, BoxIntegral.norm_integral_le_of_le_const, indicator_indepFun_process_of_bcf, ProbabilityTheory.integral_linearMap_gaussianReal, ProbabilityTheory.HasSubgaussianMGF.aemeasurable, Polynomial.Chebyshev.integral_eval_T_real_measureT_zero, ProbabilityTheory.setLIntegral_toKernel_univ, ProbabilityTheory.withDensity_preCDF, MeasureTheory.measurableEquiv_range_coe_nat_of_infinite_of_countable, ProbabilityTheory.measurable_preCDF', ProbabilityTheory.measurable_poissonPMFReal, intervalIntegral.integral_of_ge, ProbabilityTheory.condCDF_eq_stieltjesOfMeasurableRat_unit_prod, Measurable.im, IntervalIntegrable.aestronglyMeasurable, ProbabilityTheory.covarianceBilin_real_self, MeasureTheory.Measure.IicSnd_apply, NumberField.mixedEmbedding.fundamentalDomain_stdBasis, ProbabilityTheory.IsCondKernelCDF.measurable, Complex.measurable_im, Probability.cauchyMeasure_zero_scale, NumberField.mixedEmbedding.measurableSet_fundamentalCone, Measurable.re, stronglyMeasurable_sinc, Measurable.coe_nnreal_real, measurable_arccos, ProbabilityTheory.moment_truncation_eq_intervalIntegral, ProbabilityTheory.integrable_exp_mul_gaussianReal, ProbabilityTheory.measurable_geometricPMFReal, ProbabilityTheory.instIsProbabilityMeasureCondCDF, Complex.measurableEquivRealProd_symm_polarCoord_symm_apply, Complex.volume_preserving_equiv_real_prod, ProbabilityTheory.gaussianReal_map_mul_const, intervalIntegral.integral_of_le, mellin_eq_fourierIntegral, MeasureTheory.SignedMeasure.measurable_rnDeriv, ProbabilityTheory.Kernel.condKernelUnitReal.instIsCondKernel, MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProd, MeasureTheory.Measure.instSigmaFiniteElemRealIoiOfNatVolumeIoiPow, hasPDF_iff, ProbabilityTheory.covarianceBilin_apply_pi, AddCircle.measurePreserving_equivIoc, ProbabilityTheory.Kernel.isRatCondKernelCDF_density_Iic, NumberField.mixedEmbedding.covolume_integerLattice, EuclideanSpace.volume_ball_fin_three, intervalIntegrable_const_iff, Polynomial.Chebyshev.integral_eval_T_real_mul_eval_T_real_measureT, ProbabilityTheory.covarianceBilin_apply_basisFun, ProbabilityTheory.measure_cdf, ProbabilityTheory.setIntegral_preCDF_fst, ProbabilityTheory.IdentDistrib.norm, MeasureTheory.Measure.IicSnd_le_fst, OrthonormalBasis.measurePreserving_repr_symm, measurable_arcsin, MeasureTheory.ContinuousOn.hasBoxIntegral, Measurable.infDist, MeasureTheory.measureReal_abs_gt_le_integral_charFun, UnitAddCircle.measurePreserving_mk, MeasureTheory.addHaarMeasure_eq_volume_pi, intervalIntegral.integral_const_of_cdf, intervalIntegral.integral_const', intervalIntegrable_iff_integrableOn_Ioo_of_le, ProbabilityTheory.IsMeasurableRatCDF.measure_stieltjesFunction_Iic, AEMeasurable.carg, ProbabilityTheory.gaussianReal_map_sub_const, MeasureTheory.hausdorffMeasure_smul_right_image, ProbabilityTheory.compProd_toKernel, ZLattice.volume_image_eq_volume_div_covolume, map_linearMap_volume_pi_eq_smul_volume_pi, ProbabilityTheory.IsMeasurableRatCDF.measurable_stieltjesFunction, ProbabilityTheory.memLp_id_gaussianReal, Complex.measurableEquivPi_symm_apply, MeasureTheory.Measure.map_linearMap_addHaar_pi_eq_smul_addHaar, span_fourierLp_closure_eq_top, EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp, ProbabilityTheory.variance_id_gaussianReal, zero_at_infty_fourier, Polynomial.Chebyshev.integral_eval_T_real_measureT_of_ne_zero, MeasureTheory.Measure.iInf_rat_gt_prod_Iic, Complex.volume_preserving_equiv_pi, ProbabilityTheory.integral_condCDF, NumberField.mixedEmbedding.volume_preserving_homeoRealMixedSpacePolarSpace, EuclideanSpace.volume_ball_fin_two, ProbabilityTheory.covarianceBilin_real, measurable_exp, MeasureTheory.exists_measurableEmbedding_real, EuclideanSpace.volume_ball, ProbabilityTheory.IsRatCondKernelCDFAux.measurable_right, RCLike.measurable_im, MeasureTheory.MemLp.haarAddCircle, measurableSet_of_differentiableWithinAt_Ioi, ProbabilityTheory.isRatCondKernelCDFAux_preCDF, ENNReal.measurable_ofReal, AEMeasurable.ereal_toReal, CFC.exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₀₁, ProbabilityTheory.Kernel.isRatCondKernelCDFAux_density_Iic, measurable_derivWithin_Ioi, Measurable.dist, MeasureTheory.exists_nat_measurableEquiv_range_coe_fin_of_finite, measurable_coe_nnreal_real, measurable_coe_real_ereal, InformationTheory.stronglyMeasurable_klFun, stronglyMeasurable_derivWithin_Ici, ProbabilityTheory.measurable_exponentialPDFReal, ProbabilityTheory.isCondKernelCDF_condCDF, ProbabilityTheory.measurable_gaussianPDFReal, MonotoneOn.exists_tendsto_deriv_liminf_lintegral_enorm_le, MeasureTheory.hausdorffMeasure_real, NumberField.mixedEmbedding.measurable_polarCoord_symm, ProbabilityTheory.Kernel.borelMarkovFromReal_apply, ProbabilityTheory.gaussianReal_map_add_const, MeasureTheory.Measure.toBoxAdditive_apply, ProbabilityTheory.instIsMarkovKernel_toKernel, ProbabilityTheory.stronglyMeasurable_gaussianPDFReal, indicator_indepFun_of_bcf, ProbabilityTheory.Kernel.measurable_density_left, exists_eq_interval_average_of_measure, MeasureTheory.charFun_map_mul, MeasureTheory.measurable_llr, MeasureTheory.Measure.tendsto_IicSnd_atTop, NNReal.hasMeasurablePow, ProbabilityTheory.complexMGF_id_gaussianReal, IntervalIntegrable.def', AddCircle.measurePreserving_mk, AddCircle.measurable_mk', WeakFEPair.hg_int, tendsto_Icc_vitaliFamily_left, tendsto_measure_Icc_nhdsWithin_right', intervalIntegral.abs_integral_eq_abs_integral_uIoc, ProbabilityTheory.integral_id_gaussianReal, map_volume_mul_right, ProbabilityTheory.isProbabilityMeasureGamma, unitInterval.measurableEmbedding_coe, volume_euclideanSpace_eq_dirac, ProbabilityTheory.IsRatCondKernelCDFAux.setIntegral_iInf_rat_gt, BoxIntegral.Box.volume_apply, WeakFEPair.hf_int, Measurable.ennreal_toReal, measurable_sin, ProbabilityTheory.gaussianReal_map_const_sub, TemperedDistribution.derivCLM_toTemperedDistributionCLM_eq, StieltjesFunction.ae_hasDerivAt, hasSum_sq_fourierCoeff, ProbabilityTheory.measure_condCDF_Iic, measurable_log, ProbabilityTheory.gaussianReal_map_const_add, ProbabilityTheory.Kernel.instIsMarkovKernelCondKernelReal, ProbabilityTheory.measurable_measure_condCDF, ProbabilityTheory.variance_linearMap_gaussianReal, ProbabilityTheory.stronglyMeasurable_gammaPDFReal, fourierBasis_repr, ProbabilityTheory.mgf_id_gaussianReal, BoxIntegral.Box.measurableSet_Ioo, ProbabilityTheory.lintegral_preCDF_fst, ProbabilityTheory.IsRatCondKernelCDF.measurable, intervalIntegral.norm_integral_eq_norm_integral_uIoc, ProbabilityTheory.IsMeasurableRatCDF.measurable, Polynomial.Chebyshev.integral_eval_T_real_mul_eval_T_real_measureT_of_ne, MeasureTheory.addHaarMeasure_eq_volume, ProbabilityTheory.setLIntegral_condCDF, ProbabilityTheory.isProbabilityMeasureBeta, ProbabilityTheory.IsMeasurableRatCDF.measurable_measure_stieltjesFunction, ProbabilityTheory.measure_condCDF_univ, ProbabilityTheory.lintegral_stieltjesOfMeasurableRat, Probability.stronglyMeasurable_cauchyPDFReal, MeasureTheory.Measure.IicSnd_univ, indicator_indepFun_process_of_prod_bcf, MeasureTheory.Measure.volumeIoiPow_apply_Iio, ProbabilityTheory.Kernel.measurable_densityProcess_right, EuclideanSpace.coe_measurableEquiv, borelSpace, EReal.measurableEmbedding_coe, AEMeasurable.re, Polynomial.Chebyshev.integral_eval_T_real_mul_self_measureT_zero, ProbabilityTheory.measurable_condCDF, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm, ProbabilityTheory.stronglyMeasurable_betaPDFReal, IntervalIntegrable.aestronglyMeasurable_restrict_uIoc, ProbabilityTheory.IsCondKernelCDF.lintegral, tsum_sq_fourierCoeff, aemeasurable_derivWithin_Ici, ProbabilityTheory.measurable_betaPDFReal, Icc_mem_vitaliFamily_at_right, hasDerivAt_fourierIntegral, EuclideanSpace.measurableEquiv_toEquiv, Probability.instIsProbabilityMeasure_cauchyMeasure, MeasureTheory.Measure.IicSnd_ac_fst, intervalIntegral.integral_eq_integral_of_support_subset, Complex.measurable_ofReal, MeasureTheory.charFun_map_eq_charFunDual_smul, SchwartzMap.tsum_eq_tsum_fourierIntegral, MeasureTheory.intervalIntegrable_charFun, ProbabilityTheory.isProbabilityMeasureExponential, ProbabilityTheory.gaussianReal_apply_eq_integral, ProbabilityTheory.IsRatCondKernelCDFAux.setIntegral, AEMeasurable.coe_nnreal_real, ProbabilityTheory.setIntegral_stieltjesOfMeasurableRat_rat, ProbabilityTheory.charFun_gaussianReal, measurable_infDist, measurable_derivWithin_Ici, Complex.measurableEquivRealProd_symm_apply, fourierIntegral_deriv, OrthonormalBasis.measurePreserving_measurableEquiv, fourierIntegral_real_eq, NumberField.mixedEmbedding.fundamentalCone.measurableSet_paramSet, AEMeasurable.ennreal_toReal, Probability.measurable_cauchyPDF, ProbabilityTheory.stronglyMeasurable_paretoPDFReal, intervalIntegral.norm_integral_le_integral_norm_uIoc, ProbabilityTheory.setLIntegral_stieltjesOfMeasurableRat, NumberField.mixedEmbedding.fundamentalCone.measurableSet_normLeOne, volume_preserving_transvectionStruct, ProbabilityTheory.Kernel.measurable_density_right, measurableSet_of_differentiableWithinAt_Ici, ProbabilityTheory.Kernel.measurable_rnDerivAux_right, isAddFundamentalDomain_Ioc', exists_measure_rpow_eq_integral, Measurable.carg, EuclideanSpace.volume_closedBall, ProbabilityTheory.stronglyMeasurable_exponentialPDFReal, NumberField.mixedEmbedding.measurable_polarSpaceCoord_symm, Measurable.norm, ProbabilityTheory.IsGaussian.eq_gaussianReal, EuclideanSpace.coe_measurableEquiv_symm, AEMeasurable.dist, fourier_gaussian_pi, coeFn_fourierLp, deriv_fourier, MeasureTheory.measurable_embeddingReal, measurable_coe_nnreal_real_iff, ProbabilityTheory.ofReal_cdf, fourierIntegral_gaussian_pi', unitInterval.symm_symmMeasurableEquiv, ProbabilityTheory.integral_preCDF_fst, ProbabilityTheory.setLIntegral_toKernel_Iic, ProbabilityTheory.IsCondKernelCDF.toKernel_apply, ProbabilityTheory.instIsProbabilityMeasurecdf, SchwartzMap.tsum_eq_tsum_fourier, ZLattice.covolume_eq_det, tendsto_Icc_vitaliFamily_right, ProbabilityTheory.gaussianReal_absolutelyContinuous, map_volume_mul_left, aemeasurable_derivWithin_Ioi, measurable_dist bridge: MeasureTheory.SimpleFunc.hasBoxIntegral, MeasureTheory.SimpleFunc.box_integral_eq_integral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
borelSpace 📖	mathematical	—	BorelSpace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace measurableSpace	—	—

SecondCountableTopologyEither

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
out 📖	mathematical	—	SecondCountableTopology	—	—

Subtype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
borelSpace 📖	mathematical	—	BorelSpace instTopologicalSpaceSubtype instMeasurableSpace	—	BorelSpace.measurable_eq borel_comap
opensMeasurableSpace 📖	mathematical	—	OpensMeasurableSpace instTopologicalSpaceSubtype instMeasurableSpace	—	borel_comap MeasurableSpace.comap_mono OpensMeasurableSpace.borel_le

TopologicalSpace.IsTopologicalBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
borel_eq_generateFrom 📖	mathematical	TopologicalSpace.IsTopologicalBasis	borel MeasurableSpace.generateFrom	—	borel_eq_generateFrom_of_subbasis eq_generateFrom

Topology.IsClosedEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurableEmbedding 📖	mathematical	Topology.IsClosedEmbedding	MeasurableEmbedding	—	Topology.IsEmbedding.measurableEmbedding isEmbedding IsClosed.measurableSet BorelSpace.opensMeasurable isClosed_range

Topology.IsEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurableEmbedding 📖	mathematical	Topology.IsEmbedding MeasurableSet Set.range	MeasurableEmbedding	—	Subtype.borelSpace MeasurableEmbedding.comp MeasurableEmbedding.subtype_coe MeasurableEquiv.measurableEmbedding

Topology.IsOpenEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurableEmbedding 📖	mathematical	Topology.IsOpenEmbedding	MeasurableEmbedding	—	Topology.IsEmbedding.measurableEmbedding isEmbedding IsOpen.measurableSet BorelSpace.opensMeasurable isOpen_range

ULift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instBorelSpace 📖	mathematical	—	BorelSpace topologicalSpace instMeasurableSpace	—	MeasurableEmbedding.borelSpace MeasurableEquiv.measurableEmbedding Homeomorph.isInducing

Unit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
borelSpace 📖	mathematical	—	BorelSpace instTopologicalSpacePUnit PUnit.instMeasurableSpace	—	borel_eq_top_of_discrete instDiscreteTopologyPUnit

(root)

Definitions

Name	Category	Theorems
BorelSpace 📖	CompData	33 math math: QuotientGroup.borelSpace, Int.borelSpace, Complex.borelSpace, RCLike.borelSpace, Rat.borelSpace, OrderDual.borelSpace, WithLp.borelSpace, Unit.borelSpace, WithTop.instBorelSpace, DiscreteMeasurableSpace.toBorelSpace, Prod.borelSpace, UpgradedStandardBorel.toBorelSpace, instBorelSpaceSubtypeMemOpens, ULift.instBorelSpace, Empty.borelSpace, EReal.borelSpace, Countable.instBorelSpace, StandardBorelSpace.polish, ENNReal.borelSpace, NNReal.borelSpace, CosetSpace.borelSpace, MeasurableSet.isClopenable', Real.borelSpace, ContinuousLinearMap.instBorelSpace, Subtype.borelSpace, QuotientAddGroup.borelSpace, Bool.borelSpace, exists_borelSpace_of_countablyGenerated_of_separatesPoints, MeasurableEmbedding.borelSpace, AddCosetSpace.borelSpace, Measurable.borelSpace_codomain, Nat.borelSpace, Quotient.borelSpace
OpensMeasurableSpace 📖	CompData	6 math math: Subtype.opensMeasurableSpace, exists_opensMeasurableSpace_of_countablySeparated, BorelSpace.opensMeasurable, OrderDual.opensMeasurableSpace, opensMeasurableSpace_iff_forall_measurableSet, Prod.opensMeasurableSpace
SecondCountableTopologyEither 📖	CompData	2 math math: secondCountableTopologyEither_of_left, secondCountableTopologyEither_of_right
borel 📖	CompOp	42 math math: MeasureTheory.OuterMeasure.IsMetric.borel_le_caratheodory, borel_eq_generateFrom_isClosed, borel_eq_generateFrom_Ici, Real.borel_eq_generateFrom_Iio_rat, OpensMeasurableSpace.borel_le, Real.borel_eq_generateFrom_Ioo_rat, BorelSpace.measurable_eq, borel_eq_generateFrom_of_subbasis, generateFrom_Icc_mem_le_borel, borel_eq_generateFrom_Icc, generateFrom_Ico_mem_le_borel, MeasureTheory.distribHaarChar_apply, Real.borel_eq_generateFrom_Ioi_rat, borel_eq_top_of_discrete, StieltjesFunction.borel_le_measurable, borel_eq_generateFrom_Ioc, Real.borel_eq_generateFrom_Ici_rat, Continuous.borel_measurable, Dense.borel_eq_generateFrom_Ico_mem, Continuous.map_eq_borel, ProbabilityTheory.IsKolmogorovProcess.measurablePair, Dense.borel_eq_generateFrom_Ico_mem_aux, Continuous.map_borel_eq, pi_le_borel_pi, Dense.borel_eq_generateFrom_Ioc_mem_aux, borel_eq_generateFrom_Ico, borel_eq_generateFrom_Ioc_le, borel_eq_generateFrom_Ioi, borel_eq_generateFrom_Iio, borel_eq_top_of_countable, prod_le_borel_prod, borel_anti, borel_eq_generateFrom_Iic, Real.borel_eq_generateFrom_Iic_rat, borel_comap, MeasureTheory.borel_eq_borel_of_le, eq_borel_upgradeStandardBorel, Dense.borel_eq_generateFrom_Ioc_mem, Dense.borel_eq_generateFrom_Icc_mem, TopologicalSpace.IsTopologicalBasis.borel_eq_generateFrom, Dense.borel_eq_generateFrom_Icc_mem_aux, Measurable.map_measurableSpace_eq_borel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
borel_anti 📖	mathematical	—	Antitone TopologicalSpace MeasurableSpace PartialOrder.toPreorder TopologicalSpace.instPartialOrder MeasurableSpace.instPartialOrder borel	—	MeasurableSpace.generateFrom_le
borel_comap 📖	mathematical	—	borel TopologicalSpace.induced MeasurableSpace.comap	—	MeasurableSpace.comap_generateFrom
borel_eq_generateFrom_isClosed 📖	mathematical	—	borel MeasurableSpace.generateFrom setOf Set IsClosed	—	le_antisymm MeasurableSpace.generateFrom_le MeasurableSet.of_compl isClosed_compl_iff isOpen_compl_iff
borel_eq_generateFrom_of_subbasis 📖	mathematical	TopologicalSpace.generateFrom	borel MeasurableSpace.generateFrom	—	le_antisymm MeasurableSpace.generateFrom_le MeasurableSet.univ MeasurableSet.inter TopologicalSpace.isOpen_sUnion_countable MeasurableSet.sUnion
borel_eq_top_of_countable 📖	mathematical	—	borel Top.top MeasurableSpace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice MeasurableSpace.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	top_unique MeasurableSet.of_discrete MeasurableSingletonClass.toDiscreteMeasurableSpace MeasurableSpace.MeasurableSingletonClass.of_separatesPoints OpensMeasurableSpace.separatesPoints BorelSpace.opensMeasurable
borel_eq_top_of_discrete 📖	mathematical	—	borel Top.top MeasurableSpace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice MeasurableSpace.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	top_le_iff isOpen_discrete
closure_ae_eq_of_null_frontier 📖	mathematical	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike frontier instZeroENNReal	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure.instOuterMeasureClass closure	—	Filter.EventuallyLE.antisymm MeasureTheory.Measure.instOuterMeasureClass Filter.EventuallyLE.trans MeasureTheory.ae_le_set HasSubset.Subset.eventuallyLE interior_subset subset_closure
instCountablySeparatedElemOfHasCountableSeparatingOnIsOpen 📖	mathematical	—	MeasurableSpace.CountablySeparated Set.Elem Subtype.instMeasurableSpace Set Set.instMembership	—	MeasurableSpace.CountablySeparated.subtype_iff HasCountableSeparatingOn.mono IsOpen.measurableSet Set.Subset.rfl
instMeasurableEqOfSecondCountableTopologyOfT2Space 📖	mathematical	—	MeasurableEq	—	IsClosed.measurableSet Prod.opensMeasurableSpace secondCountableTopologyEither_of_right isClosed_diagonal
interior_ae_eq_of_null_frontier 📖	mathematical	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike frontier instZeroENNReal	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure.instOuterMeasureClass interior	—	Filter.EventuallyLE.antisymm MeasureTheory.Measure.instOuterMeasureClass HasSubset.Subset.eventuallyLE interior_subset Filter.EventuallyLE.trans subset_closure MeasureTheory.ae_le_set
isPiSystem_isClosed 📖	mathematical	—	IsPiSystem setOf Set IsClosed	—	IsClosed.inter
isPiSystem_isOpen 📖	mathematical	—	IsPiSystem setOf Set IsOpen	—	IsOpen.inter
measurableSet_closure 📖	mathematical	—	MeasurableSet closure	—	IsClosed.measurableSet isClosed_closure
measurableSet_frontier 📖	mathematical	—	MeasurableSet frontier	—	MeasurableSet.diff measurableSet_closure measurableSet_interior
measurableSet_interior 📖	mathematical	—	MeasurableSet interior	—	IsOpen.measurableSet isOpen_interior
measurableSet_of_continuousAt 📖	mathematical	—	MeasurableSet setOf ContinuousAt UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace	—	IsGδ.measurableSet IsGδ.setOf_continuousAt PseudoEMetricSpace.pseudoMetrizableSpace
measurable_of_continuousOn_compl_singleton 📖	mathematical	ContinuousOn Compl.compl Set Set.instCompl Set.instSingletonSet	Measurable	—	measurable_of_measurable_on_compl_singleton OpensMeasurableSpace.toMeasurableSingletonClass Continuous.measurable Subtype.opensMeasurableSpace continuousOn_iff_continuous_restrict
measurable_of_isClosed 📖	mathematical	MeasurableSet Set.preimage	Measurable	—	measurable_of_isOpen MeasurableSet.compl_iff Set.preimage_compl isClosed_compl_iff
measurable_of_isClosed' 📖	mathematical	MeasurableSet Set.preimage	Measurable	—	measurable_of_isClosed Set.eq_empty_or_nonempty
measurable_of_isOpen 📖	mathematical	MeasurableSet Set.preimage	Measurable	—	BorelSpace.measurable_eq measurable_generateFrom
measure_closure_of_null_frontier 📖	mathematical	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike frontier instZeroENNReal	closure	—	MeasureTheory.measure_congr MeasureTheory.Measure.instOuterMeasureClass closure_ae_eq_of_null_frontier
measure_interior_of_null_frontier 📖	mathematical	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike frontier instZeroENNReal	interior	—	MeasureTheory.measure_congr MeasureTheory.Measure.instOuterMeasureClass interior_ae_eq_of_null_frontier
nhds_isMeasurablyGenerated 📖	mathematical	—	Filter.IsMeasurablyGenerated nhds	—	nhds_def iInf_subtype' Filter.iInf_isMeasurablyGenerated MeasurableSet.principal_isMeasurablyGenerated IsOpen.measurableSet
nullMeasurableSet_of_null_frontier 📖	mathematical	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike frontier instZeroENNReal	MeasureTheory.NullMeasurableSet	—	MeasureTheory.Measure.instOuterMeasureClass IsOpen.measurableSet isOpen_interior Filter.EventuallyEq.symm interior_ae_eq_of_null_frontier
null_frontier_inter 📖	mathematical	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike frontier instZeroENNReal	Set.instInter	—	bot_unique MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass HasSubset.Subset.trans Set.instIsTransSubset frontier_inter_subset MeasureTheory.measure_union_le add_zero
opensMeasurableSpace_iff_forall_measurableSet 📖	mathematical	—	OpensMeasurableSpace MeasurableSet	—	OpensMeasurableSpace.borel_le MeasurableSpace.generateFrom_le
pi_le_borel_pi 📖	mathematical	BorelSpace	MeasurableSpace MeasurableSpace.instLE MeasurableSpace.pi borel Pi.topologicalSpace	—	BorelSpace.measurable_eq iSup_le MeasurableSpace.comap_le_iff_le_map Continuous.borel_measurable continuous_apply
prod_le_borel_prod 📖	mathematical	—	MeasurableSpace MeasurableSpace.instLE Prod.instMeasurableSpace borel instTopologicalSpaceProd	—	BorelSpace.measurable_eq sup_le MeasurableSpace.comap_le_iff_le_map Continuous.borel_measurable continuous_fst continuous_snd
secondCountableTopologyEither_of_left 📖	mathematical	—	SecondCountableTopologyEither	—	—
secondCountableTopologyEither_of_right 📖	mathematical	—	SecondCountableTopologyEither	—	—
separatesPointsOfOpensMeasurableSpaceOfT0Space 📖	mathematical	—	MeasurableSpace.SeparatesPoints	—	Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_forall_eq MeasurableSpace.exists_measurableSet_of_ne OpensMeasurableSpace.separatesPoints

---

← Back to Index