subset_interior_normLeOne — Mathlib

English

The equality of normLeOne with the preimage under normAtAllPlaces of expMapBasis''(paramSet) holds.

Русский

Равенство normLeOne и предобраза normAtAllPlaces от expMapBasis''(paramSet) выполняется.

LaTeX

$$normLeOne K = normAtAllPlaces^{-1}(expMapBasis''(paramSet K))$$

Lean4

theorem subset_interior_normLeOne :
    normAtAllPlaces ⁻¹' (expMapBasis '' interior (paramSet K)) ⊆ interior (normLeOne K) :=
  by
  rw [normLeOne_eq_preimage]
  refine
    subset_trans (Set.preimage_mono ?_) <| preimage_interior_subset_interior_preimage (continuous_normAtAllPlaces K)
  have : IsOpen (expMapBasis '' (interior (paramSet K))) :=
    expMapBasis.isOpen_image_of_subset_source isOpen_interior (by simp [expMapBasis_source])
  exact interior_maximal (Set.image_mono interior_subset) this

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