closure_normLeOne_subset — Mathlib

English

The closure of normLeOne(K) is contained in the preimage of compactSet(K) under normAtAllPlaces.

Русский

Замыкание normLeOne(K) содержится в предобразе через normAtAllPlaces от компактного множества compactSet(K).

LaTeX

$$$\\overline{\\operatorname{normLeOne}}(K) \\subseteq \\operatorname{normAtAllPlaces}^{-1}\\bigl(\\operatorname{compactSet}(K)\\bigr)$$$

Lean4

theorem closure_normLeOne_subset : closure (normLeOne K) ⊆ normAtAllPlaces ⁻¹' (compactSet K) :=
  by
  rw [normLeOne_eq_preimage]
  refine ((continuous_normAtAllPlaces K).closure_preimage_subset _).trans (Set.preimage_mono ?_)
  refine (isCompact_compactSet K).isClosed.closure_subset_iff.mpr ?_
  exact (Set.image_mono subset_closure).trans (expMapBasis_closure_subset_compactSet _)

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