FinsetTerms

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

Statistics

Metric	Count
Definitions MinimallyAllowsFinsetTerms, instDecidableMinimallyAllowsFinsetTerms, minTopBottom	3
Theorems allowsTerm_bottomYukawa_of_mem_minTopBottom, allowsTerm_of_minimallyAllowsFinsetTerms, allowsTerm_topYukawa_of_mem_minTopBottom, mem_minTopBottom_of_minimallyAllowsFinsetTerms, minimallyAllowsFinsetTerms_singleton	5
Total	8

SuperSymmetry.SU5.ChargeSpectrum

Definitions

Name	Category	Theorems
MinimallyAllowsFinsetTerms 📖	MathDef	1 math math: minimallyAllowsFinsetTerms_singleton
instDecidableMinimallyAllowsFinsetTerms 📖	CompOp	—
minTopBottom 📖	CompOp	1 math math: mem_minTopBottom_of_minimallyAllowsFinsetTerms

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
allowsTerm_bottomYukawa_of_mem_minTopBottom 📖	mathematical	SuperSymmetry.SU5.ChargeSpectrum minTopBottom	AllowsTerm SuperSymmetry.SU5.PotentialTerm.bottomYukawa	—	allowsTerm_iff_subset_allowsTermForm subset_def
allowsTerm_of_minimallyAllowsFinsetTerms 📖	mathematical	MinimallyAllowsFinsetTerms SuperSymmetry.SU5.PotentialTerm	AllowsTerm	—	self_mem_powerset
allowsTerm_topYukawa_of_mem_minTopBottom 📖	mathematical	SuperSymmetry.SU5.ChargeSpectrum minTopBottom	AllowsTerm SuperSymmetry.SU5.PotentialTerm.topYukawa	—	allowsTerm_iff_subset_allowsTermForm subset_def
mem_minTopBottom_of_minimallyAllowsFinsetTerms 📖	mathematical	MinimallyAllowsFinsetTerms SuperSymmetry.SU5.PotentialTerm SuperSymmetry.SU5.instDecidableEqPotentialTerm SuperSymmetry.SU5.PotentialTerm.topYukawa SuperSymmetry.SU5.PotentialTerm.bottomYukawa SuperSymmetry.SU5.ChargeSpectrum ofFinset	minTopBottom	—	allowsTerm_of_minimallyAllowsFinsetTerms allowsTerm_iff_subset_allowsTermForm mem_ofFinset_iff
minimallyAllowsFinsetTerms_singleton 📖	mathematical	—	MinimallyAllowsFinsetTerms SuperSymmetry.SU5.PotentialTerm MinimallyAllowsTerm	—	—

---

← Back to Index