Base positions

In this file, we define position functions for atoms, litters, and near-litters.

Main declarations

• ConNF.instPositionLitter: The position function for litters.
• ConNF.instPositionAtom: The position function for atoms.
• ConNF.instPositionNearLitter: The position function for near-litters.

TODO: These position functions are very simple to define but might not have all the required properties (e.g. joint injectivity, positions of litters compared to their near-litters). We should investigate this later, once we know precisely what is needed. The properties of the position function on litters allows for a concise description of the fuzz map condition.

instance ConNF.instPositionLitter [Params] : Position Litter

Equations

• ConNF.instPositionLitter = { pos := { toFun := ConNF.funOfDeny ⋯ (fun (L : ConNF.Litter) => {L.ν}) ⋯, inj' := ⋯ } }

theorem ConNF.Litter.lt_pos [Params] (L : Litter) : L.ν < pos L

instance ConNF.instPositionAtom [Params] : Position Atom

Equations

• ConNF.instPositionAtom = { pos := { toFun := ConNF.funOfDeny ⋯ (fun (a : ConNF.Atom) => {ConNF.pos aᴸ}) ⋯, inj' := ⋯ } }

theorem ConNF.Atom.pos_litter_lt_pos [Params] (a : Atom) : pos aᴸ < pos a

instance ConNF.instPositionNearLitter [Params] : Position NearLitter

Equations

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

theorem ConNF.NearLitter.pos_litter_lt_pos [Params] (N : NearLitter) : pos Nᴸ < pos N

theorem ConNF.NearLitter.pos_atom_lt_pos [Params] (N : NearLitter) (a : Atom) (h : a ∈ symmDiff Nᴬ Nᴸᴬ) : pos a < pos N