PhysLean Documentation

PhysLean.Particles.SuperSymmetry.SU5.Charges.MinimalSuperSet

Minimal super set #

Given a a colleciton of charges x, and two sets of charges S5 and S10, a minimal super set of x is the collection of charge y which is a super sets of x, for which the the additional charges in y are corresponding in S5 and S10, and which is minimal in this regard.

source
def SuperSymmetry.SU5.Charges.minimalSuperSet (S5 S10 : Finset ℤ) (x : Charges) :
Finset Charges

Given a collection of charges x in ofFinset S5 S10, the minimimal charges y in ofFinset S5 S10 which are a super sets of x.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem SuperSymmetry.SU5.Charges.self_subset_mem_minimalSuperSet (S5 S10 : Finset ℤ) (x y : Charges) (hy : y ∈ minimalSuperSet S5 S10 x) :
    x ⊆ y
    source
    @[simp]
    theorem SuperSymmetry.SU5.Charges.self_not_mem_minimalSuperSet (S5 S10 : Finset ℤ) (x : Charges) :
    x ∉ minimalSuperSet S5 S10 x
    source
    theorem SuperSymmetry.SU5.Charges.self_neq_mem_minimalSuperSet (S5 S10 : Finset ℤ) (x y : Charges) (hy : y ∈ minimalSuperSet S5 S10 x) :
    x ≠ y
    source
    theorem SuperSymmetry.SU5.Charges.card_of_mem_minimalSuperSet {S5 S10 : Finset ℤ} {x : Charges} (y : Charges) (hy : y ∈ minimalSuperSet S5 S10 x) :
    y.card = x.card + 1
    source
    theorem SuperSymmetry.SU5.Charges.insert_Q5_mem_minimalSuperSet {S5 S10 : Finset ℤ} {x : Charges} (z : ℤ) (hz : z ∈ S5) (hznot : z ∉ x.2.2.1) :
    (x.1, x.2.1, insert z x.2.2.1, x.2.2.2) ∈ minimalSuperSet S5 S10 x
    source
    theorem SuperSymmetry.SU5.Charges.insert_Q10_mem_minimalSuperSet {S5 S10 : Finset ℤ} {x : Charges} (z : ℤ) (hz : z ∈ S10) (hznot : z ∉ x.2.2.2) :
    (x.1, x.2.1, x.2.2.1, insert z x.2.2.2) ∈ minimalSuperSet S5 S10 x
    source
    theorem SuperSymmetry.SU5.Charges.some_qHd_mem_minimalSuperSet_of_none {S5 S10 : Finset ℤ} {x2 : Option ℤ × Finset ℤ × Finset ℤ} (z : ℤ) (hz : z ∈ S5) :
    (some z, x2) ∈ minimalSuperSet S5 S10 (none, x2)
    source
    theorem SuperSymmetry.SU5.Charges.some_qHu_mem_minimalSuperSet_of_none {S5 S10 : Finset ℤ} {x1 : Option ℤ} {x2 : Finset ℤ × Finset ℤ} (z : ℤ) (hz : z ∈ S5) :
    (x1, some z, x2) ∈ minimalSuperSet S5 S10 (x1, none, x2)
    source
    theorem SuperSymmetry.SU5.Charges.exists_minimalSuperSet (S5 S10 : Finset ℤ) {x y : Charges} (hy : y ∈ ofFinset S5 S10) (hsubset : x ⊆ y) (hxneqy : x ≠ y) :
    ∃ z ∈ minimalSuperSet S5 S10 x, z ⊆ y
    source
    theorem SuperSymmetry.SU5.Charges.minimalSuperSet_induction_on_inductive {S5 S10 : Finset ℤ} (p : Charges → Prop) (hp : ∀ (x : Charges), p x → ∀ y ∈ minimalSuperSet S5 S10 x, p y) (x : Charges) (hbase : p x) (y : Charges) (hy : y ∈ ofFinset S5 S10) (hsubset : x ⊆ y) (n : ℕ) (hn : n = y.card - x.card) :
    p y