casesOn_mk — Mathlib

English

For any r and x ∈ F(M F), PFunctor.M.casesOn (M.mk x) f = f x; i.e., casesOn respects the M.mk construction.

Русский

Для любых r и x ∈ F(M F) справедливо PFunctor.M.casesOn (M.mk x) f = f x; то есть casesOn сохраняет M.mk.

LaTeX

$$$\\forall {r : M F \\to \\mathrm{Sort}*}\\; (x : F (M F))\\; (f : \\forall x : F (M F), r (M.mk x)),\\; \\mathrm{PFunctor.M.casesOn} (M.mk x) f = f x$$$

Lean4

@[simp]
theorem casesOn_mk {r : M F → Sort*} (x : F (M F)) (f : ∀ x : F (M F), r (M.mk x)) :
    PFunctor.M.casesOn (M.mk x) f = f x :=
  cases_mk x f

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