Documentation Verification Report

MinimalSuperSet

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

Statistics

MetricCount
DefinitionsminimalSuperSet
1
Theoremscard_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
Total14

SuperSymmetry.SU5.ChargeSpectrum

Definitions

NameCategoryTheorems
minimalSuperSet 📖CompOp
6 mathmath: 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

NameKindAssumesProvesValidatesDepends On
card_of_mem_minimalSuperSet 📖mathematicalSuperSymmetry.SU5.ChargeSpectrum
minimalSuperSet
card
exists_minimalSuperSet 📖mathematicalSuperSymmetry.SU5.ChargeSpectrum
ofFinset
hasSubset
minimalSuperSetHasSubset.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 📖mathematicalQ10SuperSymmetry.SU5.ChargeSpectrum
minimalSuperSet
qHd
qHu
Q5
insert_Q5_mem_minimalSuperSet 📖mathematicalQ5SuperSymmetry.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 📖mathematicalSuperSymmetry.SU5.ChargeSpectrum
minimalSuperSet
self_subset_mem_minimalSuperSet 📖mathematicalSuperSymmetry.SU5.ChargeSpectrum
minimalSuperSet
hasSubsetHasSubset.Subset.eq_1
some_qHd_mem_minimalSuperSet_of_none 📖mathematicalSuperSymmetry.SU5.ChargeSpectrum
minimalSuperSet
some_qHu_mem_minimalSuperSet_of_none 📖mathematicalSuperSymmetry.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