compactSet_eq_union — Mathlib

English

Let K be a number field. Then the compact set associated to K is exactly the image of the closure of the paramSet under expMapBasis, together with the origin; i.e., compactSet(K) = expMapBasis(closure(paramSet(K))) ∪ {0}.

Русский

Пусть K — число поле. Тогда компактное множество, связанное с K, совпадает с образом замыкания paramSet(K) под expMapBasis, дополненным нулем; то есть compactSet(K) = expMapBasis(closure(paramSet(K))) ∪ {0}.

LaTeX

$$$\\operatorname{compactSet}(K) = \\expMapBasis\\bigl(\\overline{\\operatorname{paramSet}(K)}\\bigr) \\cup \\{0\\}$$$

Lean4

theorem compactSet_eq_union : compactSet K = expMapBasis '' closure (paramSet K) ∪ {0} := by
  classical
  ext x
  by_cases hx₀ : x = 0
  · simpa [hx₀] using zero_mem_compactSet K
  · refine ⟨fun hx ↦ Set.mem_union_left _ (compactSet_eq_union_aux₁ hx₀ hx), fun hx ↦ ?_⟩
    simp only [Set.union_singleton, Set.mem_insert_iff, hx₀, false_or] at hx
    exact compactSet_eq_union_aux₂ hx₀ hx

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