Structures · Topology
IsUltrametricDist
The dist : X → X → ℝ respects the ultrametric inequality
of dist(x, z) ≤ max (dist(x,y)) (dist(y,z)).
- Defined in
- Mathlib.Topology.MetricSpace.Ultra.Basic
- Shape
- One type argument · adds dist_triangle_max
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances6
- Padic
- PadicComplex
- PadicAlgCl
- PadicInt
- Subtype
- ContinuousMap
How is a type an instance?
Loading the hierarchy index…
Assumed by199
- NormedField.toValued
- spectralAlgNorm
- IsUltrametricDist.dist_triangle_max
- IsUltrametricDist.isNonarchimedean_norm
- PadicInt.addChar_of_value_at_one
- IsUltrametricDist.norm_add_le_max
- IsUltrametricDist.algNormOfAlgEquiv
- NormedField.valuation
- IsUltrametricDist.invariantExtension
- spectralMulAlgNorm
- Finset.Nonempty.norm_sum_le_sup'_norm
- spectralAlgNorm_of_finiteDimensional_normal
- IsUltrametricDist.norm_mul_le_max
- IsUltrametricDist.norm_mul_eq_max_of_norm_ne_norm
- spectralNorm_eq_invariantExtension
- isPowMul_spectralNorm
- spectralNorm_unique
- IsUltrametricDist.norm_add_eq_max_of_norm_ne_norm
- IsUltrametricDist.closedBall_eq_of_mem
- spectralAlgNorm_of_finiteDimensional_normal_def
- IsUltrametricDist.isOpen_closedBall
- PadicInt.mahlerSeries_apply_nat
- Finset.Nonempty.norm_prod_le_sup'_norm
- IsUltrametricDist.nnnorm_mul_eq_max_of_nnnorm_ne_nnnorm
- IsUltrametricDist.nnnorm_pow_le
- IsUltrametricDist.norm_tprod_le
- PadicInt.continuousAddCharEquiv
- IsUltrametricDist.nnnorm_natCast_le_one
- IsUltrametricDist.ball_eq_of_mem
- IsUltrametricDist.nnnorm_add_eq_max_of_nnnorm_ne_nnnorm
- Valued.integer.exists_norm_coe_lt_one
- IsUltrametricDist.exists_norm_finsetProd_le_of_nonempty
- IsUltrametricDist.exists_norm_finsetSum_le_of_nonempty
- IsUltrametricDist.nnnorm_nsmul_le
- IsUltrametricDist.norm_sum_le_of_forall_le_of_nonneg
- algNormFromConst
- IsUltrametricDist.dist_eq_max_of_dist_ne_dist
- PadicInt.mahlerEquiv
- PadicInt.hasSum_mahlerSeries
- IsUltrametricDist.isClopen_closedBall
- spectralAlgNorm_def
- PadicInt.fwdDiff_tendsto_zero
- PadicInt.continuousAddCharEquiv_of_norm_mul
- IsUltrametricDist.norm_tsum_le
- IsUltrametricDist.of_normedAlgebra
- spectralNorm.spectralNorm_pow_natDegree_eq_prod_roots
- IsUltrametricDist.norm_tsum_le_of_forall_le
- PadicInt.addChar_of_value_at_one_def
- IsUltrametricDist.norm_div_eq_max_of_norm_div_ne_norm_div
- PadicInt.fwdDiff_iter_le_of_forall_le
Ancestors0
No ancestors.