English
If a ≤ b, then composing the gluing map IicProdIoc with the projection to the left component equals taking the left component alone; equivalently, frestrictLe₂ composed with IicProdIoc equals Prod.fst.
Русский
При a ≤ b композиция IicProdIoc с проекцией на левую часть совпадает с простой проекцией на левую часть; то есть frestrictLe₂ ∘ IicProdIoc = Prod.fst.
LaTeX
$$$\mathrm{frestrictLe\_2}(a \le b) \circ \mathrm{IicProdIoc}(a,b) = \mathrm{Prod.fst}$$$
Lean4
theorem frestrictLe₂_comp_IicProdIoc {a b : ι} (hab : a ≤ b) :
(frestrictLe₂ hab) ∘ (IicProdIoc (X := X) a b) = Prod.fst :=
by
ext x i
simp [IicProdIoc, mem_Iic.1 i.2]