Theorems · Theorem · functional analysis
Balanced.interior
∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {A : Set E}
[inst_3 : TopologicalSpace E] [ContinuousSMul 𝕜 E], Balanced 𝕜 A → 0 ∈ interior A → Balanced 𝕜 (interior A)The interior of a balanced set is balanced if it contains the origin.
- Defined in
- Mathlib.Analysis.LocallyConvex.Basic
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 105 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- Modulestatement and proof · cited by 20,661
- AddCommGroupstatement and proof · cited by 12,871
- NormedFieldstatement and proof · cited by 1,084
- ContinuousSMulstatement and proof · cited by 1,016
- interiorstatement and proof · cited by 714
- Balancedstatement and proof · cited by 77
- Set.insert_eq_selfproof · cited by 5
- Balanced.zero_insert_interiorproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- nhds_hasBasis_absConvex_openproof · cited by 2