New file

In this file...

Main declarations

• ConNF.foo: Something new.

def ConNF.InternalWellOrder [Params] {α β γ δ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (r : TSet ↑α) : Prop

A set in our model that is a well-order. Internal well-orders are exactly external well-orders, so we externalise the definition for convenience.

Equations

• ConNF.InternalWellOrder hβ hγ hδ r = IsWellOrder (↑(ConNF.ExternalRel hβ hγ hδ r).field) (InvImage (ConNF.ExternalRel hβ hγ hδ r) Subtype.val)

def ConNF.InternallyWellOrdered [Params] {α β γ δ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (x : TSet ↑γ) : Prop

Equations

• ConNF.InternallyWellOrdered hβ hγ hδ x = ({y : ConNF.TSet ↑δ | y ∈[hδ] x}.Subsingleton ∨ ∃ (r : ConNF.TSet ↑α), ConNF.InternalWellOrder hβ hγ hδ r ∧ x = ConNF.field hβ hγ hδ r)

@[simp]

theorem ConNF.externalRel_smul [Params] {α β γ δ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (r : TSet ↑α) (ρ : AllPerm ↑α) : ExternalRel hβ hγ hδ (ρ • r) = InvImage (ExternalRel hβ hγ hδ r) fun (x : TSet ↑δ) => (ρ ↘ hβ ↘ hγ ↘ hδ)⁻¹ • x

theorem ConNF.apply_eq_of_isWellOrder {X : Type u_1} {r : Rel X X} {f : X → X} (hr : IsWellOrder X r) (hf : Function.Bijective f) (hf' : ∀ (x y : X), r x y ↔ r (f x) (f y)) (x : X) : f x = x

Well-orders are rigid.

theorem ConNF.apply_eq_of_isWellOrder' {X : Type u_1} {r : Rel X X} {f : X → X} (hr : IsWellOrder (↑r.field) (InvImage r Subtype.val)) (hf : Function.Bijective f) (hf' : ∀ (x y : X), r x y ↔ r (f x) (f y)) (x : X) : x ∈ r.field → f x = x

theorem ConNF.exists_common_support_of_internallyWellOrdered' [Params] {β γ δ ε : Λ} (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑δ) {x : TSet ↑δ} (h : InternallyWellOrdered hγ hδ hε x) : ∃ (S : Support ↑β), ∀ (y : TSet ↑ε), y ∈[hε] x → S.Supports {{{y}[hε]}[hδ]}[hγ]

theorem ConNF.Support.Supports.ofSingleton [Params] {α β γ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) {S : Support ↑α} {x : TSet ↑β} (h : S.Supports {x}[hβ]) : (S.strong ↘ hβ).Supports x

theorem ConNF.supports_of_supports_singletons [Params] {α β γ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) {S : Support ↑α} {s : Set (TSet ↑β)} (h : ∀ x ∈ s, S.Supports {x}[hβ]) : ∃ (S : Support ↑β), ∀ x ∈ s, S.Supports x

theorem ConNF.exists_common_support_of_internallyWellOrdered [Params] {β γ δ ε : Λ} (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑δ) {x : TSet ↑δ} (h : InternallyWellOrdered hγ hδ hε x) : ∃ (S : Support ↑δ), ∀ (y : TSet ↑ε), y ∈[hε] x → S.Supports {y}[hε]

theorem ConNF.internallyWellOrdered_of_common_support_of_nontrivial [Params] {α β γ δ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) {x : TSet ↑γ} (hx : {y : TSet ↑δ | y ∈[hδ] x}.Nontrivial) (S : Support ↑δ) (hS : ∀ (y : TSet ↑δ), y ∈[hδ] x → S.Supports y) : InternallyWellOrdered hβ hγ hδ x

theorem ConNF.internallyWellOrdered_of_common_support [Params] {α β γ δ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) {x : TSet ↑γ} (S : Support ↑δ) (hS : ∀ (y : TSet ↑δ), y ∈[hδ] x → S.Supports y) : InternallyWellOrdered hβ hγ hδ x

theorem ConNF.powerset_internallyWellOrdered [Params] {α β γ δ ε : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑δ) {x : TSet ↑δ} (h : InternallyWellOrdered hγ hδ hε x) : InternallyWellOrdered hβ hγ hδ (powerset hδ hε x)