English
disjWithin(a,b) is the set of finite sequences of pairs (a_i,b_i) with a_i,b_i ∈ [a,b] and the corresponding uIoc(a_i,b_i) are pairwise disjoint.
Русский
disjWithin(a,b) — множество конечных последовательностей пар (a_i,b_i) с a_i,b_i ∈ [a,b] и интервалов uIoc(a_i,b_i) попарно непересекаются.
LaTeX
$$$ \text{disjWithin}(a,b) = \{ E : \mathbb{N} \times (\mathbb{N} \to \mathbb{R} \times \mathbb{R}) \mid (\forall i < E.1, (E.2 i).1, (E.2 i).2 ∈ uIcc a b) \wedge\ (\text{PairwiseDisjoint} (\mathrm{Finset.range}\, E.1) (\lambda i, uIoc ((E.2 i).1) ((E.2 i).2))) \}$$$
Lean4
/-- The subcollection of all the finite sequences of `uIoc` intervals consisting of
`uIoc (a i) (b i)`, `i < n` where `a i`, `b i` are all in `uIcc a b` for `i < n` and
`uIoc (a i) (b i)` are mutually disjoint for `i < n`. Technically the finite sequence
`uIoc (a i) (b i)`, `i < n` is represented by any `E : ℕ × (ℕ → ℝ × ℝ)` which satisfies
`E.1 = n` and `E.2 i = (a i, b i)` for `i < n`. -/
def disjWithin (a b : ℝ) :=
{E : ℕ × (ℕ → ℝ × ℝ) |
(∀ i ∈ Finset.range E.1, (E.2 i).1 ∈ uIcc a b ∧ (E.2 i).2 ∈ uIcc a b) ∧
Set.PairwiseDisjoint (Finset.range E.1) (fun i ↦ uIoc (E.2 i).1 (E.2 i).2)}
