SimpleFuncDense

📁 Source: Mathlib/MeasureTheory/Function/SimpleFuncDense.lean

Statistics

Metric	Count
Definitions approxOn, nearestPt, nearestPtInd	3
Theorems exists_simpleFunc_approx_of_prod, measurable_of_prod, approxOn_comp, approxOn_mem, approxOn_range_nonneg, approxOn_zero, edist_approxOn_le, edist_approxOn_mono, edist_approxOn_y0_le, edist_nearestPt_le, nearestPtInd_le, nearestPtInd_succ, nearestPtInd_zero, nearestPt_zero, tendsto_approxOn, tendsto_nearestPt	16
Total	19

HasCompactSupport

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_simpleFunc_approx_of_prod 📖	mathematical	Continuous instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace HasCompactSupport Real Real.instLT Real.instZero	Dist.dist PseudoMetricSpace.toDist DFunLike.coe MeasureTheory.SimpleFunc Prod.instMeasurableSpace MeasureTheory.SimpleFunc.instFunLike	—	IsCompact.induction_on Set.instReflSubset instIsEmptyFalse HasSubset.Subset.trans Set.instIsTransSubset MeasurableSet.union Set.union_subset_union Set.mem_union mem_nhds_prod_iff' Metric.continuousAt_iff' Continuous.continuousAt nhdsWithin_le_nhds IsOpen.mem_nhds IsOpen.prod Set.mk_mem_prod MeasurableSet.prod IsOpen.measurableSet Set.Subset.rfl Mathlib.Tactic.Contrapose.contrapose₂ subset_tsupport Function.mem_support dist_self
measurable_of_prod 📖	mathematical	Continuous instTopologicalSpaceProd HasCompactSupport	Measurable Prod.instMeasurableSpace	—	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 exists_simpleFunc_approx_of_prod tendsto_iff_dist_tendsto_zero squeeze_zero dist_nonneg dist_comm LT.lt.le measurable_of_tendsto_metrizable MeasureTheory.SimpleFunc.measurable tendsto_pi_nhds

MeasureTheory.SimpleFunc

Definitions

Name	Category	Theorems
approxOn 📖	CompOp	25 math math: tendsto_approxOn_range_L1_enorm, MeasureTheory.tendsto_integral_approxOn_of_measurable, approxOn_comp, nnnorm_approxOn_le, MeasureTheory.tendsto_integral_approxOn_of_measurable_of_range_subset, norm_approxOn_y₀_le, memLp_approxOn_range, MeasureTheory.tendsto_setToFun_approxOn_of_measurable_of_range_subset, edist_approxOn_y0_le, edist_approxOn_mono, approxOn_mem, tendsto_approxOn, memLp_approxOn, integrable_approxOn_range, integrable_approxOn, norm_approxOn_zero_le, MeasureTheory.tendsto_setToFun_approxOn_of_measurable, tendsto_approxOn_L1_enorm, MeasureTheory.tendsto_integral_norm_approxOn_sub, edist_approxOn_le, tendsto_approxOn_range_Lp, tendsto_approxOn_Lp_eLpNorm, approxOn_zero, tendsto_approxOn_range_Lp_eLpNorm, approxOn_range_nonneg
nearestPt 📖	CompOp	3 math math: tendsto_nearestPt, nearestPt_zero, edist_nearestPt_le
nearestPtInd 📖	CompOp	3 math math: nearestPtInd_succ, nearestPtInd_le, nearestPtInd_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
approxOn_comp 📖	mathematical	Measurable Set Set.instMembership	approxOn Measurable.comp comp	—	Measurable.comp
approxOn_mem 📖	mathematical	Measurable Set Set.instMembership	DFunLike.coe MeasureTheory.SimpleFunc instFunLike approxOn	—	Subtype.mem
approxOn_range_nonneg 📖	mathematical	Pi.hasLe Preorder.toLE Pi.instZero Measurable	MeasureTheory.SimpleFunc instLE instZero approxOn Set Set.instUnion Set.range Set.instSingletonSet	—	Set.union_singleton approxOn_mem
approxOn_zero 📖	mathematical	Measurable Set Set.instMembership	DFunLike.coe MeasureTheory.SimpleFunc instFunLike approxOn	—	—
edist_approxOn_le 📖	mathematical	Measurable Set Set.instMembership	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist DFunLike.coe MeasureTheory.SimpleFunc instFunLike approxOn	—	edist_approxOn_mono zero_le Nat.instCanonicallyOrderedAdd
edist_approxOn_mono 📖	mathematical	Measurable Set Set.instMembership	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist DFunLike.coe MeasureTheory.SimpleFunc instFunLike approxOn	—	edist_nearestPt_le LE.le.trans nearestPtInd_le
edist_approxOn_y0_le 📖	mathematical	Measurable Set Set.instMembership	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist DFunLike.coe MeasureTheory.SimpleFunc instFunLike approxOn Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	edist_triangle_right le_imp_le_of_le_of_le add_le_add_right IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid edist_approxOn_le le_refl
edist_nearestPt_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist DFunLike.coe MeasureTheory.SimpleFunc instFunLike nearestPt	—	nonpos_iff_eq_zero Nat.instCanonicallyOrderedAdd nearestPtInd_succ LE.le.eq_or_lt le_rfl LT.lt.le Mathlib.Tactic.Push.not_forall_eq LE.le.trans
nearestPtInd_le 📖	mathematical	—	DFunLike.coe MeasureTheory.SimpleFunc instFunLike nearestPtInd	—	nearestPtInd_succ le_rfl LE.le.trans
nearestPtInd_succ 📖	mathematical	—	DFunLike.coe MeasureTheory.SimpleFunc instFunLike nearestPtInd ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist	—	—
nearestPtInd_zero 📖	mathematical	—	nearestPtInd const	—	—
nearestPt_zero 📖	mathematical	—	nearestPt const	—	—
tendsto_approxOn 📖	mathematical	Measurable Set Set.instMembership closure UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace	Filter.Tendsto DFunLike.coe MeasureTheory.SimpleFunc instFunLike approxOn Filter.atTop Nat.instPreorder nhds	—	tendsto_nearestPt closure_minimal Set.range_comp closure_union Set.Subset.trans image_closure_subset_closure_image continuous_subtype_val Set.subset_union_right isClosed_closure Dense.closure_eq TopologicalSpace.denseRange_denseSeq Set.image_univ Subtype.range_coe
tendsto_nearestPt 📖	mathematical	Set Set.instMembership closure UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace Set.range	Filter.Tendsto DFunLike.coe MeasureTheory.SimpleFunc instFunLike nearestPt Filter.atTop Nat.instPreorder nhds	—	Filter.HasBasis.tendsto_iff Filter.atTop_basis instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Metric.nhds_basis_eball EMetric.mem_closure_iff LE.le.trans_lt edist_nearestPt_le PseudoEMetricSpace.edist_comm

---

← Back to Index