English
From two coordinate functions l,u : ι → ℝ, mk' creates a WithBot(Box ι) by taking ⟨l,u,h⟩ if l_i < u_i for all i, otherwise bottom; the underlying set is { x : ι → ℝ | ∀ i, x_i ∈ Ioc(l_i,u_i) }.
Русский
Из двух функций координат l и u: ι → ℝ строится WithBot(Box ι) через ⟨l,u,h⟩ при условии l_i < u_i для всех i, иначе ⊥; множество, соответствующее этим координатам, равно { x | ∀ i, l_i < x_i < u_i }.
LaTeX
$$def mk'(l u : ι → Real) : WithBot (Box ι)$$
Lean4
/-- Make a `WithBot (Box ι)` from a pair of corners `l u : ι → ℝ`. If `l i < u i` for all `i`,
then the result is `⟨l, u, _⟩ : Box ι`, otherwise it is `⊥`. In any case, the result interpreted
as a set in `ι → ℝ` is the set `{x : ι → ℝ | ∀ i, x i ∈ Ioc (l i) (u i)}`. -/
def mk' (l u : ι → ℝ) : WithBot (Box ι) :=
if h : ∀ i, l i < u i then ↑(⟨l, u, h⟩ : Box ι) else ⊥
