pi_Ioo_mem_nhds' — Mathlib

English

Variant with primes: if ha and hb hold coordinatewise, then Ioo(a',b') is a neighborhood of x'.

Русский

Вариант с апострофами: если ha и hb выполняются покомпонентно, то Ioo(a',b') является окрестностью x'.

LaTeX

$$$\left(\forall i, a'_i < x'_i\right) \rightarrow \left(\forall i, x'_i < b'_i\right) \rightarrow Ioo(a',b') \in \mathcal{N}(x')$$$

Lean4

theorem pi_Ioo_mem_nhds' (ha : ∀ i, a' i < x' i) (hb : ∀ i, x' i < b' i) : Ioo a' b' ∈ 𝓝 x' :=
  pi_Ioo_mem_nhds ha hb

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