Mathlib.Order.SuccPred.InitialSeg

InitialSeg.apply_covBy_apply_iff theorem

(f : α ≤i β) : f a ⋖ f b ↔ a ⋖ b

Full source

@[simp]
theorem apply_covBy_apply_iff (f : α ≤i β) : f a ⋖ f bf a ⋖ f b ↔ a ⋖ b :=
  (isLowerSet_range f).ordConnected.apply_covBy_apply_iff f.toOrderEmbedding

Covering Relation is Preserved by Initial Segment Embeddings

Informal description

Let $f : \alpha \to \beta$ be an initial segment embedding between two types $\alpha$ and $\beta$ with well-founded orders. For any elements $a, b \in \alpha$, the images $f(a)$ and $f(b)$ are covering in $\beta$ (denoted $f(a) \lessdot f(b)$) if and only if $a$ and $b$ are covering in $\alpha$ (denoted $a \lessdot b$). Here, $x \lessdot y$ means that $x$ is covered by $y$ in the order, i.e., $x < y$ and there is no element strictly between $x$ and $y$.

InitialSeg.apply_wCovBy_apply_iff theorem

(f : α ≤i β) : f a ⩿ f b ↔ a ⩿ b

Full source

@[simp]
theorem apply_wCovBy_apply_iff (f : α ≤i β) : f a ⩿ f bf a ⩿ f b ↔ a ⩿ b := by
  simp [wcovBy_iff_eq_or_covBy]

Weak covering relation is preserved by initial segment embeddings

Informal description

Let $f : \alpha \to \beta$ be an initial segment embedding between two types $\alpha$ and $\beta$ with well-founded orders. For any elements $a, b \in \alpha$, the images $f(a)$ and $f(b)$ are weakly covering in $\beta$ (denoted $f(a) ⩿ f(b)$) if and only if $a$ and $b$ are weakly covering in $\alpha$ (denoted $a ⩿ b$). Here, $x ⩿ y$ means that $x < y$ and there is no element strictly between $x$ and $y$ in the order.

InitialSeg.map_succ theorem

[SuccOrder α] [NoMaxOrder α] [SuccOrder β] (f : α ≤i β) (a : α) : f (succ a) = succ (f a)

Full source

theorem map_succ [SuccOrder α] [NoMaxOrder α] [SuccOrder β] (f : α ≤i β) (a : α) :
    f (succ a) = succ (f a) :=
  (f.apply_covBy_apply_iff.2 (covBy_succ a)).succ_eq.symm

Initial Segment Embedding Preserves Successor Operation

Informal description

Let $\alpha$ and $\beta$ be ordered types with successor operations, where $\alpha$ has no maximal element. For any initial segment embedding $f : \alpha \to \beta$ and any element $a \in \alpha$, the image of the successor of $a$ under $f$ equals the successor of the image of $a$ under $f$, i.e., $f(\mathrm{succ}(a)) = \mathrm{succ}(f(a))$.

InitialSeg.map_pred theorem

[PredOrder α] [NoMinOrder α] [PredOrder β] (f : α ≤i β) (a : α) : f (pred a) = pred (f a)

Full source

theorem map_pred [PredOrder α] [NoMinOrder α] [PredOrder β] (f : α ≤i β) (a : α) :
    f (pred a) = pred (f a) :=
  (f.apply_covBy_apply_iff.2 (pred_covBy a)).pred_eq.symm

Initial Segment Embedding Preserves Predecessor Operation

Informal description

Let $\alpha$ and $\beta$ be ordered types with predecessor operations, where $\alpha$ has no minimal element. For any initial segment embedding $f : \alpha \leq_i \beta$ and any element $a \in \alpha$, the image of the predecessor of $a$ under $f$ equals the predecessor of the image of $a$ under $f$, i.e., $f(\mathrm{pred}(a)) = \mathrm{pred}(f(a))$.

InitialSeg.isSuccPrelimit_apply_iff theorem

(f : α ≤i β) : IsSuccPrelimit (f a) ↔ IsSuccPrelimit a

Full source

@[simp]
theorem isSuccPrelimit_apply_iff (f : α ≤i β) : IsSuccPrelimitIsSuccPrelimit (f a) ↔ IsSuccPrelimit a := by
  constructor <;> intro h b hb
  · rw [← f.apply_covBy_apply_iff] at hb
    exact h _ hb
  · obtain ⟨c, rfl⟩ := f.mem_range_of_rel hb.lt
    rw [f.apply_covBy_apply_iff] at hb
    exact h _ hb

Initial Segment Embedding Preserves Successor Pre-Limit Property

Informal description

For an initial segment embedding $f : \alpha \leq_i \beta$ between two ordered types $\alpha$ and $\beta$, an element $f(a)$ is a successor pre-limit in $\beta$ if and only if $a$ is a successor pre-limit in $\alpha$. Here, an element $x$ is called a *successor pre-limit* if it is not a successor of any other element in the order.

InitialSeg.isSuccLimit_apply_iff theorem

(f : α ≤i β) : IsSuccLimit (f a) ↔ IsSuccLimit a

Full source

@[simp]
theorem isSuccLimit_apply_iff (f : α ≤i β) : IsSuccLimitIsSuccLimit (f a) ↔ IsSuccLimit a := by
  simp [IsSuccLimit]

Initial Segment Embedding Preserves Successor Limit Property

