def Equiv.le {α : Type u} {β : Type v} (e : α ≃ β) [LE β] : LE α

Equations

• e.le = { le := InvImage (fun (x1 x2 : β) => x1 ≤ x2) ⇑e }

theorem Equiv.le_def {α : Type u} {β : Type v} (e : α ≃ β) [LE β] (x y : α) : x ≤ y ↔ e x ≤ e y

def Equiv.lt {α : Type u} {β : Type v} (e : α ≃ β) [LT β] : LT α

Equations

• e.lt = { lt := InvImage (fun (x1 x2 : β) => x1 < x2) ⇑e }

theorem Equiv.lt_def {α : Type u} {β : Type v} (e : α ≃ β) [LT β] (x y : α) : x < y ↔ e x < e y

def Equiv.min {α : Type u} {β : Type v} (e : α ≃ β) [Min β] : Min α

Equations

• e.min = { min := fun (x y : α) => e.symm (e x ⊓ e y) }

theorem Equiv.min_def {α : Type u} {β : Type v} (e : α ≃ β) [Min β] (x y : α) : x ⊓ y = e.symm (e x ⊓ e y)

theorem Equiv.apply_min {α : Type u} {β : Type v} (e : α ≃ β) [Min β] (x y : α) : e (x ⊓ y) = e x ⊓ e y

def Equiv.max {α : Type u} {β : Type v} (e : α ≃ β) [Max β] : Max α

Equations

• e.max = { max := fun (x y : α) => e.symm (e x ⊔ e y) }

theorem Equiv.max_def {α : Type u} {β : Type v} (e : α ≃ β) [Max β] (x y : α) : x ⊔ y = e.symm (e x ⊔ e y)

theorem Equiv.apply_max {α : Type u} {β : Type v} (e : α ≃ β) [Max β] (x y : α) : e (x ⊔ y) = e x ⊔ e y

def Equiv.compare {α : Type u} {β : Type v} (e : α ≃ β) [Ord β] : Ord α

Equations

• e.compare = { compare := fun (x y : α) => compare (e x) (e y) }

theorem Equiv.compare_def {α : Type u} {β : Type v} (e : α ≃ β) [Ord β] (x y : α) : compare x y = compare (e x) (e y)

def Equiv.decidableLE {α : Type u} {β : Type v} (e : α ≃ β) [LE β] [DecidableRel fun (x1 x2 : β) => x1 ≤ x2] : DecidableRel fun (x1 x2 : α) => x1 ≤ x2

Equations

• e.decidableLE x y = inferInstanceAs (Decidable (e x ≤ e y))

def Equiv.decidableLT {α : Type u} {β : Type v} (e : α ≃ β) [LT β] [DecidableRel fun (x1 x2 : β) => x1 < x2] : DecidableRel fun (x1 x2 : α) => x1 < x2

Equations

• e.decidableLT x y = inferInstanceAs (Decidable (e x < e y))

def Equiv.leIso {α : Type u} {β : Type v} (e : α ≃ β) [LE β] : (fun (x1 x2 : α) => x1 ≤ x2) ≃r fun (x1 x2 : β) => x1 ≤ x2

Equations

• e.leIso = { toEquiv := e, map_rel_iff' := ⋯ }

def Equiv.orderIso {α : Type u} {β : Type v} (e : α ≃ β) [LE β] : α ≃o β

Equations

• e.orderIso = e.leIso

def Equiv.ltIso {α : Type u} {β : Type v} (e : α ≃ β) [LT β] : (fun (x1 x2 : α) => x1 < x2) ≃r fun (x1 x2 : β) => x1 < x2

Equations

• e.ltIso = { toEquiv := e, map_rel_iff' := ⋯ }

def Equiv.preorder {α : Type u} {β : Type v} (e : α ≃ β) [Preorder β] : Preorder α

Equations

• e.preorder = Preorder.lift ⇑e

def Equiv.partialOrder {α : Type u} {β : Type v} (e : α ≃ β) [PartialOrder β] : PartialOrder α

Equations

• e.partialOrder = PartialOrder.lift ⇑e ⋯

def Equiv.linearOrder {α : Type u} {β : Type v} (e : α ≃ β) [LinearOrder β] : LinearOrder α

Equations

• e.linearOrder = LinearOrder.liftWithOrd ⇑e ⋯ ⋯ ⋯ ⋯

def Equiv.ltWellOrder {α : Type u} {β : Type v} (e : α ≃ β) [LtWellOrder β] : LtWellOrder α

Equations

• e.ltWellOrder = LtWellOrder.mk

theorem Equiv.ltWellOrder_type {α : Type u} {β : Type v} (e : α ≃ β) [LtWellOrder β] : Ordinal.lift.{max u v, u} (Ordinal.type fun (x1 x2 : α) => x1 < x2) = Ordinal.lift.{max u v, v} (Ordinal.type fun (x1 x2 : β) => x1 < x2)

theorem Equiv.ltWellOrder_typein {α : Type u} {β : Type v} (e : α ≃ β) [i : LtWellOrder β] (x : α) : Ordinal.lift.{max u v, v} ((Ordinal.typein fun (x1 x2 : β) => x1 < x2).toRelEmbedding (e x)) = Ordinal.lift.{max u v, u} ((Ordinal.typein fun (x1 x2 : α) => x1 < x2).toRelEmbedding x)

theorem Equiv.noMaxOrder {α : Type u} {β : Type v} (e : α ≃ β) [LT β] [NoMaxOrder β] : NoMaxOrder α

def Equiv.ofNat {α : Type u} {β : Type v} (e : α ≃ β) (n : ℕ) [OfNat β n] : OfNat α n

Equations

• e.ofNat n = { ofNat := e.symm (OfNat.ofNat n) }

theorem Equiv.apply_add {α : Type u} {β : Type v} (e : α ≃ β) [Add β] (x y : α) : e (x + y) = e x + e y

theorem Equiv.apply_sub {α : Type u} {β : Type v} (e : α ≃ β) [Sub β] (x y : α) : e (x - y) = e x - e y

theorem Equiv.apply_zero {α : Type u} {β : Type v} (e : α ≃ β) [Zero β] : e 0 = 0