Mappings between UpwardEnumerable types

In this file we build machinery for pulling back lawfulness properties for UpwardEnumerable along injective functions that commute with the relevant operations.

structure Std.PRange.UpwardEnumerable.Map (α : Type u) (β : Type v) [UpwardEnumerable α] [UpwardEnumerable β] : Type (max u v)

An injective mapping between two types implementing UpwardEnumerable that commutes with succ? and succMany?.

Having such a mapping means that all of the Prop-valued lawfulness classes around UpwardEnumerable can be pulled back.

• toFun : α → β
• injective : Function.Injective self.toFun
• succ?_toFun (a : α) : succ? (self.toFun a) = Option.map self.toFun (succ? a)
• succMany?_toFun (n : Nat) (a : α) : succMany? n (self.toFun a) = Option.map self.toFun (succMany? n a)

theorem Std.PRange.UpwardEnumerable.Map.succ?_eq_none_iff {α : Type u_1} {β : Type u_2} [UpwardEnumerable α] [UpwardEnumerable β] (f : Map α β) {a : α} : succ? a = none ↔ succ? (f.toFun a) = none

theorem Std.PRange.UpwardEnumerable.Map.succ?_eq_some_iff {α : Type u_1} {β : Type u_2} [UpwardEnumerable α] [UpwardEnumerable β] (f : Map α β) {a b : α} : succ? a = some b ↔ succ? (f.toFun a) = some (f.toFun b)

theorem Std.PRange.UpwardEnumerable.Map.le_iff {α : Type u_1} {β : Type u_2} [UpwardEnumerable α] [UpwardEnumerable β] (f : Map α β) {a b : α} : UpwardEnumerable.LE a b ↔ UpwardEnumerable.LE (f.toFun a) (f.toFun b)

theorem Std.PRange.UpwardEnumerable.Map.lt_iff {α : Type u_1} {β : Type u_2} [UpwardEnumerable α] [UpwardEnumerable β] (f : Map α β) {a b : α} : UpwardEnumerable.LT a b ↔ UpwardEnumerable.LT (f.toFun a) (f.toFun b)

theorem Std.PRange.UpwardEnumerable.Map.succ?_toFun' {α : Type u_1} {β : Type u_2} [UpwardEnumerable α] [UpwardEnumerable β] (f : Map α β) : succ? ∘ f.toFun = Option.map f.toFun ∘ succ?

class Std.PRange.UpwardEnumerable.Map.PreservesLE {α : Type u_1} {β : Type u_2} [UpwardEnumerable α] [UpwardEnumerable β] [LE α] [LE β] (f : Map α β) : Prop

Compatibility class for Map and ≤.

• le_iff {a b : α} : a ≤ b ↔ f.toFun a ≤ f.toFun b

class Std.PRange.UpwardEnumerable.Map.PreservesLT {α : Type u_1} {β : Type u_2} [UpwardEnumerable α] [UpwardEnumerable β] [LT α] [LT β] (f : Map α β) : Prop

Compatibility class for Map and <.

• lt_iff {a b : α} : a < b ↔ f.toFun a < f.toFun b

class Std.PRange.UpwardEnumerable.Map.PreservesRxcSize {α : Type u_1} {β : Type u_2} [UpwardEnumerable α] [UpwardEnumerable β] [Rxc.HasSize α] [Rxc.HasSize β] (f : Map α β) : Prop

Compatibility class for Map and Rxc.HasSize.

• size_eq {a b : α} : Rxc.HasSize.size a b = Rxc.HasSize.size (f.toFun a) (f.toFun b)

class Std.PRange.UpwardEnumerable.Map.PreservesRxoSize {α : Type u_1} {β : Type u_2} [UpwardEnumerable α] [UpwardEnumerable β] [Rxo.HasSize α] [Rxo.HasSize β] (f : Map α β) : Prop

Compatibility class for Map and Rxo.HasSize.

• size_eq {a b : α} : Rxo.HasSize.size a b = Rxo.HasSize.size (f.toFun a) (f.toFun b)

class Std.PRange.UpwardEnumerable.Map.PreservesRxiSize {α : Type u_1} {β : Type u_2} [UpwardEnumerable α] [UpwardEnumerable β] [Rxi.HasSize α] [Rxi.HasSize β] (f : Map α β) : Prop

Compatibility class for Map and Rxi.HasSize.

• size_eq {b : α} : Rxi.HasSize.size b = Rxi.HasSize.size (f.toFun b)

