mem_box_iff' — Mathlib

English

A refined criterion: x ∈ box(n,ν) iff for all i, ν_i < n x_i ≤ ν_i+1.

Русский

Уточнённое условие: x ∈ box(n,ν) тогда и только тогда, когда для всех i выполняется ν_i < n x_i ≤ ν_i+1.

LaTeX

$$$x \in box(n,\nu) \iff ∀ i, \ \nu_i < n x_i \land n x_i ≤ ν_i+1$$$

Lean4

theorem mem_box_iff' [NeZero n] {ν : ι → ℤ} {x : ι → ℝ} : x ∈ box n ν ↔ ∀ i, ν i < n * x i ∧ n * x i ≤ ν i + 1 :=
  by
  have h : 0 < (n : ℝ) := Nat.cast_pos.mpr <| n.pos_of_neZero
  simp_rw [mem_box_iff, ← _root_.le_div_iff₀' h, ← div_lt_iff₀' h]

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