Reindexing coherent protected chains

noncomputable def ScottishBook155.ProtectedChain.withTopCoeOrderEmbedding {ι : Type u} [LinearOrder ι] : ι ↪o WithTop ι

The canonical inclusion of an ordered type into the same type with a new top element.

Equations

• ScottishBook155.ProtectedChain.withTopCoeOrderEmbedding = { toFun := fun (i : ι) => ↑i, inj' := ⋯, map_rel_iff' := ⋯ }

noncomputable def ScottishBook155.ProtectedChain.reindex {ι κ : Type u} [LinearOrder ι] [LinearOrder κ] {r L : ℝ} (C : ProtectedChain r L) (e : κ ↪o ι) : ProtectedChain r L

Pull a protected chain back along an order embedding.

Equations

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

theorem ScottishBook155.ProtectedChain.reindex_comp {ι κ : Type u} [LinearOrder ι] [LinearOrder κ] {r L : ℝ} {μ : Type u} [LinearOrder μ] (C : ProtectedChain r L) (e : κ ↪o ι) (f : μ ↪o κ) : (C.reindex e).reindex f = C.reindex (RelEmbedding.trans f e)

Two successive reindexings are the reindexing by the composite order embedding.

theorem ScottishBook155.ProtectedChain.reindex_congr {ι κ : Type u} [LinearOrder ι] [LinearOrder κ] {r L : ℝ} (C : ProtectedChain r L) (e f : κ ↪o ι) (h : ∀ (k : κ), e k = f k) : C.reindex e = C.reindex f

Reindexing depends only on the pointwise action of the order embedding.

noncomputable def ScottishBook155.ProtectedChain.restrictionLE {ι : Type u} [LinearOrder ι] {r L : ℝ} (C : ProtectedChain r L) (j : ι) : ProtectedChain r L

Restrict a chain to the closed initial segment ending at j.

Equations

• C.restrictionLE j = C.reindex (OrderEmbedding.subtype fun (x : ι) => x ∈ Set.Iic j)

noncomputable def ScottishBook155.ProtectedChain.restrictionLT {ι : Type u} [LinearOrder ι] {r L : ℝ} (C : ProtectedChain r L) (j : ι) : ProtectedChain r L

Restrict a chain to the open initial segment below j.

Equations

• C.restrictionLT j = C.reindex (OrderEmbedding.subtype fun (x : ι) => x ∈ Set.Iio j)