Documentation Verification Report

OfFinset

📁 Source: PhysLean/Particles/SuperSymmetry/SU5/ChargeSpectrum/MinimallyAllowsTerm/OfFinset.lean

Statistics

Metric	Count
Definitions `minimallyAllowsTermsOfFinset`, `toMultisetsOne`, `toMultisetsThree`, `toMultisetsTwo`	4
Theorems `allowsTerm_of_mem_minimallyAllowsTermOfFinset`, `eq_allowsTermForm_of_mem_minimallyAllowsTermOfFinset`, `mem_minimallyAllowsTermOfFinset_of_minimallyAllowsTerm`, `mem_ofFinset_of_mem_minimallyAllowsTermOfFinset`, `mem_toMultisetsOne_iff`, `mem_toMultisetsThree_iff`, `mem_toMultisetsTwo_iff`, `minimallyAllowsTermOfFinset_subset_ofFinset`, `minimallyAllowsTermOfFinset_subset_of_subset`, `minimallyAllowsTerm_iff_mem_minimallyAllowsTermOfFinset`, `minimallyAllowsTerm_of_mem_minimallyAllowsTermOfFinset`, `not_isPhenoConstrained_of_minimallyAllowsTermsOfFinset_topYukawa`	12
Total	16

SuperSymmetry.SU5.ChargeSpectrum

Definitions

Name	Category	Theorems
`minimallyAllowsTermsOfFinset` 📖	CompOp	4 math math: `minimallyAllowsTermOfFinset_subset_ofFinset`, `minimallyAllowsTermOfFinset_subset_of_subset`, `minimallyAllowsTerm_iff_mem_minimallyAllowsTermOfFinset`, `mem_minimallyAllowsTermOfFinset_of_minimallyAllowsTerm`
`toMultisetsOne` 📖	CompOp	1 math math: `mem_toMultisetsOne_iff`
`toMultisetsThree` 📖	CompOp	1 math math: `mem_toMultisetsThree_iff`
`toMultisetsTwo` 📖	CompOp	1 math math: `mem_toMultisetsTwo_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`allowsTerm_of_mem_minimallyAllowsTermOfFinset` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum` `minimallyAllowsTermsOfFinset`	`AllowsTerm`	—	`eq_allowsTermForm_of_mem_minimallyAllowsTermOfFinset` `allowsTermForm_allowsTerm`
`eq_allowsTermForm_of_mem_minimallyAllowsTermOfFinset` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum` `minimallyAllowsTermsOfFinset`	`allowsTermForm`	—	—
`mem_minimallyAllowsTermOfFinset_of_minimallyAllowsTerm` 📖	mathematical	`MinimallyAllowsTerm` `SuperSymmetry.SU5.ChargeSpectrum` `ofFinset`	`minimallyAllowsTermsOfFinset`	—	`eq_allowsTermForm_of_minimallyAllowsTerm` `mem_ofFinset_iff`
`mem_ofFinset_of_mem_minimallyAllowsTermOfFinset` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum` `minimallyAllowsTermsOfFinset`	`ofFinset`	—	`mem_ofFinset_iff`
`mem_toMultisetsOne_iff` 📖	mathematical	—	`toMultisetsOne`	—	—
`mem_toMultisetsThree_iff` 📖	mathematical	—	`toMultisetsThree`	—	—
`mem_toMultisetsTwo_iff` 📖	mathematical	—	`toMultisetsTwo`	—	—
`minimallyAllowsTermOfFinset_subset_ofFinset` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum` `minimallyAllowsTermsOfFinset` `ofFinset`	—	`mem_ofFinset_of_mem_minimallyAllowsTermOfFinset`
`minimallyAllowsTermOfFinset_subset_of_subset` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum` `minimallyAllowsTermsOfFinset`	—	`mem_ofFinset_of_mem_minimallyAllowsTermOfFinset` `minimallyAllowsTerm_iff_mem_minimallyAllowsTermOfFinset` `ofFinset_subset_of_subset`
`minimallyAllowsTerm_iff_mem_minimallyAllowsTermOfFinset` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum` `ofFinset`	`MinimallyAllowsTerm` `minimallyAllowsTermsOfFinset`	—	`mem_minimallyAllowsTermOfFinset_of_minimallyAllowsTerm` `minimallyAllowsTerm_of_mem_minimallyAllowsTermOfFinset`
`minimallyAllowsTerm_of_mem_minimallyAllowsTermOfFinset` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum` `minimallyAllowsTermsOfFinset`	`MinimallyAllowsTerm`	—	`eq_allowsTermForm_of_mem_minimallyAllowsTermOfFinset` `allowsTermForm_minimallyAllowsTerm` `MinimallyAllowsTerm.congr_simp`
`not_isPhenoConstrained_of_minimallyAllowsTermsOfFinset_topYukawa` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum` `minimallyAllowsTermsOfFinset` `SuperSymmetry.SU5.PotentialTerm.topYukawa`	`IsPhenoConstrained`	—	—

---

← Back to Index