class PiBase.EberleinCompactSpace (X : Type u) [TopologicalSpace X] extends CompactSpace X : Prop

• isCompact_univ : IsCompact Set.univ
• eberlein_compact : ∃ (E : Type u) (x : NormedAddCommGroup E) (x_1 : NormedSpace ℝ E) (f : X → WeakSpace ℝ E), CompleteSpace E ∧ Topology.IsEmbedding f