idealSetEquiv_symm_apply — Mathlib

English

Norm compatibilities persist under the mappings between integerSet and idealSet data.

Русский

Сохранение норм сохраняется между данными integerSet и idealSet.

LaTeX

$$$\\operatorname{intNorm} = \\operatorname{mixedEmbedding.norm}$ on corresponding elements.$$

Lean4

theorem idealSetEquiv_symm_apply (a : { a : integerSet K // (preimageOfMemIntegerSet a : 𝓞 K) ∈ (J : Set (𝓞 K)) }) :
    ((idealSetEquiv K J).symm a : mixedSpace K) = a := by
  rw [← (idealSetEquiv_apply ((idealSetEquiv K J).symm a)), Equiv.apply_symm_apply]

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