Initial segments and successors

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

@[simp]

theorem InitialSeg.apply_covBy_apply_iff {α : Type u_1} {β : Type u_2} {a b : α} [PartialOrder α] [PartialOrder β] (f : (fun (x1 x2 : α) => x1 < x2) ≼i fun (x1 x2 : β) => x1 < x2) : f a ⋖ f b ↔ a ⋖ b

@[simp]

theorem InitialSeg.apply_wCovBy_apply_iff {α : Type u_1} {β : Type u_2} {a b : α} [PartialOrder α] [PartialOrder β] (f : (fun (x1 x2 : α) => x1 < x2) ≼i fun (x1 x2 : β) => x1 < x2) : f a ⩿ f b ↔ a ⩿ b

theorem InitialSeg.map_succ {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] [SuccOrder α] [NoMaxOrder α] [SuccOrder β] (f : (fun (x1 x2 : α) => x1 < x2) ≼i fun (x1 x2 : β) => x1 < x2) (a : α) : f (Order.succ a) = Order.succ (f a)

theorem InitialSeg.map_pred {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] [PredOrder α] [NoMinOrder α] [PredOrder β] (f : (fun (x1 x2 : α) => x1 < x2) ≼i fun (x1 x2 : β) => x1 < x2) (a : α) : f (Order.pred a) = Order.pred (f a)

@[simp]

theorem InitialSeg.isSuccPrelimit_apply_iff {α : Type u_1} {β : Type u_2} {a : α} [PartialOrder α] [PartialOrder β] (f : (fun (x1 x2 : α) => x1 < x2) ≼i fun (x1 x2 : β) => x1 < x2) : Order.IsSuccPrelimit (f a) ↔ Order.IsSuccPrelimit a

@[simp]

theorem InitialSeg.isSuccLimit_apply_iff {α : Type u_1} {β : Type u_2} {a : α} [PartialOrder α] [PartialOrder β] (f : (fun (x1 x2 : α) => x1 < x2) ≼i fun (x1 x2 : β) => x1 < x2) : Order.IsSuccLimit (f a) ↔ Order.IsSuccLimit a

@[simp]

theorem PrincipalSeg.apply_covBy_apply_iff {α : Type u_1} {β : Type u_2} {a b : α} [PartialOrder α] [PartialOrder β] (f : (fun (x1 x2 : α) => x1 < x2) ≺i fun (x1 x2 : β) => x1 < x2) : f.toRelEmbedding a ⋖ f.toRelEmbedding b ↔ a ⋖ b

@[simp]

theorem PrincipalSeg.apply_wCovBy_apply_iff {α : Type u_1} {β : Type u_2} {a b : α} [PartialOrder α] [PartialOrder β] (f : (fun (x1 x2 : α) => x1 < x2) ≺i fun (x1 x2 : β) => x1 < x2) : f.toRelEmbedding a ⩿ f.toRelEmbedding b ↔ a ⩿ b

theorem PrincipalSeg.map_succ {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] [SuccOrder α] [NoMaxOrder α] [SuccOrder β] (f : (fun (x1 x2 : α) => x1 < x2) ≺i fun (x1 x2 : β) => x1 < x2) (a : α) : f.toRelEmbedding (Order.succ a) = Order.succ (f.toRelEmbedding a)

theorem PrincipalSeg.map_pred {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] [PredOrder α] [NoMinOrder α] [PredOrder β] (f : (fun (x1 x2 : α) => x1 < x2) ≼i fun (x1 x2 : β) => x1 < x2) (a : α) : f (Order.pred a) = Order.pred (f a)

@[simp]

theorem PrincipalSeg.isSuccPrelimit_apply_iff {α : Type u_1} {β : Type u_2} {a : α} [PartialOrder α] [PartialOrder β] (f : (fun (x1 x2 : α) => x1 < x2) ≺i fun (x1 x2 : β) => x1 < x2) : Order.IsSuccPrelimit (f.toRelEmbedding a) ↔ Order.IsSuccPrelimit a

@[simp]

theorem PrincipalSeg.isSuccLimit_apply_iff {α : Type u_1} {β : Type u_2} {a : α} [PartialOrder α] [PartialOrder β] (f : (fun (x1 x2 : α) => x1 < x2) ≺i fun (x1 x2 : β) => x1 < x2) : Order.IsSuccLimit (f.toRelEmbedding a) ↔ Order.IsSuccLimit a