toSubtype' — Mathlib

English

A refinement of toSubtype' that preserves equality under projection to the last coordinate.

Русский

Уточнение toSubtype', сохраняющее равенство под проекцией на последнюю координату.

LaTeX

$$$\\text{toSubtype}'\n\\mathrm{eq\_2}$$$

Lean4

/-- similar to `toSubtype` adapted to relations (i.e. predicate on product) -/
def toSubtype' {n} {α : TypeVec.{u} n} (p : α ⊗ α ⟹ «repeat» n Prop) :
    (fun i : Fin2 n => { x : α i × α i // ofRepeat <| p i (prod.mk _ x.1 x.2) }) ⟹ Subtype_ p
  | Fin2.fs i, x => toSubtype' (dropFun p) i x
  | Fin2.fz, x => ⟨x.val, cast (by congr) x.property⟩

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