OAI/Analysis/SeparableQuotients/ChangedPredual.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SeparableQuotient.ActualSpace.restrict line 18
2. lemma OAI.SeparableQuotient.ActualSpace.coordinate_restriction_countable line 21
3. lemma OAI.SeparableQuotient.ActualSpace.predual_restriction_separable line 38

   Source documentation

   Restrictions of the coordinate predual to a separable subspace form a norm-separable set.

   lemma predual_restriction_separable (F : Submodule ℝ E) [SeparableSpace F] :
       IsSeparable (restrict F '' (X₀ : Set (StrongDual ℝ E))) := by
   …

   Mentions: OAI.SeparableQuotient.ActualSpace.E, OAI.SeparableQuotient.ActualSpace.restrict, OAI.SeparableQuotient.ActualSpace.X₀

4. lemma OAI.SeparableQuotient.ActualSpace.eval0_isometry line 74
5. lemma OAI.SeparableQuotient.ActualSpace.eval0_surjective line 75
6. def OAI.SeparableQuotient.ActualSpace.X line 80

   Source documentation

   The changed predual is the kernel of the perturbed quotient map.

   def X : Submodule ℝ (StrongDual ℝ E) := (X₀.mkQL - B hCH).ker

   Mentions: OAI.SeparableQuotient.ActualSpace.E, OAI.SeparableQuotient.ActualSpace.B

7. instance OAI.SeparableQuotient.ActualSpace.X_isClosed line 81
8. instance OAI.SeparableQuotient.ActualSpace.X_complete line 82
9. lemma OAI.SeparableQuotient.ActualSpace.twist_data line 84
10. def OAI.SeparableQuotient.ActualSpace.twistedIso line 97
11. lemma OAI.SeparableQuotient.ActualSpace.twistedIso_apply line 98
12. lemma OAI.SeparableQuotient.ActualSpace.X_infinite line 101
13. lemma OAI.SeparableQuotient.ActualSpace.quotient_eq_B_on_X line 107
14. lemma OAI.SeparableQuotient.ActualSpace.X_quotient_image line 112
15. lemma OAI.SeparableQuotient.ActualSpace.path_mem_twisted_sum line 119
16. lemma OAI.SeparableQuotient.ActualSpace.X_restriction_nonseparable line 145

    Source documentation

    The branch obstruction for the changed predual, using the open quotient map.

    lemma X_restriction_nonseparable (F : Submodule ℝ E) (hF : IsClosed (F : Set E))
        (hFi : ¬ FiniteDimensional ℝ F) [SeparableSpace F] :
        ¬ IsSeparable (restrict F '' (X hCH : Set (StrongDual ℝ E))) := by
    …

    Mentions: OAI.SeparableQuotient.ActualSpace.E, OAI.SeparableQuotient.ActualSpace.restrict, OAI.SeparableQuotient.ActualSpace.X

17. lemma OAI.SeparableQuotient.ActualSpace.X_no_separableQuotient line 176