DensityContractsModel.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.MatroidProphet.DensityExpansionContract line 10
Source documentation
lem:density, including the convention of closing a nonflat argument.
```
def DensityExpansionContract (M : Matroid α) (hE : M.E = univ)
    (κ : ℕ) (D : Set α) : Prop :=
…
```
def OAI.MatroidProphet.PathPropertiesContract line 24
Source documentation
lem:paths: both paths, all integer endpoints, and the true least birth.
```
def PathPropertiesContract (M : Matroid α) (hE : M.E = univ)
    (κ : ℕ) (D C : ℕ → Set α) : Prop :=
…
```
def OAI.MatroidProphet.GeneratorBudgetContract line 48
Source documentation
lem:generators: one budget and one increasing family for the entire ℤ path.
```
def GeneratorBudgetContract (M : Matroid α) (hE : M.E = univ)
    (κ : ℕ) (D C : ℕ → Set α) : Prop :=
…
```