mixedEmbedding_preimageOfMemIntegerSet

English

The integer set norm, viewed as a real, coincides with the mixedEmbedding norm on the corresponding element.

Русский

Норма intNorm элемента integerSet(K), приведенная к вещественному числу, совпадает с нормой смешанного вложения.

LaTeX

$$(intNorm a) as Real equals mixedEmbedding.norm (a : mixedSpace K) for a ∈ integerSet(K).$$

Lean4

@[simp]
theorem mixedEmbedding_preimageOfMemIntegerSet (a : integerSet K) :
    mixedEmbedding K (preimageOfMemIntegerSet a : 𝓞 K) = (a : mixedSpace K) := by
  rw [preimageOfMemIntegerSet, (mem_integerSet.mp a.prop).2.choose_spec]

Похожие утверждения