mem_normLeOne — Mathlib

English

The normLeOne set is the preimage under normAtAllPlaces of the image of normLeOne under normAtAllPlaces: normLeOne = (normAtAllPlaces)^{-1}((normAtAllPlaces)''(normLeOne)).

Русский

Множество normLeOne равно прообразу образа normLeOne под normAtAllPlaces.

LaTeX

$$$ \\operatorname{normLeOne} \\ K = (\\operatorname{normAtAllPlaces})^{-1}\\big( (\\operatorname{normAtAllPlaces})''( \\operatorname{normLeOne} \\ K) \\big)$$$

Lean4

theorem mem_normLeOne {x : mixedSpace K} : x ∈ normLeOne K ↔ x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1 :=
  Set.mem_sep_iff

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