English
Let a ≤ b be elements of a linear order. There is a canonical way to glue the data given on the lower closed interval Iic(a) and the half-open interval Ioc(a, b) to obtain a data on the closed interval Iic(b). Concretely, given a pair of dependent families x1 on Iic(a) and x2 on Ioc(a, b), we obtain a dependent family on Iic(b) by taking the left piece on all indices i ≤ a and the right piece on indices a < i ≤ b, identifying i with the corresponding index in Iic(a) or Ioc(a, b) as appropriate. This construction is the gluing map IicProdIoc(a, b).
Русский
Пусть a ≤ b в линейном порядке. существует канонический способ «склеить» данные, заданные на замкнутом подотрезке Iic(a) и на полупрерывном отрезке Ioc(a, b), чтобы получить данные на Iic(b). Грубо: пары семей x1 на Iic(a) и x2 на Ioc(a, b) приводят к семейству на Iic(b) так, что на i ≤ a берём x1(i), а на a < i ≤ b — x2(i), с соответствующими вложениями индексов.
LaTeX
$$$\mathrm{IicProdIoc}(a,b) : (\prod_{i\in \mathrm{Iic}(a)} X_i) \times (\prod_{i\in \mathrm{Ioc}(a,b)} X_i) \to \prod_{i\in \mathrm{Iic}(b)} X_i \\ (x)(i) = \begin{cases} x_1(i) & \text{if } i \le a \\ x_2(i) & \text{if } i > a \end{cases} \,,$$$
Lean4
/-- Gluing `Iic a` and `Ioc a b` into `Iic b`. If `b < a`, this is just a projection on the first
coordinate followed by a restriction, see `IicProdIoc_le`. -/
def IicProdIoc (a b : ι) (x : (Π i : Iic a, X i) × (Π i : Ioc a b, X i)) (i : Iic b) : X i :=
if h : i ≤ a then x.1 ⟨i, mem_Iic.2 h⟩ else x.2 ⟨i, mem_Ioc.2 ⟨not_le.1 h, mem_Iic.1 i.2⟩⟩
