Main results

The main results that the formalization.yaml of FormalFrontier/vector-bundles lists under status.main_results at commit e3fb9de3, each that the scan finds declared in the file the yaml gives, with its line. They are listed here, not made articles: in several Formal Frontier libraries this list is close to the whole API. The notes are the yaml's.

Declaration	Kind	Where	Note
VectorBundle.continuousHermitianMetric	def	VectorBundles/Topology/VectorBundle/MetricExistence.lean, line 48
VectorBundle.continuousRiemannianMetric	def	VectorBundles/Topology/VectorBundle/Metric.lean, line 45
Bundle.ContinuousHermitianMetric.orthogonalBundle	def	VectorBundles/Topology/VectorBundle/OrthogonalComplement.lean, line 505
Bundle.ContinuousHermitianMetric.orthogonalAdditionHomeomorph	def	VectorBundles/Topology/VectorBundle/OrthogonalAddition.lean, line 147
Bundle.ContinuousHermitianMetric.orthogonalProjectionTotal	def	VectorBundles/Topology/VectorBundle/OrthogonalProjection.lean, line 91
Bundle.ContinuousHermitianMetric.orthogonalComplementProjectionTotal	def	VectorBundles/Topology/VectorBundle/OrthogonalProjection.lean, line 103
Bundle.ContinuousHermitianMetric.orthonormalizeTrivialization	def	VectorBundles/Topology/VectorBundle/OrthonormalTrivialization.lean, line 396
VectorBundle.homeomorphOfFiberwiseLinearEquivOfIsModuleTopology	def	VectorBundles/Topology/VectorBundle/Isomorphism.lean, line 212
VectorBundle.of_isLinear	theorem	VectorBundles/Topology/VectorBundle/CoordinateMap.lean, line 198
VectorBundle.finiteComplement	def	VectorBundles/Topology/VectorBundle/FiniteComplement.lean, line 291
FiberBundle.sigmaCompactSpace	instance	VectorBundles/Topology/FiberBundle/SigmaCompact.lean, line 60
Bundle.Trivialization.sigmaCompactSpace_model_of_isClosed	theorem	VectorBundles/Topology/FiberBundle/SigmaCompact.lean, line 101
FiberBundle.sigmaCompactSpace_model	theorem	VectorBundles/Topology/FiberBundle/SigmaCompact.lean, line 124
FiberBundle.sigmaCompactSpace_totalSpace_iff	theorem	VectorBundles/Topology/FiberBundle/SigmaCompact.lean, line 140

Quoted from the main results in formalization.yaml of FormalFrontier/vector-bundles at commit e3fb9de3, Apache-2.0.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.