Lean 4.33.1
Dependencies: Mathlib 4.33.1 (see bundled lake-manifest.json)
File: Kantorovich.lean
SHA-256: a5c479a4a9e32d1d7175879d068b10ab37301c520cd34ba080676e81e600aefb
Result: passed

'PaperToLean.Kantorovich.scalar_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Kantorovich.weighted_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Kantorovich.product_from_linear_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Kantorovich.inequality' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Kantorovich.endpoint_sharp' depends on axioms: [propext, Classical.choice, Quot.sound]
