Survival

SE.Persistence.Relation.Survival

Identity survives from x to y when y is reachable from x by a finite sequence of preserving steps.

Survival is directed. Its symmetric closure is the identity relation of SE.Persistence.Relation.Equivalence, and the two differ: on the free dynamics a preserving step survives forward but not backward.

def SE.Persistence.Classification.stepRel {T C : Type} (c : Classification T) (d : Dynamics T C) : C → C → Prop

One step of a preserving transformation of c.

Equations

• c.stepRel d x y = ∃ (t : T), c.IsPrs t ∧ d.step t x y

def SE.Persistence.Classification.Survives {T C : Type} (c : Classification T) (d : Dynamics T C) : C → C → Prop

Identity survives from x to y: a finite chain of preserving steps.

Equations

• c.Survives d x y = SE.Persistence.Reach (c.stepRel d) x y

theorem SE.Persistence.Classification.survives_refl {T C : Type} (c : Classification T) (d : Dynamics T C) (x : C) : c.Survives d x x

Survival is reflexive.

theorem SE.Persistence.Classification.survives_of_stepRel {T C : Type} {c : Classification T} {d : Dynamics T C} {x y : C} (h : c.stepRel d x y) : c.Survives d x y

A preserving step is a survival.

theorem SE.Persistence.Classification.Survives.trans {T C : Type} {c : Classification T} {d : Dynamics T C} {x y z : C} (h1 : c.Survives d x y) (h2 : c.Survives d y z) : c.Survives d x z

Survival is transitive.

theorem SE.Persistence.Classification.survives_mono {T C : Type} {c c' : Classification T} {d : Dynamics T C} (h : ∀ (t : T), c.IsPrs t → c'.IsPrs t) {x y : C} (hs : c.Survives d x y) : c'.Survives d x y

Preserving more transformations survives more.

theorem SE.Persistence.Classification.survives_free_true {T : Type} (c : Classification T) {t : T} {y : T × Bool} (h : c.Survives (freeDynamics T) (t, true) y) : y = (t, true)

On the free dynamics nothing leaves a state of the form (t, true).