Structures · Topology
EDist
EDist α means that α is equipped with an extended distance.
- Defined in
- Mathlib.Topology.EMetricSpace.Defs
- Shape
- One type argument · adds edist
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by3
Forgetful instances
Provided automatically by
Concrete types that are instances14
- SeparationQuotient
- WithLp
- UniformFun
- UniformOnFun
- PiLp
- OnePoint
- Metric.Snowflaking
- Subtype
- OrderDual
- WithTop
- WithBot
- Multiplicative
- Additive
- Option
How is a type an instance?
Loading the hierarchy index…
Assumed by92
- EDist.edist
- Metric.eball
- MeasureTheory.TendstoInMeasure
- Set.einfsep
- Set.infsep
- Metric.mem_eball
- Set.Subsingleton.infsep_zero
- PiCountable.edist
- WithLp.prod_edist_eq_add
- Set.Subsingleton.einfsep
- Set.einfsep_le_edist_of_mem
- MeasureTheory.tendstoInMeasure_of_ne_top
- MeasureTheory.TendstoInMeasure.congr
- PiLp.edist_eq_sum
- MeasureTheory.TendstoInMeasure.comp
- Set.le_einfsep
- Set.le_einfsep_iff
- edist_le_pi_edist
- Set.einfsep_of_fintype
- Set.Nontrivial.einfsep_exists_of_finite
- Set.einfsep_top
- Set.einfsep_pair_le_left
- Set.einfsep_pair_eq_inf
- Set.einfsep_anti
- PiLp.edist_eq_card
- Set.nontrivial_of_einfsep_lt_top
- WithLp.prod_edist_eq_card
- Set.infsep_zero
- edist_pi_le_iff
- PiCountable.edist_le_two
- edist_pi_def
- Set.einfsep_zero
- Set.einfsep_lt_top
- Set.einfsep_insert_le
- Metric.Snowflaking.edist_def
- MeasureTheory.TendstoInMeasure.congr'
- Set.infsep_pos
- Set.infsep_singleton
- PiCountable.edist_eq_tsum
- Set.nontrivial_of_einfsep_ne_top
- Set.einfsep_empty
- PiCountable.min_edist_le_edist_pi
- Set.le_edist_of_le_einfsep
- Set.einfsep_singleton
- MeasureTheory.tendstoInMeasure_iff_tendsto_toNNReal
- Set.le_einfsep_pair
- Set.einfsep_pair_le_right
- Metric.Snowflaking.edist_ofSnowflaking_ofSnowflaking
- Set.einfsep_pos
- Option.WeakPseudoEMetricSpace.OfIsOpenEmbedding
Ancestors0
No ancestors.