compactSet_eq_union_aux₁ — Mathlib

English

The set compactSet is compact.

Русский

Множество compactSet компактно.

LaTeX

$$IsCompact (compactSet K)$$

Lean4

theorem compactSet_eq_union_aux₁ {x : realSpace K} (hx₀ : x ≠ 0) (hx₁ : x ∈ compactSet K) :
    x ∈ expMapBasis '' closure (paramSet K) := by
  classical
  obtain ⟨c, hc, ⟨_, ⟨y, hy, rfl⟩, rfl⟩⟩ := hx₁
  refine ⟨fun w ↦ if w = w₀ then Real.log c else y w, ?_, ?_⟩
  · rw [closure_paramSet, Set.mem_univ_pi]
    intro w
    split_ifs with h
    · refine Real.log_nonpos hc.1 hc.2
    · simpa [h] using hy w (Set.mem_univ _)
  · have hc' : 0 < c := by
      contrapose! hx₀
      rw [le_antisymm hx₀ hc.1, zero_smul]
    rw [expMapBasis_apply'', if_pos rfl, Real.exp_log hc']
    congr with w
    split_ifs with h
    · simpa [h, eq_comm] using hy w₀
    · rfl

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