Documentation Verification Report

MinimalSuperSet

📁 Source: PhysLean/Particles/SuperSymmetry/SU5/ChargeSpectrum/MinimalSuperSet.lean

Statistics

Metric	Count
Definitions `minimalSuperSet`	1
Theorems `card_of_mem_minimalSuperSet`, `exists_minimalSuperSet`, `insert_Q10_mem_minimalSuperSet`, `insert_Q5_mem_minimalSuperSet`, `insert_filter_card_zero`, `minimalSuperSet_induction_on_inductive`, `self_neq_mem_minimalSuperSet`, `self_not_mem_minimalSuperSet`, `self_subset_mem_minimalSuperSet`, `some_qHd_mem_minimalSuperSet_of_none`, `some_qHu_mem_minimalSuperSet_of_none`, `subset_insert_filter_card_zero`, `subset_insert_filter_card_zero_inductive`	13
Total	14

SuperSymmetry.SU5.ChargeSpectrum

Definitions

Name	Category	Theorems
`minimalSuperSet` 📖	CompOp	6 math math: `exists_minimalSuperSet`, `self_not_mem_minimalSuperSet`, `insert_Q10_mem_minimalSuperSet`, `insert_Q5_mem_minimalSuperSet`, `some_qHu_mem_minimalSuperSet_of_none`, `some_qHd_mem_minimalSuperSet_of_none`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_of_mem_minimalSuperSet` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum` `minimalSuperSet`	`card`	—	—
`exists_minimalSuperSet` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum` `ofFinset` `hasSubset`	`minimalSuperSet`	—	`HasSubset.Subset.eq_1` `insert_Q5_mem_minimalSuperSet` `insert_Q10_mem_minimalSuperSet` `some_qHd_mem_minimalSuperSet_of_none` `some_qHu_mem_minimalSuperSet_of_none`
`insert_Q10_mem_minimalSuperSet` 📖	mathematical	`Q10`	`SuperSymmetry.SU5.ChargeSpectrum` `minimalSuperSet` `qHd` `qHu` `Q5`	—	—
`insert_Q5_mem_minimalSuperSet` 📖	mathematical	`Q5`	`SuperSymmetry.SU5.ChargeSpectrum` `minimalSuperSet` `qHd` `qHu` `Q10`	—	—
`insert_filter_card_zero` 📖	—	`IsComplete` `SuperSymmetry.SU5.ChargeSpectrum` `instDecidableEq` `qHd` `qHu` `Q5` `Q10` `minimalSuperSet`	—	—	—
`minimalSuperSet_induction_on_inductive` 📖	—	`SuperSymmetry.SU5.ChargeSpectrum` `ofFinset` `hasSubset` `card`	—	—	`eq_of_subset_card` `card_mono` `exists_minimalSuperSet` `card_of_mem_minimalSuperSet`
`self_neq_mem_minimalSuperSet` 📖	—	`SuperSymmetry.SU5.ChargeSpectrum` `minimalSuperSet`	—	—	—
`self_not_mem_minimalSuperSet` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum` `minimalSuperSet`	—	—
`self_subset_mem_minimalSuperSet` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum` `minimalSuperSet`	`hasSubset`	—	`HasSubset.Subset.eq_1`
`some_qHd_mem_minimalSuperSet_of_none` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum` `minimalSuperSet`	—	—
`some_qHu_mem_minimalSuperSet_of_none` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum` `minimalSuperSet`	—	—
`subset_insert_filter_card_zero` 📖	—	`IsComplete` `SuperSymmetry.SU5.ChargeSpectrum` `hasSubset` `ofFinset` `instDecidableEq` `qHd` `qHu` `Q5` `Q10`	—	—	`subset_insert_filter_card_zero_inductive`
`subset_insert_filter_card_zero_inductive` 📖	—	`IsComplete` `SuperSymmetry.SU5.ChargeSpectrum` `hasSubset` `ofFinset` `instDecidableEq` `qHd` `qHu` `Q5` `Q10` `card`	—	—	`eq_of_subset_card` `card_mono` `exists_minimalSuperSet` `insert_filter_card_zero` `card_of_mem_minimalSuperSet`

---

← Back to Index