Informal description

For an initial segment embedding $f : \alpha \leq_i \beta$ between two ordered types $\alpha$ and $\beta$, an element $f(a)$ is a successor limit in $\beta$ if and only if $a$ is a successor limit in $\alpha$.

PrincipalSeg.apply_covBy_apply_iff theorem

(f : α <i β) : f a ⋖ f b ↔ a ⋖ b

Full source

@[simp]
theorem apply_covBy_apply_iff (f : α <i β) : f a ⋖ f bf a ⋖ f b ↔ a ⋖ b :=
  (f : α ≤i β).apply_covBy_apply_iff

Principal Segment Embedding Preserves Covering Relation

Informal description

Let $f : \alpha \to \beta$ be a principal segment embedding between two ordered types $\alpha$ and $\beta$. For any elements $a, b \in \alpha$, the images $f(a)$ and $f(b)$ are covering in $\beta$ (denoted $f(a) \lessdot f(b)$) if and only if $a$ and $b$ are covering in $\alpha$ (denoted $a \lessdot b$). Here, $x \lessdot y$ means that $x < y$ and there is no element strictly between $x$ and $y$ in the order.

PrincipalSeg.apply_wCovBy_apply_iff theorem

(f : α <i β) : f a ⩿ f b ↔ a ⩿ b

Full source

@[simp]
theorem apply_wCovBy_apply_iff (f : α <i β) : f a ⩿ f bf a ⩿ f b ↔ a ⩿ b :=
  (f : α ≤i β).apply_wCovBy_apply_iff

Weak Covering Relation is Preserved by Principal Segment Embeddings

Informal description

Let $f : \alpha \to \beta$ be a principal segment embedding between two ordered types $\alpha$ and $\beta$. For any elements $a, b \in \alpha$, the images $f(a)$ and $f(b)$ are weakly covering in $\beta$ (denoted $f(a) ⩿ f(b)$) if and only if $a$ and $b$ are weakly covering in $\alpha$ (denoted $a ⩿ b$). Here, $x ⩿ y$ means that $x < y$ and there is no element strictly between $x$ and $y$ in the order.

PrincipalSeg.map_succ theorem

[SuccOrder α] [NoMaxOrder α] [SuccOrder β] (f : α <i β) (a : α) : f (succ a) = succ (f a)

Full source

theorem map_succ [SuccOrder α] [NoMaxOrder α] [SuccOrder β] (f : α <i β) (a : α) :
    f (succ a) = succ (f a) :=
  (f : α ≤i β).map_succ a

Principal Segment Embedding Preserves Successor Operation

Informal description

Let $\alpha$ and $\beta$ be ordered types equipped with successor operations, where $\alpha$ has no maximal element. For any principal segment embedding $f : \alpha \to \beta$ and any element $a \in \alpha$, the image of the successor of $a$ under $f$ equals the successor of the image of $a$ under $f$, i.e., $f(\mathrm{succ}(a)) = \mathrm{succ}(f(a))$.

PrincipalSeg.map_pred theorem

[PredOrder α] [NoMinOrder α] [PredOrder β] (f : α ≤i β) (a : α) : f (pred a) = pred (f a)

Full source

theorem map_pred [PredOrder α] [NoMinOrder α] [PredOrder β] (f : α ≤i β) (a : α) :
    f (pred a) = pred (f a) :=
  (f : α ≤i β).map_pred a

Principal Segment Embedding Preserves Predecessor Operation

Informal description

Let $\alpha$ and $\beta$ be ordered types equipped with predecessor operations, where $\alpha$ has no minimal element. For any principal segment embedding $f : \alpha \to \beta$ and any element $a \in \alpha$, the image of the predecessor of $a$ under $f$ equals the predecessor of the image of $a$ under $f$, i.e., $f(\mathrm{pred}(a)) = \mathrm{pred}(f(a))$.

PrincipalSeg.isSuccPrelimit_apply_iff theorem

(f : α <i β) : IsSuccPrelimit (f a) ↔ IsSuccPrelimit a

Full source

@[simp]
theorem isSuccPrelimit_apply_iff (f : α <i β) : IsSuccPrelimitIsSuccPrelimit (f a) ↔ IsSuccPrelimit a :=
  (f : α ≤i β).isSuccPrelimit_apply_iff

Preservation of Successor Pre-Limit Property under Principal Segment Embeddings

Informal description

For a principal segment embedding $f : \alpha <_i \beta$ between two ordered types $\alpha$ and $\beta$, an element $f(a)$ is a successor pre-limit in $\beta$ if and only if $a$ is a successor pre-limit in $\alpha$. Here, an element $x$ is called a *successor pre-limit* if it is not a successor of any other element in the order.

PrincipalSeg.isSuccLimit_apply_iff theorem

(f : α <i β) : IsSuccLimit (f a) ↔ IsSuccLimit a

Full source

@[simp]
theorem isSuccLimit_apply_iff (f : α <i β) : IsSuccLimitIsSuccLimit (f a) ↔ IsSuccLimit a :=
  (f : α ≤i β).isSuccLimit_apply_iff

Principal Segment Embedding Preserves Successor Limit Property

Informal description

For a principal segment embedding $f : \alpha <_i \beta$ between two ordered types $\alpha$ and $\beta$, an element $f(a)$ is a successor limit in $\beta$ if and only if $a$ is a successor limit in $\alpha$.