exists_enorm_lt' — Mathlib

English

Same as above with slightly different hypotheses; there exists nontrivial element with norm less than c.

Русский

То же самое с другим набором предпосылок; существует элемент ≠ 1 со norme меньшим чем c.

LaTeX

$$$$ \\exists x \\neq 1, \\; \\|x\\|_{e} < c $$$$

Lean4

@[to_additive exists_enorm_lt]
theorem exists_enorm_lt' (E : Type*) [TopologicalSpace E] [ESeminormedMonoid E] [hbot : NeBot (𝓝[≠] (1 : E))] {c : ℝ≥0∞}
    (hc : c ≠ 0) : ∃ x ≠ (1 : E), ‖x‖ₑ < c :=
  frequently_iff_neBot.mpr hbot |>.and_eventually
      (ContinuousENorm.continuous_enorm.tendsto' 1 0 (by simp) |>.eventually_lt_const hc.bot_lt) |>.exists

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