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

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

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