From c120b0fbc9c7a9ac79aec390e0b0212456d583e5 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 7 Aug 2024 07:08:02 +0000 Subject: [PATCH] feat(RelSeries): {head,last}_map (#15387) from the Carleson project --- Mathlib/Order/RelSeries.lean | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/Mathlib/Order/RelSeries.lean b/Mathlib/Order/RelSeries.lean index 45f5e2f12ec4c..802ccaa4fc078 100644 --- a/Mathlib/Order/RelSeries.lean +++ b/Mathlib/Order/RelSeries.lean @@ -305,6 +305,10 @@ def map (p : RelSeries r) (f : r →r s) : RelSeries s where @[simp] lemma map_apply (p : RelSeries r) (f : r →r s) (i : Fin (p.length + 1)) : p.map f i = f (p i) := rfl +@[simp] lemma head_map (p : RelSeries r) (f : r →r s) : (p.map f).head = f p.head := rfl + +@[simp] lemma last_map (p : RelSeries r) (f : r →r s) : (p.map f).last = f p.last := rfl + /-- If `a₀ -r→ a₁ -r→ ... -r→ aₙ` is an `r`-series and `a` is such that `aᵢ -r→ a -r→ a_ᵢ₊₁`, then @@ -638,6 +642,12 @@ can be pushed out to a strict chain of `β` by def map (p : LTSeries α) (f : α → β) (hf : StrictMono f) : LTSeries β := LTSeries.mk p.length (f.comp p) (hf.comp p.strictMono) +@[simp] lemma head_map (p : LTSeries α) (f : α → β) (hf : StrictMono f) : + (p.map f hf).head = f p.head := rfl + +@[simp] lemma last_map (p : LTSeries α) (f : α → β) (hf : StrictMono f) : + (p.map f hf).last = f p.last := rfl + /-- For two preorders `α, β`, if `f : α → β` is surjective and strictly comonotonic, then a strict series of `β` can be pulled back to a strict chain of `α` by