OAI/Analysis/SeparableQuotients/NegativeComplex.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SeparableQuotient.HasSeparableQuotient.of_equiv line 12
2. lemma OAI.SeparableQuotient.HasSeparableQuotient.restrictScalars line 22

   Source documentation

   A complex quotient gives a real quotient of the underlying real space.

   lemma HasSeparableQuotient.restrictScalars {X : Type u}
       [NormedAddCommGroup X] [NormedSpace ℂ X] [NormedSpace ℝ X]
       [IsScalarTower ℝ ℂ X]
       (h : HasSeparableQuotient ℂ X) : HasSeparableQuotient ℝ X := by
   …

   Mentions: OAI.SeparableQuotient.HasSeparableQuotient

3. lemma OAI.SeparableQuotient.complexify_noSQ line 37

   Source documentation

   A real space without a separable quotient has a complexification without a complex separable quotient.

   lemma complexify_noSQ (X : Type u) [NormedAddCommGroup X]
       [NormedSpace ℝ X] [CompleteSpace X] (h : ¬ HasSeparableQuotient ℝ X) :
       ¬ HasSeparableQuotient ℂ (Complexify X) := by
   …

   Mentions: OAI.SeparableQuotient.HasSeparableQuotient, OAI.SeparableQuotient.Complexify

4. theorem OAI.SeparableQuotient.negative_complex line 46

   Source documentation

   CH refutes the complex separable quotient assertion in every universe.

   theorem negative_complex (hCH : CH) : ¬ SQ.{u} ℂ := by
   …

   Mentions: OAI.SeparableQuotient.CH