class Std.PRange.UpwardEnumerable.Map.PreservesLeast? {α : Type u_1} {β : Type u_2} [UpwardEnumerable α] [UpwardEnumerable β] [Least? α] [Least? β] (f : Map α β) : Prop

Compatibility class for Map and Least?.

• map_least? : Option.map f.toFun least? = least?

theorem Std.PRange.LawfulUpwardEnumerable.ofMap {α : Type u_2} {β : Type u_1} [UpwardEnumerable α] [UpwardEnumerable β] [LawfulUpwardEnumerable β] (f : UpwardEnumerable.Map α β) : LawfulUpwardEnumerable α

instance Std.PRange.instPreservesLTOfLawfulOrderLTOfPreservesLE {α : Type u_1} {β : Type u_2} [UpwardEnumerable α] [UpwardEnumerable β] [LE α] [LT α] [LawfulOrderLT α] [LE β] [LT β] [LawfulOrderLT β] (f : UpwardEnumerable.Map α β) [f.PreservesLE] : f.PreservesLT

theorem Std.PRange.LawfulUpwardEnumerableLE.ofMap {α : Type u_1} {β : Type u_2} [UpwardEnumerable α] [UpwardEnumerable β] [LE α] [LE β] [LawfulUpwardEnumerableLE β] (f : UpwardEnumerable.Map α β) [f.PreservesLE] : LawfulUpwardEnumerableLE α

theorem Std.PRange.LawfulUpwardEnumerableLT.ofMap {α : Type u_1} {β : Type u_2} [UpwardEnumerable α] [UpwardEnumerable β] [LT α] [LT β] [LawfulUpwardEnumerableLT β] (f : UpwardEnumerable.Map α β) [f.PreservesLT] : LawfulUpwardEnumerableLT α

theorem Std.PRange.LawfulUpwardEnumerableLeast?.ofMap {α : Type u_1} {β : Type u_2} [UpwardEnumerable α] [UpwardEnumerable β] [Least? α] [Least? β] [LawfulUpwardEnumerableLeast? β] (f : UpwardEnumerable.Map α β) [f.PreservesLeast?] : LawfulUpwardEnumerableLeast? α

theorem Std.Rxc.LawfulHasSize.ofMap {α : Type u_1} {β : Type u_2} [PRange.UpwardEnumerable α] [PRange.UpwardEnumerable β] [LE α] [LE β] [HasSize α] [HasSize β] [LawfulHasSize β] (f : PRange.UpwardEnumerable.Map α β) [f.PreservesLE] [f.PreservesRxcSize] : LawfulHasSize α

theorem Std.Rxo.LawfulHasSize.ofMap {α : Type u_1} {β : Type u_2} [PRange.UpwardEnumerable α] [PRange.UpwardEnumerable β] [LT α] [LT β] [HasSize α] [HasSize β] [LawfulHasSize β] (f : PRange.UpwardEnumerable.Map α β) [f.PreservesLT] [f.PreservesRxoSize] : LawfulHasSize α

theorem Std.Rxi.LawfulHasSize.ofMap {α : Type u_1} {β : Type u_2} [PRange.UpwardEnumerable α] [PRange.UpwardEnumerable β] [HasSize α] [HasSize β] [LawfulHasSize β] (f : PRange.UpwardEnumerable.Map α β) [f.PreservesRxiSize] : LawfulHasSize α

theorem Std.Rxc.IsAlwaysFinite.ofMap {α : Type u_1} {β : Type u_2} [PRange.UpwardEnumerable α] [PRange.UpwardEnumerable β] [LE α] [LE β] [IsAlwaysFinite β] (f : PRange.UpwardEnumerable.Map α β) [f.PreservesLE] : IsAlwaysFinite α

theorem Std.Rxo.IsAlwaysFinite.ofMap {α : Type u_1} {β : Type u_2} [PRange.UpwardEnumerable α] [PRange.UpwardEnumerable β] [LT α] [LT β] [IsAlwaysFinite β] (f : PRange.UpwardEnumerable.Map α β) [f.PreservesLT] : IsAlwaysFinite α

theorem Std.Rxi.IsAlwaysFinite.ofMap {α : Type u_2} {β : Type u_1} [PRange.UpwardEnumerable α] [PRange.UpwardEnumerable β] [IsAlwaysFinite β] (f : PRange.UpwardEnumerable.Map α β) : IsAlwaysFinite α