IsComplete of nonPhenoConstrainedCharges

We prove that each charge in the trees nonPhenoConstrainedCharges I, is complete.

theorem FTheory.SU5U1.Charges.isComplete_of_mem_nonPhenoConstrainedCharge_same (x : Option ℤ × Option ℤ × Finset ℤ × Finset ℤ) : x ∈ (nonPhenoConstrainedCharges CodimensionOneConfig.same).toMultiset → IsComplete x

theorem FTheory.SU5U1.Charges.isComplete_of_mem_nonPhenoConstrainedCharge_nearestNeighbor (x : Option ℤ × Option ℤ × Finset ℤ × Finset ℤ) : x ∈ (nonPhenoConstrainedCharges CodimensionOneConfig.nearestNeighbor).toMultiset → IsComplete x

theorem FTheory.SU5U1.Charges.isComplete_of_mem_nonPhenoConstrainedCharge_nextToNearestNeighbor (x : Option ℤ × Option ℤ × Finset ℤ × Finset ℤ) : x ∈ (nonPhenoConstrainedCharges CodimensionOneConfig.nextToNearestNeighbor).toMultiset → IsComplete x

theorem FTheory.SU5U1.Charges.isComplete_of_mem_nonPhenoConstrainedCharge (I : CodimensionOneConfig) (x : Option ℤ × Option ℤ × Finset ℤ × Finset ℤ) : x ∈ (nonPhenoConstrainedCharges I).toMultiset → IsComplete x