y_support — Mathlib

English

The support of y(D) equals the ball of radius 1+D around 0 when D>0 and D<1.

Русский

Опора y(D) равна шарe радиуса 1+D вокруг нуля при D>0 и D<1.

LaTeX

$$Function.support (y D) = ball 0 (1+D)$$

Lean4

theorem y_support {D : ℝ} (Dpos : 0 < D) (D_lt_one : D < 1) : support (y D : E → ℝ) = ball (0 : E) (1 + D) :=
  support_eq_iff.2 ⟨fun _ hx => (y_pos_of_mem_ball Dpos D_lt_one hx).ne', fun _ hx => y_eq_zero_of_notMem_ball Dpos hx⟩

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