ofArrows_pUnit — Mathlib

English

The ofArrows construction over a unit index set reduces to the singleton presieve.

Русский

Конструкция ofArrows над единичной декомпозицией индексов эквивалентна одинарной предсистеме.

LaTeX

$$$\\mathrm{ofArrows}\\; (\\lambda _ => Y)\\; (\\lambda _ => f) = \\mathrm{singleton}\\; f$$$

Lean4

theorem ofArrows_pUnit : (ofArrows _ fun _ : PUnit => f) = singleton f :=
  by
  funext Y
  ext g
  constructor
  · rintro ⟨_⟩
    apply singleton.mk
  · rintro ⟨_⟩
    exact ofArrows.mk PUnit.unit

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