Theorems · Theorem · functional analysis
NonarchAddGroupSeminorm.coe_iSup_apply
∀ {E : Type u_3} [inst : AddGroup E] {ι : Type u_6} (f : ι → NonarchAddGroupSeminorm E),
BddAbove (Set.range f) → ∀ {x : E}, (⨆ i, f i) x = ⨆ i, (f i) x- Defined in
- Mathlib.Analysis.Normed.Group.Seminorm
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 121 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
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
- Realstatement and proof · cited by 25,697
- Set.rangestatement and proof · cited by 4,705
- AddGroupstatement and proof · cited by 4,410
- iSupstatement and proof · cited by 2,415
- BddAbovestatement and proof · cited by 620
- Set.rangeFactorizationproof · cited by 56
- NonarchAddGroupSeminormstatement and proof · cited by 26
- sSup_rangeproof · cited by 20
- Set.rangeFactorization_surjectiveproof · cited by 20
- Function.Surjective.iSup_congrproof · cited by 14
- NonarchAddGroupSeminorm.coe_sSup_applyproof · cited by 2
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.