normAtAllPlaces_mem_fundamentalCone_iff

English

Let x be an element of the mixed space. Then x lies in the fundamental cone if and only if its real-space image under normAtAllPlaces also lies in the fundamental cone: mixedSpaceOfRealSpace(normAtAllPlaces x) ∈ fundamentalCone K iff x ∈ fundamentalCone K.

Русский

Пусть x ∈ смешанное пространство. Тогда x ∈ фундаментальный конус тогда и только тогда, когда образ x под normAtAllPlaces в пространстве действительных координат тоже лежит в фундаментальном конусе.

LaTeX

$$$ mixedSpaceOfRealSpace(\\operatorname{normAtAllPlaces} x) \\in \\mathrm{fundamentalCone} \\ K \\;\\iff\\; x \\in \\mathrm{fundamentalCone} \\ K$$$

Lean4

theorem normAtAllPlaces_mem_fundamentalCone_iff {x : mixedSpace K} :
    mixedSpaceOfRealSpace (normAtAllPlaces x) ∈ fundamentalCone K ↔ x ∈ fundamentalCone K := by
  simp_rw [fundamentalCone, Set.mem_diff, Set.mem_preimage, logMap_normAtAllPlaces, Set.mem_setOf_eq,
    norm_normAtAllPlaces]

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