Thickening

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

Statistics

Metric	Count
Definitions `cthickening`, `thickening`	2
Theorems `cthickening`, `thickening`, `exists_cthickenings`, `exists_thickenings`, `of_cthickening_subset_self`, `of_thickening_subset_self`, `cthickening_eq_biUnion_closedBall`, `cthickening`, `cthickening_eq_biUnion_closedBall`, `exists_cthickening_subset_open`, `exists_isCompact_cthickening`, `exists_thickening_image_subset`, `exists_thickening_subset_open`, `ball_subset_thickening`, `closedBall_subset_cthickening`, `closedBall_subset_cthickening_singleton`, `closure_eq_iInter_cthickening`, `closure_eq_iInter_cthickening'`, `closure_eq_iInter_thickening`, `closure_eq_iInter_thickening'`, `closure_subset_cthickening`, `closure_subset_thickening`, `closure_thickening_subset_cthickening`, `cthickening_closure`, `cthickening_cthickening_subset`, `cthickening_empty`, `cthickening_eq_biUnion_closedBall`, `cthickening_eq_iInter_cthickening`, `cthickening_eq_iInter_cthickening'`, `cthickening_eq_iInter_thickening`, `cthickening_eq_iInter_thickening'`, `cthickening_eq_iInter_thickening''`, `cthickening_eq_preimage_infEDist`, `cthickening_eq_preimage_infEdist`, `cthickening_max_zero`, `cthickening_mem_nhdsSet`, `cthickening_mono`, `cthickening_of_nonpos`, `cthickening_singleton`, `cthickening_subset_iUnion_closedBall_of_lt`, `cthickening_subset_of_subset`, `cthickening_subset_thickening`, `cthickening_subset_thickening'`, `cthickening_thickening_subset`, `cthickening_union`, `cthickening_zero`, `diam_cthickening_le`, `diam_thickening_le`, `ediam_cthickening_le`, `ediam_thickening_le`, `eventually_notMem_cthickening_of_infEDist_pos`, `eventually_notMem_cthickening_of_infEdist_pos`, `eventually_notMem_thickening_of_infEDist_pos`, `eventually_notMem_thickening_of_infEdist_pos`, `frontier_cthickening_disjoint`, `frontier_cthickening_subset`, `frontier_thickening_disjoint`, `frontier_thickening_subset`, `hasBasis_nhdsSet_cthickening`, `hasBasis_nhdsSet_thickening`, `infEDist_le_infEDist_cthickening_add`, `infEDist_le_infEDist_thickening_add`, `infEdist_le_infEdist_cthickening_add`, `infEdist_le_infEdist_thickening_add`, `isClosed_cthickening`, `isOpen_thickening`, `mem_cthickening_iff`, `mem_cthickening_of_dist_le`, `mem_cthickening_of_edist_le`, `mem_thickening_iff`, `mem_thickening_iff_exists_edist_lt`, `mem_thickening_iff_infDist_lt`, `mem_thickening_iff_infEDist_lt`, `mem_thickening_iff_infEdist_lt`, `self_subset_cthickening`, `self_subset_thickening`, `subset_compl_thickening_compl_thickening_self`, `thickening_ball`, `thickening_biUnion`, `thickening_closure`, `thickening_compl_thickening_self_subset_compl`, `thickening_cthickening_subset`, `thickening_empty`, `thickening_eq_biUnion_ball`, `thickening_eq_empty_iff`, `thickening_eq_empty_iff_of_pos`, `thickening_eq_preimage_infEDist`, `thickening_eq_preimage_infEdist`, `thickening_iUnion`, `thickening_mem_nhdsSet`, `thickening_mono`, `thickening_nonempty_iff`, `thickening_nonempty_iff_of_pos`, `thickening_of_nonpos`, `thickening_singleton`, `thickening_subset_cthickening`, `thickening_subset_cthickening_of_le`, `thickening_subset_interior_cthickening`, `thickening_subset_of_subset`, `thickening_thickening_subset`, `thickening_union`	101
Total	103

Bornology.IsBounded

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cthickening` 📖	mathematical	`Bornology.IsBounded` `PseudoMetricSpace.toBornology`	`Metric.cthickening` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`thickening` `subset` `Metric.cthickening_subset_thickening'` `LT.lt.trans_le` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `le_max_right` `lt_add_one` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `le_max_left`
`thickening` 📖	mathematical	`Bornology.IsBounded` `PseudoMetricSpace.toBornology`	`Metric.thickening` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`Set.eq_empty_or_nonempty` `Metric.thickening_empty` `Metric.isBounded_iff_subset_closedBall` `Metric.dist_le_infDist_add_diam` `le_imp_le_of_le_of_le` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `le_of_lt` `Metric.mem_thickening_iff_infDist_lt` `le_refl`

Disjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_cthickenings` 📖	mathematical	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `IsCompact` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	`Real` `Real.instLT` `Real.instZero` `Metric.cthickening`	—	`exists_thickenings` `Nat.instAtLeastTwoHAddOfNat` `half_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `mono` `Metric.cthickening_subset_thickening'` `half_lt_self`
`exists_thickenings` 📖	mathematical	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `IsCompact` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	`Real` `Real.instLT` `Real.instZero` `Metric.thickening`	—	`Metric.exists_pos_forall_lt_edist` `Nat.instAtLeastTwoHAddOfNat` `half_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `NNReal.coe_pos` `disjoint_iff_inf_le` `ENNReal.ofReal_coe_nnreal` `NNReal.coe_div` `NNReal.coe_two` `Metric.mem_thickening_iff_exists_edist_lt` `LT.lt.not_ge` `edist_triangle_left` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `LT.lt.le` `ENNReal.coe_add` `add_halves` `CharZero.NeZero.two` `IsStrictOrderedRing.toCharZero` `NNReal.instIsStrictOrderedRing`

IsClopen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_cthickening_subset_self` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Set` `Set.instHasSubset` `Metric.cthickening`	`IsClopen` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`of_thickening_subset_self` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Metric.thickening_subset_cthickening`
`of_thickening_subset_self` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Set` `Set.instHasSubset` `Metric.thickening`	`IsClopen` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`le_antisymm` `Metric.self_subset_thickening` `closure_subset_iff_isClosed` `Metric.closure_eq_iInter_thickening` `LE.le.trans_eq` `Set.biInter_subset_of_mem` `Metric.isOpen_thickening`

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cthickening_eq_biUnion_closedBall` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`Metric.cthickening` `PseudoMetricSpace.toPseudoEMetricSpace` `Set.iUnion` `Set` `Set.instMembership` `Metric.closedBall`	—	`Metric.cthickening_eq_biUnion_closedBall` `closure_eq`

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cthickening` 📖	mathematical	`IsCompact` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	`Metric.cthickening` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`Metric.isCompact_of_isClosed_isBounded` `Metric.isClosed_cthickening` `Bornology.IsBounded.cthickening` `isBounded`
`cthickening_eq_biUnion_closedBall` 📖	mathematical	`IsCompact` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real` `Real.instLE` `Real.instZero`	`Metric.cthickening` `PseudoMetricSpace.toPseudoEMetricSpace` `Set.iUnion` `Set` `Set.instMembership` `Metric.closedBall`	—	`Set.eq_empty_or_nonempty` `Metric.cthickening_empty` `Set.biUnion_empty` `Set.Subset.antisymm` `exists_infEDist_eq_edist` `LE.le.trans` `le_of_eq` `ENNReal.ofReal_le_ofReal_iff` `edist_dist` `Set.mem_biUnion` `Set.iUnion₂_subset` `Metric.closedBall_subset_cthickening`
`exists_cthickening_subset_open` 📖	mathematical	`IsCompact` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `IsOpen` `Set` `Set.instHasSubset`	`Real` `Real.instLT` `Real.instZero` `Metric.cthickening`	—	`Set.disjoint_compl_right_iff_subset` `Disjoint.mono_right` `Metric.self_subset_cthickening` `Disjoint.exists_cthickenings` `HasSubset.Subset.disjoint_compl_right` `IsOpen.isClosed_compl`
`exists_isCompact_cthickening` 📖	mathematical	`IsCompact` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	`Real` `Real.instLT` `Real.instZero` `Metric.cthickening`	—	`exists_compact_superset` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `exists_cthickening_subset_open` `isOpen_interior` `of_isClosed_subset` `Metric.isClosed_cthickening` `HasSubset.Subset.trans` `Set.instIsTransSubset` `interior_subset`
`exists_thickening_image_subset` 📖	mathematical	`IsCompact` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `IsOpen` `ContinuousAt` `Set.MapsTo`	`Real` `Real.instLT` `Real.instZero` `Set` `Filter` `Filter.instMembership` `nhdsSet` `Set.instHasSubset` `Metric.thickening` `Set.image`	—	`induction_on` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `nhdsSet_empty` `Set.image_empty` `Metric.thickening_empty` `nhdsSet_mono` `lt_min` `union_mem_nhdsSet` `Set.image_union` `Metric.thickening_union` `Set.union_subset_union` `Metric.thickening_mono` `Set.union_self` `Set.singleton_subset_iff` `exists_thickening_subset_open` `isCompact_singleton` `Nat.instAtLeastTwoHAddOfNat` `IsOpen.mem_nhds` `Metric.isOpen_thickening` `Metric.self_subset_thickening` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Mathlib.Meta.NormNum.instAtLeastTwo` `inter_mem_nhdsWithin` `interior_mem_nhds` `subset_interior_iff_mem_nhdsSet` `Metric.thickening_subset_of_subset` `Set.image_preimage_subset` `Metric.thickening_thickening_subset` `add_halves` `CharZero.NeZero.two` `IsStrictOrderedRing.toCharZero`
`exists_thickening_subset_open` 📖	mathematical	`IsCompact` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `IsOpen` `Set` `Set.instHasSubset`	`Real` `Real.instLT` `Real.instZero` `Metric.thickening`	—	`exists_cthickening_subset_open` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Metric.thickening_subset_cthickening`

Metric

Definitions

