OAI/Analysis/SeparableQuotients/SeparableSubspaces.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SeparableQuotient.exists_separable_closed_ID line 11
2. lemma OAI.SeparableQuotient.countable_of_separated_range line 32
3. lemma OAI.SeparableQuotient.boolSeq_uncountable line 55
4. lemma OAI.SeparableQuotient.quotient_closure_lift line 67
5. lemma OAI.SeparableQuotient.separable_restriction_of_quotient line 93

   Source documentation

   Transfer the necessary evaluation criterion through the actual predual isomorphism, retaining a separable closed infinite-dimensional subspace.

   lemma separable_restriction_of_quotient
       (R : E ≃L[ℝ] StrongDual ℝ X) (J : X →L[ℝ] StrongDual ℝ E)
       (hR : ∀ e x, R e x = J x e) (hSQ : HasSeparableQuotient ℝ X) :
       ∃ F : Submodule ℝ E, IsClosed (F : Set E) ∧ ¬ FiniteDimensional ℝ F ∧
         IsSeparable (F : Set E) ∧
         IsSeparable (range (fun x : X => (J x).comp F.subtypeL)) := by
   …

   Mentions: OAI.SeparableQuotient.HasSeparableQuotient