Documentation

Mathlib.Order.WithBot

WithBot, WithTop #

Adding a bot or a top to an order.

Main declarations #

def WithBot (α : Type u_1) :
Type u_1

Attach to a type.

Equations
instance WithBot.instReprWithBot {α : Type u_1} [inst : Repr α] :
Equations
@[match_pattern]
def WithBot.some {α : Type u_1} :
αWithBot α

The canonical map from α into WithBot α

Equations
  • WithBot.some = some
instance WithBot.coeTC {α : Type u_1} :
CoeTC α (WithBot α)
Equations
  • WithBot.coeTC = { coe := WithBot.some }
instance WithBot.bot {α : Type u_1} :
Equations
  • WithBot.bot = { bot := none }
instance WithBot.inhabited {α : Type u_1} :
Equations
  • WithBot.inhabited = { default := }
theorem WithBot.coe_injective {α : Type u_1} :
Function.Injective fun a => a
@[simp]
theorem WithBot.coe_inj {α : Type u_1} {a : α} {b : α} :
a = b a = b
theorem WithBot.forall {α : Type u_1} {p : WithBot αProp} :
((x : WithBot α) → p x) p ((x : α) → p x)
theorem WithBot.exists {α : Type u_1} {p : WithBot αProp} :
(x, p x) p x, p x
theorem WithBot.none_eq_bot {α : Type u_1} :
none =
theorem WithBot.some_eq_coe {α : Type u_1} (a : α) :
some a = a
@[simp]
theorem WithBot.bot_ne_coe {α : Type u_1} {a : α} :
a
@[simp]
theorem WithBot.coe_ne_bot {α : Type u_1} {a : α} :
a
def WithBot.recBotCoe {α : Type u_1} {C : WithBot αSort u_2} (bot : C ) (coe : (a : α) → C a) (n : WithBot α) :
C n

Recursor for WithBot using the preferred forms and ↑a.

Equations
@[simp]
theorem WithBot.recBotCoe_bot {α : Type u_1} {C : WithBot αSort u_2} (d : C ) (f : (a : α) → C a) :
@[simp]
theorem WithBot.recBotCoe_coe {α : Type u_1} {C : WithBot αSort u_2} (d : C ) (f : (a : α) → C a) (x : α) :
WithBot.recBotCoe d f x = f x
def WithBot.unbot' {α : Type u_1} (d : α) (x : WithBot α) :
α

Specialization of Option.get_or_else to values in WithBot α that respects API boundaries.

Equations
@[simp]
theorem WithBot.unbot'_bot {α : Type u_1} (d : α) :
@[simp]
theorem WithBot.unbot'_coe {α : Type u_1} (d : α) (x : α) :
WithBot.unbot' d x = x
theorem WithBot.coe_eq_coe {α : Type u_1} {a : α} {b : α} :
a = b a = b
theorem WithBot.unbot'_eq_iff {α : Type u_1} {d : α} {y : α} {x : WithBot α} :
WithBot.unbot' d x = y x = y x = y = d
@[simp]
theorem WithBot.unbot'_eq_self_iff {α : Type u_1} {d : α} {x : WithBot α} :
WithBot.unbot' d x = d x = d x =
theorem WithBot.unbot'_eq_unbot'_iff {α : Type u_1} {d : α} {x : WithBot α} {y : WithBot α} :
WithBot.unbot' d x = WithBot.unbot' d y x = y x = d y = x = y = d
def WithBot.map {α : Type u_1} {β : Type u_2} (f : αβ) :
WithBot αWithBot β

Lift a map f : α → β to WithBot α → WithBot β. Implemented using Option.map.

Equations
@[simp]
theorem WithBot.map_bot {α : Type u_2} {β : Type u_1} (f : αβ) :
@[simp]
theorem WithBot.map_coe {α : Type u_2} {β : Type u_1} (f : αβ) (a : α) :
WithBot.map f a = ↑(f a)
theorem WithBot.map_comm {α : Type u_1} {β : Type u_3} {γ : Type u_4} {δ : Type u_2} {f₁ : αβ} {f₂ : αγ} {g₁ : βδ} {g₂ : γδ} (h : g₁ f₁ = g₂ f₂) (a : α) :
WithBot.map g₁ (WithBot.map f₁ a) = WithBot.map g₂ (WithBot.map f₂ a)
theorem WithBot.ne_bot_iff_exists {α : Type u_1} {x : WithBot α} :
x a, a = x
def WithBot.unbot {α : Type u_1} (x : WithBot α) :
x α

Deconstruct a x : WithBot α to the underlying value in α, given a proof that x ≠ ⊥.

