English
If a ≤ b, then composing the right-projection-restricted map restrict₂ with IicProdIoc gives Prod.snd; i.e., (restrict₂ Ioc_subset_Iic_self) ∘ (IicProdIoc a b) = Prod.snd.
Русский
При a ≤ b композиция ограниченной проекции справа и IicProdIoc даёт правую проекцию: (restrict₂ Ioc_subset_Iic_self) ∘ IicProdIoc = Prod.snd.
LaTeX
$$$ (\text{restrict}_2 \; Ioc\_subset\_Iic\_self) \circ \mathrm{IicProdIoc}(a,b) = \mathrm{Prod.snd}$$$
Lean4
theorem restrict₂_comp_IicProdIoc (a b : ι) : (restrict₂ Ioc_subset_Iic_self) ∘ (IicProdIoc (X := X) a b) = Prod.snd :=
by
ext x i
simp [IicProdIoc, not_le.2 (mem_Ioc.1 i.2).1]