Map

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

Statistics

Metric	Count
Definitions `map`, `preimageOfFinset`, `preimageOfFinsetCard`	3
Theorems `allowsTermForm_map`, `map_allowsTerm`, `map_empty`, `map_id`, `map_isComplete_iff`, `map_isPhenoConstrained`, `map_map`, `map_ofFieldLabel`, `map_ofPotentialTerm'_toFinset`, `map_ofPotentialTerm_toFinset`, `map_ofYukawaTermsNSum_toFinset`, `map_ofYukawaTerms_toFinset`, `map_phenoConstrainingChargesSP_toFinset`, `map_subset`, `map_yukawaGeneratesDangerousAtLevel`, `mem_map_ofPotentialTerm'_iff`, `mem_map_ofPotentialTerm_iff`, `mem_map_ofYukawaTermsNSum_iff`, `mem_map_ofYukawaTerms_iff`, `not_isPhenoConstrained_of_map`, `not_yukawaGeneratesDangerousAtLevel_of_map`, `preimageOfFinset_card_eq`, `preimageOfFinset_eq`	23
Total	26

SuperSymmetry.SU5.ChargeSpectrum

Definitions

Name	Category	Theorems
`map` 📖	CompOp	22 math math: `map_ofYukawaTermsNSum_toFinset`, `map_phenoConstrainingChargesSP_toFinset`, `map_ofYukawaTerms_toFinset`, `map_isPhenoConstrained`, `map_ofPotentialTerm_toFinset`, `map_ofPotentialTerm'_toFinset`, `map_map`, `map_isComplete_iff`, `mem_map_ofYukawaTermsNSum_iff`, `mem_map_ofYukawaTerms_iff`, `map_empty`, `map_id`, `map_subset`, `map_yukawaGeneratesDangerousAtLevel`, `preimageOfFinset_eq`, `mem_map_ofPotentialTerm'_iff`, `mem_map_ofPotentialTerm_iff`, `allowsTermForm_map`, `FTheory.SU5.ChargeSpectrum.isAnomalyFree_map`, `map_ofFieldLabel`, `FTheory.SU5.Quanta.map_to_Z2_of_isViable`, `map_allowsTerm`
`preimageOfFinset` 📖	CompOp	2 math math: `preimageOfFinset_eq`, `preimageOfFinset_card_eq`
`preimageOfFinsetCard` 📖	CompOp	1 math math: `preimageOfFinset_card_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`allowsTermForm_map` 📖	mathematical	—	`map` `allowsTermForm`	—	—
`map_allowsTerm` 📖	mathematical	`AllowsTerm`	`map`	—	`allowsTerm_iff_subset_allowsTermForm` `allowsTermForm_map` `map_subset`
`map_empty` 📖	mathematical	—	`map` `SuperSymmetry.SU5.ChargeSpectrum` `emptyInst`	—	`empty_qHd` `empty_qHu` `empty_Q5` `empty_Q10`
`map_id` 📖	mathematical	—	`map`	—	—
`map_isComplete_iff` 📖	mathematical	—	`IsComplete` `map`	—	—
`map_isPhenoConstrained` 📖	mathematical	`IsPhenoConstrained`	`map`	—	`map_allowsTerm`
`map_map` 📖	mathematical	—	`map`	—	—
`map_ofFieldLabel` 📖	mathematical	—	`ofFieldLabel` `map`	—	—
`map_ofPotentialTerm'_toFinset` 📖	mathematical	—	`ofPotentialTerm'` `map`	—	`mem_map_ofPotentialTerm'_iff`
`map_ofPotentialTerm_toFinset` 📖	mathematical	—	`ofPotentialTerm` `map`	—	`mem_ofPotentialTerm_iff_mem_ofPotentialTerm` `ofPotentialTerm'_μ_finset` `ofPotentialTerm'_β_finset` `ofPotentialTerm'_W2_finset` `ofPotentialTerm'_W3_finset` `ofPotentialTerm'_W4_finset` `ofPotentialTerm'_K2_finset` `ofPotentialTerm'_topYukawa_finset` `ofPotentialTerm'_bottomYukawa_finset`
`map_ofYukawaTermsNSum_toFinset` 📖	mathematical	—	`ofYukawaTermsNSum` `map`	—	`mem_map_ofYukawaTerms_iff`
`map_ofYukawaTerms_toFinset` 📖	mathematical	—	`ofYukawaTerms` `map`	—	`mem_map_ofPotentialTerm'_iff`
`map_phenoConstrainingChargesSP_toFinset` 📖	mathematical	—	`phenoConstrainingChargesSP` `map`	—	`map_ofPotentialTerm'_toFinset`
`map_subset` 📖	mathematical	`SuperSymmetry.SU5.ChargeSpectrum` `hasSubset`	`map`	—	—
`map_yukawaGeneratesDangerousAtLevel` 📖	mathematical	`YukawaGeneratesDangerousAtLevel`	`map`	—	`yukawaGeneratesDangerousAtLevel_iff_toFinset` `map_phenoConstrainingChargesSP_toFinset` `map_ofYukawaTermsNSum_toFinset`
`mem_map_ofPotentialTerm'_iff` 📖	mathematical	—	`ofPotentialTerm'` `map`	—	`mem_ofPotentialTerm_iff_mem_ofPotentialTerm` `mem_map_ofPotentialTerm_iff`
`mem_map_ofPotentialTerm_iff` 📖	mathematical	—	`ofPotentialTerm` `map`	—	`map_ofPotentialTerm_toFinset`
`mem_map_ofYukawaTermsNSum_iff` 📖	mathematical	—	`ofYukawaTermsNSum` `map`	—	`map_ofYukawaTermsNSum_toFinset`
`mem_map_ofYukawaTerms_iff` 📖	mathematical	—	`ofYukawaTerms` `map`	—	`map_ofYukawaTerms_toFinset`
`not_isPhenoConstrained_of_map` 📖	—	`IsPhenoConstrained` `map`	—	—	`map_isPhenoConstrained`
`not_yukawaGeneratesDangerousAtLevel_of_map` 📖	—	`YukawaGeneratesDangerousAtLevel` `map`	—	—	`map_yukawaGeneratesDangerousAtLevel`
`preimageOfFinset_card_eq` 📖	mathematical	—	`preimageOfFinsetCard` `SuperSymmetry.SU5.ChargeSpectrum` `preimageOfFinset`	—	`preimageOfFinset.eq_1`
`preimageOfFinset_eq` 📖	mathematical	—	`SuperSymmetry.SU5.ChargeSpectrum` `preimageOfFinset` `map` `ofFinset`	—	`mem_ofFinset_iff`

---

← Back to Index