Injective functions from denied sets

In this file, we construct a mechanism for creating injective functions satisfying particular constraints.

Main declarations

• ConNF.funOfDeny: An injective function satisfying particular requirements.

def ConNF.initialEquiv {X : Type u_1} : X ≃ (Cardinal.mk X).ord.toType

Equations

• ConNF.initialEquiv = ⋯.some

def ConNF.initialWellOrder (X : Type u_1) : LtWellOrder X

Endow a type X with a well-order of smallest possible order type.

Equations

• ConNF.initialWellOrder X = ConNF.initialEquiv.ltWellOrder

theorem ConNF.initialWellOrder_type {X : Type u_1} : (Ordinal.type fun (x1 x2 : X) => x1 < x2) = (Cardinal.mk X).ord

theorem ConNF.initialWellOrder_card_Iio {X : Type u_1} (x : X) : Cardinal.mk ↑{y : X | y < x} < Cardinal.mk X

def ConNF.chooseOfCardLt {X : Type u_1} {s : Set X} (h : Cardinal.mk ↑s < Cardinal.mk X) : X

Equations

• ConNF.chooseOfCardLt h = Exists.choose ⋯

theorem ConNF.chooseOfCardLt_not_mem {X : Type u_1} {s : Set X} (h : Cardinal.mk ↑s < Cardinal.mk X) : chooseOfCardLt h ∉ s

theorem ConNF.gtOfDeny_aux [Params] {X : Type u} (h₁ : Cardinal.mk X ≤ Cardinal.mk μ) (deny : X → Set μ) (h₂ : ∀ (x : X), Cardinal.mk ↑(deny x) < (Cardinal.mk μ).ord.cof) (x : X) (ih : (y : X) → y < x → μ) : Cardinal.mk ↑({ν : μ | ∃ (y : X) (h : y < x), ν = ih y h} ∪ {ν : μ | ∃ ξ ∈ deny x, ν ≤ ξ}) < Cardinal.mk μ

def ConNF.gtOfDeny [Params] {X : Type u} (h₁ : Cardinal.mk X ≤ Cardinal.mk μ) (deny : X → Set μ) (h₂ : ∀ (x : X), Cardinal.mk ↑(deny x) < (Cardinal.mk μ).ord.cof) (x : X) (ih : (y : X) → y < x → μ) : μ

Equations

• ConNF.gtOfDeny h₁ deny h₂ x ih = ConNF.chooseOfCardLt ⋯

theorem ConNF.gtOfDeny_spec [Params] {X : Type u} (h₁ : Cardinal.mk X ≤ Cardinal.mk μ) (deny : X → Set μ) (h₂ : ∀ (x : X), Cardinal.mk ↑(deny x) < (Cardinal.mk μ).ord.cof) (x : X) (ih : (y : X) → y < x → μ) : gtOfDeny h₁ deny h₂ x ih ∉ {ν : μ | ∃ (y : X) (h : y < x), ν = ih y h} ∪ {ν : μ | ∃ ξ ∈ deny x, ν ≤ ξ}

def ConNF.funOfDeny [Params] {X : Type u} (h₁ : Cardinal.mk X ≤ Cardinal.mk μ) (deny : X → Set μ) (h₂ : ∀ (x : X), Cardinal.mk ↑(deny x) < (Cardinal.mk μ).ord.cof) : X → μ

Equations

• ConNF.funOfDeny h₁ deny h₂ = ⋯.fix fun (x : X) (ih : (y : X) → y < x → (fun (x : X) => ConNF.μ) y) => ConNF.gtOfDeny h₁ deny h₂ x ih

theorem ConNF.funOfDeny_eq [Params] {X : Type u} (h₁ : Cardinal.mk X ≤ Cardinal.mk μ) (deny : X → Set μ) (h₂ : ∀ (x : X), Cardinal.mk ↑(deny x) < (Cardinal.mk μ).ord.cof) (x : X) : funOfDeny h₁ deny h₂ x = gtOfDeny h₁ deny h₂ x fun (y : X) (x : y < x) => funOfDeny h₁ deny h₂ y

theorem ConNF.funOfDeny_spec [Params] {X : Type u} (h₁ : Cardinal.mk X ≤ Cardinal.mk μ) (deny : X → Set μ) (h₂ : ∀ (x : X), Cardinal.mk ↑(deny x) < (Cardinal.mk μ).ord.cof) (x : X) : funOfDeny h₁ deny h₂ x ∉ {ν : μ | ∃ (y : X) (_ : y < x), ν = funOfDeny h₁ deny h₂ y} ∪ {ν : μ | ∃ ξ ∈ deny x, ν ≤ ξ}

theorem ConNF.funOfDeny_gt_deny [Params] {X : Type u} (h₁ : Cardinal.mk X ≤ Cardinal.mk μ) (deny : X → Set μ) (h₂ : ∀ (x : X), Cardinal.mk ↑(deny x) < (Cardinal.mk μ).ord.cof) (x : X) (ν : μ) (hν : ν ∈ deny x) : ν < funOfDeny h₁ deny h₂ x

theorem ConNF.funOfDeny_injective [Params] {X : Type u} (h₁ : Cardinal.mk X ≤ Cardinal.mk μ) (deny : X → Set μ) (h₂ : ∀ (x : X), Cardinal.mk ↑(deny x) < (Cardinal.mk μ).ord.cof) : Function.Injective (funOfDeny h₁ deny h₂)