isBounded_normLeOne — Mathlib

English

The set normLeOne(K) is bounded in the ambient real mixed space.

Русский

Множество normLeOne(K) ограничено в реальном смешанном пространстве.

LaTeX

$$$\\text{IsBounded}\\bigl(\\operatorname{normLeOne}(K)\\bigr)$$$

Lean4

theorem isBounded_normLeOne : IsBounded (normLeOne K) := by
  classical
  rw [normLeOne_eq_preimage]
  suffices IsBounded (expMapBasis '' paramSet K)
    by
    obtain ⟨C, hC⟩ := isBounded_iff_forall_norm_le.mp this
    refine isBounded_iff_forall_norm_le.mpr ⟨C, fun x hx ↦ ?_⟩
    rw [norm_eq_sup'_normAtPlace]
    refine sup'_le _ _ fun w _ ↦ ?_
    simpa [normAtAllPlaces_apply, Real.norm_of_nonneg (normAtPlace_nonneg w x)] using
      (pi_norm_le_iff_of_nonempty _).mp (hC _ hx) w
  refine IsBounded.subset ?_ (Set.image_mono subset_closure)
  exact (isCompact_compactSet K).isBounded.subset (expMapBasis_closure_subset_compactSet K)

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