Documentation

ConNF.External.WellOrder

New file #

In this file...

Main declarations #

source
def ConNF.InternalWellOrder [ConNF.Params] {α β γ δ : ConNF.Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (r : ConNF.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
Instances For
    source
    def ConNF.InternallyWellOrdered [ConNF.Params] {α β γ δ : ConNF.Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (x : ConNF.TSet ↑γ) :
    Prop
    Equations
    Instances For
      source
      @[simp]
      theorem ConNF.externalRel_smul [ConNF.Params] {α β γ δ : ConNF.Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (r : ConNF.TSet ↑α) (ρ : ConNF.AllPerm ↑α) :
      ConNF.ExternalRel hβ hγ hδ (ρ • r) = InvImage (ConNF.ExternalRel hβ hγ hδ r) fun (x : ConNF.TSet ↑δ) => (ρ ↘ hβ ↘ hγ ↘ hδ)⁻¹ • x
      source
      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.

      source
      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
      source
      theorem ConNF.exists_common_support_of_internallyWellOrdered' [ConNF.Params] {β γ δ ε : ConNF.Λ} (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑δ) {x : ConNF.TSet ↑δ} (h : ConNF.InternallyWellOrdered hγ hδ hε x) :
      ∃ (S : ConNF.Support ↑β), ∀ (y : ConNF.TSet ↑ε), y ∈[hε] x → S.Supports {{{y}[hε]}[hδ]}[hγ]
      source
      theorem ConNF.Support.Supports.ofSingleton [ConNF.Params] {α β γ : ConNF.Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) {S : ConNF.Support ↑α} {x : ConNF.TSet ↑β} (h : S.Supports {x}[hβ]) :
      (S.strong ↘ hβ).Supports x
      source
      theorem ConNF.supports_of_supports_singletons [ConNF.Params] {α β γ : ConNF.Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) {S : ConNF.Support ↑α} {s : Set (ConNF.TSet ↑β)} (h : ∀ x ∈ s, S.Supports {x}[hβ]) :
      ∃ (S : ConNF.Support ↑β), ∀ x ∈ s, S.Supports x
      source
      theorem ConNF.exists_common_support_of_internallyWellOrdered [ConNF.Params] {β γ δ ε : ConNF.Λ} (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑δ) {x : ConNF.TSet ↑δ} (h : ConNF.InternallyWellOrdered hγ hδ hε x) :
      ∃ (S : ConNF.Support ↑δ), ∀ (y : ConNF.TSet ↑ε), y ∈[hε] x → S.Supports {y}[hε]
      source
      theorem ConNF.internallyWellOrdered_of_common_support_of_nontrivial [ConNF.Params] {α β γ δ : ConNF.Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) {x : ConNF.TSet ↑γ} (hx : {y : ConNF.TSet ↑δ | y ∈[hδ] x}.Nontrivial) (S : ConNF.Support ↑δ) (hS : ∀ (y : ConNF.TSet ↑δ), y ∈[hδ] x → S.Supports y) :
      ConNF.InternallyWellOrdered hβ hγ hδ x
      source
      theorem ConNF.internallyWellOrdered_of_common_support [ConNF.Params] {α β γ δ : ConNF.Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) {x : ConNF.TSet ↑γ} (S : ConNF.Support ↑δ) (hS : ∀ (y : ConNF.TSet ↑δ), y ∈[hδ] x → S.Supports y) :
      ConNF.InternallyWellOrdered hβ hγ hδ x
      source
      theorem ConNF.powerset_internallyWellOrdered [ConNF.Params] {α β γ δ ε : ConNF.Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑δ) {x : ConNF.TSet ↑δ} (h : ConNF.InternallyWellOrdered hγ hδ hε x) :
      ConNF.InternallyWellOrdered hβ hγ hδ (ConNF.powerset hδ hε x)