Theorems · Definition · functional analysis
SeminormFamily
(R : Type u_1) → (E : Type u_6) → Type u_9 → [inst : SeminormedRing R] → [inst_1 : AddCommGroup E] → [Module R E] → Type (max u_9 u_6)
An abbreviation for indexed families of seminorms. This is mainly to allow for dot-notation.
- Cited by
- 68 results in Mathlib
- Foundations
- Depth 8 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement and proof · cited by 20,661
- AddCommGroupstatement and proof · cited by 12,871
- SeminormedRingstatement and proof · cited by 446
- Seminormproof · cited by 272
Cited by83
Results whose statement or proof uses this declaration.
- WithSeminormsstatement · cited by 69
- SeminormFamily.basisSetsstatement and proof · cited by 22
- SeminormFamily.basisSets_iffstatement and proof · cited by 16
- WithSeminorms.topologicalAddGroupstatement and proof · cited by 11
- SeminormFamily.moduleFilterBasisstatement and proof · cited by 10
- SeminormFamily.compstatement and proof · cited by 8
- SeminormFamily.withSeminorms_iff_nhds_eq_iInfstatement and proof · cited by 8
- SeminormFamily.basisSets_memstatement and proof · cited by 6
- schwartzSeminormFamilystatement · cited by 6
- WithSeminorms.continuous_seminormstatement and proof · cited by 5
- WithSeminorms.hasBasisstatement and proof · cited by 5
- WithSeminorms.topology_eq_withSeminormsstatement and proof · cited by 5