# Initial segments and successors #

We establish some connections between initial segment embeddings and successors and predecessors.

source
@[simp]
theorem InitialSeg.apply_covBy_apply_iff {α : Type u_1} {β : Type u_2} {a b : α} [PartialOrder α] [PartialOrder β] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :
f a ⋖ f b ↔ a ⋖ b
source
@[simp]
theorem InitialSeg.apply_wCovBy_apply_iff {α : Type u_1} {β : Type u_2} {a b : α} [PartialOrder α] [PartialOrder β] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :
f a ⩿ f b ↔ a ⩿ b
source
theorem InitialSeg.map_succ {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] [SuccOrder α] [NoMaxOrder α] [SuccOrder β] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) (a : α) :
f (Order.succ a) = Order.succ (f a)
source
theorem InitialSeg.map_pred {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] [PredOrder α] [NoMinOrder α] [PredOrder β] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) (a : α) :
f (Order.pred a) = Order.pred (f a)
source
@[simp]
theorem InitialSeg.isSuccPrelimit_apply_iff {α : Type u_1} {β : Type u_2} {a : α} [PartialOrder α] [PartialOrder β] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :
Order.IsSuccPrelimit (f a) ↔ Order.IsSuccPrelimit a
source
@[simp]
theorem InitialSeg.isSuccLimit_apply_iff {α : Type u_1} {β : Type u_2} {a : α} [PartialOrder α] [PartialOrder β] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :
Order.IsSuccLimit (f a) ↔ Order.IsSuccLimit a
source
theorem InitialSeg.map_isSuccPrelimit {α : Type u_1} {β : Type u_2} {a : α} [PartialOrder α] [PartialOrder β] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :
Order.IsSuccPrelimit a → Order.IsSuccPrelimit (f a)

Alias of the reverse direction of `InitialSeg.isSuccPrelimit_apply_iff`.

source
theorem InitialSeg.map_isSuccLimit {α : Type u_1} {β : Type u_2} {a : α} [PartialOrder α] [PartialOrder β] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :
Order.IsSuccLimit a → Order.IsSuccLimit (f a)

Alias of the reverse direction of `InitialSeg.isSuccLimit_apply_iff`.

source
@[simp]
theorem PrincipalSeg.apply_covBy_apply_iff {α : Type u_1} {β : Type u_2} {a b : α} [PartialOrder α] [PartialOrder β] (f : PrincipalSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :
f.toRelEmbedding a ⋖ f.toRelEmbedding b ↔ a ⋖ b
source
@[simp]
theorem PrincipalSeg.apply_wCovBy_apply_iff {α : Type u_1} {β : Type u_2} {a b : α} [PartialOrder α] [PartialOrder β] (f : PrincipalSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :
f.toRelEmbedding a ⩿ f.toRelEmbedding b ↔ a ⩿ b
source
theorem PrincipalSeg.map_succ {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] [SuccOrder α] [NoMaxOrder α] [SuccOrder β] (f : PrincipalSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) (a : α) :
f.toRelEmbedding (Order.succ a) = Order.succ (f.toRelEmbedding a)
source
theorem PrincipalSeg.map_pred {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] [PredOrder α] [NoMinOrder α] [PredOrder β] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) (a : α) :
f (Order.pred a) = Order.pred (f a)
source
@[simp]
theorem PrincipalSeg.isSuccPrelimit_apply_iff {α : Type u_1} {β : Type u_2} {a : α} [PartialOrder α] [PartialOrder β] (f : PrincipalSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :
Order.IsSuccPrelimit (f.toRelEmbedding a) ↔ Order.IsSuccPrelimit a
source
@[simp]
theorem PrincipalSeg.isSuccLimit_apply_iff {α : Type u_1} {β : Type u_2} {a : α} [PartialOrder α] [PartialOrder β] (f : PrincipalSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :
Order.IsSuccLimit (f.toRelEmbedding a) ↔ Order.IsSuccLimit a
source
theorem PrincipalSeg.map_isSuccPrelimit {α : Type u_1} {β : Type u_2} {a : α} [PartialOrder α] [PartialOrder β] (f : PrincipalSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :
Order.IsSuccPrelimit a → Order.IsSuccPrelimit (f.toRelEmbedding a)

Alias of the reverse direction of `PrincipalSeg.isSuccPrelimit_apply_iff`.

source
theorem PrincipalSeg.map_isSuccLimit {α : Type u_1} {β : Type u_2} {a : α} [PartialOrder α] [PartialOrder β] (f : PrincipalSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :
Order.IsSuccLimit a → Order.IsSuccLimit (f.toRelEmbedding a)

Alias of the reverse direction of `PrincipalSeg.isSuccLimit_apply_iff`.