Equations
@[simp]
theorem WithBot.coe_unbot {α : Type u_1} (x : WithBot α) (h : x ) :
↑(WithBot.unbot x h) = x
@[simp]
theorem WithBot.unbot_coe {α : Type u_1} (x : α) (h : optParam (x ) (_ : x )) :
WithBot.unbot (x) h = x
instance WithBot.canLift {α : Type u_1} :
CanLift (WithBot α) α WithBot.some fun r => r
Equations
  • WithBot.canLift = { prf := (_ : ∀ (x : WithBot α), x y, y = x) }
instance WithBot.le {α : Type u_1} [inst : LE α] :
LE (WithBot α)
Equations
  • WithBot.le = { le := fun o₁ o₂ => ∀ (a : α), a o₁b, b o₂ a b }
@[simp]
theorem WithBot.some_le_some {α : Type u_1} {a : α} {b : α} [inst : LE α] :
some a some b a b
@[simp]
theorem WithBot.coe_le_coe {α : Type u_1} {a : α} {b : α} [inst : LE α] :
a b a b
@[simp]
theorem WithBot.none_le {α : Type u_1} [inst : LE α] {a : WithBot α} :
none a
instance WithBot.orderBot {α : Type u_1} [inst : LE α] :
Equations
instance WithBot.orderTop {α : Type u_1} [inst : LE α] [inst : OrderTop α] :
Equations
instance WithBot.instBoundedOrderWithBotLe {α : Type u_1} [inst : LE α] [inst : OrderTop α] :
Equations
  • WithBot.instBoundedOrderWithBotLe = let src := WithBot.orderBot; let src_1 := WithBot.orderTop; BoundedOrder.mk
theorem WithBot.not_coe_le_bot {α : Type u_1} [inst : LE α] (a : α) :
¬a
theorem WithBot.coe_le {α : Type u_1} {a : α} {b : α} [inst : LE α] {o : Option α} :
b o → (a o a b)
theorem WithBot.coe_le_iff {α : Type u_1} {a : α} [inst : LE α] {x : WithBot α} :
a x b, x = b a b
theorem WithBot.le_coe_iff {α : Type u_1} {b : α} [inst : LE α] {x : WithBot α} :
x b ∀ (a : α), x = aa b
theorem IsMax.withBot {α : Type u_1} {a : α} [inst : LE α] (h : IsMax a) :
IsMax a
instance WithBot.lt {α : Type u_1} [inst : LT α] :
LT (WithBot α)
Equations
  • WithBot.lt = { lt := fun o₁ o₂ => b, b o₂ ∀ (a : α), a o₁a < b }
@[simp]
theorem WithBot.some_lt_some {α : Type u_1} {a : α} {b : α} [inst : LT α] :
some a < some b a < b
@[simp]
theorem WithBot.coe_lt_coe {α : Type u_1} {a : α} {b : α} [inst : LT α] :
a < b a < b
@[simp]
theorem WithBot.none_lt_some {α : Type u_1} [inst : LT α] (a : α) :
none < a
theorem WithBot.bot_lt_coe {α : Type u_1} [inst : LT α] (a : α) :
< a
@[simp]
theorem WithBot.not_lt_none {α : Type u_1} [inst : LT α] (a : WithBot α) :
¬a < none
theorem WithBot.lt_iff_exists_coe {α : Type u_1} [inst : LT α] {a : WithBot α} {b : WithBot α} :
a < b p, b = p a < p
theorem WithBot.lt_coe_iff {α : Type u_1} {b : α} [inst : LT α] {x : WithBot α} :
x < b ∀ (a : WithBot α), x = aa < b
theorem WithBot.bot_lt_iff_ne_bot {α : Type u_1} [inst : LT α] {x : WithBot α} :

A version of bot_lt_iff_ne_bot for WithBot that only requires LT α, not PartialOrder α.

instance WithBot.preorder {α : Type u_1} [inst : Preorder α] :
Equations
instance WithBot.partialOrder {α : Type u_1} [inst : PartialOrder α] :
Equations
  • WithBot.partialOrder = let src := WithBot.preorder; PartialOrder.mk (_ : ∀ (o₁ o₂ : WithBot α), o₁ o₂o₂ o₁o₁ = o₂)
