ConNF.FOA.Properties.ConstrainedAction

source

def ConNF.StructApprox.transConstrained [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (c : ConNF.Address ↑β) (d : ConNF.Address ↑β) :

Set (ConNF.Address ↑β)

Equations

ConNF.StructApprox.transConstrained c d = {e : ConNF.Address ↑β | e < c} ∪ {e : ConNF.Address ↑β | e < d}

Instances For

source

def ConNF.StructApprox.reflTransConstrained [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (c : ConNF.Address ↑β) (d : ConNF.Address ↑β) :

Set (ConNF.Address ↑β)

Equations

ConNF.StructApprox.reflTransConstrained c d = {e : ConNF.Address ↑β | e ≤ c} ∪ {e : ConNF.Address ↑β | e ≤ d}

Instances For

source

theorem ConNF.StructApprox.transConstrained_symm [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (c : ConNF.Address ↑β) (d : ConNF.Address ↑β) :

ConNF.StructApprox.transConstrained c d = ConNF.StructApprox.transConstrained d c

source

theorem ConNF.StructApprox.reflTransConstrained_symm [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (c : ConNF.Address ↑β) (d : ConNF.Address ↑β) :

ConNF.StructApprox.reflTransConstrained c d = ConNF.StructApprox.reflTransConstrained d c

source

@[simp]

theorem ConNF.StructApprox.transConstrained_self [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (c : ConNF.Address ↑β) :

ConNF.StructApprox.transConstrained c c = {e : ConNF.Address ↑β | e < c}

source

@[simp]

theorem ConNF.StructApprox.reflTransConstrained_self [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (c : ConNF.Address ↑β) :

ConNF.StructApprox.reflTransConstrained c c = {e : ConNF.Address ↑β | e ≤ c}

source

theorem ConNF.StructApprox.mem_reflTransConstrained_of_mem_transConstrained [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {c : ConNF.Address ↑β} {d : ConNF.Address ↑β} {e : ConNF.Address ↑β} (he : e ∈ ConNF.StructApprox.transConstrained c d) :

e ∈ ConNF.StructApprox.reflTransConstrained c d

source

theorem ConNF.StructApprox.transConstrained_trans [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {c : ConNF.Address ↑β} {d : ConNF.Address ↑β} {e : ConNF.Address ↑β} {f : ConNF.Address ↑β} (he : e ∈ ConNF.StructApprox.transConstrained c d) (hf : f ≤ e) :

f ∈ ConNF.StructApprox.transConstrained c d

source

theorem ConNF.StructApprox.reflTransConstrained_trans [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {c : ConNF.Address ↑β} {d : ConNF.Address ↑β} {e : ConNF.Address ↑β} {f : ConNF.Address ↑β} (he : e ∈ ConNF.StructApprox.reflTransConstrained c d) (hf : f ≤ e) :

f ∈ ConNF.StructApprox.reflTransConstrained c d

source

theorem ConNF.StructApprox.transConstrained_of_reflTransConstrained_of_trans_constrains [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {c : ConNF.Address ↑β} {d : ConNF.Address ↑β} {e : ConNF.Address ↑β} {f : ConNF.Address ↑β} (he : e ∈ ConNF.StructApprox.reflTransConstrained c d) (hf : f < e) :

f ∈ ConNF.StructApprox.transConstrained c d

source

theorem ConNF.StructApprox.transConstrained_of_constrains [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {c : ConNF.Address ↑β} {d : ConNF.Address ↑β} {e : ConNF.Address ↑β} {f : ConNF.Address ↑β} (he : e ∈ ConNF.StructApprox.transConstrained c d) (hf : f ≺ e) :

f ∈ ConNF.StructApprox.transConstrained c d

source

theorem ConNF.StructApprox.reflTransConstrained_of_constrains [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {c : ConNF.Address ↑β} {d : ConNF.Address ↑β} {e : ConNF.Address ↑β} {f : ConNF.Address ↑β} (he : e ∈ ConNF.StructApprox.reflTransConstrained c d) (hf : f ≺ e) :

f ∈ ConNF.StructApprox.reflTransConstrained c d

source

theorem ConNF.StructApprox.transConstrained_of_reflTransConstrained_of_constrains [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {c : ConNF.Address ↑β} {d : ConNF.Address ↑β} {e : ConNF.Address ↑β} {f : ConNF.Address ↑β} (he : e ∈ ConNF.StructApprox.reflTransConstrained c d) (hf : f ≺ e) :

f ∈ ConNF.StructApprox.transConstrained c d

source

theorem ConNF.StructApprox.fst_transConstrained [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {c : ConNF.Address ↑β} {d : ConNF.Address ↑β} {A : ConNF.ExtendedIndex ↑β} {a : ConNF.Atom} (hac : { path := A, value := Sum.inl a } ∈ ConNF.StructApprox.reflTransConstrained c d) :

{ path := A, value := Sum.inr a.1.toNearLitter } ∈ ConNF.StructApprox.transConstrained c d

source

theorem ConNF.StructApprox.fst_mem_trans_constrained' [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {c : ConNF.Address ↑β} {d : ConNF.Address ↑β} {A : ConNF.ExtendedIndex ↑β} {a : ConNF.Atom} (h : { path := A, value := Sum.inl a } ∈ ConNF.StructApprox.transConstrained c d) :

{ path := A, value := Sum.inr a.1.toNearLitter } ∈ ConNF.StructApprox.transConstrained c d

source

theorem ConNF.StructApprox.fst_mem_transConstrained [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {c : ConNF.Address ↑β} {d : ConNF.Address ↑β} {A : ConNF.ExtendedIndex ↑β} {N : ConNF.NearLitter} (hN : { path := A, value := Sum.inr N } ∈ ConNF.StructApprox.transConstrained c d) :

{ path := A, value := Sum.inr N.fst.toNearLitter } ∈ ConNF.StructApprox.transConstrained c d

source

theorem ConNF.StructApprox.fst_mem_refl_trans_constrained' [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {c : ConNF.Address ↑β} {d : ConNF.Address ↑β} {A : ConNF.ExtendedIndex ↑β} {a : ConNF.Atom} (h : { path := A, value := Sum.inl a } ∈ ConNF.StructApprox.reflTransConstrained c d) :

{ path := A, value := Sum.inr a.1.toNearLitter } ∈ ConNF.StructApprox.reflTransConstrained c d

source

theorem ConNF.StructApprox.fst_mem_reflTransConstrained [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {c : ConNF.Address ↑β} {d : ConNF.Address ↑β} {A : ConNF.ExtendedIndex ↑β} {N : ConNF.NearLitter} (hN : { path := A, value := Sum.inr N } ∈ ConNF.StructApprox.reflTransConstrained c d) :

{ path := A, value := Sum.inr N.fst.toNearLitter } ∈ ConNF.StructApprox.reflTransConstrained c d

source

theorem ConNF.StructApprox.fst_mem_transConstrained_of_mem_symmDiff [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {c : ConNF.Address ↑β} {d : ConNF.Address ↑β} {A : ConNF.ExtendedIndex ↑β} {N : ConNF.NearLitter} {a : ConNF.Atom} (h : a ∈ symmDiff (ConNF.litterSet N.fst) ↑N) (hN : { path := A, value := Sum.inr N } ∈ ConNF.StructApprox.transConstrained c d) :

{ path := A, value := Sum.inr a.1.toNearLitter } ∈ ConNF.StructApprox.transConstrained c d

source

theorem ConNF.StructApprox.fst_mem_reflTransConstrained_of_mem_symmDiff [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {c : ConNF.Address ↑β} {d : ConNF.Address ↑β} {A : ConNF.ExtendedIndex ↑β} {N : ConNF.NearLitter} {a : ConNF.Atom} (h : a ∈ symmDiff (ConNF.litterSet N.fst) ↑N) (hN : { path := A, value := Sum.inr N } ∈ ConNF.StructApprox.reflTransConstrained c d) :

{ path := A, value := Sum.inr a.1.toNearLitter } ∈ ConNF.StructApprox.reflTransConstrained c d

source

theorem ConNF.StructApprox.fst_mem_transConstrained_of_mem [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {c : ConNF.Address ↑β} {d : ConNF.Address ↑β} {A : ConNF.ExtendedIndex ↑β} {N : ConNF.NearLitter} {a : ConNF.Atom} (h : a ∈ N) (hN : { path := A, value := Sum.inr N } ∈ ConNF.StructApprox.transConstrained c d) :

{ path := A, value := Sum.inr a.1.toNearLitter } ∈ ConNF.StructApprox.transConstrained c d

source

theorem ConNF.StructApprox.eq_of_sublitter_bijection_apply_eq [ConNF.Params] {π : ConNF.BaseApprox} {L₁ : ConNF.Litter} {L₂ : ConNF.Litter} {L₃ : ConNF.Litter} {L₄ : ConNF.Litter} {a : ↥(π.largestSublitter L₁)} {b : ↥(π.largestSublitter L₃)} :

↑(((π.largestSublitter L₁).equiv (π.largestSublitter L₂)) a) = ↑(((π.largestSublitter L₃).equiv (π.largestSublitter L₄)) b) → L₁ = L₃ → L₂ = L₄ → ↑a = ↑b

source

noncomputable def ConNF.StructApprox.constrainedAction [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] (π : ConNF.StructApprox ↑β) (s : Set (ConNF.Address ↑β)) (hs : ConNF.Small s) :

ConNF.StructLAction ↑β

Equations

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

Instances For

source

noncomputable def ConNF.StructApprox.ihsAction [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] (π : ConNF.StructApprox ↑β) (c : ConNF.Address ↑β) (d : ConNF.Address ↑β) :

ConNF.StructLAction ↑β

An object like ih_action that can take two addresses.

Equations

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

Instances For

source

@[simp]

theorem ConNF.StructApprox.constrainedAction_atomMap [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} {s : Set (ConNF.Address ↑β)} {hs : ConNF.Small s} {B : ConNF.ExtendedIndex ↑β} {a : ConNF.Atom} :

(π.constrainedAction s hs B).atomMap a = { Dom := ∃ c ∈ s, { path := B, value := Sum.inl a } ≤ c, get := fun (x : ∃ c ∈ s, { path := B, value := Sum.inl a } ≤ c) => π.completeAtomMap B a }

source

@[simp]

theorem ConNF.StructApprox.constrainedAction_litterMap [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} {s : Set (ConNF.Address ↑β)} {hs : ConNF.Small s} {B : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} :

(π.constrainedAction s hs B).litterMap L = { Dom := ∃ c ∈ s, { path := B, value := Sum.inr L.toNearLitter } ≤ c, get := fun (x : ∃ c ∈ s, { path := B, value := Sum.inr L.toNearLitter } ≤ c) => π.completeNearLitterMap B L.toNearLitter }

source

@[simp]

theorem ConNF.StructApprox.ihsAction_atomMap [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} {c : ConNF.Address ↑β} {d : ConNF.Address ↑β} {B : ConNF.ExtendedIndex ↑β} {a : ConNF.Atom} :

(π.ihsAction c d B).atomMap a = { Dom := { path := B, value := Sum.inl a } ∈ ConNF.StructApprox.transConstrained c d, get := fun (x : { path := B, value := Sum.inl a } ∈ ConNF.StructApprox.transConstrained c d) => π.completeAtomMap B a }

source

@[simp]

theorem ConNF.StructApprox.ihsAction_litterMap [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} {c : ConNF.Address ↑β} {d : ConNF.Address ↑β} {B : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} :

(π.ihsAction c d B).litterMap L = { Dom := { path := B, value := Sum.inr L.toNearLitter } ∈ ConNF.StructApprox.transConstrained c d, get := fun (x : { path := B, value := Sum.inr L.toNearLitter } ∈ ConNF.StructApprox.transConstrained c d) => π.completeNearLitterMap B L.toNearLitter }

source

theorem ConNF.StructApprox.ihsAction_symm [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] (π : ConNF.StructApprox ↑β) (c : ConNF.Address ↑β) (d : ConNF.Address ↑β) :

π.ihsAction c d = π.ihsAction d c

source

@[simp]

theorem ConNF.StructApprox.ihsAction_self [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] (π : ConNF.StructApprox ↑β) (c : ConNF.Address ↑β) :

π.ihsAction c c = ConNF.StructApprox.ihAction π.foaHypothesis

source

theorem ConNF.StructApprox.constrainedAction_mono [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} {s : Set (ConNF.Address ↑β)} {t : Set (ConNF.Address ↑β)} {hs : ConNF.Small s} {ht : ConNF.Small t} (h : s ⊆ t) :

π.constrainedAction s hs ≤ π.constrainedAction t ht

source

theorem ConNF.StructApprox.ihAction_le_constrainedAction [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} {s : Set (ConNF.Address ↑β)} {hs : ConNF.Small s} (c : ConNF.Address ↑β) (hc : ∃ d ∈ s, c ≤ d) :

ConNF.StructApprox.ihAction π.foaHypothesis ≤ π.constrainedAction s hs

source

theorem ConNF.StructApprox.ihAction_eq_constrainedAction [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] (π : ConNF.StructApprox ↑β) (c : ConNF.Address ↑β) :

ConNF.StructApprox.ihAction π.foaHypothesis = π.constrainedAction {d : ConNF.Address ↑β | d ≺ c} ⋯

source

theorem ConNF.StructApprox.ihsAction_eq_constrainedAction [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] (π : ConNF.StructApprox ↑β) (c : ConNF.Address ↑β) (d : ConNF.Address ↑β) :

π.ihsAction c d = π.constrainedAction ({e : ConNF.Address ↑β | e ≺ c} ∪ {e : ConNF.Address ↑β | e ≺ d}) ⋯

source

theorem ConNF.StructApprox.ihAction_le_ihsAction [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] (π : ConNF.StructApprox ↑β) (c : ConNF.Address ↑β) (d : ConNF.Address ↑β) :

ConNF.StructApprox.ihAction π.foaHypothesis ≤ π.ihsAction c d

source

theorem ConNF.StructApprox.ihAction_le [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} {c : ConNF.Address ↑β} {d : ConNF.Address ↑β} (h : c ≤ d) :

ConNF.StructApprox.ihAction π.foaHypothesis ≤ ConNF.StructApprox.ihAction π.foaHypothesis