Documentation Verification Report

Shatter

📁 Source: Mathlib/Combinatorics/SetFamily/Shatter.lean

Statistics

Metric	Count
Definitions `Shatters`, `instDecidablePredShatters`, `shatterer`, `vcDim`	4
Theorems `card_le_vcDim`, `exists_inter_eq_singleton`, `exists_superset`, `mono_left`, `mono_right`, `nonempty`, `of_compression`, `shatterer`, `subset_iff`, `card_le_card_shatterer`, `card_shatterer_le_sum_vcDim`, `isLowerSet_shatterer`, `mem_shatterer`, `shatterer_compress_subset_shatterer`, `shatterer_eq`, `shatterer_idem`, `shatterer_mono`, `shatters_empty`, `shatters_iff`, `shatters_of_forall_subset`, `shatters_shatterer`, `shatters_univ`, `subset_shatterer`, `univ_shatters`, `vcDim_compress_le`, `vcDim_mono`	26
Total	30

Finset

Definitions

Name	Category	Theorems
`Shatters` 📖	MathDef	7 math math: `shatters_empty`, `shatters_of_forall_subset`, `univ_shatters`, `shatters_shatterer`, `shatters_iff`, `mem_shatterer`, `shatters_univ`
`instDecidablePredShatters` 📖	CompOp	—
`shatterer` 📖	CompOp	11 math math: `Shatters.shatterer`, `shatterer_mono`, `shatterer_compress_subset_shatterer`, `isLowerSet_shatterer`, `card_le_card_shatterer`, `shatterer_eq`, `shatters_shatterer`, `shatterer_idem`, `card_shatterer_le_sum_vcDim`, `subset_shatterer`, `mem_shatterer`
`vcDim` 📖	CompOp	4 math math: `Shatters.card_le_vcDim`, `vcDim_mono`, `vcDim_compress_le`, `card_shatterer_le_sum_vcDim`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_le_card_shatterer` 📖	mathematical	—	`card` `Finset` `shatterer`	—	`memberFamily_induction_on` `le_refl` `card_image_of_injOn` `Set.InjOn.mono` `coe_inter` `mem_filter` `Set.LeftInvOn.injOn` `insert_erase_invOn` `card_memberSubfamily_add_card_nonMemberSubfamily` `LE.le.trans` `card_union_add_card_inter` `card_union_of_disjoint` `mem_memberSubfamily` `mem_insert_self` `mem_nonMemberSubfamily` `card_mono` `union_subset` `inter_insert_of_notMem` `Shatters.exists_inter_eq_singleton` `singleton_subset_iff` `inter_subset_right` `shatterer_mono` `filter_subset` `forall_mem_image` `mem_shatterer` `subset_insert_iff` `insert_inter_distrib` `insert_erase` `insert_inter_of_notMem` `erase_eq_self`
`card_shatterer_le_sum_vcDim` 📖	mathematical	—	`card` `Finset` `shatterer` `sum` `Nat.instAddCommMonoid` `Iic` `Nat.instPreorder` `LocallyFiniteOrder.toLocallyFiniteOrderBot` `Nat.instOrderBot` `Nat.instLocallyFiniteOrder` `vcDim` `Nat.choose` `Fintype.card`	—	`sum_congr` `LE.le.trans` `card_le_card` `mem_biUnion` `mem_Iic` `Shatters.card_le_vcDim` `mem_shatterer` `mem_powersetCard_univ` `card_biUnion_le`
`isLowerSet_shatterer` 📖	mathematical	—	`IsLowerSet` `Finset` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `SetLike.coe` `instSetLike` `shatterer`	—	`Shatters.mono_right`
`mem_shatterer` 📖	mathematical	—	`Finset` `instMembership` `shatterer` `Shatters`	—	`mem_filter` `Shatters.exists_superset`
`shatterer_compress_subset_shatterer` 📖	mathematical	—	`Finset` `instHasSubset` `shatterer` `Down.compression`	—	`Shatters.of_compression`
`shatterer_eq` 📖	mathematical	—	`shatterer` `IsLowerSet` `Finset` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `SetLike.coe` `instSetLike`	—	`isLowerSet_shatterer` `Subset.antisymm` `Shatters.exists_superset` `mem_shatterer` `subset_shatterer`
`shatterer_idem` 📖	mathematical	—	`shatterer`	—	—
`shatterer_mono` 📖	mathematical	`Finset` `instHasSubset`	`shatterer`	—	`Shatters.mono_left`
`shatters_empty` 📖	mathematical	—	`Shatters` `Finset` `instEmptyCollection` `Nonempty`	—	`Shatters.nonempty` `empty_inter` `subset_empty`
`shatters_iff` 📖	mathematical	—	`Shatters` `image` `Finset` `decidableEq` `instInter` `powerset`	—	`ext` `mem_image` `mem_powerset` `Shatters.subset_iff`
`shatters_of_forall_subset` 📖	mathematical	`Finset` `instMembership`	`Shatters`	—	`inter_eq_right`
`shatters_shatterer` 📖	mathematical	—	`Shatters` `shatterer`	—	`shatterer_idem`
`shatters_univ` 📖	mathematical	—	`Shatters` `univ` `Finset` `fintype`	—	`shatters_iff` `powerset_univ` `univ_inter` `image_id'`
`subset_shatterer` 📖	mathematical	`IsLowerSet` `Finset` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `SetLike.coe` `instSetLike`	`instHasSubset` `shatterer`	—	`mem_shatterer` `inter_eq_right`
`univ_shatters` 📖	mathematical	—	`Shatters` `univ` `Finset` `fintype`	—	`shatters_of_forall_subset` `mem_univ`
`vcDim_compress_le` 📖	mathematical	—	`vcDim` `Down.compression`	—	`sup_mono` `shatterer_compress_subset_shatterer`
`vcDim_mono` 📖	mathematical	`Finset` `instHasSubset`	`vcDim`	—	`sup_mono` `shatterer_mono`

