toSubtype'_of_subtype' — Mathlib

English

The composition of toSubtype' r with ofSubtype' r is the identity.

Русский

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

LaTeX

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

Lean4

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

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