StronglyMeasurable

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

Statistics

Metric	Count
Definitions StronglyMeasurable	1
Theorems limUnder, measurableSet_exists_tendsto	2
Total	3

MeasureTheory

Definitions

Name	Category	Theorems
StronglyMeasurable 📖	MathDef	74 math math: stronglyMeasurable_const, finStronglyMeasurable_iff_stronglyMeasurable_and_exists_set_sigmaFinite, stronglyMeasurable_derivWithin_Ioi, Continuous.stronglyMeasurable_of_hasCompactSupport, ProbabilityTheory.stronglyMeasurable_geometricPMFReal, IsUnit.stronglyMeasurable_const_smul_iff, Continuous.stronglyMeasurable_of_hasCompactMulSupport, Lp.stronglyMeasurable, Lp.simpleFunc.stronglyMeasurable, Measurable.stronglyMeasurable, stronglyMeasurable_lineDeriv, stronglyMeasurable_id, ProbabilityTheory.stronglyMeasurable_condExpKernel, ProbabilityTheory.IsMeasurableRatCDF.stronglyMeasurable_stieltjesFunction, ProbabilityTheory.stronglyMeasurable_poissonPMFReal, stronglyMeasurable_one, StronglyAdapted.stronglyMeasurable_stoppedProcess, StronglyMeasurable.of_subsingleton_cod, stronglyMeasurable_iff_measurable_separable, Submartingale.stronglyMeasurable, stronglyMeasurable_const_smul_iff, StronglyMeasurable.of_discrete, stronglyMeasurable_lineDeriv_uncurry, condExp_def, Probability.stronglyMeasurable_cauchyPDF, ProbabilityTheory.IsKolmogorovProcess.stronglyMeasurable_edist, StronglyAdapted.stronglyMeasurable, ProbabilityTheory.stronglyMeasurable_stieltjesOfMeasurableRat, AEStronglyMeasurable.stronglyMeasurable_mk, Continuous.stronglyMeasurable, Real.stronglyMeasurable_sinc, stronglyMeasurable_llr, Supermartingale.stronglyMeasurable, ProgMeasurable.stronglyMeasurable_stoppedProcess, Filtration.stronglyMeasurable_limit_process', stronglyMeasurable_deriv, StronglyAdapted.stronglyMeasurable_stoppedProcess_of_discrete, exists_stronglyMeasurable_limit_of_tendsto_ae, ProbabilityTheory.Kernel.stronglyMeasurable_countableFiltration_densityProcess, Continuous.stronglyMeasurable_of_mulSupport_subset_isCompact, stronglyMeasurable_condExp, L1.stronglyMeasurable_coeFn, ProbabilityTheory.condVar_of_sigmaFinite, StronglyAdapted.stronglyMeasurable_le, FinStronglyMeasurable.stronglyMeasurable, stronglyMeasurable_charFun, InformationTheory.stronglyMeasurable_klFun, stronglyMeasurable_derivWithin_Ici, ProbabilityTheory.stronglyMeasurable_gaussianPDFReal, SimpleFunc.stronglyMeasurable, Embedding.comp_stronglyMeasurable_iff, condExp_of_sigmaFinite, ProbabilityTheory.stronglyMeasurable_condCDF, Continuous.stronglyMeasurable_of_support_subset_isCompact, stronglyMeasurable_bot_iff, ProbabilityTheory.stronglyMeasurable_gammaPDFReal, stronglyMeasurable_zero, stronglyMeasurable_iff_measurable, Probability.stronglyMeasurable_cauchyPDFReal, StronglyMeasurable.of_subsingleton_dom, HasCompactSupport.stronglyMeasurable_of_prod, stronglyMeasurable_deriv_with_param, AEEqFun.stronglyMeasurable, ProbabilityTheory.stronglyMeasurable_betaPDFReal, stronglyMeasurable_const', AEStronglyMeasurable.exists_stronglyMeasurable_range_subset, stronglyMeasurable_const_smul_iff₀, Martingale.stronglyMeasurable, ProbabilityTheory.stronglyMeasurable_paretoPDFReal, memLp_trim_of_mem_lpMeasSubgroup, ProbabilityTheory.stronglyMeasurable_exponentialPDFReal, ProbabilityTheory.stronglyMeasurable_condVar, stronglyMeasurable_stoppedValue_of_le, Filtration.stronglyMeasurable_limitProcess

MeasureTheory.StronglyMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
limUnder 📖	mathematical	MeasureTheory.StronglyMeasurable	limUnder	—	Filter.eq_or_neBot lim.congr_simp Filter.map_bot MeasureTheory.stronglyMeasurable_const stronglyMeasurable_iff_measurable_separable TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace TopologicalSpace.IsCompletelyMetrizableSpace.MetrizableSpace measurableSet_exists_tendsto Function.extend_val_apply Function.extend_val_apply' limUnder_of_not_tendsto MeasurableEmbedding.measurable_extend MeasurableEmbedding.subtype_coe measurable_of_tendsto_metrizable' Measurable.comp measurable measurable_subtype_coe tendsto_pi_nhds Filter.Tendsto.limUnder_eq TopologicalSpace.t2Space_of_metrizableSpace measurable_const TopologicalSpace.IsSeparable.union TopologicalSpace.IsSeparable.closure TopologicalSpace.IsSeparable.iUnion isSeparable_range Set.Finite.isSeparable Set.finite_singleton TopologicalSpace.IsSeparable.mono Set.subset_union_left mem_closure_of_tendsto Filter.Eventually.of_forall Set.mem_iUnion Set.subset_union_right Set.mem_singleton
measurableSet_exists_tendsto 📖	mathematical	MeasureTheory.StronglyMeasurable	MeasurableSet setOf Filter.Tendsto nhds	—	Filter.eq_or_neBot UniformSpace.secondCountable_of_separable instIsCountablyGeneratedProdElemUniformity EMetric.instIsCountablyGeneratedUniformity TopologicalSpace.IsSeparable.separableSpace PseudoEMetricSpace.pseudoMetrizableSpace TopologicalSpace.IsSeparable.closure TopologicalSpace.IsSeparable.iUnion isSeparable_range IsClosed.isCompletelyMetrizableSpace isClosed_closure subset_closure Set.mem_iUnion measurable mem_closure_of_tendsto Filter.Eventually.of_forall tendsto_subtype_rng MeasureTheory.measurableSet_exists_tendsto Subtype.opensMeasurableSpace BorelSpace.opensMeasurable

---

← Back to Index