exists_enorm_lt — Mathlib

English

For ENNReal r, if r > 0, there exists x with 0 < ‖x‖ₑ and ‖x‖ₑ < r.

Русский

Для ENNReal r > 0 существует x с 0 < ‖x‖ₑ и ‖x‖ₑ < r.

LaTeX

$$$ \forall r : \mathrm{ENNReal},\ r > 0 \Rightarrow \exists x : α, 0 < \|x\|_e \land \|x\|_e < r $$$

Lean4

/-- TODO: merge with `_root_.exists_enorm_lt`. -/
theorem exists_enorm_lt {r : ℝ≥0∞} (hr : 0 < r) : ∃ x : α, 0 < ‖x‖ₑ ∧ ‖x‖ₑ < r :=
  match r with
  | ∞ => exists_one_lt_enorm α |>.imp fun _ hx => ⟨zero_le_one.trans_lt hx, ENNReal.coe_lt_top⟩
  | (r : ℝ≥0) =>
    exists_nnnorm_lt α (ENNReal.coe_pos.mp hr) |>.imp fun _ => And.imp ENNReal.coe_pos.mpr ENNReal.coe_lt_coe.mpr

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