English
ext_aux gives an explicit extension principle: under assumptions on Agree' n z x and Agree' n z y and a compatibility condition hrec for all paths, the nth+1 approximations of x and y coincide.
Русский
ext_aux задаёт явный принцип расширения: при предположениях о Agree' n z x и Agree' n z y и совместимости hrec для всех путей, аппроксимации x и y на уровне n+1 совпадают.
LaTeX
$$$\\operatorname{ext\\_aux} [Inhabited (M F)] [DecidableEq F.A] \\{n : \\mathbb{N}\\} (x y z : M F) (hx : Agree' n z x) (hy : Agree' n z y) (hrec : \\forall ps : Path F, n = ps.length → iselect ps x = iselect ps y) : x.approx (n + 1) = y.approx (n + 1)$$$
Lean4
@[simp]
theorem ichildren_mk [DecidableEq F.A] [Inhabited (M F)] (x : F (M F)) (i : F.Idx) : ichildren i (M.mk x) = x.iget i :=
by
dsimp only [ichildren, PFunctor.Obj.iget]
congr with h
