Structures · Analysis
HasSolidNorm
Let α be an AddCommGroup with a Lattice structure. A norm on α is solid if, for a
and b in α, with absolute values |a| and |b| respectively, |a| ≤ |b| implies ‖a‖ ≤ ‖b‖.
- Defined in
- Mathlib.Analysis.Normed.Order.Lattice
- Shape
- One type argument · adds solid
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances6
- Int
- Real
- Rat
- BoundedContinuousFunction
- Subtype
- OrderDual
How is a type an instance?
Loading the hierarchy index…
Assumed by81
- Module.Basis.ofZLatticeBasis
- continuous_posPart
- Module.Basis.ofZLatticeBasis_apply
- HasSolidNorm.solid
- continuous_negPart
- Module.Basis.ofZLatticeBasis_span
- norm_le_norm_of_abs_le_abs
- ZLattice.rank
- Module.Basis.ofZLatticeBasis_repr_apply
- Monotone.tendstoLocallyUniformly_of_forall_tendsto
- MeasureTheory.Integrable.abs
- tendsto_smul_comp_nat_floor_of_tendsto_mul
- ZLattice.module_finite
- ZSpan.fundamentalDomain_isBounded
- ZSpan.norm_fract_le
- ZLattice.module_free
- MeasureTheory.Submartingale.pos
- lipschitzWith_posPart
- MeasureTheory.Integrable.measure_le_lt_top
- norm_abs_eq_norm
- MeasureTheory.integral_abs_condExp_le
- MeasureTheory.Integrable.measure_gt_lt_top
- MeasureTheory.MemLp.abs
- MeasureTheory.Integrable.sup
- MeasureTheory.MemLp.sup
- Monotone.tendstoLocallyUniformlyOn_of_forall_tendsto
- MeasureTheory.abs_condExp_ae_le_condExp_abs
- norm_inf_sub_inf_le_add_norm
- ContinuousMap.tendsto_of_monotone_of_pointwise
- Monotone.tendstoUniformly_of_forall_tendsto
- norm_sup_sub_sup_le_add_norm
- MeasureTheory.setIntegral_abs_condExp_le
- tendsto_smul_comp_nat_floor_of_tendsto_nsmul
- MeasureTheory.HasFiniteIntegral.mono_nonneg
- norm_sup_le_add
- MeasureTheory.Integrable.measure_ge_lt_top
- lipschitzWith_negPart
- lipschitzWith_sup_right
- norm_sup_sub_sup_le_norm
- MeasureTheory.Integrable.mono_nonneg
- MeasureTheory.Submartingale.sup
- Monotone.tendstoUniformlyOn_of_forall_tendsto
- norm_inf_le_add
- Module.Basis.ofZLatticeBasis_comap
- ZLattice.FG
- MeasureTheory.MemLp.inf
- MeasureTheory.Lp.coeFn_sup
- Module.Basis.ofZLatticeBasis.congr_simp
- norm_abs_sub_abs
- ContinuousMap.tendsto_of_antitone_of_pointwise
Ancestors0
No ancestors.