def ConNF.StructApprox.nearLitterHypothesis [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (A : ConNF.ExtendedIndex ↑β) (N : ConNF.NearLitter) (H : ConNF.HypAction { path := A, value := Sum.inr N }) : ConNF.HypAction { path := A, value := Sum.inr N.fst.toNearLitter }

Equations

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

def ConNF.StructApprox.nearLitterCompletionMap [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] (π : ConNF.StructApprox ↑β) (A : ConNF.ExtendedIndex ↑β) (N : ConNF.NearLitter) (H : ConNF.HypAction { path := A, value := Sum.inr N }) : Set ConNF.Atom

Equations

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

theorem ConNF.StructApprox.nearLitterCompletionMap_isNearLitter [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] (π : ConNF.StructApprox ↑β) (A : ConNF.ExtendedIndex ↑β) (N : ConNF.NearLitter) (H : ConNF.HypAction { path := A, value := Sum.inr N }) : ConNF.IsNearLitter (π.litterCompletion A N.fst (ConNF.StructApprox.nearLitterHypothesis A N H)) (π.nearLitterCompletionMap A N H)

noncomputable def ConNF.StructApprox.nearLitterCompletion [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] (π : ConNF.StructApprox ↑β) (A : ConNF.ExtendedIndex ↑β) (N : ConNF.NearLitter) (H : ConNF.HypAction { path := A, value := Sum.inr N }) : ConNF.NearLitter

Equations

• π.nearLitterCompletion A N H = ⟨π.litterCompletion A N.fst (ConNF.StructApprox.nearLitterHypothesis A N H), ⟨π.nearLitterCompletionMap A N H, ⋯⟩⟩

@[simp]

theorem ConNF.StructApprox.nearLitterCompletion_fst_eq [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] (π : ConNF.StructApprox ↑β) (A : ConNF.ExtendedIndex ↑β) (N : ConNF.NearLitter) (H : ConNF.HypAction { path := A, value := Sum.inr N }) : (π.nearLitterCompletion A N H).fst = π.litterCompletion A N.fst (ConNF.StructApprox.nearLitterHypothesis A N H)