approx_mk — Mathlib

English

If a ∈ F.A and f : F.B a → M F, then the (succ i)-th approximation of M.mk ⟨a,f⟩ is the CofixA.intro a (fun j => (f j).approx i).

Русский

Пусть a ∈ F.A и f : F.B a → M F. Тогда приближение (succ i) для M.mk ⟨a,f⟩ равно CofixA.intro a (fun j => (f j).approx i).

LaTeX

$$$\\bigl(M.mk \\langle a, f \\rangle\\bigr).approx(\\operatorname{succ} i) = \\operatorname{CofixA.intro} a\\; (\\lambda j. (f j).approx i) $$$

Lean4

theorem approx_mk (a : F.A) (f : F.B a → M F) (i : ℕ) :
    (M.mk ⟨a, f⟩).approx (succ i) = CofixA.intro a fun j => (f j).approx i :=
  rfl

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