Name	Category	Theorems
`cthickening` 📖	CompOp	99 math math: `cthickening_closure`, `cthickening_mono`, `cthickening_cthickening_subset`, `Disjoint.exists_cthickenings`, `IsCompact.closedBall_mul`, `closure_thickening`, `IsCompact.mul_closedBall_one`, `thickening_subset_cthickening`, `mem_cthickening_iff`, `cthickening_thickening_subset`, `IsCompact.closedBall_zero_add`, `isCover_iff_subset_cthickening`, `Convex.cthickening`, `cthickening_eq_preimage_infEdist`, `mem_cthickening_of_dist_le`, `mem_cthickening_of_edist_le`, `cthickening_eq_iInter_thickening`, `IsCompact.div_closedBall`, `blimsup_cthickening_ae_le_of_eventually_mul_le_aux`, `IsLowerSet.cthickening`, `tendsto_measure_cthickening`, `IsCompact.cthickening_eq_biUnion_closedBall`, `blimsup_cthickening_ae_le_of_eventually_mul_le`, `cthickening_thickening`, `cthickening_zero`, `ediam_cthickening_le`, `IsCompact.mul_closedBall`, `closure_eq_iInter_cthickening`, `neg_cthickening`, `IsCompact.closedBall_one_mul`, `IsCompact.closedBall_div`, `cthickening_eq_preimage_infEDist`, `cthickening_eq_iInter_cthickening'`, `cthickening_eq_biUnion_closedBall`, `IsClosed.cthickening_eq_biUnion_closedBall`, `closure_thickening_subset_cthickening`, `thickening_subset_interior_cthickening`, `cthickening_singleton`, `hasBasis_nhdsSet_cthickening`, `self_subset_cthickening`, `IsCompact.sub_closedBall_zero`, `cthickening_subset_thickening'`, `cthickening_closedBall`, `IsCompact.cthickening`, `cthickening_mem_nhdsSet`, `closure_subset_cthickening`, `cthickening_subset_of_subset`, `cthickening_eq_iInter_thickening'`, `infEdist_le_infEdist_cthickening_add`, `indicator_cthickening_eventually_eq_indicator_closure`, `IsCompact.closedBall_one_div`, `cthickening_eq_iInter_cthickening`, `IsCompact.sub_closedBall`, `infEdist_cthickening`, `cthickening_eq_iInter_thickening''`, `thickening_cthickening`, `IsCompact.closedBall_zero_sub`, `infEDist_cthickening`, `tendsto_measure_cthickening_of_isClosed`, `frontier_cthickening_disjoint`, `cthickening_max_zero`, `IsCompact.exists_cthickening_subset_open`, `eventually_notMem_cthickening_of_infEdist_pos`, `tendsto_indicator_cthickening_indicator_closure`, `blimsup_cthickening_ae_eq_blimsup_thickening`, `isClosed_cthickening`, `eventually_notMem_cthickening_of_infEDist_pos`, `closure_eq_iInter_cthickening'`, `IsCover.subset_cthickening`, `tendsto_measure_cthickening_of_isCompact`, `infEDist_le_infEDist_cthickening_add`, `cthickening_of_nonpos`, `IsUpperSet.cthickening'`, `cthickening_cthickening`, `IsCompact.closedBall_add`, `inv_cthickening`, `cthickening_subset_thickening`, `cthickening_ball`, `blimsup_cthickening_mul_ae_eq`, `frontier_cthickening_subset`, `Bornology.IsBounded.cthickening`, `mulIndicator_cthickening_eventually_eq_mulIndicator_closure`, `IsCompact.div_closedBall_one`, `Complex.exists_cthickening_tendstoUniformlyOn`, `cthickening_union`, `IsCompact.exists_isCompact_cthickening`, `closedBall_subset_cthickening_singleton`, `IsCompact.add_closedBall_zero`, `thickening_cthickening_subset`, `tendsto_mulIndicator_cthickening_mulIndicator_closure`, `thickening_subset_cthickening_of_le`, `IsLowerSet.cthickening'`, `cthickening_subset_iUnion_closedBall_of_lt`, `diam_cthickening_le`, `closedBall_subset_cthickening`, `IsCompact.add_closedBall`, `IsUpperSet.cthickening`, `cthickening_empty`, `IsCompact.closedBall_sub`
`thickening` 📖	CompOp	102 math math: `ball_sub`, `thickening_eq_biUnion_ball`, `mul_ball`, `mem_thickening_iff_infEDist_lt`, `infEdist_thickening`, `closure_thickening`, `thickening_subset_cthickening`, `ball_div_one`, `IsCompact.exists_thickening_image_subset`, `ediam_thickening_le`, `cthickening_thickening_subset`, `indicator_thickening_eventually_eq_indicator_closure`, `ball_mul_one`, `ball_subset_thickening`, `infEdist_le_infEdist_thickening_add`, `blimsup_thickening_mul_ae_eq_aux`, `thickening_eq_preimage_infEDist`, `isOpen_thickening`, `mem_thickening_iff`, `thickening_biUnion`, `ball_mul`, `cthickening_eq_iInter_thickening`, `thickening_empty`, `ball_add_zero`, `subset_compl_thickening_compl_thickening_self`, `neg_thickening`, `frontier_thickening_subset`, `diam_thickening_le`, `cthickening_thickening`, `div_ball`, `thickening_eq_empty_iff`, `IsUpperSet.thickening'`, `ball_sub_zero`, `MeasureTheory.exists_null_frontier_thickening`, `add_ball_zero`, `tendsto_measure_thickening`, `thickening_mono`, `ball_div`, `thickening_iUnion`, `thickening_closedBall`, `closure_thickening_subset_cthickening`, `thickening_subset_interior_cthickening`, `cthickening_subset_thickening'`, `IsUpperSet.thickening`, `thickening_ball`, `mem_thickening_iff_infDist_lt`, `thickening_compl_thickening_self_subset_compl`, `thickening_nonempty_iff_of_pos`, `thickening_of_nonpos`, `mem_thickening_iff_exists_edist_lt`, `infEDist_thickening`, `cthickening_eq_iInter_thickening'`, `frontier_thickening_disjoint`, `thickening_eq_empty_iff_of_pos`, `thickening_singleton`, `ball_add`, `cthickening_eq_iInter_thickening''`, `thickening_thickening`, `thickening_cthickening`, `mem_thickening_iff_infEdist_lt`, `add_ball`, `hasBasis_nhdsSet_thickening`, `self_subset_thickening`, `closure_eq_iInter_thickening'`, `div_ball_one`, `infEDist_le_infEDist_thickening_add`, `mul_ball_one`, `tendsto_mulIndicator_thickening_mulIndicator_closure`, `MeasureTheory.BoundedContinuousFunction.integral_le_of_levyProkhorovEDist_lt`, `IsLowerSet.thickening`, `MeasureTheory.exists_null_frontiers_thickening`, `eventually_notMem_thickening_of_infEdist_pos`, `MeasureTheory.left_measure_le_of_levyProkhorovEDist_lt`, `blimsup_cthickening_ae_eq_blimsup_thickening`, `eventually_notMem_thickening_of_infEDist_pos`, `thickening_nonempty_iff`, `blimsup_thickening_mul_ae_eq`, `sub_ball_zero`, `MeasureTheory.right_measure_le_of_levyProkhorovEDist_lt`, `IsCompact.exists_thickening_subset_open`, `cthickening_subset_thickening`, `thickening_union`, `Bornology.IsBounded.thickening`, `thickening_mem_nhdsSet`, `IsLowerSet.thickening'`, `thickening_subset_of_subset`, `thickening_ball`, `closure_subset_thickening`, `mulIndicator_thickening_eventually_eq_mulIndicator_closure`, `Disjoint.exists_thickenings`, `inv_thickening`, `thickening_cthickening_subset`, `tendsto_measure_thickening_of_isClosed`, `thickening_subset_cthickening_of_le`, `sub_ball`, `Convex.thickening`, `MeasureTheory.tendsto_integral_meas_thickening_le`, `tendsto_indicator_thickening_indicator_closure`, `thickening_thickening_subset`, `closure_eq_iInter_thickening`, `thickening_eq_preimage_infEdist`, `thickening_closure`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ball_subset_thickening` 📖	mathematical	`Set` `Set.instMembership`	`Set.instHasSubset` `ball` `thickening` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`Set.Subset.trans` `thickening_singleton` `Set.instReflSubset` `thickening_subset_of_subset` `Set.singleton_subset_iff`
`closedBall_subset_cthickening` 📖	mathematical	`Set` `Set.instMembership`	`Set.instHasSubset` `closedBall` `cthickening` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `closedBall_subset_cthickening_singleton` `cthickening_subset_of_subset`
`closedBall_subset_cthickening_singleton` 📖	mathematical	—	`Set` `Set.instHasSubset` `closedBall` `cthickening` `PseudoMetricSpace.toPseudoEMetricSpace` `Set.instSingletonSet`	—	`lt_or_ge` `closedBall_eq_empty` `cthickening_singleton`
`closure_eq_iInter_cthickening` 📖	mathematical	—	`closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `Set.iInter` `Real` `Real.instLT` `Real.instZero` `cthickening`	—	`cthickening_zero` `cthickening_eq_iInter_cthickening`
`closure_eq_iInter_cthickening'` 📖	mathematical	`Set.Nonempty` `Real` `Set` `Set.instInter` `Set.Ioc` `Real.instPreorder` `Real.instZero`	`closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `Set.iInter` `Set.instMembership` `cthickening`	—	`cthickening_zero` `cthickening_eq_iInter_cthickening'` `Set.not_subset` `Set.Subset.antisymm` `Set.subset_iInter₂` `closure_subset_cthickening` `cthickening_of_nonpos` `not_lt` `Set.mem_Ioi` `Set.biInter_subset_of_mem`
`closure_eq_iInter_thickening` 📖	mathematical	—	`closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `Set.iInter` `Real` `Real.instLT` `Real.instZero` `thickening`	—	`cthickening_zero` `cthickening_eq_iInter_thickening` `Eq.ge`
`closure_eq_iInter_thickening'` 📖	mathematical	`Set` `Real` `Set.instHasSubset` `Set.Ioi` `Real.instPreorder` `Real.instZero` `Set.Nonempty` `Set.instInter` `Set.Ioc`	`closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `Set.iInter` `Set.instMembership` `thickening`	—	`cthickening_zero` `cthickening_eq_iInter_thickening'` `le_rfl`
`closure_subset_cthickening` 📖	mathematical	—	`Set` `Set.instHasSubset` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `cthickening`	—	`cthickening_of_nonpos` `min_le_right` `cthickening_mono` `min_le_left`
`closure_subset_thickening` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Set` `Set.instHasSubset` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `thickening`	—	`cthickening_zero` `cthickening_subset_thickening'`
`closure_thickening_subset_cthickening` 📖	mathematical	—	`Set` `Set.instHasSubset` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `thickening` `cthickening`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `closure_mono` `thickening_subset_cthickening` `IsClosed.closure_subset` `isClosed_cthickening`
`cthickening_closure` 📖	mathematical	—	`cthickening` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`infEDist_closure`
`cthickening_cthickening_subset` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`Set` `Set.instHasSubset` `cthickening` `Real.instAdd`	—	`ENNReal.ofReal_add` `LE.le.trans` `infEDist_le_infEDist_cthickening_add` `le_imp_le_of_le_of_le` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `le_refl`
`cthickening_empty` 📖	mathematical	—	`cthickening` `Set` `Set.instEmptyCollection`	—	`infEDist_empty`
`cthickening_eq_biUnion_closedBall` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`cthickening` `PseudoMetricSpace.toPseudoEMetricSpace` `Set.iUnion` `Set` `Set.instMembership` `closure` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `closedBall`	—	`Set.eq_empty_or_nonempty` `cthickening_empty` `Set.iUnion_congr_Prop` `closure_empty` `Set.biUnion_empty` `cthickening_closure` `Set.Subset.antisymm` `IsClosed.exists_infDist_eq_dist` `isClosed_closure` `closure_nonempty_iff` `ENNReal.ofReal_le_ofReal_iff` `LE.le.trans` `Eq.le` `ENNReal.ofReal_toReal_le` `Set.mem_biUnion` `Set.iUnion₂_subset` `closedBall_subset_cthickening`
`cthickening_eq_iInter_cthickening` 📖	mathematical	—	`cthickening` `Set.iInter` `Real` `Real.instLT`	—	`cthickening_eq_iInter_cthickening'` `Eq.subset` `Set.instReflSubset` `Set.inter_eq_right` `Set.Ioc_subset_Ioi_self` `Set.nonempty_Ioc`
`cthickening_eq_iInter_cthickening'` 📖	mathematical	`Set` `Real` `Set.instHasSubset` `Set.Ioi` `Real.instPreorder` `Set.Nonempty` `Set.instInter` `Set.Ioc`	`cthickening` `Set.iInter` `Set.instMembership`	—	`Set.Subset.antisymm` `Set.subset_iInter₂` `cthickening_mono` `le_of_lt` `ENNReal.le_of_forall_pos_le_add` `lt_add_of_pos_right` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `NNReal.coe_pos` `LE.le.trans` `ENNReal.ofReal_le_ofReal` `ENNReal.coe_nnreal_eq` `ENNReal.ofReal_add_le`
`cthickening_eq_iInter_thickening` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`cthickening` `Set.iInter` `Real.instLT` `thickening`	—	`cthickening_eq_iInter_thickening'` `Eq.subset` `Set.instReflSubset` `Set.inter_eq_right` `Set.Ioc_subset_Ioi_self` `Set.nonempty_Ioc`
`cthickening_eq_iInter_thickening'` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Set` `Set.instHasSubset` `Set.Ioi` `Real.instPreorder` `Set.Nonempty` `Set.instInter` `Set.Ioc`	`cthickening` `Set.iInter` `Set.instMembership` `thickening`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `Set.subset_iInter₂` `cthickening_subset_thickening'` `lt_of_le_of_lt` `HasSubset.Subset.trans` `Set.instIsTransSubset` `thickening_mono` `cthickening_eq_iInter_cthickening'` `Set.iInter₂_mono` `thickening_subset_cthickening`
`cthickening_eq_iInter_thickening''` 📖	mathematical	—	`cthickening` `Set.iInter` `Real` `Real.instLT` `Real.instMax` `Real.instZero` `thickening`	—	`cthickening_max_zero` `cthickening_eq_iInter_thickening` `le_max_left`
`cthickening_eq_preimage_infEDist` 📖	mathematical	—	`cthickening` `Set.preimage` `ENNReal` `infEDist` `Set.Iic` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofReal`	—	—
`cthickening_eq_preimage_infEdist` 📖	mathematical	—	`cthickening` `Set.preimage` `ENNReal` `infEDist` `Set.Iic` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofReal`	—	`cthickening_eq_preimage_infEDist`
`cthickening_max_zero` 📖	mathematical	—	`cthickening` `Real` `Real.instMax` `Real.instZero`	—	`le_total` `sup_of_le_left` `cthickening_of_nonpos` `sup_of_le_right`
`cthickening_mem_nhdsSet` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Set` `Filter` `Filter.instMembership` `nhdsSet` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `cthickening`	—	`Filter.mem_of_superset` `thickening_mem_nhdsSet` `thickening_subset_cthickening`
`cthickening_mono` 📖	mathematical	`Real` `Real.instLE`	`Set` `Set.instHasSubset` `cthickening`	—	`Set.preimage_mono` `Set.Iic_subset_Iic` `ENNReal.ofReal_le_ofReal`
`cthickening_of_nonpos` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`cthickening` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`Set.ext` `ENNReal.ofReal_eq_zero` `ENNReal.instCanonicallyOrderedAdd`
`cthickening_singleton` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`cthickening` `PseudoMetricSpace.toPseudoEMetricSpace` `Set` `Set.instSingletonSet` `closedBall`	—	`Set.ext` `infEDist_singleton` `edist_dist` `ENNReal.ofReal_le_ofReal_iff`
`cthickening_subset_iUnion_closedBall_of_lt` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Set` `Set.instHasSubset` `cthickening` `PseudoMetricSpace.toPseudoEMetricSpace` `Set.iUnion` `Set.instMembership` `closedBall`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `cthickening_subset_thickening'` `mem_thickening_iff` `Set.mem_iUnion₂` `LT.lt.le`
`cthickening_subset_of_subset` 📖	mathematical	`Set` `Set.instHasSubset`	`cthickening`	—	`le_trans` `infEDist_anti`
`cthickening_subset_thickening` 📖	mathematical	`Real` `Real.instLT` `NNReal.toReal`	`Set` `Set.instHasSubset` `cthickening` `thickening`	—	`LE.le.trans_lt` `Membership.mem.out` `ENNReal.ofReal_lt_ofReal_iff` `lt_of_le_of_lt` `Subtype.prop`
`cthickening_subset_thickening'` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Set` `Set.instHasSubset` `cthickening` `thickening`	—	`lt_of_le_of_lt` `Membership.mem.out` `ENNReal.ofReal_lt_ofReal_iff`
`cthickening_thickening_subset` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`Set` `Set.instHasSubset` `cthickening` `thickening` `Real.instAdd`	—	`le_total` `thickening_of_nonpos` `cthickening_empty` `ENNReal.ofReal_add` `LE.le.trans` `infEDist_le_infEDist_thickening_add` `le_imp_le_of_le_of_le` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `le_refl`
`cthickening_union` 📖	mathematical	—	`cthickening` `Set` `Set.instUnion`	—	`infEDist_union`
`cthickening_zero` 📖	mathematical	—	`cthickening` `Real` `Real.instZero` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`cthickening_of_nonpos` `le_rfl`
`diam_cthickening_le` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`diam` `cthickening` `PseudoMetricSpace.toPseudoEMetricSpace` `Real.instAdd` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `CanLift.prf` `NNReal.canLift` `LE.le.trans_eq` `ENNReal.toReal_le_add'` `ediam_cthickening_le` `top_unique` `ediam_mono` `self_subset_cthickening` `ENNReal.instCharZero` `instIsEmptyFalse` `ENNReal.toReal_mul` `ENNReal.toReal_ofNat`
`diam_thickening_le` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`diam` `thickening` `PseudoMetricSpace.toPseudoEMetricSpace` `Real.instAdd` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `LE.le.trans` `diam_mono` `thickening_subset_cthickening` `Bornology.IsBounded.cthickening` `diam_cthickening_le` `LE.le.eq_or_lt` `thickening_of_nonpos` `diam_empty` `MulZeroClass.mul_zero` `add_zero` `diam_eq_zero_of_unbounded` `Bornology.IsBounded.subset` `self_subset_thickening` `le_of_lt` `Right.add_pos_of_nonneg_of_pos` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `diam_nonneg` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo`
`ediam_cthickening_le` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ediam` `cthickening` `NNReal.toReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Distrib.toMul` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `ENNReal.ofNNReal`	—	`ediam_le` `Nat.instAtLeastTwoHAddOfNat` `ENNReal.le_of_forall_pos_le_add` `ENNReal.coe_lt_coe` `lt_add_of_pos_right` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `NNReal.addLeftMono` `LE.le.trans_lt` `ENNReal.ofReal_coe_nnreal` `mem_cthickening_iff` `infEDist_lt_iff` `edist_triangle_right` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `LT.lt.le` `edist_le_infEDist_add_ediam` `le_imp_le_of_le_of_le` `add_le_add_right` `add_le_add_left` `le_refl` `two_mul` `AddSemigroup.to_isAssociative` `AddCommMagma.to_isCommutative`
`ediam_thickening_le` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ediam` `thickening` `NNReal.toReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Distrib.toMul` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `ENNReal.ofNNReal`	—	`LE.le.trans` `Nat.instAtLeastTwoHAddOfNat` `ediam_mono` `thickening_subset_cthickening` `ediam_cthickening_le`
`eventually_notMem_cthickening_of_infEDist_pos` 📖	mathematical	`Set` `Set.instMembership` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	`Filter.Eventually` `Real` `cthickening` `nhds` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero`	—	`exists_real_pos_lt_infEDist_of_notMem_closure` `Filter.mp_mem` `eventually_lt_nhds` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `Filter.univ_mem'` `LT.lt.trans` `ENNReal.ofReal_lt_ofReal_iff`
`eventually_notMem_cthickening_of_infEdist_pos` 📖	mathematical	`Set` `Set.instMembership` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	`Filter.Eventually` `Real` `cthickening` `nhds` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero`	—	`eventually_notMem_cthickening_of_infEDist_pos`
`eventually_notMem_thickening_of_infEDist_pos` 📖	mathematical	`Set` `Set.instMembership` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	`Filter.Eventually` `Real` `thickening` `nhds` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero`	—	`exists_real_pos_lt_infEDist_of_notMem_closure` `Filter.mp_mem` `eventually_lt_nhds` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `Filter.univ_mem'` `LE.le.trans` `ENNReal.ofReal_le_ofReal` `LT.lt.le`
`eventually_notMem_thickening_of_infEdist_pos` 📖	mathematical	`Set` `Set.instMembership` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	`Filter.Eventually` `Real` `thickening` `nhds` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero`	—	`eventually_notMem_thickening_of_infEDist_pos`
`frontier_cthickening_disjoint` 📖	mathematical	—	`Pairwise` `NNReal` `Function.onFun` `Set` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `frontier` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `cthickening` `NNReal.toReal`	—	`Disjoint.mono` `frontier_cthickening_subset` `Disjoint.preimage` `Set.disjoint_singleton` `ENNReal.ofReal_coe_nnreal`
`frontier_cthickening_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `frontier` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `cthickening` `setOf` `ENNReal` `infEDist` `ENNReal.ofReal`	—	`frontier_le_subset_eq` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `continuous_infEDist` `continuous_const`
`frontier_thickening_disjoint` 📖	mathematical	—	`Pairwise` `Real` `Function.onFun` `Set` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `frontier` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `thickening`	—	`pairwise_disjoint_on` `le_total` `thickening_of_nonpos` `frontier_empty` `Disjoint.mono` `frontier_thickening_subset` `Disjoint.preimage` `Set.disjoint_singleton` `LT.lt.ne` `ENNReal.toReal_ofReal` `LE.le.trans` `LT.lt.le`
`frontier_thickening_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `frontier` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `thickening` `setOf` `ENNReal` `infEDist` `ENNReal.ofReal`	—	`frontier_lt_subset_eq` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `continuous_infEDist` `continuous_const`
`hasBasis_nhdsSet_cthickening` 📖	mathematical	`IsCompact` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	`Filter.HasBasis` `Real` `nhdsSet` `Real.instLT` `Real.instZero` `cthickening`	—	`Filter.HasBasis.to_hasBasis'` `hasBasis_nhdsSet` `IsCompact.exists_cthickening_subset_open` `cthickening_mem_nhdsSet`
`hasBasis_nhdsSet_thickening` 📖	mathematical	`IsCompact` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	`Filter.HasBasis` `Real` `nhdsSet` `Real.instLT` `Real.instZero` `thickening`	—	`Filter.HasBasis.to_hasBasis'` `hasBasis_nhdsSet` `IsCompact.exists_thickening_subset_open` `thickening_mem_nhdsSet`
`infEDist_le_infEDist_cthickening_add` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `infEDist` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `cthickening` `ENNReal.ofReal`	—	`le_of_forall_gt` `ENNReal.instOrderedSub` `LE.le.trans_lt` `infEDist_le_edist_add_infEDist` `LT.lt.trans_eq` `ENNReal.add_lt_add_of_lt_of_le` `LT.lt.ne` `ENNReal.ofReal_lt_top` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `ENNReal.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `LE.le.trans` `le_self_add` `LT.lt.le` `lt_tsub_iff_left`
`infEDist_le_infEDist_thickening_add` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `infEDist` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `thickening` `ENNReal.ofReal`	—	`LE.le.trans` `infEDist_le_infEDist_cthickening_add` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `infEDist_anti` `thickening_subset_cthickening`
`infEdist_le_infEdist_cthickening_add` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `infEDist` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `cthickening` `ENNReal.ofReal`	—	`infEDist_le_infEDist_cthickening_add`
`infEdist_le_infEdist_thickening_add` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `infEDist` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `thickening` `ENNReal.ofReal`	—	`infEDist_le_infEDist_thickening_add`
`isClosed_cthickening` 📖	mathematical	—	`IsClosed` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `cthickening`	—	`IsClosed.preimage` `continuous_infEDist` `isClosed_Iic` `instClosedIicTopology` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology`
`isOpen_thickening` 📖	mathematical	—	`IsOpen` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `thickening`	—	`Continuous.isOpen_preimage` `continuous_infEDist` `isOpen_Iio` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology`
`mem_cthickening_iff` 📖	mathematical	—	`Set` `Set.instMembership` `cthickening` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `infEDist` `ENNReal.ofReal`	—	—
`mem_cthickening_of_dist_le` 📖	mathematical	`Set` `Set.instMembership` `Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist`	`cthickening` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`mem_cthickening_of_edist_le` `edist_dist` `ENNReal.ofReal_le_ofReal`
`mem_cthickening_of_edist_le` 📖	mathematical	`Set` `Set.instMembership` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist` `ENNReal.ofReal`	`cthickening`	—	`LE.le.trans` `infEDist_le_edist_of_mem`
`mem_thickening_iff` 📖	mathematical	—	`Set` `Set.instMembership` `thickening` `PseudoMetricSpace.toPseudoEMetricSpace` `Real` `Real.instLT` `Dist.dist` `PseudoMetricSpace.toDist`	—	`dist_edist` `ENNReal.lt_ofReal_iff_toReal_lt` `edist_ne_top`
`mem_thickening_iff_exists_edist_lt` 📖	mathematical	—	`Set` `Set.instMembership` `thickening` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist` `ENNReal.ofReal`	—	`infEDist_lt_iff`
`mem_thickening_iff_infDist_lt` 📖	mathematical	`Set.Nonempty`	`Set` `Set.instMembership` `thickening` `PseudoMetricSpace.toPseudoEMetricSpace` `Real` `Real.instLT` `infDist`	—	`ENNReal.lt_ofReal_iff_toReal_lt` `infEDist_ne_top`
`mem_thickening_iff_infEDist_lt` 📖	mathematical	—	`Set` `Set.instMembership` `thickening` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `infEDist` `ENNReal.ofReal`	—	—
`mem_thickening_iff_infEdist_lt` 📖	mathematical	—	`Set` `Set.instMembership` `thickening` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `infEDist` `ENNReal.ofReal`	—	`mem_thickening_iff_infEDist_lt`
`self_subset_cthickening` 📖	mathematical	—	`Set` `Set.instHasSubset` `cthickening`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `subset_closure` `closure_subset_cthickening`
`self_subset_thickening` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Set` `Set.instHasSubset` `thickening`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `subset_closure` `closure_subset_thickening`
`subset_compl_thickening_compl_thickening_self` 📖	mathematical	—	`Set` `Set.instHasSubset` `Compl.compl` `Set.instCompl` `thickening`	—	`le_infEDist` `PseudoEMetricSpace.edist_comm` `le_trans` `infEDist_le_edist_of_mem`
`thickening_ball` 📖	mathematical	—	`Set` `Set.instHasSubset` `thickening` `PseudoMetricSpace.toPseudoEMetricSpace` `ball` `Real` `Real.instAdd`	—	`thickening_singleton` `thickening_thickening_subset`
`thickening_biUnion` 📖	mathematical	—	`thickening` `Set.iUnion` `Set` `Set.instMembership`	—	`thickening_iUnion`
`thickening_closure` 📖	mathematical	—	`thickening` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`infEDist_closure`
`thickening_compl_thickening_self_subset_compl` 📖	mathematical	—	`Set` `Set.instHasSubset` `thickening` `Compl.compl` `Set.instCompl`	—	`Set.compl_subset_compl` `compl_compl` `subset_compl_thickening_compl_thickening_self`
`thickening_cthickening_subset` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`Set` `Set.instHasSubset` `thickening` `cthickening` `Real.instAdd`	—	`le_total` `thickening_of_nonpos` `ENNReal.ofReal_add` `LE.le.trans_lt` `infEDist_le_edist_add_infEDist` `ENNReal.add_lt_add_of_lt_of_le` `LT.lt.ne` `ENNReal.ofReal_lt_top`
`thickening_empty` 📖	mathematical	—	`thickening` `Set` `Set.instEmptyCollection`	—	`infEDist_empty`
`thickening_eq_biUnion_ball` 📖	mathematical	—	`thickening` `PseudoMetricSpace.toPseudoEMetricSpace` `Set.iUnion` `Set` `Set.instMembership` `ball`	—	`Set.ext` `mem_thickening_iff`
`thickening_eq_empty_iff` 📖	mathematical	—	`thickening` `Set` `Set.instEmptyCollection` `Real` `Real.instLE` `Real.instZero`	—	`lt_or_ge` `thickening_of_nonpos`
`thickening_eq_empty_iff_of_pos` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`thickening` `Set` `Set.instEmptyCollection`	—	`Set.subset_eq_empty` `self_subset_thickening` `thickening_empty`
`thickening_eq_preimage_infEDist` 📖	mathematical	—	`thickening` `Set.preimage` `ENNReal` `infEDist` `Set.Iio` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofReal`	—	—
`thickening_eq_preimage_infEdist` 📖	mathematical	—	`thickening` `Set.preimage` `ENNReal` `infEDist` `Set.Iio` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofReal`	—	`thickening_eq_preimage_infEDist`
`thickening_iUnion` 📖	mathematical	—	`thickening` `Set.iUnion`	—	`infEDist_iUnion` `Set.setOf_exists`
`thickening_mem_nhdsSet` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Set` `Filter` `Filter.instMembership` `nhdsSet` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `thickening`	—	`IsOpen.mem_nhdsSet` `isOpen_thickening` `self_subset_thickening`
`thickening_mono` 📖	mathematical	`Real` `Real.instLE`	`Set` `Set.instHasSubset` `thickening`	—	`Set.preimage_mono` `Set.Iio_subset_Iio` `ENNReal.ofReal_le_ofReal`
`thickening_nonempty_iff` 📖	mathematical	—	`Set.Nonempty` `thickening` `Real` `Real.instLT` `Real.instZero`	—	—
`thickening_nonempty_iff_of_pos` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Set.Nonempty` `thickening`	—	`thickening_eq_empty_iff_of_pos`
`thickening_of_nonpos` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`thickening` `Set` `Set.instEmptyCollection`	—	`Set.eq_empty_of_forall_notMem` `LE.le.not_gt` `Eq.trans_le` `ENNReal.ofReal_of_nonpos` `bot_le`
`thickening_singleton` 📖	mathematical	—	`thickening` `PseudoMetricSpace.toPseudoEMetricSpace` `Set` `Set.instSingletonSet` `ball`	—	`Set.ext`
`thickening_subset_cthickening` 📖	mathematical	—	`Set` `Set.instHasSubset` `thickening` `cthickening`	—	`LT.lt.le` `Set.mem_setOf_eq` `thickening.eq_1`
`thickening_subset_cthickening_of_le` 📖	mathematical	`Real` `Real.instLE`	`Set` `Set.instHasSubset` `thickening` `cthickening`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `thickening_subset_cthickening` `cthickening_mono`
`thickening_subset_interior_cthickening` 📖	mathematical	—	`Set` `Set.instHasSubset` `thickening` `interior` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `cthickening`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `subset_interior_iff_isOpen` `isOpen_thickening` `interior_mono` `thickening_subset_cthickening`
`thickening_subset_of_subset` 📖	mathematical	`Set` `Set.instHasSubset`	`thickening`	—	`lt_of_le_of_lt` `infEDist_anti`
`thickening_thickening_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `thickening` `Real` `Real.instAdd`	—	`le_total` `thickening_of_nonpos` `thickening_empty` `ENNReal.ofReal_add` `LE.le.trans_lt` `PseudoEMetricSpace.edist_triangle` `ENNReal.add_lt_add`
`thickening_union` 📖	mathematical	—	`thickening` `Set` `Set.instUnion`	—	`infEDist_union`

---

← Back to Index