Other lemmas related to nonPhenoConstrainedCharges

theorem FTheory.SU5U1.Charges.card_Q5_le_three_of_nonPhenoConstrainedCharges_of_same (x : Option ℤ × Option ℤ × Finset ℤ × Finset ℤ) : x ∈ (nonPhenoConstrainedCharges CodimensionOneConfig.same).toMultiset → x.2.2.1.card ≤ 4

theorem FTheory.SU5U1.Charges.card_Q5_le_three_of_nonPhenoConstrainedCharges_of_nearestNeighbor (x : Option ℤ × Option ℤ × Finset ℤ × Finset ℤ) : x ∈ (nonPhenoConstrainedCharges CodimensionOneConfig.nearestNeighbor).toMultiset → x.2.2.1.card ≤ 4

theorem FTheory.SU5U1.Charges.card_Q5_le_three_of_nonPhenoConstrainedCharges_of_nextToNearestNeighbor (x : Option ℤ × Option ℤ × Finset ℤ × Finset ℤ) : x ∈ (nonPhenoConstrainedCharges CodimensionOneConfig.nextToNearestNeighbor).toMultiset → x.2.2.1.card ≤ 4

theorem FTheory.SU5U1.Charges.card_Q5_le_three_of_nonPhenoConstrainedCharges (I : CodimensionOneConfig) (x : Option ℤ × Option ℤ × Finset ℤ × Finset ℤ) : x ∈ (nonPhenoConstrainedCharges I).toMultiset → x.2.2.1.card ≤ 4

theorem FTheory.SU5U1.Charges.card_Q10_le_three_of_nonPhenoConstrainedCharges_of_same (x : Option ℤ × Option ℤ × Finset ℤ × Finset ℤ) : x ∈ (nonPhenoConstrainedCharges CodimensionOneConfig.same).toMultiset → x.2.2.2.card ≤ 3

theorem FTheory.SU5U1.Charges.card_Q10_le_three_of_nonPhenoConstrainedCharges_of_nearestNeighbor (x : Option ℤ × Option ℤ × Finset ℤ × Finset ℤ) : x ∈ (nonPhenoConstrainedCharges CodimensionOneConfig.nearestNeighbor).toMultiset → x.2.2.2.card ≤ 3

theorem FTheory.SU5U1.Charges.card_Q10_le_three_of_nonPhenoConstrainedCharges_of_nextToNearestNeighbor (x : Option ℤ × Option ℤ × Finset ℤ × Finset ℤ) : x ∈ (nonPhenoConstrainedCharges CodimensionOneConfig.nextToNearestNeighbor).toMultiset → x.2.2.2.card ≤ 3

theorem FTheory.SU5U1.Charges.card_Q10_le_three_of_nonPhenoConstrainedCharges (I : CodimensionOneConfig) (x : Option ℤ × Option ℤ × Finset ℤ × Finset ℤ) : x ∈ (nonPhenoConstrainedCharges I).toMultiset → x.2.2.2.card ≤ 3