∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  Function.Injective (Quotient.lift (NumberField.mixedEmbedding.fundamentalCone.integerSetToAssociates K) ⋯) ∧
    Function.Surjective (Quotient.lift (NumberField.mixedEmbedding.fundamentalCone.integerSetToAssociates K) ⋯)