toSet — Mathlib

English

The set I is precisely the set of functions x with x_i in (lower_i, upper_i].

Русский

Множество I точно задает множество функций x с x_i ∈ (lower_i, upper_i].

LaTeX

$$$$I^{toSet} = \\{ x: \\iota \\to \\mathbb{R} \\mid \\forall i, I.lower i < x_i \\le I.upper i \\}.$$$$

Lean4

/-- The set of points in this box: this is the product of half-open intervals `(lower i, upper i]`,
where `lower` and `upper` are this box' corners. -/
@[coe]
def toSet (I : Box ι) : Set (ι → ℝ) :=
  {x | x ∈ I}

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