theorem WithBot.coe_strictMono {α : Type u_1} [inst : Preorder α] :
StrictMono fun a => a
theorem WithBot.coe_mono {α : Type u_1} [inst : Preorder α] :
Monotone fun a => a
theorem WithBot.monotone_iff {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {f : WithBot αβ} :
Monotone f (Monotone fun a => f a) ∀ (x : α), f f x
@[simp]
theorem WithBot.monotone_map_iff {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {f : αβ} :
theorem Monotone.withBot_map {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {f : αβ} :

Alias of the reverse direction of WithBot.monotone_map_iff.

theorem WithBot.strictMono_iff {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {f : WithBot αβ} :
StrictMono f (StrictMono fun a => f a) ∀ (x : α), f < f x
theorem WithBot.strictAnti_iff {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {f : WithBot αβ} :
StrictAnti f (StrictAnti fun a => f a) ∀ (x : α), f x < f
@[simp]
theorem WithBot.strictMono_map_iff {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {f : αβ} :
theorem StrictMono.withBot_map {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {f : αβ} :

Alias of the reverse direction of WithBot.strictMono_map_iff.

theorem WithBot.map_le_iff {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] (f : αβ) (mono_iff : ∀ {a b : α}, f a f b a b) (a : WithBot α) (b : WithBot α) :
theorem WithBot.le_coe_unbot' {α : Type u_1} [inst : Preorder α] (a : WithBot α) (b : α) :
a ↑(WithBot.unbot' b a)
theorem WithBot.unbot'_bot_le_iff {α : Type u_1} [inst : LE α] [inst : OrderBot α] {a : WithBot α} {b : α} :
theorem WithBot.unbot'_lt_iff {α : Type u_1} [inst : LT α] {a : WithBot α} {b : α} {c : α} (ha : a ) :
WithBot.unbot' b a < c a < c
instance WithBot.semilatticeSup {α : Type u_1} [inst : SemilatticeSup α] :
Equations
  • One or more equations did not get rendered due to their size.
theorem WithBot.coe_sup {α : Type u_1} [inst : SemilatticeSup α] (a : α) (b : α) :
↑(a b) = a b
instance WithBot.semilatticeInf {α : Type u_1} [inst : SemilatticeInf α] :
Equations
  • One or more equations did not get rendered due to their size.
theorem WithBot.coe_inf {α : Type u_1} [inst : SemilatticeInf α] (a : α) (b : α) :
↑(a b) = a b
instance WithBot.lattice {α : Type u_1} [inst : Lattice α] :
Equations
  • One or more equations did not get rendered due to their size.
instance WithBot.distribLattice {α : Type u_1} [inst : DistribLattice α] :
Equations
instance WithBot.decidableLE {α : Type u_1} [inst : LE α] [inst : DecidableRel fun x x_1 => x x_1] :
DecidableRel fun x x_1 => x x_1
Equations
  • One or more equations did not get rendered due to their size.
instance WithBot.decidableLT {α : Type u_1} [inst : LT α] [inst : DecidableRel fun x x_1 => x < x_1] :
DecidableRel fun x x_1 => x < x_1
Equations
  • One or more equations did not get rendered due to their size.
instance WithBot.isTotal_le {α : Type u_1} [inst : LE α] [inst : IsTotal α fun x x_1 => x x_1] :
IsTotal (WithBot α) fun x x_1 => x x_1
Equations
instance WithBot.linearOrder {α : Type u_1} [inst : LinearOrder α] :
Equations
@[simp]
theorem WithBot.coe_min {α : Type u_1} [inst : LinearOrder α] (x : α) (y : α) :
↑(min x y) = min x y
@[simp]
theorem WithBot.coe_max {α : Type u_1} [inst : LinearOrder α] (x : α) (y : α) :
↑(max x y) = max x y
theorem WithBot.wellFounded_lt {α : Type u_1} [inst : Preorder α] (h : WellFounded fun x x_1 => x < x_1) :
WellFounded fun x x_1 => x < x_1
theorem WithBot.lt_iff_exists_coe_btwn {α : Type u_1} [inst : Preorder α] [inst : DenselyOrdered α] [inst : NoMinOrder α] {a : WithBot α} {b : WithBot α} :
a < b x, a < x x < b
instance WithBot.noTopOrder {α : Type u_1} [inst : LE α] [inst : NoTopOrder α] [inst : Nonempty α] :
Equations
instance WithBot.noMaxOrder {α : Type u_1} [inst : LT α] [inst : NoMaxOrder α] [inst : Nonempty α] :
Equations
def WithTop (α : Type u_1) :
Type u_1

Attach to a type.

Equations
instance WithTop.instReprWithTop {α : Type u_1} [inst : Repr α] :
Equations
@[match_pattern]
def WithTop.some {α : Type u_1} :
αWithTop α

The canonical map from α into WithTop α

Equations
  • WithTop.some = some
instance WithTop.coeTC {α : Type u_1} :
CoeTC α (WithTop α)
Equations
  • WithTop.coeTC = { coe := WithTop.some }
instance WithTop.top {α : Type u_1} :
Equations
  • WithTop.top = { top := none }
instance WithTop.inhabited {α : Type u_1} :
Equations
  • WithTop.inhabited = { default := }
theorem WithTop.forall {α : Type u_1} {p : WithTop αProp} :
((x : WithTop α) → p x) p ((x : α) → p x)
theorem WithTop.exists {α : Type u_1} {p : WithTop αProp} :
(x, p x) p x, p x
theorem WithTop.none_eq_top {α : Type u_1} :
none =
theorem WithTop.some_eq_coe {α : Type u_1} (a : α) :
some a = a
@[simp]
theorem WithTop.top_ne_coe {α : Type u_1} {a : α} :
a
@[simp]
theorem WithTop.coe_ne_top {α : Type u_1} {a : α} :
a
def WithTop.recTopCoe {α : Type u_1} {C : WithTop αSort u_2} (top : C ) (coe : (a : α) → C a) (n : WithTop α) :
C n

Recursor for WithTop using the preferred forms and ↑a.

Equations
@[simp]
theorem WithTop.recTopCoe_top {α : Type u_1} {C : WithTop αSort u_2} (d : C ) (f : (a : α) → C a) :
@[simp]
theorem WithTop.recTopCoe_coe {α : Type u_1} {C : WithTop αSort u_2} (d : C ) (f : (a : α) → C a) (x : α) :
WithTop.recTopCoe d f x = f x

WithTop.toDual is the equivalence sending to and any a : α to toDual a : αᵒᵈ. See WithTop.toDualBotEquiv for the related order-iso.

Equations

WithTop.ofDual is the equivalence sending to and any a : αᵒᵈ to ofDual a : α. See WithTop.toDualBotEquiv for the related order-iso.

Equations

WithBot.toDual is the equivalence sending to and any a : α to toDual a : αᵒᵈ. See WithBot.toDual_top_equiv for the related order-iso.

Equations

WithBot.ofDual is the equivalence sending to and any a : αᵒᵈ to ofDual a : α. See WithBot.ofDual_top_equiv for the related order-iso.

Equations
@[simp]
theorem WithTop.toDual_symm_apply {α : Type u_1} (a : WithBot αᵒᵈ) :
↑(Equiv.symm WithTop.toDual) a = WithBot.ofDual a
@[simp]
theorem WithTop.ofDual_symm_apply {α : Type u_1} (a : WithBot α) :
↑(Equiv.symm WithTop.ofDual) a = WithBot.toDual a
@[simp]
theorem WithTop.toDual_apply_top {α : Type u_1} :
WithTop.toDual =
@[simp]
theorem WithTop.ofDual_apply_top {α : Type u_1} :
WithTop.ofDual =
@[simp]
theorem WithTop.toDual_apply_coe {α : Type u_1} (a : α) :
WithTop.toDual a = ↑(OrderDual.toDual a)
@[simp]
theorem WithTop.ofDual_apply_coe {α : Type u_1} (a : αᵒᵈ) :
WithTop.ofDual a = ↑(OrderDual.ofDual a)
def WithTop.untop' {α : Type u_1} (d : α) (x : WithTop α) :
α

Specialization of Option.get_or_else to values in WithTop α that respects API boundaries.

Equations
@[simp]
theorem WithTop.untop'_top {α : Type u_1} (d : α) :
@[simp]
theorem WithTop.untop'_coe {α : Type u_1} (d : α) (x : α) :
WithTop.untop' d x = x
@[simp]
theorem WithTop.coe_eq_coe {α : Type u_1} {a : α} {b : α} :
a = b a = b
theorem WithTop.untop'_eq_iff {α : Type u_1} {d : α} {y : α} {x : WithTop α} :
WithTop.untop' d x = y x = y x = y = d
@[simp]
theorem WithTop.untop'_eq_self_iff {α : Type u_1} {d : α} {x : WithTop α} :
WithTop.untop' d x = d x = d x =
theorem WithTop.untop'_eq_untop'_iff {α : Type u_1} {d : α} {x : WithTop α} {y : WithTop α} :
WithTop.untop' d x = WithTop.untop' d y x = y x = d y = x = y = d
def WithTop.map {α : Type u_1} {β : Type u_2} (f : αβ) :
WithTop αWithTop β

Lift a map f : α → β to WithTop α → WithTop β. Implemented using Option.map.

Equations
@[simp]
theorem WithTop.map_top {α : Type u_2} {β : Type u_1} (f : αβ) :
@[simp]
theorem WithTop.map_coe {α : Type u_2} {β : Type u_1} (f : αβ) (a : α) :
WithTop.map f a = ↑(f a)
theorem WithTop.map_comm {α : Type u_1} {β : Type u_3} {γ : Type u_4} {δ : Type u_2} {f₁ : αβ} {f₂ : αγ} {g₁ : βδ} {g₂ : γδ} (h : g₁ f₁ = g₂ f₂) (a : α) :
WithTop.map g₁ (WithTop.map f₁ a) = WithTop.map g₂ (WithTop.map f₂ a)
theorem WithTop.map_toDual {α : Type u_1} {β : Type u_2} (f : αᵒᵈβᵒᵈ) (a : WithBot α) :
WithTop.map f (WithBot.toDual a) = WithBot.map (OrderDual.toDual f) a
theorem WithTop.map_ofDual {α : Type u_1} {β : Type u_2} (f : αβ) (a : WithBot αᵒᵈ) :
WithTop.map f (WithBot.ofDual a) = WithBot.map (OrderDual.ofDual f) a
theorem WithTop.toDual_map {α : Type u_1} {β : Type u_2} (f : αβ) (a : WithTop α) :
WithTop.toDual (WithTop.map f a) = WithBot.map (OrderDual.toDual f OrderDual.ofDual) (WithTop.toDual a)
theorem WithTop.ofDual_map {α : Type u_1} {β : Type u_2} (f : αᵒᵈβᵒᵈ) (a : WithTop αᵒᵈ) :
WithTop.ofDual (WithTop.map f a) = WithBot.map (OrderDual.ofDual f OrderDual.toDual) (WithTop.ofDual a)
theorem WithTop.ne_top_iff_exists {α : Type u_1} {x : WithTop α} :
x a, a = x
def WithTop.untop {α : Type u_1} (x : WithTop α) :
x α

Deconstruct a x : WithTop α to the underlying value in α, given a proof that x ≠ ⊤.

Equations
  • WithTop.untop = WithBot.unbot
@[simp]
theorem WithTop.coe_untop {α : Type u_1} (x : WithTop α) (h : x ) :
↑(WithTop.untop x h) = x
@[simp]
theorem WithTop.untop_coe {α : Type u_1} (x : α) (h : optParam (x ) (_ : x )) :
WithTop.untop (x) h = x
instance WithTop.canLift {α : Type u_1} :
CanLift (WithTop α) α WithTop.some fun r => r
Equations
  • WithTop.canLift = { prf := (_ : ∀ (x : WithTop α), x y, y = x) }
instance WithTop.le {α : Type u_1} [inst : LE α] :
LE (WithTop α)
Equations
  • WithTop.le = { le := fun o₁ o₂ => ∀ (a : α), a o₂b, b o₁ b a }
theorem WithTop.toDual_le_iff {α : Type u_1} [inst : LE α] {a : WithTop α} {b : WithBot αᵒᵈ} :
WithTop.toDual a b WithBot.ofDual b a
theorem WithTop.le_toDual_iff {α : Type u_1} [inst : LE α] {a : WithBot αᵒᵈ} {b : WithTop α} :
a WithTop.toDual b b WithBot.ofDual a
@[simp]
theorem WithTop.toDual_le_toDual_iff {α : Type u_1} [inst : LE α] {a : WithTop α} {b : WithTop α} :
WithTop.toDual a WithTop.toDual b b a
theorem WithTop.ofDual_le_iff {α : Type u_1} [inst : LE α] {a : WithTop αᵒᵈ} {b : WithBot α} :
WithTop.ofDual a b WithBot.toDual b a
theorem WithTop.le_ofDual_iff {α : Type u_1} [inst : LE α] {a : WithBot α} {b : WithTop αᵒᵈ} :
a WithTop.ofDual b b WithBot.toDual a
@[simp]
theorem WithTop.ofDual_le_ofDual_iff {α : Type u_1} [inst : LE α] {a : WithTop αᵒᵈ} {b : WithTop αᵒᵈ} :
WithTop.ofDual a WithTop.ofDual b b a
@[simp]
theorem WithTop.coe_le_coe {α : Type u_1} {a : α} {b : α} [inst : LE α] :
a b a b
@[simp]
theorem WithTop.some_le_some {α : Type u_1} {a : α} {b : α} [inst : LE α] :
some a some b a b
@[simp]
theorem WithTop.le_none {α : Type u_1} [inst : LE α] {a : WithTop α} :
a none
instance WithTop.orderTop {α : Type u_1} [inst : LE α] :
Equations
instance WithTop.orderBot {α : Type u_1} [inst : LE α] [inst : OrderBot α] :
Equations
instance WithTop.boundedOrder {α : Type u_1} [inst : LE α] [inst : OrderBot α] :
Equations
  • WithTop.boundedOrder = let src := WithTop.orderTop; let src_1 := WithTop.orderBot; BoundedOrder.mk
theorem WithTop.not_top_le_coe {α : Type u_1} [inst : LE α] (a : α) :
¬ a
theorem WithTop.le_coe {α : Type u_1} {a : α} {b : α} [inst : LE α] {o : Option α} :
a o → (o b a b)
theorem WithTop.le_coe_iff {α : Type u_1} {b : α} [inst : LE α] {x : WithTop α} :
x b a, x = a a b
theorem WithTop.coe_le_iff {α : Type u_1} {a : α} [inst : LE α] {x : WithTop α} :
a x ∀ (b : α), x = ba b
theorem IsMin.withTop {α : Type u_1} {a : α} [inst : LE α] (h : IsMin a) :
IsMin a
instance WithTop.lt {α : Type u_1} [inst : LT α] :
LT (WithTop α)
Equations
  • WithTop.lt = { lt := fun o₁ o₂ => b, b o₁ ∀ (a : α), a o₂b < a }
theorem WithTop.toDual_lt_iff {α : Type u_1} [inst : LT α] {a : WithTop α} {b : WithBot αᵒᵈ} :
WithTop.toDual a < b WithBot.ofDual b < a
theorem WithTop.lt_toDual_iff {α : Type u_1} [inst : LT α] {a : WithBot αᵒᵈ} {b : WithTop α} :
a < WithTop.toDual b b < WithBot.ofDual a
@[simp]
theorem WithTop.toDual_lt_toDual_iff {α : Type u_1} [inst : LT α] {a : WithTop α} {b : WithTop α} :
WithTop.toDual a < WithTop.toDual b b < a
theorem WithTop.ofDual_lt_iff {α : Type u_1} [inst : LT α] {a : WithTop αᵒᵈ} {b : WithBot α} :
WithTop.ofDual a < b WithBot.toDual b < a
theorem WithTop.lt_ofDual_iff {α : Type u_1} [inst : LT α] {a : WithBot α} {b : WithTop αᵒᵈ} :
a < WithTop.ofDual b b < WithBot.toDual a
@[simp]
theorem WithTop.ofDual_lt_ofDual_iff {α : Type u_1} [inst : LT α] {a : WithTop αᵒᵈ} {b : WithTop αᵒᵈ} :
WithTop.ofDual a < WithTop.ofDual b b < a
@[simp]
theorem WithBot.toDual_symm_apply {α : Type u_1} (a : WithTop αᵒᵈ) :
↑(Equiv.symm WithBot.toDual) a = WithTop.ofDual a
@[simp]
theorem WithBot.ofDual_symm_apply {α : Type u_1} (a : WithTop α) :
↑(Equiv.symm WithBot.ofDual) a = WithTop.toDual a
@[simp]
theorem WithBot.toDual_apply_bot {α : Type u_1} :
WithBot.toDual =
@[simp]
theorem WithBot.ofDual_apply_bot {α : Type u_1} :
WithBot.ofDual =
@[simp]
theorem WithBot.toDual_apply_coe {α : Type u_1} (a : α) :
WithBot.toDual a = ↑(OrderDual.toDual a)
@[simp]
theorem WithBot.ofDual_apply_coe {α : Type u_1} (a : αᵒᵈ) :
WithBot.ofDual a = ↑(OrderDual.ofDual a)
theorem WithBot.map_toDual {α : Type u_1} {β : Type u_2} (f : αᵒᵈβᵒᵈ) (a : WithTop α) :
WithBot.map f (WithTop.toDual a) = WithTop.map (OrderDual.toDual f) a
theorem WithBot.map_ofDual {α : Type u_1} {β : Type u_2} (f : αβ) (a : WithTop αᵒᵈ) :
WithBot.map f (WithTop.ofDual a) = WithTop.map (OrderDual.ofDual f) a
theorem WithBot.toDual_map {α : Type u_1} {β : Type u_2} (f : αβ) (a : WithBot α) :
WithBot.toDual (WithBot.map f a) = WithBot.map (OrderDual.toDual f OrderDual.ofDual) (WithBot.toDual a)
theorem WithBot.ofDual_map {α : Type u_1} {β : Type u_2} (f : αᵒᵈβᵒᵈ) (a : WithBot αᵒᵈ) :
WithBot.ofDual (WithBot.map f a) = WithBot.map (OrderDual.ofDual f OrderDual.toDual) (WithBot.ofDual a)
theorem WithBot.toDual_le_iff {α : Type u_1} [inst : LE α] {a : WithBot α} {b : WithTop αᵒᵈ} :
WithBot.toDual a b WithTop.ofDual b a
theorem WithBot.le_toDual_iff {α : Type u_1} [inst : LE α] {a : WithTop αᵒᵈ} {b : WithBot α} :
a WithBot.toDual b b WithTop.ofDual a
@[simp]
theorem WithBot.toDual_le_toDual_iff {α : Type u_1} [inst : LE α] {a : WithBot α} {b : WithBot α} :
WithBot.toDual a WithBot.toDual b b a
theorem WithBot.ofDual_le_iff {α : Type u_1} [inst : LE α] {a : WithBot αᵒᵈ} {b : WithTop α} :
WithBot.ofDual a b WithTop.toDual b a
theorem WithBot.le_ofDual_iff {α : Type u_1} [inst : LE α] {a : WithTop α} {b : WithBot αᵒᵈ} :
a WithBot.ofDual b b WithTop.toDual a
@[simp]
theorem WithBot.ofDual_le_ofDual_iff {α : Type u_1} [inst : LE α] {a : WithBot αᵒᵈ} {b : WithBot αᵒᵈ} :
WithBot.ofDual a WithBot.ofDual b b a
theorem WithBot.toDual_lt_iff {α : Type u_1} [inst : LT α] {a : WithBot α} {b : WithTop αᵒᵈ} :
WithBot.toDual a < b WithTop.ofDual b < a
theorem WithBot.lt_toDual_iff {α : Type u_1} [inst : LT α] {a : WithTop αᵒᵈ} {b : WithBot α} :
a < WithBot.toDual b b < WithTop.ofDual a
@[simp]
theorem WithBot.toDual_lt_toDual_iff {α : Type u_1} [inst : LT α] {a : WithBot α} {b : WithBot α} :
WithBot.toDual a < WithBot.toDual b b < a
theorem WithBot.ofDual_lt_iff {α : Type u_1} [inst : LT α] {a : WithBot αᵒᵈ} {b : WithTop α} :
WithBot.ofDual a < b WithTop.toDual b < a
theorem WithBot.lt_ofDual_iff {α : Type u_1} [inst : LT α] {a : WithTop α} {b : WithBot αᵒᵈ} :
a < WithBot.ofDual b b < WithTop.toDual a
@[simp]
theorem WithBot.ofDual_lt_ofDual_iff {α : Type u_1} [inst : LT α] {a : WithBot αᵒᵈ} {b : WithBot αᵒᵈ} :
WithBot.ofDual a < WithBot.ofDual b b < a
@[simp]
theorem WithTop.coe_lt_coe {α : Type u_1} [inst : LT α] {a : α} {b : α} :
a < b a < b
@[simp]
theorem WithTop.some_lt_some {α : Type u_1} [inst : LT α] {a : α} {b : α} :
some a < some b a < b
theorem WithTop.coe_lt_top {α : Type u_1} [inst : LT α] (a : α) :
a <
@[simp]
theorem WithTop.some_lt_none {α : Type u_1} [inst : LT α] (a : α) :
some a < none
@[simp]
theorem WithTop.not_none_lt {α : Type u_1} [inst : LT α] (a : WithTop α) :
¬none < a
theorem WithTop.lt_iff_exists_coe {α : Type u_1} [inst : LT α] {a : WithTop α} {b : WithTop α} :
a < b p, a = p p < b
theorem WithTop.coe_lt_iff {α : Type u_1} [inst : LT α] {a : α} {x : WithTop α} :
a < x ∀ (b : WithTop α), x = ba < b
theorem WithTop.lt_top_iff_ne_top {α : Type u_1} [inst : LT α] {x : WithTop α} :

A version of lt_top_iff_ne_top for WithTop that only requires LT α, not PartialOrder α.

instance WithTop.preorder {α : Type u_1} [inst : Preorder α] :
Equations
instance WithTop.partialOrder {α : Type u_1} [inst : PartialOrder α] :
Equations
theorem WithTop.coe_strictMono {α : Type u_1} [inst : Preorder α] :
StrictMono fun a => a
theorem WithTop.coe_mono {α : Type u_1} [inst : Preorder α] :
Monotone fun a => a
theorem WithTop.monotone_iff {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {f : WithTop αβ} :
Monotone f (Monotone fun a => f a) ∀ (x : α), f x f
@[simp]
theorem WithTop.monotone_map_iff {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {f : αβ} :
theorem Monotone.withTop_map {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {f : αβ} :

Alias of the reverse direction of WithTop.monotone_map_iff.

theorem WithTop.strictMono_iff {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {f : WithTop αβ} :
StrictMono f (StrictMono fun a => f a) ∀ (x : α), f x < f
theorem WithTop.strictAnti_iff {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {f : WithTop αβ} :
StrictAnti f (StrictAnti fun a => f a) ∀ (x : α), f < f x
@[simp]
theorem WithTop.strictMono_map_iff {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {f : αβ} :
theorem StrictMono.withTop_map {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {f : αβ} :

Alias of the reverse direction of WithTop.strictMono_map_iff.

theorem WithTop.map_le_iff {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] (f : αβ) (a : WithTop α) (b : WithTop α) (mono_iff : ∀ {a b : α}, f a f b a b) :
instance WithTop.semilatticeInf {α : Type u_1} [inst : SemilatticeInf α] :
Equations
  • One or more equations did not get rendered due to their size.
theorem WithTop.coe_inf {α : Type u_1} [inst : SemilatticeInf α] (a : α) (b : α) :
↑(a b) = a b
instance WithTop.semilatticeSup {α : Type u_1} [inst : SemilatticeSup α] :
Equations
  • One or more equations did not get rendered due to their size.
theorem WithTop.coe_sup {α : Type u_1} [inst : SemilatticeSup α] (a : α) (b : α) :
↑(a b) = a b
instance WithTop.lattice {α : Type u_1} [inst : Lattice α] :
Equations
  • One or more equations did not get rendered due to their size.
instance WithTop.distribLattice {α : Type u_1} [inst : DistribLattice α] :
Equations
instance WithTop.decidableLE {α : Type u_1} [inst : LE α] [inst : DecidableRel fun x x_1 => x x_1] :
DecidableRel fun x x_1 => x x_1
Equations
instance WithTop.decidableLT {α : Type u_1} [inst : LT α] [inst : DecidableRel fun x x_1 => x < x_1] :
DecidableRel fun x x_1 => x < x_1
Equations
instance WithTop.isTotal_le {α : Type u_1} [inst : LE α] [inst : IsTotal α fun x x_1 => x x_1] :
IsTotal (WithTop α) fun x x_1 => x x_1
Equations
instance WithTop.linearOrder {α : Type u_1} [inst : LinearOrder α] :
Equations
@[simp]
theorem WithTop.coe_min {α : Type u_1} [inst : LinearOrder α] (x : α) (y : α) :
↑(min x y) = min x y
@[simp]
theorem WithTop.coe_max {α : Type u_1} [inst : LinearOrder α] (x : α) (y : α) :
↑(max x y) = max x y
theorem WithTop.wellFounded_lt {α : Type u_1} [inst : Preorder α] (h : WellFounded fun x x_1 => x < x_1) :
WellFounded fun x x_1 => x < x_1
theorem WithTop.wellFounded_gt {α : Type u_1} [inst : Preorder α] (h : WellFounded fun x x_1 => x > x_1) :
WellFounded fun x x_1 => x > x_1
theorem WithBot.wellFounded_gt {α : Type u_1} [inst : Preorder α] (h : WellFounded fun x x_1 => x > x_1) :
WellFounded fun x x_1 => x > x_1
instance WithTop.trichotomous.lt {α : Type u_1} [inst : Preorder α] [inst : IsTrichotomous α fun x x_1 => x < x_1] :
IsTrichotomous (WithTop α) fun x x_1 => x < x_1
Equations
instance WithTop.IsWellOrder.lt {α : Type u_1} [inst : Preorder α] [h : IsWellOrder α fun x x_1 => x < x_1] :
IsWellOrder (WithTop α) fun x x_1 => x < x_1
Equations
instance WithTop.trichotomous.gt {α : Type u_1} [inst : Preorder α] [inst : IsTrichotomous α fun x x_1 => x > x_1] :
IsTrichotomous (WithTop α) fun x x_1 => x > x_1
Equations
instance WithTop.IsWellOrder.gt {α : Type u_1} [inst : Preorder α] [h : IsWellOrder α fun x x_1 => x > x_1] :
IsWellOrder (WithTop α) fun x x_1 => x > x_1
Equations
instance WithBot.trichotomous.lt {α : Type u_1} [inst : Preorder α] [h : IsTrichotomous α fun x x_1 => x < x_1] :
IsTrichotomous (WithBot α) fun x x_1 => x < x_1
Equations
instance WithBot.isWellOrder.lt {α : Type u_1} [inst : Preorder α] [h : IsWellOrder α fun x x_1 => x < x_1] :
IsWellOrder (WithBot α) fun x x_1 => x < x_1
Equations
instance WithBot.trichotomous.gt {α : Type u_1} [inst : Preorder α] [h : IsTrichotomous α fun x x_1 => x > x_1] :
IsTrichotomous (WithBot α) fun x x_1 => x > x_1
Equations
instance WithBot.isWellOrder.gt {α : Type u_1} [inst : Preorder α] [h : IsWellOrder α fun x x_1 => x > x_1] :
IsWellOrder (WithBot α) fun x x_1 => x > x_1
Equations
theorem WithTop.lt_iff_exists_coe_btwn {α : Type u_1} [inst : Preorder α] [inst : DenselyOrdered α] [inst : NoMaxOrder α] {a : WithTop α} {b : WithTop α} :
a < b x, a < x x < b
instance WithTop.noBotOrder {α : Type u_1} [inst : LE α] [inst : NoBotOrder α] [inst : Nonempty α] :
Equations
instance WithTop.noMinOrder {α : Type u_1} [inst : LT α] [inst : NoMinOrder α] [inst : Nonempty α] :
Equations