DiracProba

📁 Source: Mathlib/MeasureTheory/Measure/DiracProba.lean

Statistics

Metric	Count
Definitions diracProba, diracProbaEquiv, diracProbaHomeomorph, diracProbaInverse	4
Theorems exists_BCNN, continuous_diracProba, continuous_diracProbaEquiv, continuous_diracProbaEquivSymm, diracProbaInverse_eq, diracProba_comp_diracProbaEquiv_symm_eq_val, diracProba_diracProbaInverse, diracProba_toMeasure_apply, diracProba_toMeasure_apply', diracProba_toMeasure_apply_of_mem, injective_diracProba, isEmbedding_diracProba, not_tendsto_diracProba_of_not_tendsto, tendsto_diracProbaEquivSymm_iff_tendsto, tendsto_diracProba_iff_tendsto	15
Total	19

CompletelyRegularSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_BCNN 📖	mathematical	Set Set.instMembership	DFunLike.coe BoundedContinuousFunction NNReal instPseudoMetricSpaceNNReal BoundedContinuousFunction.instFunLike instOneNNReal instZeroNNReal	—	Real.instIsOrderedRing completely_regular LE.le.trans LipschitzWith.dist_le_mul Real.lipschitzWith_toNNReal one_mul Real.dist_le_of_mem_Icc_01 Subtype.prop Continuous.comp continuous_real_toNNReal Continuous.subtype_val instBoundedSubNNReal NNReal.instContinuousSub Real.toNNReal_zero tsub_zero NNReal.instOrderedSub Real.toNNReal_one tsub_self NNReal.instCanonicallyOrderedAdd

MeasureTheory

Definitions

Name	Category	Theorems
diracProba 📖	CompOp	13 math math: injective_diracProba, diracProba_diracProbaInverse, continuous_diracProbaEquiv, tendsto_diracProba_iff_tendsto, diracProba_comp_diracProbaEquiv_symm_eq_val, isEmbedding_diracProba, diracProba_toMeasure_apply', tendsto_diracProbaEquivSymm_iff_tendsto, diracProba_toMeasure_apply, continuous_diracProba, continuous_diracProbaEquivSymm, not_tendsto_diracProba_of_not_tendsto, diracProba_toMeasure_apply_of_mem
diracProbaEquiv 📖	CompOp	4 math math: continuous_diracProbaEquiv, diracProba_comp_diracProbaEquiv_symm_eq_val, tendsto_diracProbaEquivSymm_iff_tendsto, continuous_diracProbaEquivSymm
diracProbaHomeomorph 📖	CompOp	—
diracProbaInverse 📖	CompOp	2 math math: diracProba_diracProbaInverse, diracProbaInverse_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_diracProba 📖	mathematical	—	Continuous ProbabilityMeasure ProbabilityMeasure.instTopologicalSpace diracProba	—	continuous_iff_continuousAt ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto measurable_coe_nnreal_ennreal_iff Continuous.measurable NNReal.borelSpace BoundedContinuousFunction.continuous lintegral_dirac' Continuous.continuousAt Continuous.comp ENNReal.continuous_coe
continuous_diracProbaEquiv 📖	mathematical	—	Continuous Set.Elem ProbabilityMeasure Set.range diracProba instTopologicalSpaceSubtype Set Set.instMembership ProbabilityMeasure.instTopologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike diracProbaEquiv	—	continuous_diracProba Set.mem_range_self
continuous_diracProbaEquivSymm 📖	mathematical	—	Continuous Set.Elem ProbabilityMeasure Set.range diracProba instTopologicalSpaceSubtype Set Set.instMembership ProbabilityMeasure.instTopologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm diracProbaEquiv	—	continuous_iff_continuousAt continuousAt_of_tendsto_nhds T2Space.t1Space T25Space.t2Space T3Space.t25Space instT3Space CompletelyRegularSpace.instRegularSpace tendsto_diracProbaEquivSymm_iff_tendsto
diracProbaInverse_eq 📖	mathematical	ProbabilityMeasure Set Set.instMembership Set.range diracProba	diracProbaInverse	—	injective_diracProba separatesPointsOfOpensMeasurableSpaceOfT0Space Set.mem_range Subtype.prop
diracProba_comp_diracProbaEquiv_symm_eq_val 📖	mathematical	—	Set.Elem ProbabilityMeasure Set.range diracProba DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm diracProbaEquiv Set Set.instMembership	—	diracProba_diracProbaInverse
diracProba_diracProbaInverse 📖	mathematical	—	diracProba diracProbaInverse ProbabilityMeasure Set Set.instMembership Set.range	—	Set.mem_range Subtype.prop
diracProba_toMeasure_apply 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike ProbabilityMeasure.toMeasure diracProba Set.indicator instZeroENNReal Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	Measure.dirac_apply
diracProba_toMeasure_apply' 📖	mathematical	MeasurableSet	DFunLike.coe Measure Set ENNReal Measure.instFunLike ProbabilityMeasure.toMeasure diracProba Set.indicator instZeroENNReal Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	Measure.dirac_apply'
diracProba_toMeasure_apply_of_mem 📖	mathematical	Set Set.instMembership	DFunLike.coe Measure ENNReal Measure.instFunLike ProbabilityMeasure.toMeasure diracProba AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	Measure.dirac_apply_of_mem
injective_diracProba 📖	mathematical	—	ProbabilityMeasure diracProba	—	dirac_eq_dirac_iff
isEmbedding_diracProba 📖	mathematical	—	Topology.IsEmbedding ProbabilityMeasure ProbabilityMeasure.instTopologicalSpace diracProba	—	Topology.IsEmbedding.comp Topology.IsEmbedding.subtypeVal Homeomorph.isEmbedding
not_tendsto_diracProba_of_not_tendsto 📖	mathematical	Filter.Tendsto nhds	ProbabilityMeasure diracProba ProbabilityMeasure.instTopologicalSpace	—	Mathlib.Tactic.Contrapose.contrapose₂ Mathlib.Tactic.Push.not_and_eq CompletelyRegularSpace.exists_BCNN IsOpen.isClosed_compl isOpen_interior mem_of_mem_nhds ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto lintegral_dirac' measurable_coe_nnreal_ennreal_iff Continuous.measurable NNReal.borelSpace BoundedContinuousFunction.continuous Filter.not_tendsto_iff_exists_frequently_notMem Ioi_mem_nhds instClosedIicTopology OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing NeZero.charZero_one ENNReal.instCharZero Filter.Frequently.mp Filter.Eventually.of_forall Set.compl_subset_compl interior_subset
tendsto_diracProbaEquivSymm_iff_tendsto 📖	mathematical	—	Filter.Tendsto Set.Elem ProbabilityMeasure Set.range diracProba DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm diracProbaEquiv nhds instTopologicalSpaceSubtype Set Set.instMembership ProbabilityMeasure.instTopologicalSpace	—	tendsto_diracProba_iff_tendsto Filter.map_map Equiv.self_comp_symm Filter.map_id Filter.tendsto_map'_iff Equiv.symm_comp_self diracProba_comp_diracProbaEquiv_symm_eq_val Set.apply_rangeSplitting tendsto_subtype_rng
tendsto_diracProba_iff_tendsto 📖	mathematical	—	Filter.Tendsto ProbabilityMeasure diracProba nhds ProbabilityMeasure.instTopologicalSpace	—	Mathlib.Tactic.Contrapose.contrapose₁ not_tendsto_diracProba_of_not_tendsto Continuous.continuousAt continuous_diracProba Filter.Tendsto.comp

---

← Back to Index