pi_Ioc_mem_nhds' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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