toSubtype_of_subtype

Mathlib.Data.TypeVec

URI: https://scilib.ai/kg/mathlib#TypeVec.toSubtype_of_subtype

← MathLib Explorer

English

Composition of toSubtype with ofSubtype is the identity.

Русский

Составление toSubtype с ofSubtype даёт тождество.

LaTeX

$$\operatorname{toSubtype}(p) \circ \operatorname{ofSubtype}(p) = \operatorname{id}$$

Lean4

@[simp]
theorem toSubtype_of_subtype {α : TypeVec n} (p : α ⟹ «repeat» n Prop) : toSubtype p ⊚ ofSubtype p = id :=
  by
  ext i x
  induction i <;> simp only [id, toSubtype, comp, ofSubtype] at *
  simp [*]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru