Minimally allows terms given sets of allowed charges

In this module our main definition is minimallyAllowsTermsOfFinset S5 S10 T, which is the set of charges that minimally allows the potential term T which live in ofFinset S5 S10.

To define this function we need some auxiliary functions that take a finite set of integers and return multisets of integers of a given cardinality containing only those elements.

Auxillary results: Multisets from Finsets of given cardinality.

def FTheory.SU5U1.Charges.toMultisetsOne (s : Finset ℤ) : Multiset (Multiset ℤ)

The multisets of cardinality 1 containing elements from a finite set s.

Equations

• FTheory.SU5U1.Charges.toMultisetsOne s = Multiset.map (fun (X : Finset ℤ) => X.val) (Finset.powersetCard 1 s).val

@[simp]

theorem FTheory.SU5U1.Charges.mem_toMultisetsOne_iff {s : Finset ℤ} (X : Multiset ℤ) : X ∈ toMultisetsOne s ↔ X.toFinset ⊆ s ∧ X.card = 1

def FTheory.SU5U1.Charges.toMultisetsTwo (s : Finset ℤ) : Multiset (Multiset ℤ)

The multisets of cardinality 2 containing elements from a finite set s.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem FTheory.SU5U1.Charges.mem_toMultisetsTwo_iff {s : Finset ℤ} (X : Multiset ℤ) : X ∈ toMultisetsTwo s ↔ X.toFinset ⊆ s ∧ X.card = 2

def FTheory.SU5U1.Charges.toMultisetsThree (s : Finset ℤ) : Multiset (Multiset ℤ)

The multisets of cardinality 3 containing elements from a finite set s.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem FTheory.SU5U1.Charges.mem_toMultisetsThree_iff {s : Finset ℤ} (X : Multiset ℤ) : X ∈ toMultisetsThree s ↔ X.toFinset ⊆ s ∧ X.card = 3

minimallyAllowsTermOfFinset

def FTheory.SU5U1.Charges.minimallyAllowsTermsOfFinset (S5 S10 : Finset ℤ) (T : SuperSymmetry.SU5.PotentialTerm) : Multiset Charges

The multiset of all charges within ofFinset S5 S10 which minimally allow the potential term T.

Equations

• One or more equations did not get rendered due to their size.

theorem FTheory.SU5U1.Charges.eq_allowsTermForm_of_mem_minimallyAllowsTermOfFinset {S5 S10 : Finset ℤ} {T : SuperSymmetry.SU5.PotentialTerm} {x : Charges} (hx : x ∈ minimallyAllowsTermsOfFinset S5 S10 T) : ∃ (a : ℤ) (b : ℤ) (c : ℤ), x = allowsTermForm a b c T

theorem FTheory.SU5U1.Charges.allowsTerm_of_mem_minimallyAllowsTermOfFinset {S5 S10 : Finset ℤ} {T : SuperSymmetry.SU5.PotentialTerm} {x : Charges} (hx : x ∈ minimallyAllowsTermsOfFinset S5 S10 T) : x.AllowsTerm T

theorem FTheory.SU5U1.Charges.mem_minimallyAllowsTermOfFinset_of_minimallyAllowsTerm {S5 S10 : Finset ℤ} {T : SuperSymmetry.SU5.PotentialTerm} (x : Charges) (h : x.MinimallyAllowsTerm T) (hx : x ∈ ofFinset S5 S10) : x ∈ minimallyAllowsTermsOfFinset S5 S10 T

theorem FTheory.SU5U1.Charges.minimallyAllowsTerm_of_mem_minimallyAllowsTermOfFinset {S5 S10 : Finset ℤ} {T : SuperSymmetry.SU5.PotentialTerm} {x : Charges} (hx : x ∈ minimallyAllowsTermsOfFinset S5 S10 T) : x.MinimallyAllowsTerm T

theorem FTheory.SU5U1.Charges.mem_ofFinset_of_mem_minimallyAllowsTermOfFinset {S5 S10 : Finset ℤ} {T : SuperSymmetry.SU5.PotentialTerm} {x : Charges} (hx : x ∈ minimallyAllowsTermsOfFinset S5 S10 T) : x ∈ ofFinset S5 S10

theorem FTheory.SU5U1.Charges.minimallyAllowsTermOfFinset_subset_ofFinset {S5 S10 : Finset ℤ} {T : SuperSymmetry.SU5.PotentialTerm} : minimallyAllowsTermsOfFinset S5 S10 T ⊆ (ofFinset S5 S10).val

theorem FTheory.SU5U1.Charges.minimallyAllowsTerm_iff_mem_minimallyAllowsTermOfFinset {S5 S10 : Finset ℤ} {T : SuperSymmetry.SU5.PotentialTerm} {x : Charges} (hx : x ∈ ofFinset S5 S10) : x.MinimallyAllowsTerm T ↔ x ∈ minimallyAllowsTermsOfFinset S5 S10 T

theorem FTheory.SU5U1.Charges.minimallyAllowsTermOfFinset_subset_of_subset {S5 S5' S10 S10' : Finset ℤ} {T : SuperSymmetry.SU5.PotentialTerm} (h5 : S5' ⊆ S5) (h10 : S10' ⊆ S10) : minimallyAllowsTermsOfFinset S5' S10' T ⊆ minimallyAllowsTermsOfFinset S5 S10 T