Mathlib Map

Theorems · Definition · functional analysis

balancedCore

(𝕜 : Type u_1) → {E : Type u_2} → [SeminormedRing 𝕜] → [SMul 𝕜 E] → Set E → Set E

The largest balanced subset of s.

Defined in
Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Cited by
18 results in Mathlib
Foundations
Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
SeminormedRingSMul
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

nhds_basis_balanced · cited by 10nhds_basis_balancedbalancedCore_subset · cited by 8balancedCore_subsetbalancedCore_balanced · cited by 6balancedCore_balancedbalancedCore_mem_nhds_zero · cited by 4balancedCore_mem_nhds_zeromem_balancedCore_iff · cited by 2mem_balancedCore_iffnhds_hasBasis_absConvex · cited by 2nhds_hasBasis_absConvexbalancedCore_eq_iInter · cited by 2balancedCore_eq_iInterbalancedCore_nonempty_iff · cited by 2balancedCore_nonempty_iffbalancedCore_zero_mem · cited by 2balancedCore_zero_memBalanced.subset_balancedCore_of_subset · cited by 2Balanced.subset_balancedC…subset_balancedCore · cited by 1subset_balancedCoreBalanced.balancedCore_eq · cited by 1Balanced.balancedCore_eqbalancedCore_subset_balancedCoreAux · cited by 1balancedCore_subset_balan…smul_balancedCore_subset · cited by 1smul_balancedCore_subsetunique_topology_of_t2 · cited by 1unique_topology_of_t2Set · cited by 53352SetSet.ofPred · cited by 6101Set.ofPredSeminormedRing · cited by 446SeminormedRingSet.sUnion · cited by 392Set.sUnionBalanced · cited by 77BalancedbalancedCoreCITED BYCITES

Cites5

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

Cited by18

Results whose statement or proof uses this declaration.