English
The gluing map IicProdIoc is the unique function described by the piecewise rule above; more precisely, for all x and i, IicProdIoc(a,b)(x,i) = x.1( i, mem_Iic.2 h ) if h: i ≤ a, and x.2( i, mem_Ioc.2 ⟨¬h, mem_Iic.1 i.2⟩ ) otherwise.
Русский
Формула клея IicProdIoc задаётся по правилу: для x и индекса i выполняется IicProdIoc(a,b)(x,i) = x.1( i, mem_Iic.2 h ) если h: i ≤ a, иначе x.2( i, mem_Ioc.2 ⟨¬h, mem_Iic.1 i.2⟩ ).
LaTeX
$$$(IicProdIoc(a,b)) = (x,i) \mapsto \begin{cases} x_1(i,\, \text{mem}_\text{Iic}(i)) & i \le a \\$ x_2(i,\, \text{mem}_\text{Ioc}(i)) & \text{otherwise} \end{cases}$$$
Lean4
/-- When `IicProdIoc` is only partially applied (i.e. `IicProdIoc a b x` but not
`IicProdIoc a b x i`) `simp [IicProdIoc]` won't unfold the definition.
This lemma allows to unfold it by writing `simp [IicProdIoc_def]`. -/
theorem IicProdIoc_def (a b : ι) :
IicProdIoc (X := X) a b = fun x i ↦
if h : i.1 ≤ 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⟩⟩ :=
rfl
