class Poset (α : Type u_1) : Type u_1

• le : α → α → Prop
• le_refl (x : α) : le x x
• le_trans {x y z : α} : le x y → le y z → le x z
• le_antisym {x y : α} : le x y → le y x → x = y

def «term_≤[_]_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def monotone {L : Type u_1} {M : Type u_2} [Poset L] [Poset M] (f : L → M) : Prop

Equations

• monotone f = ∀ (x y : L), Poset.le x y → Poset.le (f x) (f y)

def dual_poset (L : Type u_1) [Poset L] : Poset L

Equations

• dual_poset L = { le := fun (x y : L) => Poset.le y x, le_refl := ⋯, le_trans := ⋯, le_antisym := ⋯ }