Thin independence

Stream: Seymour

[Martin Dvořák]

In Section 2.6 of https://arxiv.org/pdf/1003.3919 my brain is unable to parse the definition of when a family of functions is thinly independent.

Do we have somebody brave in the team who would formalize the definition in Lean? If we have thin independence in Lean, I will give it another try and maybe finally understand what it is about.

The motivation should be working with vector matroids of infinite rank, but I cannot say more until I understand what the definition means.