OAI/Geometry/ComplexBundle/
772 declarations, 0 contain sorry, 0 declared as axioms; 32 files
Files
- Avoidance.lean 25 declarations
- BundleIncidence.lean 3 declarations
- Complement.lean 47 declarations
- Coordinates.lean 12 declarations
- CoordinatesMetric.lean 10 declarations
- DirectSum.lean 36 declarations
- Evaluation.lean 41 declarations
- Frames.lean 38 declarations
- Grassmann.lean 56 declarations
- GrassmannManifold.lean 24 declarations
- Hom.lean 16 declarations
- Hyperplane.lean 46 declarations
- HyperplaneProduct.lean 16 declarations
- Incidence.lean 33 declarations
- Kernel.lean 57 declarations
- LineStage.lean 24 declarations
- Maps.lean 15 declarations
- OpenIncidence.lean 8 declarations
- Orthonormal.lean 26 declarations
- PointExpansion.lean 10 declarations
- Projection.lean 29 declarations
- ProjectionBundle.lean 20 declarations
- Projective.lean 29 declarations
- Pullback.lean 9 declarations
- RealModel.lean 17 declarations
- Replacement.lean 29 declarations
- Sections.lean 8 declarations
- SmoothLine.lean 26 declarations
- StageMaps.lean 9 declarations
- Tensor.lean 15 declarations
- Tuples.lean 14 declarations
- ZeroSign.lean 24 declarations