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) : ConNF.chooseOfCardLt h ∉ s

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

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

Equations

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

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

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

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

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

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

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