pi_Ico_mem_nhds' — Mathlib

English

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

Русский

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

LaTeX

$$$\left(\forall i, a_i < x_i\right) \rightarrow \left(\forall i, x_i < b_i\right) \rightarrow Ico(a,b) \in \mathcal{N}(x)$$$

Lean4

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

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