Mathlib Map

Theorems · Theorem · functional analysis

Filter.hasBasis_cobounded_norm

∀ {E : Type u_2} [inst : SeminormedAddGroup E],
  (Bornology.cobounded E).HasBasis (fun x => True) fun x => {x_1 | x ≤ ‖x_1‖}
Defined in
Mathlib.Analysis.Normed.Group.Bounded
Cited by
1 results in Mathlib
Foundations
Depth 117 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
SeminormedAddGroup
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded · cited by 5tendsto_zero_of_isBounded…Real · cited by 25697RealSet.ofPred · cited by 6101Set.ofPredNorm.norm · cited by 5413Norm.normFilter.HasBasis · cited by 604Filter.HasBasisSeminormedAddGroup · cited by 331SeminormedAddGroupBornology.cobounded · cited by 162Bornology.coboundedFilter.atTop_basis · cited by 42Filter.atTop_basisFilter.HasBasis.cobounded_of_norm · cited by 4HasBasis.cobounded_of_normFilter.hasBasis_cobounded_normCITED BYCITES

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.