The inductive construction theorem

structure ICT.IndHyp {I : Type u} {r : I → I → Prop} [IsTrans I r] {α : I → Type v} {p : (i : I) → α i → ((j : I) → r j i → α j) → Prop} (i : I) (t : (j : I) → r j i → Part (α j)) : Prop

• dom : ∀ (j : I) (h : r j i), (t j h).Dom
• prop : ∀ (j : I) (h : r j i), p j ((t j h).get ⋯) fun (k : I) (h' : r k j) => (t k ⋯).get ⋯

def ICT.core {I : Type u} {r : I → I → Prop} [IsTrans I r] [inst : IsWellFounded I r] {α : I → Type v} {p : (i : I) → α i → ((j : I) → r j i → α j) → Prop} (f : (i : I) → (d : (j : I) → r j i → α j) → (∀ (j : I) (h : r j i), p j (d j h) fun (k : I) (h' : r k j) => d k ⋯) → α i) (i : I) : Part (α i)

Equations

• One or more equations did not get rendered due to their size.

theorem ICT.core_eq {I : Type u} {r : I → I → Prop} [IsTrans I r] [inst : IsWellFounded I r] {α : I → Type v} {p : (i : I) → α i → ((j : I) → r j i → α j) → Prop} (f : (i : I) → (d : (j : I) → r j i → α j) → (∀ (j : I) (h : r j i), p j (d j h) fun (k : I) (h' : r k j) => d k ⋯) → α i) (i : I) : ICT.core f i = { Dom := ICT.IndHyp i fun (j : I) (x : r j i) => ICT.core f j, get := fun (h : ICT.IndHyp i fun (j : I) (x : r j i) => ICT.core f j) => f i (fun (j : I) (h' : r j i) => (ICT.core f j).get ⋯) ⋯ }

theorem ICT.core_get_eq {I : Type u} {r : I → I → Prop} [IsTrans I r] [inst : IsWellFounded I r] {α : I → Type v} {p : (i : I) → α i → ((j : I) → r j i → α j) → Prop} (f : (i : I) → (d : (j : I) → r j i → α j) → (∀ (j : I) (h : r j i), p j (d j h) fun (k : I) (h' : r k j) => d k ⋯) → α i) (i : I) (h : (ICT.core f i).Dom) : (ICT.core f i).get h = f i (fun (j : I) (h' : r j i) => (ICT.core f j).get ⋯) ⋯

theorem ICT.core_dom {I : Type u} {r : I → I → Prop} [IsTrans I r] [inst : IsWellFounded I r] {α : I → Type v} {p : (i : I) → α i → ((j : I) → r j i → α j) → Prop} (f : (i : I) → (d : (j : I) → r j i → α j) → (∀ (j : I) (h : r j i), p j (d j h) fun (k : I) (h' : r k j) => d k ⋯) → α i) (hp : ∀ (i : I) (d : (j : I) → r j i → α j) (h : ∀ (j : I) (h : r j i), p j (d j h) fun (k : I) (h' : r k j) => d k ⋯), p i (f i d h) d) (i : I) : (ICT.core f i).Dom

def ICT.fix' {I : Type u} {r : I → I → Prop} [IsTrans I r] [inst : IsWellFounded I r] {α : I → Type v} {p : (i : I) → α i → ((j : I) → r j i → α j) → Prop} (f : (i : I) → (d : (j : I) → r j i → α j) → (∀ (j : I) (h : r j i), p j (d j h) fun (k : I) (h' : r k j) => d k ⋯) → α i) (hp : ∀ (i : I) (d : (j : I) → r j i → α j) (h : ∀ (j : I) (h : r j i), p j (d j h) fun (k : I) (h' : r k j) => d k ⋯), p i (f i d h) d) (i : I) : α i

Equations

• ICT.fix' f hp i = (ICT.core f i).get ⋯

theorem ICT.fix'_prop {I : Type u} {r : I → I → Prop} [IsTrans I r] [inst : IsWellFounded I r] {α : I → Type v} {p : (i : I) → α i → ((j : I) → r j i → α j) → Prop} (f : (i : I) → (d : (j : I) → r j i → α j) → (∀ (j : I) (h : r j i), p j (d j h) fun (k : I) (h' : r k j) => d k ⋯) → α i) (hp : ∀ (i : I) (d : (j : I) → r j i → α j) (h : ∀ (j : I) (h : r j i), p j (d j h) fun (k : I) (h' : r k j) => d k ⋯), p i (f i d h) d) (i : I) : p i (ICT.fix' f hp i) fun (j : I) (x : r j i) => ICT.fix' f hp j

theorem ICT.fix'_eq {I : Type u} {r : I → I → Prop} [IsTrans I r] [inst : IsWellFounded I r] {α : I → Type v} {p : (i : I) → α i → ((j : I) → r j i → α j) → Prop} (f : (i : I) → (d : (j : I) → r j i → α j) → (∀ (j : I) (h : r j i), p j (d j h) fun (k : I) (h' : r k j) => d k ⋯) → α i) (hp : ∀ (i : I) (d : (j : I) → r j i → α j) (h : ∀ (j : I) (h : r j i), p j (d j h) fun (k : I) (h' : r k j) => d k ⋯), p i (f i d h) d) (i : I) : ICT.fix' f hp i = f i (fun (j : I) (x : r j i) => ICT.fix' f hp j) ⋯

noncomputable def ICT.fix {I : Type u} {r : I → I → Prop} [IsTrans I r] [inst : IsWellFounded I r] {α : I → Type v} {p : (i : I) → α i → ((j : I) → r j i → α j) → Sort w} (f : (i : I) → (d : (j : I) → r j i → α j) → ((j : I) → (h : r j i) → p j (d j h) fun (k : I) (h' : r k j) => d k ⋯) → α i) (hp : (i : I) → (d : (j : I) → r j i → α j) → (h : (j : I) → (h : r j i) → p j (d j h) fun (k : I) (h' : r k j) => d k ⋯) → p i (f i d h) d) (i : I) : α i

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ICT.fix_prop {I : Type u} {r : I → I → Prop} [IsTrans I r] [inst : IsWellFounded I r] {α : I → Type v} {p : (i : I) → α i → ((j : I) → r j i → α j) → Sort w} (f : (i : I) → (d : (j : I) → r j i → α j) → ((j : I) → (h : r j i) → p j (d j h) fun (k : I) (h' : r k j) => d k ⋯) → α i) (hp : (i : I) → (d : (j : I) → r j i → α j) → (h : (j : I) → (h : r j i) → p j (d j h) fun (k : I) (h' : r k j) => d k ⋯) → p i (f i d h) d) (i : I) : p i (ICT.fix f hp i) fun (j : I) (x : r j i) => ICT.fix f hp j

Equations

• ICT.fix_prop f hp i = ⋯.some

theorem ICT.fix_eq {I : Type u} {r : I → I → Prop} [IsTrans I r] [inst : IsWellFounded I r] {α : I → Type v} {p : (i : I) → α i → ((j : I) → r j i → α j) → Sort w} (f : (i : I) → (d : (j : I) → r j i → α j) → ((j : I) → (h : r j i) → p j (d j h) fun (k : I) (h' : r k j) => d k ⋯) → α i) (hp : (i : I) → (d : (j : I) → r j i → α j) → (h : (j : I) → (h : r j i) → p j (d j h) fun (k : I) (h' : r k j) => d k ⋯) → p i (f i d h) d) (i : I) : ICT.fix f hp i = f i (fun (j : I) (x : r j i) => ICT.fix f hp j) fun (j : I) (x : r j i) => ICT.fix_prop f hp j