exists_pos_le_norm — Mathlib

English

If HasCompactMulSupport f with a base space and One E, there exists R > 0 such that for all x with ∥x∥ ≥ R we have f(x) = 1.

Русский

Если f обладает компактной поддержкой и значение единицы присутствует в диапазоне, существует R > 0 такое, что для всех x с ∥x∥ ≥ R выполнено f(x) = 1.

LaTeX

$$$\exists R>0,\forall x:\ R \le \|x\| \Rightarrow f(x)=1$$$

Lean4

@[to_additive]
theorem exists_pos_le_norm [One E] (hf : HasCompactMulSupport f) : ∃ R : ℝ, 0 < R ∧ ∀ x : α, R ≤ ‖x‖ → f x = 1 :=
  by
  obtain ⟨K, ⟨hK1, hK2⟩⟩ := exists_compact_iff_hasCompactMulSupport.mpr hf
  obtain ⟨S, hS, hS'⟩ := hK1.isBounded.exists_pos_norm_le
  refine ⟨S + 1, by positivity, fun x hx => hK2 x ((mt <| hS' x) ?_)⟩
  contrapose! hx
  exact lt_add_of_le_of_pos hx zero_lt_one

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