sMk — Mathlib

English

The constructed sequence sMk associated with x : F (M F) yields, at every step, an AllAgree property: AllAgree (Approx.sMk x).

Русский

Пусть x : F (M F). Тогда последовательность sMk образующаяся обеспечивает на каждом шаге свойство AllAgree: AllAgree(Approx.sMk x).

LaTeX

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

Lean4

/-- generates the approximations needed for `M.mk` -/
protected def sMk (x : F (M F)) : ∀ n, CofixA F n
  | 0 => CofixA.continue
  | succ n => CofixA.intro x.1 fun i => (x.2 i).approx n

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