instance instLEQuotCurry_bourbakiLean2 {α : Type u_1} {r : Relation α α} [LE α] : LE (Quot (Function.curry r))

Equations

• instLEQuotCurry_bourbakiLean2 = { le := fun (a b : Quot (Function.curry r)) => ∀ (x : α), Quot.mk (Function.curry r) x = a → ∃ (y : α), Quot.mk (Function.curry r) y = b ∧ x ≤ y }

instance instPreorderQuotCurryOfIsEquivalence {α : Type u_3} {r : Relation α α} [r.IsEquivalence] [Preorder α] : Preorder (Quot (Function.curry r))

Equations

• instPreorderQuotCurryOfIsEquivalence = Preorder.mk ⋯ ⋯ ⋯

theorem Quot.monotone_of_comp_monotone {α : Type u_1} {β : Type u_2} {r : Relation α α} [LE α] [LE β] {g : Quot (Function.curry r) → β} (h : Monotone (g ∘ Quot.mk (Function.curry r))) : Monotone g

theorem Quot.mk_monotone_iff {α : Type u_1} {r : Relation α α} [Preorder α] : Monotone (Quot.mk (Function.curry r)) ↔ ∀ (x x' y : α), x ≤ y → Quot.mk (Function.curry r) x' = Quot.mk (Function.curry r) x → ∃ (y' : α), Quot.mk (Function.curry r) y' = Quot.mk (Function.curry r) y ∧ x' ≤ y'

def WeaklyOrderCompatible {α : Type u_1} [Preorder α] (r : Relation α α) : Prop

Equations

• WeaklyOrderCompatible r = Monotone (Quot.mk (Function.curry r))

theorem weaklyOrderCompatible_product_collapse {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] : WeaklyOrderCompatible (Function.identified_under Prod.fst)

theorem prod_quotient_order_iso {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {b : β} : IsOrderIso fun (x : α) => Quot.mk (Function.curry (Function.identified_under Prod.fst)) (x, b)

instance Quot.partialOrder_of {α : Type u_1} {r : Relation α α} [PartialOrder α] [r.IsEquivalence] (h' : ∀ (x y z : α), x ≤ y → y ≤ z → Quot.mk (Function.curry r) x = Quot.mk (Function.curry r) z → Quot.mk (Function.curry r) x = Quot.mk (Function.curry r) y) : PartialOrder (Quot (Function.curry r))

Equations

• Quot.partialOrder_of h' = PartialOrder.mk ⋯

theorem Monotone.partialOrder_condition_quot {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [PartialOrder β] (h : Monotone f) {x y z : α} (xy : x ≤ y) (yz : y ≤ z) (eq : Quot.mk (Function.curry (Function.identified_under f)) x = Quot.mk (Function.curry (Function.identified_under f)) z) : Quot.mk (Function.curry (Function.identified_under f)) x = Quot.mk (Function.curry (Function.identified_under f)) y

theorem Monotone.identifiedUnder_weaklyOrderCompatible_iff {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] (h : Monotone f) : WeaklyOrderCompatible (Function.identified_under f) ↔ ∀ (x x' y : α), x ≤ y → f x' = f x → ∃ (y' : α), f y' = f y ∧ x' ≤ y'