noncomputable def ConNF.MainInduction.litterEquiv [ConNF.Params] : ConNF.Litter ≃ ConNF.μ

Equations

• ConNF.MainInduction.litterEquiv = ⋯.some

noncomputable def ConNF.MainInduction.nearLitterEquiv [ConNF.Params] : ConNF.NearLitter ≃ ConNF.μ

Equations

• ConNF.MainInduction.nearLitterEquiv = ⋯.some

noncomputable def ConNF.MainInduction.alMap [ConNF.Params] : ConNF.Atom ⊕ ConNF.Litter → Lex (ConNF.μ × Lex (Unit ⊕ ConNF.κ))

Equations

• ConNF.MainInduction.alMap x = match x with | Sum.inl a => (ConNF.MainInduction.litterEquiv a.1, Sum.inr a.2) | Sum.inr L => (ConNF.MainInduction.litterEquiv L, Sum.inl ())

def ConNF.MainInduction.posBound [ConNF.Params] (N : ConNF.NearLitter) : Set (Lex (ConNF.μ × Lex (Unit ⊕ ConNF.κ)))

Equations

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

def ConNF.MainInduction.posBound' [ConNF.Params] (N : ConNF.NearLitter) : Set (Lex (ConNF.μ × Lex (Unit ⊕ ConNF.κ)))

Equations

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

theorem ConNF.MainInduction.posBound_eq_posBound' [ConNF.Params] (N : ConNF.NearLitter) : ConNF.MainInduction.posBound N = ConNF.MainInduction.posBound' N

def ConNF.MainInduction.posDeny [ConNF.Params] (N : ConNF.NearLitter) : Set (Lex (ConNF.μ × Lex (Unit ⊕ ConNF.κ)))

Equations

• ConNF.MainInduction.posDeny N = {ν : Lex (ConNF.μ × Lex (Unit ⊕ ConNF.κ)) | ∃ ν' ∈ ConNF.MainInduction.posBound N, ν ≤ ν'}

theorem ConNF.MainInduction.small_posBound [ConNF.Params] (N : ConNF.NearLitter) : ConNF.Small (ConNF.MainInduction.posBound N)

instance ConNF.MainInduction.instIsWellFoundedLexSumLt_conNF {α : Type u_2} {β : Type u_1} [LinearOrder α] [LinearOrder β] [IsWellOrder α fun (x x_1 : α) => x < x_1] [IsWellOrder β fun (x x_1 : β) => x < x_1] : IsWellFounded (Lex (α ⊕ β)) fun (x x_1 : Lex (α ⊕ β)) => x < x_1

Equations

• ⋯ = ⋯

instance ConNF.MainInduction.instIsWellOrderLexProdLt_conNF {α : Type u_2} {β : Type u_1} [LinearOrder α] [LinearOrder β] [IsWellOrder α fun (x x_1 : α) => x < x_1] [IsWellOrder β fun (x x_1 : β) => x < x_1] : IsWellOrder (Lex (α × β)) fun (x x_1 : Lex (α × β)) => x < x_1

Equations

• ⋯ = ⋯

instance ConNF.MainInduction.instIsWellOrderLexSumLt_conNF {α : Type u_2} {β : Type u_1} [LinearOrder α] [LinearOrder β] [IsWellOrder α fun (x x_1 : α) => x < x_1] [IsWellOrder β fun (x x_1 : β) => x < x_1] : IsWellOrder (Lex (α ⊕ β)) fun (x x_1 : Lex (α ⊕ β)) => x < x_1

Equations

• ⋯ = ⋯

instance ConNF.MainInduction.μProdWO [ConNF.Params] {α : Type u} [LinearOrder α] [IsWellOrder α fun (x x_1 : α) => x < x_1] : IsWellOrder (Lex (ConNF.μ × α)) fun (x x_1 : Lex (ConNF.μ × α)) => x < x_1

Equations

• ⋯ = ⋯

@[simp]

