Theorems · Definition · functional analysis
Seminorm.closedBall
{𝕜 : Type u_3} →
{E : Type u_7} →
[inst : SeminormedRing 𝕜] → [inst_1 : AddCommGroup E] → [inst_2 : SMul 𝕜 E] → Seminorm 𝕜 E → E → ℝ → Set EThe closed ball of radius r at x with respect to seminorm p is the set of elements y
with p (y - x) ≤ r.
- Defined in
- Mathlib.Analysis.Seminorm
- Cited by
- 45 results in Mathlib
- Foundations
- Depth 100 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Setstatement · cited by 53,352
- Realstatement and proof · cited by 25,697
- AddCommGroupstatement and proof · cited by 12,871
- Set.ofPredproof · cited by 6,101
- SeminormedRingstatement and proof · cited by 446
- Seminormstatement and proof · cited by 272
Cited by45
Results whose statement or proof uses this declaration.
- Seminorm.mem_closedBallstatement · cited by 8
- Seminorm.ball_subset_closedBallstatement · cited by 5
- Seminorm.mem_closedBall_zerostatement · cited by 5
- Seminorm.continuousAt_zero_of_forall'statement and proof · cited by 4
- Seminorm.continuousAt_zero'statement and proof · cited by 3
- Seminorm.continuous'statement and proof · cited by 2
- closedBall_normSeminormstatement · cited by 1
- Seminorm.closedBall_botstatement · cited by 1
- Seminorm.closedBall_eq_biInter_ballstatement · cited by 1
- Seminorm.closedBall_eq_metricstatement and proof · cited by 1
- Seminorm.closedBall_finset_sup_eq_iInterstatement · cited by 1
- Seminorm.closedBall_iSupstatement and proof · cited by 1