WeakMetric.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Metrizability of norm-separable weakly compact sets

For a dense sequence in the norm carrier, choose a norming functional for each pairwise difference. These countably many functionals separate the points of the set. Their evaluations embed the compact weak carrier into a countable product of real lines. No separability of the ambient space, or of its entire dual, is assumed.

def OAI.ReflexiveFixedPoints.pairNormingFunctional line 32
Source documentation
One actual norming functional for each difference of dense points.
```
def pairNormingFunctional {K : Set X} (z : ℕ → K) (ij : ℕ × ℕ) : StrongDual ℝ X :=
…
```
theorem OAI.ReflexiveFixedPoints.pairNormingFunctional_norm line 35
theorem OAI.ReflexiveFixedPoints.pairNormingFunctional_apply line 39
theorem OAI.ReflexiveFixedPoints.pairNormingFunctional_separates line 45
Source documentation
The selected countable family separates the original norm carrier.
```
theorem pairNormingFunctional_separates {K : Set X} (z : ℕ → K)
    (hz : DenseRange z) :
    Function.Injective (fun a : K => fun ij => pairNormingFunctional z ij a) := by
…
```
Mentions: OAI.ReflexiveFixedPoints.pairNormingFunctional
theorem OAI.ReflexiveFixedPoints.weakCarrier_metrizable line 94
Source documentation
The actual weak topology on a norm-separable weakly compact set is metrizable. The empty set and zero ambient space are included.
```
theorem weakCarrier_metrizable {K : Set X} (hsep : IsSeparable K)
    (hcompact : WeaklyCompact K) : MetrizableSpace (WeakCarrier K) := by
…
```
Mentions: OAI.ReflexiveFixedPoints.WeaklyCompact, OAI.ReflexiveFixedPoints.WeakCarrier

theorem OAI.ReflexiveFixedPoints.differences_isSeparable line 122

Source documentation

The difference set of a separable set is separable in the original norm.

theorem differences_isSeparable {X : Type u} [NormedAddCommGroup X] [NormedSpace ℝ X]
    {K : Set X} (hsep : IsSeparable K) :
    IsSeparable (K - K) := by
…

theorem OAI.ReflexiveFixedPoints.differenceSpan_isSeparable line 131
Source documentation
Closing the real linear span preserves separability.
```
theorem differenceSpan_isSeparable {K : Set X} (hsep : IsSeparable K) :
    IsSeparable (differenceSpan K : Set X) := by
…
```
Mentions: OAI.ReflexiveFixedPoints.differenceSpan
theorem OAI.ReflexiveFixedPoints.differenceSpan_separableSpace line 136