mem_Ioo_self_sub_add — Mathlib

English

If x ≠ ∞, x ≠ 0, ε1 ≠ 0, ε2 ≠ 0, then x ∈ Ioo (x − ε1) (x + ε2).

Русский

Если x ≠ ∞, x ≠ 0, ε1 ≠ 0, ε2 ≠ 0, то x ∈ Ioo(x − ε1, x + ε2).

LaTeX

$$$ x \neq \infty \Rightarrow x \neq 0 \Rightarrow \epsilon_1 \neq 0 \Rightarrow \epsilon_2 \neq 0 \Rightarrow x \in Ioo (x - \epsilon_1) (x + \epsilon_2) $$$

Lean4

theorem mem_Ioo_self_sub_add : x ≠ ∞ → x ≠ 0 → ε₁ ≠ 0 → ε₂ ≠ 0 → x ∈ Ioo (x - ε₁) (x + ε₂) := fun xt x0 ε0 ε0' =>
  ⟨ENNReal.sub_lt_self xt x0 ε0, lt_add_right xt ε0'⟩

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