face — Mathlib

English

From corners l,u one constructs a box if l<u coordinatewise; the resulting box corresponds to the core set of x with l_i < x_i < u_i.

Русский

Из углов l,u строится коробка, если l_i < u_i по каждой координате; соответствующее множество состоит из точек x с l_i < x_i < u_i.

LaTeX

$$def mk' (l u : ι → Real) : WithBot (Box ι)$$

Lean4

/-- Face of a box in `ℝⁿ⁺¹ = Fin (n + 1) → ℝ`: the box in `ℝⁿ = Fin n → ℝ` with corners at
`I.lower ∘ Fin.succAbove i` and `I.upper ∘ Fin.succAbove i`. -/
@[simps +simpRhs]
def face {n} (I : Box (Fin (n + 1))) (i : Fin (n + 1)) : Box (Fin n) :=
  ⟨I.lower ∘ Fin.succAbove i, I.upper ∘ Fin.succAbove i, fun _ ↦ I.lower_lt_upper _⟩

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