LeanPool.QuasiBorelSpaces.Option.Instances

Imported Lean Pool material for LeanPool.QuasiBorelSpaces.Option.Instances.

@[implicit_reducible]

instance Option.instPreorderLeanPool {A : Type u_1} [Preorder A] : Preorder (Option A)

Equations

• Option.instPreorderLeanPool = { toLE := instLEOption, toLT := instLTOption, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

@[implicit_reducible]

instance Option.instPartialOrderLeanPool {A : Type u_1} [PartialOrder A] : PartialOrder (Option A)

Bottom-order on options: none is bottom, some is ordered pointwise.

Equations

• Option.instPartialOrderLeanPool = { toPreorder := Option.instPreorderLeanPool, le_antisymm := ⋯ }

@[implicit_reducible]

instance Option.instOrderBotLeanPool {A : Type u_1} [LE A] : OrderBot (Option A)

Equations

• Option.instOrderBotLeanPool = { bot := none, bot_le := ⋯ }