subtypeVal_toSubtype — Mathlib

English

SubtypeVal composed with toSubtype equals the constant val function.

Русский

SubtypeVal, сопоставляемое toSubtype, даёт константу Subtype.val.

LaTeX

$$\operatorname{subtypeVal}(p) \circ \operatorname{toSubtype}(p) = \lambda _ . \operatorname{Subtype.val}$$

Lean4

@[simp]
theorem subtypeVal_toSubtype {α : TypeVec n} (p : α ⟹ «repeat» n Prop) :
    subtypeVal p ⊚ toSubtype p = fun _ => Subtype.val :=
  by
  ext i x
  induction i <;> simp only [toSubtype, comp, subtypeVal] at *
  simp [*]

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