ThickenedIndicator

📁 Source: Mathlib/Topology/MetricSpace/ThickenedIndicator.lean

Statistics

Metric	Count
Definitions thickenedIndicator, thickenedIndicatorAux	2
Theorems continuous_thickenedIndicatorAux, indicator_cthickening_eventually_eq_indicator_closure, indicator_le_thickenedIndicator, indicator_le_thickenedIndicatorAux, indicator_thickening_eventually_eq_indicator_closure, lipschitzWith_thickenedIndicator, mulIndicator_cthickening_eventually_eq_mulIndicator_closure, mulIndicator_thickening_eventually_eq_mulIndicator_closure, one_le_thickenedIndicator_apply, one_le_thickenedIndicator_apply', tendsto_indicator_cthickening_indicator_closure, tendsto_indicator_thickening_indicator_closure, tendsto_mulIndicator_cthickening_mulIndicator_closure, tendsto_mulIndicator_thickening_mulIndicator_closure, coeFn_eq_comp, thickenedIndicatorAux_closure_eq, thickenedIndicatorAux_le_one, thickenedIndicatorAux_lt_top, thickenedIndicatorAux_mono, thickenedIndicatorAux_mono_infEDist, thickenedIndicatorAux_mono_infEdist, thickenedIndicatorAux_one, thickenedIndicatorAux_one_of_mem_closure, thickenedIndicatorAux_subset, thickenedIndicatorAux_tendsto_indicator_closure, thickenedIndicatorAux_zero, thickenedIndicator_apply, thickenedIndicator_le_one, thickenedIndicator_mono, thickenedIndicator_mono_infEDist, thickenedIndicator_mono_infEdist, thickenedIndicator_one, thickenedIndicator_one_of_mem_closure, thickenedIndicator_subset, thickenedIndicator_tendsto_indicator_closure, thickenedIndicator_zero	36
Total	38

(root)

Definitions

