normAtAllPlaces_image_preimage_expMapBasis

English

The image of normAtAllPlaces applied to the preimage under normAtAllPlaces of expMapBasis(s) equals expMapBasis(s).

Русский

Изображение normAtAllPlaces применённого к множеству, являющемуся предобразом normAtAllPlaces от expMapBasis(s), равно expMapBasis(s).

LaTeX

$$$\operatorname{normAtAllPlaces} '' (\operatorname{normAtAllPlaces}^{-1}'(\expMapBasis'' s)) = \expMapBasis'' s$$

Lean4

theorem normAtAllPlaces_image_preimage_expMapBasis (s : Set (realSpace K)) :
    normAtAllPlaces '' (normAtAllPlaces ⁻¹' (expMapBasis '' s)) = expMapBasis '' s :=
  by
  apply normAtAllPlaces_image_preimage_of_nonneg
  rintro _ ⟨x, _, rfl⟩ w
  exact (expMapBasis_pos _ _).le

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