subtypeVal_toSubtype' — Mathlib

English

SubtypeVal applied to r composed with toSubtype' r equals a canonical prod constructor.

Русский

SubtypeVal от r после toSubtype' r даёт конструктор prod.mk с fst, snd.

LaTeX

$$\operatorname{subtypeVal}(r) \circ \operatorname{toSubtype'}(r) = \lambda i x . \operatorname{prod.mk} i x.1.fst x.1.snd$$

Lean4

theorem subtypeVal_toSubtype' {α : TypeVec n} (r : α ⊗ α ⟹ «repeat» n Prop) :
    subtypeVal r ⊚ toSubtype' r = fun i x => prod.mk i x.1.fst x.1.snd :=
  by
  ext i x
  induction i <;> simp only [toSubtype', comp, subtypeVal, prod.mk] at *
  simp [*]

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