compactSet_eq_union_aux₂ — Mathlib

English

The image of normAtAllPlaces composed with fundamentalCone corresponds to expMapBasis applied to paramSet.

Русский

Образ normAtAllPlaces, сопоставленный с fundamentalCone, соответствует expMapBasis, применённому к paramSet.

LaTeX

$$normAtAllPlaces' (normLeOne K) image = image expMapBasis (paramSet K)$$

Lean4

theorem compactSet_eq_union_aux₂ {x : realSpace K} (hx₀ : x ≠ 0) (hx₁ : x ∈ expMapBasis '' closure (paramSet K)) :
    x ∈ compactSet K := by
  classical
  simp only [closure_paramSet, Set.mem_image, Set.mem_smul, exists_exists_and_eq_and] at hx₁ ⊢
  obtain ⟨y, hy, rfl⟩ := hx₁
  refine
    ⟨Real.exp (y w₀), ⟨Real.exp_nonneg _, ?_⟩, fun i ↦ if i = w₀ then 0 else y i, Set.mem_univ_pi.mpr fun w ↦ ?_, by
      rw [expMapBasis_apply'' y]⟩
  · exact Real.exp_le_one_iff.mpr (by simpa using hy w₀ (Set.mem_univ _))
  · split_ifs with h
    · rfl
    · simpa [h] using hy w (Set.mem_univ _)

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