OAI/Geometry/NilpotentCharts/LinearLattices.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Vector lattices, lifted bases and unit triangular linear maps.

  1. lemma OAI.RawLattice.span_eq_top_of_compact_quotient line 12
  2. theorem OAI.RawLattice.exists_vector_lattice_basis line 34
  3. lemma OAI.RawLinearBasis.basis_append_lifts line 58
  4. lemma OAI.RawLinearBasis.basis_append_projection line 102
  5. def OAI.RawLinearBasis.Triangular line 139
  6. lemma OAI.RawLinearBasis.triangular_append line 143
  7. lemma OAI.RawTriangular.injective_of_unit_triangular line 174
  8. lemma OAI.RawTriangular.bijective_of_unit_triangular line 206
  9. lemma OAI.RawTriangular.row_of_unit_triangular line 214
  10. lemma OAI.RawTriangular.sum_lower line 239
  11. lemma OAI.RawLattice.span_subtype_eq_top line 255
  12. lemma OAI.RawLattice.compact_quotient_of_span line 266
  13. lemma OAI.RawLattice.exists_vector_lattice_basis_of_span line 280