Name	Category	Theorems
thickenedIndicator 📖	CompOp	19 math math: MeasureTheory.tendsto_integral_thickenedIndicator_of_isClosed, thickenedIndicator_mono_infEDist, thickenedIndicator_one_of_mem_closure, thickenedIndicator_zero, thickenedIndicator_le_one, MeasureTheory.integrable_thickenedIndicator, lipschitzWith_thickenedIndicator, indicator_le_thickenedIndicator, measure_le_lintegral_thickenedIndicator, one_le_thickenedIndicator_apply', thickenedIndicator_tendsto_indicator_closure, thickenedIndicator_subset, thickenedIndicator_apply, MeasureTheory.tendsto_lintegral_thickenedIndicator_of_isClosed, thickenedIndicator_mono_infEdist, thickenedIndicator_one, one_le_thickenedIndicator_apply, thickenedIndicator.coeFn_eq_comp, thickenedIndicator_mono
thickenedIndicatorAux 📖	CompOp	16 math math: thickenedIndicatorAux_tendsto_indicator_closure, measure_le_lintegral_thickenedIndicatorAux, thickenedIndicatorAux_mono_infEdist, thickenedIndicatorAux_mono_infEDist, thickenedIndicatorAux_lt_top, thickenedIndicatorAux_mono, thickenedIndicatorAux_subset, indicator_le_thickenedIndicatorAux, thickenedIndicatorAux_closure_eq, thickenedIndicatorAux_zero, thickenedIndicatorAux_one, thickenedIndicator_apply, continuous_thickenedIndicatorAux, thickenedIndicatorAux_one_of_mem_closure, thickenedIndicator.coeFn_eq_comp, thickenedIndicatorAux_le_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_thickenedIndicatorAux 📖	mathematical	Real Real.instLT Real.instZero	Continuous ENNReal UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace ENNReal.instTopologicalSpace thickenedIndicatorAux	—	Continuous.comp ENNReal.continuous_nnreal_sub ENNReal.continuous_div_const Metric.continuous_infEDist
indicator_cthickening_eventually_eq_indicator_closure 📖	mathematical	—	Filter.Eventually Real Set.indicator Metric.cthickening closure UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace nhds PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	—	Filter.mp_mem Filter.univ_mem Filter.univ_mem' Metric.closure_subset_cthickening Set.indicator_of_mem Metric.eventually_notMem_cthickening_of_infEDist_pos Set.indicator_of_notMem
indicator_le_thickenedIndicator 📖	mathematical	Real Real.instLT Real.instZero	Pi.hasLe NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal Set.indicator instZeroNNReal instOneNNReal DFunLike.coe BoundedContinuousFunction UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace instPseudoMetricSpaceNNReal BoundedContinuousFunction.instFunLike thickenedIndicator	—	Set.indicator_of_mem thickenedIndicator_one Set.indicator_of_notMem NNReal.instCanonicallyOrderedAdd
indicator_le_thickenedIndicatorAux 📖	mathematical	—	Pi.hasLe ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Set.indicator instZeroENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal thickenedIndicatorAux	—	Set.indicator_of_mem thickenedIndicatorAux_one Set.indicator_of_notMem ENNReal.instCanonicallyOrderedAdd
indicator_thickening_eventually_eq_indicator_closure 📖	mathematical	—	Filter.Eventually Real Set.indicator Metric.thickening closure UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace nhdsWithin PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero Set.Ioi Real.instPreorder	—	Filter.mp_mem self_mem_nhdsWithin Filter.univ_mem' Set.indicator_of_mem Metric.closure_subset_thickening Metric.eventually_notMem_thickening_of_infEDist_pos mem_nhdsWithin_of_mem_nhds Set.indicator_of_notMem
lipschitzWith_thickenedIndicator 📖	mathematical	Real Real.instLT Real.instZero	LipschitzWith NNReal EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace instMetricSpaceNNReal NNReal.instInv Real.toNNReal DFunLike.coe BoundedContinuousFunction UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace instPseudoMetricSpaceNNReal BoundedContinuousFunction.instFunLike thickenedIndicator	—	edist_dist ENNReal.toReal_sub_of_le thickenedIndicatorAux_mono_infEDist ne_top_of_lt thickenedIndicatorAux_lt_top ENNReal.abs_toReal ENNReal.ofReal_toReal ENNReal.coe_inv ENNReal.ofReal.eq_1 div_eq_mul_inv ENNReal.sub_sub_sub_cancel_left ENNReal.one_ne_top le_refl ENNReal.sub_mul mul_comm PseudoEMetricSpace.edist_comm mul_le_mul_right IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid ENNReal.instOrderedSub Metric.infEDist_le_edist_add_infEDist tsub_eq_zero_of_le ENNReal.instCanonicallyOrderedAdd LT.lt.le not_le add_zero add_mul Distrib.rightDistribClass mul_le_mul_left covariant_swap_mul_of_covariant_mul le_of_not_ge
mulIndicator_cthickening_eventually_eq_mulIndicator_closure 📖	mathematical	—	Filter.Eventually Real Set.mulIndicator Metric.cthickening closure UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace nhds PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	—	Filter.mp_mem Filter.univ_mem Filter.univ_mem' Metric.closure_subset_cthickening Set.mulIndicator_of_mem Metric.eventually_notMem_cthickening_of_infEDist_pos Set.mulIndicator_of_notMem
mulIndicator_thickening_eventually_eq_mulIndicator_closure 📖	mathematical	—	Filter.Eventually Real Set.mulIndicator Metric.thickening closure UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace nhdsWithin PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero Set.Ioi Real.instPreorder	—	Filter.mp_mem self_mem_nhdsWithin Filter.univ_mem' Set.mulIndicator_of_mem Metric.closure_subset_thickening Metric.eventually_notMem_thickening_of_infEDist_pos mem_nhdsWithin_of_mem_nhds Set.mulIndicator_of_notMem
one_le_thickenedIndicator_apply 📖	mathematical	Real Real.instLT Real.instZero Set Set.instMembership	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal instOneNNReal DFunLike.coe BoundedContinuousFunction UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace instPseudoMetricSpaceNNReal BoundedContinuousFunction.instFunLike thickenedIndicator	—	one_le_thickenedIndicator_apply' subset_closure
one_le_thickenedIndicator_apply' 📖	mathematical	Real Real.instLT Real.instZero Set Set.instMembership closure UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal instOneNNReal DFunLike.coe BoundedContinuousFunction instPseudoMetricSpaceNNReal BoundedContinuousFunction.instFunLike thickenedIndicator	—	thickenedIndicator_one_of_mem_closure le_refl
tendsto_indicator_cthickening_indicator_closure 📖	mathematical	—	Filter.Tendsto Real Set.indicator Metric.cthickening nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero Pi.topologicalSpace closure PseudoEMetricSpace.toUniformSpace	—	tendsto_pi_nhds Filter.tendsto_congr' indicator_cthickening_eventually_eq_indicator_closure tendsto_const_nhds
tendsto_indicator_thickening_indicator_closure 📖	mathematical	—	Filter.Tendsto Real Set.indicator Metric.thickening nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero Set.Ioi Real.instPreorder nhds Pi.topologicalSpace closure PseudoEMetricSpace.toUniformSpace	—	tendsto_pi_nhds Filter.tendsto_congr' indicator_thickening_eventually_eq_indicator_closure tendsto_const_nhds
tendsto_mulIndicator_cthickening_mulIndicator_closure 📖	mathematical	—	Filter.Tendsto Real Set.mulIndicator Metric.cthickening nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero Pi.topologicalSpace closure PseudoEMetricSpace.toUniformSpace	—	tendsto_pi_nhds Filter.tendsto_congr' mulIndicator_cthickening_eventually_eq_mulIndicator_closure tendsto_const_nhds
tendsto_mulIndicator_thickening_mulIndicator_closure 📖	mathematical	—	Filter.Tendsto Real Set.mulIndicator Metric.thickening nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero Set.Ioi Real.instPreorder nhds Pi.topologicalSpace closure PseudoEMetricSpace.toUniformSpace	—	tendsto_pi_nhds Filter.tendsto_congr' mulIndicator_thickening_eventually_eq_mulIndicator_closure tendsto_const_nhds
thickenedIndicatorAux_closure_eq 📖	mathematical	—	thickenedIndicatorAux closure UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace	—	Metric.infEDist_closure
thickenedIndicatorAux_le_one 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder thickenedIndicatorAux AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	tsub_le_self ENNReal.instCanonicallyOrderedAdd ENNReal.instOrderedSub
thickenedIndicatorAux_lt_top 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder thickenedIndicatorAux Top.top instTopENNReal	—	lt_of_le_of_lt thickenedIndicatorAux_le_one ENNReal.one_lt_top
thickenedIndicatorAux_mono 📖	mathematical	Real Real.instLE	Pi.hasLe ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder thickenedIndicatorAux	—	tsub_le_tsub ENNReal.instOrderedSub IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid Eq.le ENNReal.div_le_div ENNReal.ofReal_le_ofReal
thickenedIndicatorAux_mono_infEDist 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Metric.infEDist	thickenedIndicatorAux	—	le_total ENNReal.sub_le_sub_iff_left ENNReal.div_le_div le_refl tsub_eq_zero_of_le ENNReal.instCanonicallyOrderedAdd ENNReal.instOrderedSub LE.le.trans
thickenedIndicatorAux_mono_infEdist 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Metric.infEDist	thickenedIndicatorAux	—	thickenedIndicatorAux_mono_infEDist
thickenedIndicatorAux_one 📖	mathematical	Set Set.instMembership	thickenedIndicatorAux ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	Metric.infEDist_zero_of_mem ENNReal.zero_div tsub_zero ENNReal.instOrderedSub
thickenedIndicatorAux_one_of_mem_closure 📖	mathematical	Set Set.instMembership closure UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace	thickenedIndicatorAux ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	thickenedIndicatorAux_closure_eq thickenedIndicatorAux_one
thickenedIndicatorAux_subset 📖	mathematical	Set Set.instHasSubset	Pi.hasLe ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder thickenedIndicatorAux	—	tsub_le_tsub ENNReal.instOrderedSub IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid Eq.le ENNReal.div_le_div Metric.infEDist_anti
thickenedIndicatorAux_tendsto_indicator_closure 📖	mathematical	Filter.Tendsto Real Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	thickenedIndicatorAux Pi.topologicalSpace ENNReal ENNReal.instTopologicalSpace Set.indicator instZeroENNReal closure PseudoEMetricSpace.toUniformSpace AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	tendsto_pi_nhds thickenedIndicatorAux_one_of_mem_closure Set.indicator_of_mem tendsto_const_nhds Set.indicator_of_notMem Metric.exists_real_pos_lt_infEDist_of_notMem_closure dist_zero_right instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Metric.tendsto_nhds tendsto_atTop_of_eventually_const LT.lt.le le_antisymm LE.le.trans thickenedIndicatorAux_mono lt_of_abs_lt Eq.le thickenedIndicatorAux_zero bot_le
thickenedIndicatorAux_zero 📖	mathematical	Real Real.instLT Real.instZero Set Set.instMembership Metric.thickening	thickenedIndicatorAux ENNReal instZeroENNReal	—	le_antisymm tsub_le_tsub ENNReal.instOrderedSub IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid Eq.le ENNReal.div_le_div not_lt Set.mem_setOf_eq Metric.thickening.eq_1 bot_eq_zero' ENNReal.instCanonicallyOrderedAdd tsub_self ENNReal.div_self ne_of_gt ENNReal.ofReal_pos ENNReal.ofReal_ne_top bot_le
thickenedIndicator_apply 📖	mathematical	Real Real.instLT Real.instZero	DFunLike.coe BoundedContinuousFunction NNReal UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace instPseudoMetricSpaceNNReal BoundedContinuousFunction.instFunLike thickenedIndicator ENNReal.toNNReal thickenedIndicatorAux	—	—
thickenedIndicator_le_one 📖	mathematical	Real Real.instLT Real.instZero	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal DFunLike.coe BoundedContinuousFunction UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace instPseudoMetricSpaceNNReal BoundedContinuousFunction.instFunLike thickenedIndicator instOneNNReal	—	thickenedIndicator.coeFn_eq_comp ENNReal.toNNReal_le_toNNReal ne_top_of_lt thickenedIndicatorAux_lt_top ENNReal.one_ne_top thickenedIndicatorAux_le_one
thickenedIndicator_mono 📖	mathematical	Real Real.instLT Real.instZero Real.instLE	Pi.hasLe NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal DFunLike.coe BoundedContinuousFunction UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace instPseudoMetricSpaceNNReal BoundedContinuousFunction.instFunLike thickenedIndicator	—	ENNReal.toNNReal_le_toNNReal ne_top_of_lt thickenedIndicatorAux_lt_top thickenedIndicatorAux_mono
thickenedIndicator_mono_infEDist 📖	mathematical	Real Real.instLT Real.instZero ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Metric.infEDist	NNReal instPartialOrderNNReal DFunLike.coe BoundedContinuousFunction UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace instPseudoMetricSpaceNNReal BoundedContinuousFunction.instFunLike thickenedIndicator	—	ENNReal.toNNReal_mono ne_top_of_lt thickenedIndicatorAux_lt_top thickenedIndicatorAux_mono_infEDist
thickenedIndicator_mono_infEdist 📖	mathematical	Real Real.instLT Real.instZero ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Metric.infEDist	NNReal instPartialOrderNNReal DFunLike.coe BoundedContinuousFunction UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace instPseudoMetricSpaceNNReal BoundedContinuousFunction.instFunLike thickenedIndicator	—	thickenedIndicator_mono_infEDist
thickenedIndicator_one 📖	mathematical	Real Real.instLT Real.instZero Set Set.instMembership	DFunLike.coe BoundedContinuousFunction NNReal UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace instPseudoMetricSpaceNNReal BoundedContinuousFunction.instFunLike thickenedIndicator instOneNNReal	—	thickenedIndicator_one_of_mem_closure subset_closure
thickenedIndicator_one_of_mem_closure 📖	mathematical	Real Real.instLT Real.instZero Set Set.instMembership closure UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace	DFunLike.coe BoundedContinuousFunction NNReal instPseudoMetricSpaceNNReal BoundedContinuousFunction.instFunLike thickenedIndicator instOneNNReal	—	thickenedIndicator_apply thickenedIndicatorAux_one_of_mem_closure ENNReal.toNNReal_one
thickenedIndicator_subset 📖	mathematical	Real Real.instLT Real.instZero Set Set.instHasSubset	Pi.hasLe NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal DFunLike.coe BoundedContinuousFunction UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace instPseudoMetricSpaceNNReal BoundedContinuousFunction.instFunLike thickenedIndicator	—	ENNReal.toNNReal_le_toNNReal ne_top_of_lt thickenedIndicatorAux_lt_top thickenedIndicatorAux_subset
thickenedIndicator_tendsto_indicator_closure 📖	mathematical	Real Real.instLT Real.instZero Filter.Tendsto Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	DFunLike.coe BoundedContinuousFunction NNReal PseudoEMetricSpace.toUniformSpace instPseudoMetricSpaceNNReal BoundedContinuousFunction.instFunLike thickenedIndicator Pi.topologicalSpace NNReal.instTopologicalSpace Set.indicator instZeroNNReal closure instOneNNReal	—	thickenedIndicatorAux_tendsto_indicator_closure tendsto_pi_nhds Set.comp_indicator_const ENNReal.toNNReal_zero Filter.Tendsto.comp ENNReal.tendsto_toNNReal Set.indicator_of_mem Set.indicator_of_notMem
thickenedIndicator_zero 📖	mathematical	Real Real.instLT Real.instZero Set Set.instMembership Metric.thickening	DFunLike.coe BoundedContinuousFunction NNReal UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace instPseudoMetricSpaceNNReal BoundedContinuousFunction.instFunLike thickenedIndicator instZeroNNReal	—	thickenedIndicator_apply thickenedIndicatorAux_zero ENNReal.toNNReal_zero

thickenedIndicator

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeFn_eq_comp 📖	mathematical	Real Real.instLT Real.instZero	DFunLike.coe BoundedContinuousFunction NNReal UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace instPseudoMetricSpaceNNReal BoundedContinuousFunction.instFunLike thickenedIndicator ENNReal ENNReal.toNNReal thickenedIndicatorAux	—	—

---

← Back to Index