frestrictLe₂_comp_IicProdIoc — Mathlib

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]

Похожие утверждения