Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 2 research declarations. Search 10,000 more complete Mathlib declarations.
2 results
Clear filtersCslib.MachineLearning.PACLearning.SetShatters.subset
Plain-language statement
Shattering is anti-monotone in the shattered set: if C shatters W and V ⊆ W, then C shatters V.
Source project: Lean Computer Science Library
Person-level attribution pending.
Finset.Shatters.toSetShatters
Plain-language statement
If a finite set family 𝒜 shatters a finite set s in the sense of Mathlib's Finset.Shatters, then the concept class of characteristic functions of sets in 𝒜 shatters ↑s in the sense of SetShatters. This bridges Mathlib's finset-based shattering to the predicate used by the PAC learning lower bounds.
Source project: Lean Computer Science Library
Person-level attribution pending.