IicProdIoc_le — Mathlib

English

If b ≤ a, then IicProdIoc(a,b) reduces to the left restriction: IicProdIoc(a,b) = frestrictLe₂ b≤a ∘ Prod.fst.

Русский

Если b ≤ a, то IicProdIoc(a,b) упрощается до левой ограниченной проекции: IicProdIoc(a,b) = frestrictLe₂ b≤a ∘ Prod.fst.

LaTeX

$$$\mathrm{IicProdIoc}(a,b) = \big( \mathrm{frestrictLe\_2}(b\le a) \big) \circ \mathrm{Prod.fst}$$$

Lean4

theorem IicProdIoc_le {a b : ι} (hba : b ≤ a) : IicProdIoc (X := X) a b = (frestrictLe₂ hba) ∘ Prod.fst :=
  by
  ext x i
  simp [IicProdIoc, (mem_Iic.1 i.2).trans hba]

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