halfOpenBoxes

Stream: new members

[Iocta]

How to say "the half open boxes in n dimensions"?

import Mathlib

open Set

def halfOpenBoxes1 : Set (Set ℝ) :=
  ⋃ (a : ℝ) (b : ℝ), {(Ioc a b)}

def halfOpenBoxes2 : Set ((Set ℝ) × (Set ℝ)) :=
  {⟨x,y⟩ | (x ∈ halfOpenBoxes1) ∧ (y ∈ halfOpenBoxes1)}

def halfOpenBoxesN (n : ℕ) : Set (Π i ∈ Finset.range n, Set ℝ) :=
  {b : (Π i, Set ℝ) | ∀i ∈ Finset.range n, b i ∈ halfOpenBoxes1}

[Yaël Dillies]

@Yury G. Kudryashov's work on the box integrals might give you ideas (grep for "box integral" in mathlib)

[Iocta]

BoxIntegral is interesting, thanks. I'd still like to know how to write my third def properly. (My halfOpenBoxesN doesn't compile.) Is there a way to generalize halfOpenBoxes2 to n using the same basic idea?

[Andrew Yang]

You would have to write it as

def halfOpenBoxesN (n : ℕ) : Set (Π i ∈ Finset.range n, Set ℝ) :=
  {b : (Π i ∈ Finset.range n, Set ℝ) | ∀ i (hi : i ∈ Finset.range n), b i hi ∈ halfOpenBoxes1}

But a better option is to use Fin n instead of Finset.range, as in

def halfOpenBoxesN (n : ℕ) : Set (Fin n → Set ℝ) :=
  {b : Fin n → Set ℝ | ∀ i, b i ∈ halfOpenBoxes1}

Or a slicker way (but gives the same definition as the one above) is

def halfOpenBoxesN (n : ℕ) : Set (Fin n → Set ℝ) :=
  Set.univ.pi fun _ ↦ halfOpenBoxes1

[Edward van de Meent]

Aren't the relevant sets of type Set (Fin n -> Real) instead of Fin n -> Set Real?