Mathlib Map

Theorems · Theorem · functional analysis

Seminorm.sSup_apply

∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {s : Set (Seminorm 𝕜 E)}, BddAbove s → ∀ {x : E}, (sSup s) x = ⨆ p, ↑p x
Defined in
Mathlib.Analysis.Seminorm
Cited by
2 results in Mathlib
Foundations
Depth 124 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
NormedFieldAddCommGroupModule
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Seminorm.sSup_empty · cited by 1Seminorm.sSup_emptyPiTensorProduct.injectiveSeminorm_apply · cited by 0PiTensorProduct.injective…DFunLike.coe · cited by 62936DFunLike.coeSet · cited by 53352SetReal · cited by 25697RealModule · cited by 20661ModuleAddCommGroup · cited by 12871AddCommGroupSet.Elem · cited by 7166Set.ElemiSup · cited by 2415iSupNormedField · cited by 1084NormedFieldSupSet.sSup · cited by 954SupSet.sSupBddAbove · cited by 620BddAboveSeminorm · cited by 272SeminormiSup_apply · cited by 35iSup_applySeminorm.coe_sSup_eq · cited by 2Seminorm.coe_sSup_eqSeminorm.sSup_applyCITED BYCITES

Cites13

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

  • DFunLike.coestatement and proof · cited by 62,936
  • Setstatement and proof · cited by 53,352
  • Realstatement and proof · cited by 25,697
  • Modulestatement and proof · cited by 20,661
  • AddCommGroupstatement and proof · cited by 12,871
  • Set.Elemstatement and proof · cited by 7,166
  • iSupstatement and proof · cited by 2,415
  • NormedFieldstatement and proof · cited by 1,084
  • SupSet.sSupstatement · cited by 954
  • BddAbovestatement and proof · cited by 620
  • Seminormstatement and proof · cited by 272
  • iSup_applyproof · cited by 35

Cited by2

Results whose statement or proof uses this declaration.