English
Gluing Ioc a b and Ioc b c into Ioc a c defines a family IocProdIoc with coherent restrictions.
Русский
Склейка множеств Ioc(a,b) и Ioc(b,c) в Ioc(a,c) образует семейство IocProdIoc с согласованными ограничениями.
LaTeX
$$$\\mathrm{IocProdIoc}(a,b,c) : \\text{definition such that for } i\\in \\mathrm{Ioc}(a,c), \\mathrm{IocProdIoc}(a,b,c)(i) = \\begin{cases} x(i) \\, & i \\le b \\\\ y(i) \\, & \\text{otherwise} \\end{cases}$$$
Lean4
/-- Gluing `Ioc a b` and `Ioc b c` into `Ioc a c`. -/
def IocProdIoc (a b c : ι) (x : (Π i : Ioc a b, X i) × (Π i : Ioc b c, X i)) (i : Ioc a c) : X i :=
if h : i ≤ b then x.1 ⟨i, mem_Ioc.2 ⟨(mem_Ioc.1 i.2).1, h⟩⟩ else x.2 ⟨i, mem_Ioc.2 ⟨not_le.1 h, (mem_Ioc.1 i.2).2⟩⟩
