theorem ConNF.StructApprox.completeNearLitterMap_subset_range [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (A : ConNF.ExtendedIndex ↑β) (L : ConNF.Litter) : ↑(π.completeNearLitterMap A L.toNearLitter) ⊆ Set.range (π.completeAtomMap A)

theorem ConNF.StructApprox.completeAtomMap_surjective_extends [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (A : ConNF.ExtendedIndex ↑β) (a : ConNF.Atom) (h : a.1 ∈ Set.range (π.completeLitterMap A)) : a ∈ Set.range (π.completeAtomMap A)

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

Equations

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

@[simp]

theorem ConNF.StructApprox.completeAddressMap_atom_eq [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} {a : ConNF.Atom} {B : ConNF.ExtendedIndex ↑β} : π.completeAddressMap { path := B, value := Sum.inl a } = { path := B, value := Sum.inl (π.completeAtomMap B a) }

@[simp]

theorem ConNF.StructApprox.completeAddressMap_nearLitter_eq [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} {N : ConNF.NearLitter} {B : ConNF.ExtendedIndex ↑β} : π.completeAddressMap { path := B, value := Sum.inr N } = { path := B, value := Sum.inr (π.completeNearLitterMap B N) }

theorem ConNF.StructApprox.completeAddressMap_injective [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) : Function.Injective π.completeAddressMap

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

Equations

• π.preimageConstrained c = π.completeAddressMap ⁻¹' {d : ConNF.Address ↑β | d ≺ c}

theorem ConNF.StructApprox.preimageConstrained_small [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) (c : ConNF.Address ↑β) : ConNF.Small (π.preimageConstrained c)

noncomputable def ConNF.StructApprox.preimageAction [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) (c : ConNF.Address ↑β) : ConNF.StructLAction ↑β

Equations

• ConNF.StructApprox.preimageAction hπf c = π.constrainedAction (π.preimageConstrained c) ⋯

theorem ConNF.StructApprox.preimageAction_eq_constrainedAction [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) (c : ConNF.Address ↑β) : ConNF.StructApprox.preimageAction hπf c = π.constrainedAction (π.preimageConstrained c) ⋯

theorem ConNF.StructApprox.preimageAction_lawful [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) {c : ConNF.Address ↑β} : (ConNF.StructApprox.preimageAction hπf c).Lawful

theorem ConNF.StructApprox.preimageAction_comp_mapFlexible [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} {hπf : π.Free} {γ : ConNF.Λ} {c : ConNF.Address ↑β} (A : Quiver.Path ↑β ↑γ) : ConNF.StructLAction.MapFlexible (ConNF.Tree.comp A (ConNF.StructApprox.preimageAction hπf c))

theorem ConNF.StructApprox.Relation.reflTransGen_of_eq {α : Type u_1} {r : α → α → Prop} {x : α} {y : α} (h : x = y) : Relation.ReflTransGen r x y

theorem ConNF.StructApprox.preimageAction_coherent [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) {γ : ConNF.Λ} [ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) (B : ConNF.ExtendedIndex ↑γ) (N : ConNF.NearLitter) (c : ConNF.Address ↑β) (hc : { path := A.comp B, value := Sum.inr (π.completeNearLitterMap (A.comp B) N) } ≺ c) (ρ : ConNF.Allowable ↑γ) (h : (ConNF.StructLAction.toApprox (ConNF.Tree.comp A (ConNF.StructApprox.preimageAction hπf c)) ⋯).ExactlyApproximates (ConNF.Allowable.toStructPerm ρ)) : π.completeNearLitterMap (A.comp B) N = ConNF.Tree.comp B (ConNF.Allowable.toStructPerm ρ) • N

theorem ConNF.StructApprox.preimageAction_coherent_atom [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) {γ : ConNF.Λ} [ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) (B : ConNF.ExtendedIndex ↑γ) (a : ConNF.Atom) (c : ConNF.Address ↑β) (hc : { path := A.comp B, value := Sum.inl (π.completeAtomMap (A.comp B) a) } ≺ c) (ρ : ConNF.Allowable ↑γ) (h : (ConNF.StructLAction.toApprox (ConNF.Tree.comp A (ConNF.StructApprox.preimageAction hπf c)) ⋯).ExactlyApproximates (ConNF.Allowable.toStructPerm ρ)) : π.completeAtomMap (A.comp B) a = ConNF.Tree.comp B (ConNF.Allowable.toStructPerm ρ) • a

theorem ConNF.StructApprox.completeLitterMap_surjective_extends [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) (A : ConNF.ExtendedIndex ↑β) (L : ConNF.Litter) (ha : ∀ (B : ConNF.ExtendedIndex ↑β) (a : ConNF.Atom), { path := B, value := Sum.inl a } ≺ { path := A, value := Sum.inr L.toNearLitter } → a ∈ Set.range (π.completeAtomMap B)) (hN : ∀ (B : ConNF.ExtendedIndex ↑β) (N : ConNF.NearLitter), { path := B, value := Sum.inr N } ≺ { path := A, value := Sum.inr L.toNearLitter } → N ∈ Set.range (π.completeNearLitterMap B)) : L ∈ Set.range (π.completeLitterMap A)

theorem ConNF.StructApprox.atom_mem_range_of_mem_completeNearLitterMap [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (A : ConNF.ExtendedIndex ↑β) (a : ConNF.Atom) {N : ConNF.NearLitter} (h : a ∈ π.completeNearLitterMap A N) : a ∈ Set.range (π.completeAtomMap A)

theorem ConNF.StructApprox.completeNearLitterMap_coe [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) (A : ConNF.ExtendedIndex ↑β) (N : ConNF.NearLitter) : ↑(π.completeNearLitterMap A N) = π.completeAtomMap A '' ↑N

@[simp]

theorem ConNF.StructApprox.preimage_symmDiff {α : Type u_1} {β : Type u_2} {s : Set β} {t : Set β} {f : α → β} : f ⁻¹' symmDiff s t = symmDiff (f ⁻¹' s) (f ⁻¹' t)

theorem ConNF.StructApprox.completeNearLitterMap_surjective_extends [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) (A : ConNF.ExtendedIndex ↑β) (N : ConNF.NearLitter) (hN : N.fst ∈ Set.range (π.completeLitterMap A)) (ha : symmDiff (ConNF.litterSet N.fst) ↑N ⊆ Set.range (π.completeAtomMap A)) : N ∈ Set.range (π.completeNearLitterMap A)

def ConNF.StructApprox.CompleteMapSurjectiveAt [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] (π : ConNF.StructApprox ↑β) : ConNF.Address ↑β → Prop

Equations

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

theorem ConNF.StructApprox.completeMap_surjective_extends [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) (c : ConNF.Address ↑β) (hc : ∀ d < c, π.CompleteMapSurjectiveAt d) : π.CompleteMapSurjectiveAt c

theorem ConNF.StructApprox.completeMapSurjectiveAtAll [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) (c : ConNF.Address ↑β) : π.CompleteMapSurjectiveAt c

theorem ConNF.StructApprox.completeAtomMap_surjective [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) (A : ConNF.ExtendedIndex ↑β) : Function.Surjective (π.completeAtomMap A)

theorem ConNF.StructApprox.completeNearLitterMap_surjective [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) (A : ConNF.ExtendedIndex ↑β) : Function.Surjective (π.completeNearLitterMap A)

theorem ConNF.StructApprox.completeLitterMap_surjective [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) (A : ConNF.ExtendedIndex ↑β) : Function.Surjective (π.completeLitterMap A)