`OAI/Probability/MatroidSecretary/Residual/ResidualFamilySpecification.lean`

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

def OAI.MatroidProphet.PatternFamilyClaim line 11
Source documentation
Source lem:pattern-family, with its fixed-before-focal-bits quantifiers. The source uses κ=2^100; this statement also covers every κ≥2.
```
def PatternFamilyClaim : Prop :=
…
```