theorem ConNF.MainInduction.mk_μProd [ConNF.Params] {α : Type u} (hα : Cardinal.mk α < Cardinal.mk ConNF.μ) (hα' : Cardinal.mk α ≠ 0) : Cardinal.mk (Lex (ConNF.μ × α)) = Cardinal.mk ConNF.μ

theorem ConNF.MainInduction.μProd_fst_le [ConNF.Params] {α : Type u} [LinearOrder α] {y : Lex (ConNF.μ × α)} {x : Lex (ConNF.μ × α)} (h : y < x) : y.1 ≤ x.1

theorem ConNF.MainInduction.μProd_card_iio [ConNF.Params] {α : Type u} [LinearOrder α] (hα : Cardinal.mk α < Cardinal.mk ConNF.μ) (x : Lex (ConNF.μ × α)) : Cardinal.mk ↑{y : Lex (ConNF.μ × α) | y < x} < Cardinal.mk ConNF.μ

theorem ConNF.MainInduction.μProd_typein_lt [ConNF.Params] {α : Type u} [LinearOrder α] [IsWellOrder α fun (x x_1 : α) => x < x_1] (hα : Cardinal.mk α < Cardinal.mk ConNF.μ) (x : Lex (ConNF.μ × α)) : Ordinal.typein (fun (x x_1 : Lex (ConNF.μ × α)) => x < x_1) x < Ordinal.type fun (x x_1 : ConNF.μ) => x < x_1

theorem ConNF.MainInduction.μProd_typein_lt' [ConNF.Params] {α : Type u} [LinearOrder α] [IsWellOrder α fun (x x_1 : α) => x < x_1] (hα : Cardinal.mk α < Cardinal.mk ConNF.μ) (hα' : Cardinal.mk α ≠ 0) (x : ConNF.μ) : Ordinal.typein (fun (x x_1 : ConNF.μ) => x < x_1) x < Ordinal.type fun (x x_1 : Lex (ConNF.μ × α)) => x < x_1

noncomputable def ConNF.MainInduction.μProd_toFun [ConNF.Params] {α : Type u} [LinearOrder α] [IsWellOrder α fun (x x_1 : α) => x < x_1] (hα : Cardinal.mk α < Cardinal.mk ConNF.μ) (x : Lex (ConNF.μ × α)) : ConNF.μ

Equations

• ConNF.MainInduction.μProd_toFun hα x = Ordinal.enum (fun (x x_1 : ConNF.μ) => x < x_1) (Ordinal.typein (fun (x x_1 : Lex (ConNF.μ × α)) => x < x_1) x) ⋯