Finset.Shatters

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_le_vcDim` 📖	mathematical	`Finset.Shatters`	`Finset.card` `Finset.vcDim`	—	`Finset.le_sup` `Finset.mem_shatterer`
`exists_inter_eq_singleton` 📖	mathematical	`Finset.Shatters` `Finset` `Finset.instMembership`	`Finset.instInter` `Finset.instSingleton`	—	`Finset.singleton_subset_iff`
`exists_superset` 📖	mathematical	`Finset.Shatters`	`Finset` `Finset.instMembership` `Finset.instHasSubset`	—	`Finset.Subset.rfl` `Finset.inter_eq_left`
`mono_left` 📖	—	`Finset` `Finset.instHasSubset` `Finset.Shatters`	—	—	—
`mono_right` 📖	—	`Finset` `Finset.instHasSubset` `Finset.Shatters`	—	—	`HasSubset.Subset.trans` `Finset.instIsTransSubset` `inf_congr_right` `inf_le_of_left_le`
`nonempty` 📖	mathematical	`Finset.Shatters`	`Finset.Nonempty` `Finset`	—	`Finset.Subset.rfl`
`of_compression` 📖	—	`Finset.Shatters` `Down.compression`	—	—	`Down.mem_compression` `Finset.insert_subset` `Finset.inter_erase` `Finset.erase_insert` `Finset.insert_eq_self` `Finset.mem_inter` `Finset.inter_subset_right` `Finset.mem_insert_self` `Finset.inter_insert_of_notMem`
`shatterer` 📖	mathematical	`Finset.Shatters`	`Finset.shatterer`	—	`Finset.shatters_shatterer`
`subset_iff` 📖	mathematical	`Finset.Shatters`	`Finset` `Finset.instHasSubset` `Finset.instMembership` `Finset.instInter`	—	`Finset.inter_subset_left`

---

← Back to Index