English
For any a, f, i, depth (f(i)) < depth ⟨a,f⟩; i.e., children have smaller depth than their parent.
Русский
Для любого a, f, i глубина f(i) меньше глубины узла ⟨a,f⟩.
LaTeX
$$$\forall a:\alpha, \forall f:a\to WType(\beta), \forall i:\beta(a),\text{depth}(f(i)) < \text{depth}(\langle a,f\rangle).$$$
Lean4
theorem depth_lt_depth_mk (a : α) (f : β a → WType β) (i : β a) : depth (f i) < depth ⟨a, f⟩ :=
Nat.lt_succ_of_le
(Finset.le_sup (f := (depth <| f ·)) (Finset.mem_univ i))
/-
Show that W types are encodable when `α` is an encodable fintype and for every `a : α`, `β a` is
encodable.
We define an auxiliary type `WType' β n` of trees of depth at most `n`, and then we show by
induction on `n` that these are all encodable. These auxiliary constructions are not interesting in
and of themselves, so we mark them as `private`.
-/
