mem_box_iff — Mathlib

English

x belongs to box(n,ν) if and only if for all i, ν_i/n < x_i ≤ (ν_i+1)/n.

Русский

x принадлежит box(n,ν) тогда и только тогда, когда для каждого i выполняется ν_i/n < x_i ≤ (ν_i+1)/n.

LaTeX

$$$x \in \text{box}(n,\nu) \iff \forall i, \ \frac{\nu_i}{n} < x_i \le \frac{\nu_i+1}{n}$$$

Lean4

@[simp]
theorem mem_box_iff [NeZero n] {ν : ι → ℤ} {x : ι → ℝ} : x ∈ box n ν ↔ ∀ i, ν i / n < x i ∧ x i ≤ (ν i + 1) / n := by
  simp_rw [Box.mem_def, box, Set.mem_Ioc]

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