uncurry_singleton — Mathlib

English

If s is a singleton presieve generated by a single arrow u: Y → X, then its uncurry is the singleton consisting of the pair ⟨Y, u⟩.

Русский

Если пресейв единичного типа устроен одним стрелом u: Y → X, то распакованный пресейв содержит единственную пару ⟨Y, u⟩.

LaTeX

$$$(\\mathrm{singleton}\,u).\\mathrm{uncurry} = \\{\\langle Y, u\\rangle\\}$$$

Lean4

@[simp]
theorem uncurry_singleton {Y : C} (u : Y ⟶ X) : (singleton u).uncurry = {⟨Y, u⟩} :=
  by
  ext ⟨Z, v⟩; constructor
  · rintro ⟨⟩; rfl
  · intro h
    rw [Set.mem_singleton_iff, Sigma.ext_iff] at h
    obtain ⟨rfl, h⟩ := h; subst h; constructor

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