noncomputable def ConNF.MainInduction.μProd_invFun [ConNF.Params] {α : Type u} [LinearOrder α] [IsWellOrder α fun (x x_1 : α) => x < x_1] (hα : Cardinal.mk α < Cardinal.mk ConNF.μ) (hα' : Cardinal.mk α ≠ 0) (x : ConNF.μ) : Lex (ConNF.μ × α)

Equations

• ConNF.MainInduction.μProd_invFun hα hα' x = Ordinal.enum (fun (x x_1 : Lex (ConNF.μ × α)) => x < x_1) (Ordinal.typein (fun (x x_1 : ConNF.μ) => x < x_1) x) ⋯

noncomputable def ConNF.MainInduction.μProd_equiv [ConNF.Params] {α : Type u} [LinearOrder α] [IsWellOrder α fun (x x_1 : α) => x < x_1] (hα : Cardinal.mk α < Cardinal.mk ConNF.μ) (hα' : Cardinal.mk α ≠ 0) : Lex (ConNF.μ × α) ≃o ConNF.μ

Equations

• ConNF.MainInduction.μProd_equiv hα hα' = { toFun := ConNF.MainInduction.μProd_toFun hα, invFun := ConNF.MainInduction.μProd_invFun hα hα', left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

theorem ConNF.MainInduction.μProd_type [ConNF.Params] {α : Type u} [LinearOrder α] [IsWellOrder α fun (x x_1 : α) => x < x_1] (hα : Cardinal.mk α < Cardinal.mk ConNF.μ) (hα' : Cardinal.mk α ≠ 0) : (Ordinal.type fun (x x_1 : Lex (ConNF.μ × α)) => x < x_1) = (Cardinal.mk ConNF.μ).ord

theorem ConNF.MainInduction.card_Iio_lt' [ConNF.Params] {α : Type u} [LinearOrder α] [IsWellOrder α fun (x x_1 : α) => x < x_1] (hα : Cardinal.mk α < Cardinal.mk ConNF.μ) (hα' : Cardinal.mk α ≠ 0) (x : Lex (ConNF.μ × α)) : Cardinal.mk ↑(Set.Iio x) < Cardinal.mk ConNF.μ

theorem ConNF.MainInduction.card_Iic_lt' [ConNF.Params] {α : Type u} [LinearOrder α] [IsWellOrder α fun (x x_1 : α) => x < x_1] (hα : Cardinal.mk α < Cardinal.mk ConNF.μ) (hα' : Cardinal.mk α ≠ 0) (x : Lex (ConNF.μ × α)) : Cardinal.mk ↑(Set.Iic x) < Cardinal.mk ConNF.μ

theorem ConNF.MainInduction.unitSum_lt [ConNF.Params] : Cardinal.mk (Lex (Unit ⊕ ConNF.κ)) < Cardinal.mk ConNF.μ

theorem ConNF.MainInduction.unitSum_ne_zero [ConNF.Params] : Cardinal.mk (Lex (Unit ⊕ ConNF.κ)) ≠ 0

theorem ConNF.MainInduction.mk_posDeny [ConNF.Params] (N : ConNF.NearLitter) : Cardinal.mk ↑(ConNF.MainInduction.posDeny N) < Cardinal.mk ConNF.μ

instance ConNF.MainInduction.isWellOrder [ConNF.Params] : IsWellOrder ConNF.NearLitter (InvImage (fun (x x_1 : ConNF.μ) => x < x_1) ⇑ConNF.MainInduction.nearLitterEquiv)

Equations

• ⋯ = ⋯

theorem ConNF.MainInduction.isWellOrder_type_eq [ConNF.Params] : Ordinal.type (InvImage (fun (x x_1 : ConNF.μ) => x < x_1) ⇑ConNF.MainInduction.nearLitterEquiv) = (Cardinal.mk ConNF.μ).ord

theorem ConNF.MainInduction.mk_posDeny' [ConNF.Params] (N : ConNF.NearLitter) : Cardinal.mk { N' : ConNF.NearLitter // ConNF.MainInduction.nearLitterEquiv N' < ConNF.MainInduction.nearLitterEquiv N } + Cardinal.mk ↑(ConNF.MainInduction.posDeny N) < Cardinal.mk (Lex (ConNF.μ × Lex (Unit ⊕ ConNF.κ)))

noncomputable def ConNF.MainInduction.nlMap [ConNF.Params] : ConNF.NearLitter → Lex (ConNF.μ × Lex (Unit ⊕ ConNF.κ))

Equations

• ConNF.MainInduction.nlMap = ConNF.chooseWf ConNF.MainInduction.posDeny ⋯

theorem ConNF.MainInduction.nlMap_injective [ConNF.Params] : Function.Injective ConNF.MainInduction.nlMap

theorem ConNF.MainInduction.nlMap_not_mem_posDeny [ConNF.Params] (N : ConNF.NearLitter) : ConNF.MainInduction.nlMap N ∉ ConNF.MainInduction.posDeny N

noncomputable def ConNF.MainInduction.pos [ConNF.Params] : ConNF.Atom ⊕ ConNF.NearLitter → Lex (Lex (ConNF.μ × Lex (Unit ⊕ ConNF.κ)) × ULift.{u, 0} Bool)

Equations

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

theorem ConNF.MainInduction.pos_injective [ConNF.Params] : Function.Injective ConNF.MainInduction.pos

theorem ConNF.MainInduction.lt_pos_atom' [ConNF.Params] (a : ConNF.Atom) : ConNF.MainInduction.pos (Sum.inr a.1.toNearLitter) < ConNF.MainInduction.pos (Sum.inl a)

theorem ConNF.MainInduction.lt_pos_litter' [ConNF.Params] (N : ConNF.NearLitter) (hN : ¬N.IsLitter) : ConNF.MainInduction.pos (Sum.inr N.fst.toNearLitter) < ConNF.MainInduction.pos (Sum.inr N)

theorem ConNF.MainInduction.lt_pos_symmDiff' [ConNF.Params] (a : ConNF.Atom) (N : ConNF.NearLitter) (h : a ∈ symmDiff (ConNF.litterSet N.fst) ↑N) : ConNF.MainInduction.pos (Sum.inl a) < ConNF.MainInduction.pos (Sum.inr N)

theorem ConNF.MainInduction.bool_lt [ConNF.Params] : Cardinal.lift.{u, 0} (Cardinal.mk Bool) < Cardinal.mk ConNF.μ

theorem ConNF.MainInduction.bool_ne_zero : Cardinal.lift.{u, 0} (Cardinal.mk Bool) ≠ 0

theorem ConNF.MainInduction.unitSum_le_iff [ConNF.Params] (x : Lex (Lex (ConNF.μ × Lex (Unit ⊕ ConNF.κ)) × ULift.{u, 0} Bool)) (y : Lex (Lex (ConNF.μ × Lex (Unit ⊕ ConNF.κ)) × ULift.{u, 0} Bool)) : x ≤ y ↔ Prod.Lex (fun (x x_1 : ConNF.μ) => x < x_1) (fun (x x_1 : ULift.{u, 0} Bool) => x ≤ x_1) ((ConNF.MainInduction.μProd_equiv ⋯ ⋯) x.1, x.2) ((ConNF.MainInduction.μProd_equiv ⋯ ⋯) y.1, y.2)

noncomputable def ConNF.MainInduction.posEquiv [ConNF.Params] : Lex (Lex (ConNF.μ × Lex (Unit ⊕ ConNF.κ)) × ULift.{u, 0} Bool) ≃o ConNF.μ

Equations

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

noncomputable instance ConNF.MainInduction.instBasePositions [ConNF.Params] : ConNF.BasePositions

We register this as an instance because we have no need to allow this to be customised.

Equations

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