toSubtype_of_subtype_assoc — Mathlib

English

ToSubtype(p) after OfSubtype(p) acts as the identity on f.

Русский

ToSubtype(p) после OfSubtype(p) действует как тождество на f.

LaTeX

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

Lean4

@[simp]
theorem toSubtype_of_subtype_assoc {α β : TypeVec n} (p : α ⟹ «repeat» n Prop) (f : β ⟹ Subtype_ p) :
    @toSubtype n _ p ⊚ ofSubtype _ ⊚ f = f := by rw [← comp_assoc, toSubtype_of_subtype]; simp

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