Theorems · Inductive type · functional analysis
AddGroupNorm
(G : Type u_6) → [AddGroup G] → Type u_6
A norm on an additive group G is a function f : G → ℝ that preserves zero, is subadditive
and such that f (-x) = f x and f x = 0 → x = 0 for all x.
- Defined in
- Mathlib.Analysis.Normed.Group.Seminorm
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- AddGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddGroupstatement · cited by 4,410
Cited by29
Results whose statement or proof uses this declaration.
- MeasureTheory.measure_le_eq_ltproof · cited by 3
- MeasureTheory.measure_lt_one_eq_integral_div_gammaproof · cited by 3
- AddGroupNorm.toAddGroupSeminormstatement and proof · cited by 2
- AddGroupNorm.toNormedAddCommGroupstatement and proof · cited by 2
- normRingNormproof · cited by 1
- AddGroupNorm.extstatement and proof · cited by 1
- AddGroupNorm.mk.injstatement · cited by 1
- AddGroupNorm.mk.noConfusionstatement · cited by 1
- AddGroupNorm.apply_onestatement · cited by 0
- AddGroupNorm.casesOnstatement and proof · cited by 0
- AddGroupNorm.coe_le_coestatement and proof · cited by 0
- AddGroupNorm.coe_lt_coestatement and proof · cited by 0