∀ {K : Type u_1} [inst : Field K] (A : Set (NumberField.mixedEmbedding.mixedSpace K)),
  Pairwise
    (Function.onFun Disjoint fun s => ⇑(NumberField.mixedEmbedding.negAt s) '' NumberField.mixedEmbedding.plusPart A)