Documentation

CslibFrontier.Foundations.GroupTheory.Perm.RemoveNoneExtension

Extending values over a removed permutation point #

A function on the retained points extends to Option by assigning the removed point its successor's value. If that point was fixed, the specified default is used. The extension is constant on the removed step and agrees exactly with the removeNone successor elsewhere. No finiteness or equality decision is required. These original identities let a Boolean potential give zero label to a deleted dart without changing retained differences.

source
def Equiv.Perm.extendRemoveNone {α : Type u_1} {β : Type u_2} (f : Perm (Option α)) (p : α → β) (base : β) :
Option α → β

Extend values from retained points; a removed fixed point receives base.

Instances For
    source
    theorem Equiv.Perm.extendRemoveNone_some {α : Type u_1} {β : Type u_2} (f : Perm (Option α)) (p : α → β) (base : β) (a : α) :
    f.extendRemoveNone p base (some a) = p a

    Every retained value is literally unchanged.

    source
    theorem Equiv.Perm.extendRemoveNone_none {α : Type u_1} {β : Type u_2} (f : Perm (Option α)) (p : α → β) (base : β) :
    f.extendRemoveNone p base none = f.extendRemoveNone p base (f none)

    The deleted step has constant extended value, including a deleted fixed point.

    source
    theorem Equiv.Perm.extendRemoveNone_apply_some {α : Type u_1} {β : Type u_2} (f : Perm (Option α)) (p : α → β) (base : β) (a : α) :
    f.extendRemoveNone p base (f (some a)) = p ((removeNone f) a)

    The old successor's extended value is exactly the retained permutation successor's value. This includes a step that previously led into the deleted point.