restrict₂_comp_IicProdIoc — Mathlib

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]

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