CoordinateEmbeddings.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Coordinate Embeddings

def OAI.HadwigerCounterexample.embedMat line 15
theorem OAI.HadwigerCounterexample.embedMatT line 18
theorem OAI.HadwigerCounterexample.mul_embedMat line 24
theorem OAI.HadwigerCounterexample.embedMat_mul line 30
theorem OAI.HadwigerCounterexample.embedMat_self line 36
theorem OAI.HadwigerCounterexample.embedMat_inj line 43
theorem OAI.HadwigerCounterexample.inj_fromCols line 53
theorem OAI.HadwigerCounterexample.prescribe_between line 75
Source documentation
Specify an arbitrary cross Gram bilinear form between independent columns.
```
theorem prescribe_between {A : Mat U I} {B : Mat V J}
    (hA : Injective A.mulVec) (hB : Injective B.mulVec) (M : Mat I J) :
    ∃ L : Mat U V, Aᵀ*L*B=M := by
…
```
Mentions: OAI.HadwigerCounterexample.Mat

theorem OAI.HadwigerCounterexample.prescribe_opposite line 86

Source documentation

Two opposite-direction restrictions are specifiable on disjoint bases.

theorem prescribe_opposite {A : Mat U I} {B : Mat V J} {C : Mat U K} {D : Mat V T}
    (hc : Injective (fromCols A C).mulVec) (hd : Injective (fromCols B D).mulVec)
    (M : Mat I J) (N : Mat T K) :
    ∃ L : Mat U V, Aᵀ*L*B=M ∧ Dᵀ*Lᵀ*C=N := by
…

Mentions: OAI.HadwigerCounterexample.Mat

theorem OAI.HadwigerCounterexample.rank_ge_mul line 98
theorem OAI.HadwigerCounterexample.rank_ge_congr line 124
theorem OAI.HadwigerCounterexample.choose_free line 132
Source documentation
Choose a large space in the domain which becomes disjoint from S in the target.
```
theorem choose_free {A : Mat I J} (hA : Injective A.mulVec) (S : Space (Vec I)) :
    ∃ T : Space (Vec J), Fintype.card J ≤ dim T+dim S ∧
      Disjoint S (colSp (A*pack T)) := by
…
```
Mentions: OAI.HadwigerCounterexample.Mat, OAI.HadwigerCounterexample.Space, OAI.HadwigerCounterexample.Vec, OAI.HadwigerCounterexample.dim, OAI.HadwigerCounterexample.colSp, OAI.HadwigerCounterexample.pack