Documentation

Mathlib.Order.SuccPred.InitialSeg

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 : (fun (x1 x2 : α) => x1 < x2) ≼i 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 : (fun (x1 x2 : α) => x1 < x2) ≼i 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 : (fun (x1 x2 : α) => x1 < x2) ≼i 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 : (fun (x1 x2 : α) => x1 < x2) ≼i 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 : (fun (x1 x2 : α) => x1 < x2) ≼i 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 : (fun (x1 x2 : α) => x1 < x2) ≼i fun (x1 x2 : β) => x1 < x2) :
Order.IsSuccLimit (f a) ↔ Order.IsSuccLimit a
source
@[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
source
@[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
source
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)
source
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)
source
@[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
source
@[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