mem_admissibleIndex_of_mem_box — Mathlib

English

If B has integral vertices and x ∈ B, then the index of x is admissible for B.

Русский

Если B имеет интегральные вершины и x ∈ B, то индекс x принадлежит admissibleIndex n B.

LaTeX

$$$$ index\, n\, x \in admissibleIndex\ n\ B $$$$

Lean4

/-- If `B : BoxIntegral.Box` has integral vertices and contains the point `x`, then the index of
`x` is admissible for `B`. -/
theorem mem_admissibleIndex_of_mem_box {B : Box ι} (hB : hasIntegralVertices B) {x : ι → ℝ} (hx : x ∈ B) :
    index n x ∈ admissibleIndex n B := by
  obtain ⟨l, u, hl, hu⟩ := hB
  simp_rw [mem_admissibleIndex_iff, Box.le_iff_bounds, box_lower, box_upper, Pi.le_def, index_apply, hl, hu, ←
    forall_and]
  push_cast
  refine fun i ↦ ⟨?_, ?_⟩
  · exact (mem_admissibleIndex_of_mem_box_aux₁ n (x i) (l i)).mp ((hl i) ▸ (hx i).1)
  · exact (mem_admissibleIndex_of_mem_box_aux₂ n (x i) (u i)).mp ((hu i) ▸ (hx i).2)

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