IccLeftChart_extend_interior_pos — Mathlib

English

Let x < y be real numbers and let p be a point in [x, y] with x < p < y. Then the value at 0 of the extended left chart is strictly positive: the extension of the left chart evaluated at p and then at 0 yields a positive real number.

Русский

Пусть x < y — действительные числа, и пусть p ∈ [x, y] с x < p < y. Тогда значение при аргументе 0 у продленного левого графика строго положительно: расширение левого графика, оцениваемое в p, затем в 0, даёт положительное число.

LaTeX

$$$0 < \big((IccLeftChart\ x\ y) .extend (\mathcal{R}\partial 1)\, p\big)\;0$$$

Lean4

theorem IccLeftChart_extend_interior_pos {p : Set.Icc x y} (hp : x < p.val ∧ p.val < y) :
    0 < (IccLeftChart x y).extend (𝓡∂ 1) p 0 :=
  by
  simp_rw [iccLeftChart_extend_zero]
  norm_num [hp.1]

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