egauge_ball_one_le_of_one_lt_norm

English

If 1 < ||c||, then egauge on ball radius 1 is bounded by ||c|| times ||x||.

Русский

Если 1 < ||c||, то egauge 𝕜 (ball 0 1) x ≤ ||c|| · ||x||.

LaTeX

$$$\\forall c, x:\\; 1 < \\|c\\| \\Rightarrow egauge 𝕜 (ball 0 1) x \\le \\|c\\|_e \\cdot \\|x\\|_e.$$$

Lean4

theorem egauge_ball_one_le_of_one_lt_norm (hc : 1 < ‖c‖) (x : E) : egauge 𝕜 (ball 0 1) x ≤ ‖c‖ₑ * ‖x‖ₑ := by
  simpa using egauge_ball_le_of_one_lt_norm hc (.inl one_ne_zero)

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