P_mk — Mathlib

English

The same AllAgree property holds for the Mk-construction associated with x : F (M F): AllAgree (PFunctor.M.Approx.sMk x).

Русский

Аналогично, свойство AllAgree справедливо для Mk-конструкции: AllAgree (PFunctor.M.Approx.sMk x).

LaTeX

$$$\\operatorname{PFunctor.M.Approx.P_mk} (x:\\, F.(M F)) : \\operatorname{AllAgree}(\\operatorname{PFunctor.M.Approx.sMk} x)$$$

Lean4

protected theorem P_mk (x : F (M F)) : AllAgree (Approx.sMk x)
  | 0 => by constructor
  | succ n => by
    constructor
    introv
    apply (x.2 i).consistent

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