Theorems · Theorem · general topology
Metric.thickening_subset_cthickening
∀ {α : Type u} [inst : PseudoEMetricSpace α] (δ : ℝ) (E : Set α), Metric.thickening δ E ⊆ Metric.cthickening δ EThe open thickening Metric.thickening δ E is contained in the closed thickening
Metric.cthickening δ E with the same radius.
- Defined in
- Mathlib.Topology.MetricSpace.Thickening
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 150 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- PseudoEMetricSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Realstatement and proof · cited by 25,697
- LT.lt.leproof · cited by 2,189
- PseudoEMetricSpacestatement and proof · cited by 1,536
- Metric.thickeningstatement and proof · cited by 130
- Set.mem_ofPred_eqproof · cited by 122
- Metric.cthickeningstatement · cited by 113
Cited by12
Results whose statement or proof uses this declaration.
- IsCompact.exists_thickening_subset_openproof · cited by 5
- Metric.infEDist_le_infEDist_thickening_addproof · cited by 3
- Metric.cthickening_eq_iInter_thickening'proof · cited by 2
- Metric.cthickening_mem_nhdsSetproof · cited by 1
- blimsup_cthickening_ae_eq_blimsup_thickeningproof · cited by 1
- Metric.thickening_subset_cthickening_of_leproof · cited by 1
- MeasureTheory.limsup_measure_closed_le_of_forall_tendsto_measureproof · cited by 1
- Metric.ediam_thickening_leproof · cited by 0
- Metric.diam_thickening_leproof · cited by 0
- IsClopen.of_cthickening_subset_selfproof · cited by 0
- Metric.closure_thickening_subset_cthickeningproof · cited by 0
- Metric.thickening_subset_interior_cthickeningproof · cited by 0