IicProdIoc_comp_restrict₂ — Mathlib

English

The composition with the restriction map to the right equals the right projection: IicProdIoc_comp_restrict₂ states that (restrict₂ Ioc_subset_Iic_self) ∘ (IicProdIoc a b) = Prod.snd.

Русский

Композиция с ограничением справа даёт правую проекцию: restrict₂ ∘ IicProdIoc = Prod.snd.

LaTeX

$$$\mathrm{restrict\_2} \; Ioc\_subset\_Iic\_self \circ \mathrm{IicProdIoc}(a,b) = \mathrm{Prod.snd}$$$

Lean4

theorem IicProdIoc_comp_restrict₂ {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]

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