Mathlib Map

Theorems · Theorem · functional analysis

balancedCoreAux_subset

∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (s : Set E), balancedCoreAux 𝕜 s ⊆ s
Defined in
Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Cited by
1 results in Mathlib
Foundations
Depth 117 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
NormedDivisionRingAddCommGroupModule
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

balancedCore_eq_iInter · cited by 2balancedCore_eq_iInterSet · cited by 53352SetModule · cited by 20661ModuleAddCommGroup · cited by 12871AddCommGroupone_smul · cited by 1374one_smulEq.ge · cited by 375Eq.geNormedDivisionRing · cited by 360NormedDivisionRingNormOneClass.norm_one · cited by 148NormOneClass.norm_onebalancedCoreAux · cited by 6balancedCoreAuxmem_balancedCoreAux_iff · cited by 3mem_balancedCoreAux_iffbalancedCoreAux_subsetCITED BYCITES

Cites9

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

Cited by1

Results whose statement or proof uses this declaration.