Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `MinimallyAllowsTerm`, `instDecidableMinimallyAllowsTerm`	2
Theorems `allowsTermForm_minimallyAllowsTerm`, `allowsTerm_iff_subset_minimallyAllowsTerm`, `allowsTerm_of_has_minimallyAllowsTerm_subset`, `allowsTerm_of_minimallyAllowsTerm`, `card_le_degree_of_minimallyAllowsTerm`, `eq_allowsTermForm_of_minimallyAllowsTerm`, `minimallyAllowsTerm_iff_powerset_countP_eq_one`, `minimallyAllowsTerm_iff_powerset_filter_eq`, `subset_minimallyAllowsTerm_of_allowsTerm`	9
Total	11

SuperSymmetry.SU5.ChargeSpectrum

Definitions

Name	Category	Theorems
`MinimallyAllowsTerm` 📖	MathDef	8 math math: `minimallyAllowsTerm_iff_powerset_filter_eq`, `allowsTermForm_minimallyAllowsTerm`, `allowsTerm_iff_subset_minimallyAllowsTerm`, `minimallyAllowsFinsetTerms_singleton`, `minimallyAllowsTerm_iff_mem_minimallyAllowsTermOfFinset`, `minimallyAllowsTerm_iff_powerset_countP_eq_one`, `subset_minimallyAllowsTerm_of_allowsTerm`, `minimallyAllowsTerm_of_mem_minimallyAllowsTermOfFinset`
`instDecidableMinimallyAllowsTerm` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`allowsTermForm_minimallyAllowsTerm` 📖	mathematical	—	`MinimallyAllowsTerm` `allowsTermForm`	—	`allowsTermForm_allowsTerm` `allowsTermForm_subset_allowsTerm_of_allowsTerm` `allowsTermForm_eq_of_subset` `subset_trans` `subset_antisymm`
`allowsTerm_iff_subset_minimallyAllowsTerm` 📖	mathematical	—	`AllowsTerm` `SuperSymmetry.SU5.ChargeSpectrum` `powerset` `MinimallyAllowsTerm`	—	`subset_minimallyAllowsTerm_of_allowsTerm` `allowsTerm_of_has_minimallyAllowsTerm_subset`
`allowsTerm_of_has_minimallyAllowsTerm_subset` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum` `powerset` `MinimallyAllowsTerm`	`AllowsTerm`	—	`allowsTerm_mono` `allowsTerm_of_minimallyAllowsTerm`
`allowsTerm_of_minimallyAllowsTerm` 📖	mathematical	`MinimallyAllowsTerm`	`AllowsTerm`	—	`self_mem_powerset`
`card_le_degree_of_minimallyAllowsTerm` 📖	mathematical	`MinimallyAllowsTerm`	`card` `SuperSymmetry.SU5.PotentialTerm.degree`	—	`subset_card_le_degree_allowsTerm_of_allowsTerm` `allowsTerm_of_minimallyAllowsTerm` `minimallyAllowsTerm_iff_powerset_filter_eq`
`eq_allowsTermForm_of_minimallyAllowsTerm` 📖	mathematical	`MinimallyAllowsTerm`	`allowsTermForm`	—	`allowsTermForm_subset_allowsTerm_of_allowsTerm` `allowsTerm_of_minimallyAllowsTerm` `minimallyAllowsTerm_iff_powerset_filter_eq`
`minimallyAllowsTerm_iff_powerset_countP_eq_one` 📖	mathematical	—	`MinimallyAllowsTerm` `SuperSymmetry.SU5.ChargeSpectrum` `AllowsTerm` `instDecidableAllowsTermOfDecidableEq` `powerset`	—	`minimallyAllowsTerm_iff_powerset_filter_eq` `allowsTerm_mono`
`minimallyAllowsTerm_iff_powerset_filter_eq` 📖	mathematical	—	`MinimallyAllowsTerm` `SuperSymmetry.SU5.ChargeSpectrum` `AllowsTerm` `instDecidableAllowsTermOfDecidableEq` `powerset`	—	—
`subset_minimallyAllowsTerm_of_allowsTerm` 📖	mathematical	`AllowsTerm`	`SuperSymmetry.SU5.ChargeSpectrum` `powerset` `MinimallyAllowsTerm`	—	`min_exists` `minimallyAllowsTerm_iff_powerset_filter_eq` `subset_trans`

---

← Back to Index