# WithBot, WithTop#

Adding a bot or a top to an order.

## Main declarations #

• With<Top/Bot> α: Equips Option α with the order on α plus none as the top/bottom element.
def WithBot (α : Type u_5) :
Type u_5

Attach ⊥ to a type.

Equations
Instances For
instance WithBot.instRepr {α : Type u_1} [Repr α] :
Repr ()
Equations
• WithBot.instRepr = { reprPrec := fun (o : ) (x : ) => match o with | none => | some a => ++ repr a }
@[match_pattern]
def WithBot.some {α : Type u_1} :
α

The canonical map from α into WithBot α

Equations
• WithBot.some = some
Instances For
instance WithBot.coe {α : Type u_1} :
Coe α ()
Equations
• WithBot.coe = { coe := WithBot.some }
instance WithBot.bot {α : Type u_1} :
Bot ()
Equations
• WithBot.bot = { bot := none }
instance WithBot.inhabited {α : Type u_1} :
Equations
• WithBot.inhabited = { default := }
instance WithBot.nontrivial {α : Type u_1} [] :
Equations
• =
theorem WithBot.coe_injective {α : Type u_1} :
Function.Injective WithBot.some
@[simp]
theorem WithBot.coe_inj {α : Type u_1} {a : α} {b : α} :
a = b a = b
theorem WithBot.forall {α : Type u_1} {p : Prop} :
(∀ (x : ), p x) p ∀ (x : α), p x
theorem WithBot.exists {α : Type u_1} {p : 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 : Sort u_5} (bot : C ) (coe : (a : α) → C a) (n : ) :
C n

Recursor for WithBot using the preferred forms ⊥ and ↑a.

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

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

Equations
Instances For
@[simp]
theorem WithBot.unbot'_bot {α : Type u_5} (d : α) :
= d
@[simp]
theorem WithBot.unbot'_coe {α : Type u_5} (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 : } :
= y x = y x = y = d
@[simp]
theorem WithBot.unbot'_eq_self_iff {α : Type u_1} {d : α} {x : } :
= d x = d x =
theorem WithBot.unbot'_eq_unbot'_iff {α : Type u_1} {d : α} {x : } {y : } :
= x = y x = d y = x = y = d
def WithBot.map {α : Type u_1} {β : Type u_2} (f : αβ) :

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

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

The image of a binary function f : α → β → γ as a function WithBot α → WithBot β → WithBot γ.

Mathematically this should be thought of as the image of the corresponding function α × β → γ.

Equations
• WithBot.map₂ = Option.map₂
Instances For
theorem WithBot.map₂_coe_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (a : α) (b : β) :
WithBot.map₂ f a b = (f a b)
@[simp]
theorem WithBot.map₂_bot_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (b : ) :
@[simp]
theorem WithBot.map₂_bot_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (a : ) :
@[simp]
theorem WithBot.map₂_coe_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (a : α) (b : ) :
WithBot.map₂ f (a) b = WithBot.map (fun (b : β) => f a b) b
@[simp]
theorem WithBot.map₂_coe_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (a : ) (b : β) :
WithBot.map₂ f a b = WithBot.map (fun (x : α) => f x b) a
@[simp]
theorem WithBot.map₂_eq_bot_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβγ} {a : } {b : } :
theorem WithBot.ne_bot_iff_exists {α : Type u_1} {x : } :
x ∃ (a : α), a = x
theorem WithBot.forall_ne_iff_eq_bot {α : Type u_1} {x : } :
(∀ (a : α), a x) x =
def WithBot.unbot {α : Type u_1} (x : ) :
x α

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

Equations
• x✝.unbot x = match x✝, x with | some x, x_1 => x
Instances For
@[simp]
theorem WithBot.coe_unbot {α : Type u_1} (x : ) (hx : x ) :
(x.unbot hx) = x
@[simp]
theorem WithBot.unbot_coe {α : Type u_1} (x : α) (h : optParam (x ) ) :
(x).unbot h = x
instance WithBot.canLift {α : Type u_1} :
CanLift () α WithBot.some fun (r : ) => r
Equations
• =
@[instance 10]
instance WithBot.le {α : Type u_1} [LE α] :
LE ()
Equations
• WithBot.le = { le := fun (o₁ o₂ : ) => ∀ (a : α), o₁ = a∃ (b : α), o₂ = b a b }
@[simp]
theorem WithBot.coe_le_coe {α : Type u_1} {a : α} {b : α} [LE α] :
a b a b
instance WithBot.orderBot {α : Type u_1} [LE α] :
Equations
• WithBot.orderBot =
@[simp, deprecated WithBot.coe_le_coe]
theorem WithBot.some_le_some {α : Type u_1} {a : α} {b : α} [LE α] :
some a some b a b
@[simp, deprecated bot_le]
theorem WithBot.none_le {α : Type u_1} [LE α] {a : } :
none a
instance WithBot.instTop {α : Type u_1} [Top α] :
Top ()
Equations
• WithBot.instTop = { top := }
@[simp]
theorem WithBot.coe_top {α : Type u_1} [Top α] :
=
@[simp]
theorem WithBot.coe_eq_top {α : Type u_1} [Top α] {a : α} :
a = a =
@[simp]
theorem WithBot.top_eq_coe {α : Type u_1} [Top α] {a : α} :
= a = a
instance WithBot.orderTop {α : Type u_1} [LE α] [] :
Equations
• WithBot.orderTop =
instance WithBot.instBoundedOrder {α : Type u_1} [LE α] [] :
Equations
• WithBot.instBoundedOrder = let __src := WithBot.orderBot; let __src_1 := WithBot.orderTop; BoundedOrder.mk
theorem WithBot.not_coe_le_bot {α : Type u_1} [LE α] (a : α) :
¬a
@[simp]
theorem WithBot.le_bot_iff {α : Type u_1} [LE α] {a : } :

There is a general version le_bot_iff, but this lemma does not require a PartialOrder.

theorem WithBot.coe_le {α : Type u_1} {a : α} {b : α} [LE α] {o : } :
b o(a o a b)
theorem WithBot.coe_le_iff {α : Type u_1} {a : α} [LE α] {x : } :
a x ∃ (b : α), x = b a b
theorem WithBot.le_coe_iff {α : Type u_1} {b : α} [LE α] {x : } :
x b ∀ (a : α), x = aa b
theorem IsMax.withBot {α : Type u_1} {a : α} [LE α] (h : ) :
IsMax a
theorem WithBot.le_unbot_iff {α : Type u_1} [LE α] {a : α} {b : } (h : b ) :
a b.unbot h a b
theorem WithBot.unbot_le_iff {α : Type u_1} [LE α] {a : } (h : a ) {b : α} :
a.unbot h b a b
theorem WithBot.unbot'_le_iff {α : Type u_1} [LE α] {a : } {b : α} {c : α} (h : a = b c) :
c a c
@[instance 10]
instance WithBot.lt {α : Type u_1} [LT α] :
LT ()
Equations
• WithBot.lt = { lt := fun (o₁ o₂ : ) => ∃ (b : α), o₂ = b ∀ (a : α), o₁ = aa < b }
@[simp]
theorem WithBot.coe_lt_coe {α : Type u_1} {a : α} {b : α} [LT α] :
a < b a < b
@[simp]
theorem WithBot.bot_lt_coe {α : Type u_1} [LT α] (a : α) :
< a
@[simp]
theorem WithBot.not_lt_bot {α : Type u_1} [LT α] (a : ) :
@[simp, deprecated WithBot.coe_lt_coe]
theorem WithBot.some_lt_some {α : Type u_1} {a : α} {b : α} [LT α] :
some a < some b a < b
@[simp, deprecated WithBot.bot_lt_coe]
theorem WithBot.none_lt_some {α : Type u_1} [LT α] (a : α) :
none < a
@[simp, deprecated not_lt_bot]
theorem WithBot.not_lt_none {α : Type u_1} [LT α] (a : ) :
¬a < none
theorem WithBot.lt_iff_exists_coe {α : Type u_1} [LT α] {a : } {b : } :
a < b ∃ (p : α), b = p a < p
theorem WithBot.lt_coe_iff {α : Type u_1} {b : α} [LT α] {x : } :
x < b ∀ (a : α), x = aa < b
theorem WithBot.bot_lt_iff_ne_bot {α : Type u_1} [LT α] {x : } :

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

theorem WithBot.unbot'_lt_iff {α : Type u_1} [LT α] {a : } {b : α} {c : α} (h : a = b < c) :
< c a < c
instance WithBot.preorder {α : Type u_1} [] :
Equations
instance WithBot.partialOrder {α : Type u_1} [] :
Equations
• WithBot.partialOrder = let __src := WithBot.preorder;
theorem WithBot.coe_strictMono {α : Type u_1} [] :
StrictMono fun (a : α) => a
theorem WithBot.coe_mono {α : Type u_1} [] :
Monotone fun (a : α) => a
theorem WithBot.monotone_iff {α : Type u_1} {β : Type u_2} [] [] {f : β} :
(Monotone fun (a : α) => f a) ∀ (x : α), f f x
@[simp]
theorem WithBot.monotone_map_iff {α : Type u_1} {β : Type u_2} [] [] {f : αβ} :
theorem Monotone.withBot_map {α : Type u_1} {β : Type u_2} [] [] {f : αβ} :

Alias of the reverse direction of WithBot.monotone_map_iff.

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

Alias of the reverse direction of WithBot.strictMono_map_iff.

theorem WithBot.map_le_iff {α : Type u_1} {β : Type u_2} [] [] (f : αβ) (mono_iff : ∀ {a b : α}, f a f b a b) (a : ) (b : ) :
a b
theorem WithBot.le_coe_unbot' {α : Type u_1} [] (a : ) (b : α) :
a ()
@[simp]
theorem WithBot.lt_coe_bot {α : Type u_1} [] [] {x : } :
x < x =
instance WithBot.semilatticeSup {α : Type u_1} [] :
Equations
• WithBot.semilatticeSup =
theorem WithBot.coe_sup {α : Type u_1} [] (a : α) (b : α) :
(a b) = a b
instance WithBot.semilatticeInf {α : Type u_1} [] :
Equations
• WithBot.semilatticeInf = let __src := WithBot.partialOrder; let __src_1 := WithBot.orderBot;
theorem WithBot.coe_inf {α : Type u_1} [] (a : α) (b : α) :
(a b) = a b
instance WithBot.lattice {α : Type u_1} [] :
Equations
• WithBot.lattice = let __src := WithBot.semilatticeSup; let __src_1 := WithBot.semilatticeInf; Lattice.mk
instance WithBot.distribLattice {α : Type u_1} [] :
Equations
• WithBot.distribLattice = let __src := WithBot.lattice;
instance WithBot.decidableEq {α : Type u_1} [] :
Equations
• WithBot.decidableEq =
instance WithBot.decidableLE {α : Type u_1} [LE α] [DecidableRel fun (x x_1 : α) => x x_1] :
DecidableRel fun (x x_1 : ) => x x_1
Equations
• x✝.decidableLE x = match x✝, x with | none, x => | some x, some y => if h : x y then else | some x, none =>
instance WithBot.decidableLT {α : Type u_1} [LT α] [DecidableRel fun (x x_1 : α) => x < x_1] :
DecidableRel fun (x x_1 : ) => x < x_1
Equations
• x✝.decidableLT x = match x✝, x with | none, some x => | some x, some y => if h : x < y then else | x, none =>
instance WithBot.isTotal_le {α : Type u_1} [LE α] [IsTotal α fun (x x_1 : α) => x x_1] :
IsTotal () fun (x x_1 : ) => x x_1
Equations
• =
instance WithBot.linearOrder {α : Type u_1} [] :
Equations
• WithBot.linearOrder =
@[simp]
theorem WithBot.coe_min {α : Type u_1} [] (x : α) (y : α) :
(min x y) = min x y
@[simp]
theorem WithBot.coe_max {α : Type u_1} [] (x : α) (y : α) :
(max x y) = max x y
instance WithBot.instWellFoundedLT {α : Type u_1} [LT α] [] :
Equations
• =
instance WithBot.instWellFoundedGT {α : Type u_1} [LT α] [] :
Equations
• =
instance WithBot.denselyOrdered {α : Type u_1} [LT α] [] [] :
Equations
• =
theorem WithBot.lt_iff_exists_coe_btwn {α : Type u_1} [] [] [] {a : } {b : } :
a < b ∃ (x : α), a < x x < b
instance WithBot.noTopOrder {α : Type u_1} [LE α] [] [] :
Equations
• =
instance WithBot.noMaxOrder {α : Type u_1} [LT α] [] [] :
Equations
• =
def WithTop (α : Type u_5) :
Type u_5

Attach ⊤ to a type.

Equations
Instances For
instance WithTop.instRepr {α : Type u_1} [Repr α] :
Repr ()
Equations
• WithTop.instRepr = { reprPrec := fun (o : ) (x : ) => match o with | none => | some a => ++ repr a }
@[match_pattern]
def WithTop.some {α : Type u_1} :
α

The canonical map from α into WithTop α

Equations
• WithTop.some = some
Instances For
instance WithTop.coeTC {α : Type u_1} :
CoeTC α ()
Equations
• WithTop.coeTC = { coe := WithTop.some }
instance WithTop.top {α : Type u_1} :
Top ()
Equations
• WithTop.top = { top := none }
instance WithTop.inhabited {α : Type u_1} :
Equations
• WithTop.inhabited = { default := }
instance WithTop.nontrivial {α : Type u_1} [] :
Equations
• =
theorem WithTop.coe_injective {α : Type u_1} :
Function.Injective WithTop.some
theorem WithTop.coe_inj {α : Type u_1} {a : α} {b : α} :
a = b a = b
theorem WithTop.forall {α : Type u_1} {p : Prop} :
(∀ (x : ), p x) p ∀ (x : α), p x
theorem WithTop.exists {α : Type u_1} {p : 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 : Sort u_5} (top : C ) (coe : (a : α) → C a) (n : ) :
C n

Recursor for WithTop using the preferred forms ⊤ and ↑a.

Equations
Instances For
@[simp]
theorem WithTop.recTopCoe_top {α : Type u_1} {C : Sort u_5} (d : C ) (f : (a : α) → C a) :
= d
@[simp]
theorem WithTop.recTopCoe_coe {α : Type u_1} {C : Sort u_5} (d : C ) (f : (a : α) → C a) (x : α) :
= f x
def WithTop.toDual {α : Type u_1} :

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

Equations
• WithTop.toDual =
Instances For
def WithTop.ofDual {α : Type u_1} :

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

Equations
• WithTop.ofDual =
Instances For
def WithBot.toDual {α : Type u_1} :

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.toDual =
Instances For
def WithBot.ofDual {α : Type u_1} :

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

Equations
• WithBot.ofDual =
Instances For
@[simp]
theorem WithTop.toDual_symm_apply {α : Type u_1} (a : ) :
WithTop.toDual.symm a = WithBot.ofDual a
@[simp]
theorem WithTop.ofDual_symm_apply {α : Type u_1} (a : ) :
WithTop.ofDual.symm 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 : ) :
α

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

Equations
Instances For
@[simp]
theorem WithTop.untop'_top {α : Type u_5} (d : α) :
= d
@[simp]
theorem WithTop.untop'_coe {α : Type u_5} (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 : } :
= y x = y x = y = d
@[simp]
theorem WithTop.untop'_eq_self_iff {α : Type u_1} {d : α} {x : } :
= d x = d x =
theorem WithTop.untop'_eq_untop'_iff {α : Type u_1} {d : α} {x : } {y : } :
= x = y x = d y = x = y = d
def WithTop.map {α : Type u_1} {β : Type u_2} (f : αβ) :

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

Equations
Instances For
@[simp]
theorem WithTop.map_top {α : Type u_1} {β : Type u_2} (f : αβ) :
@[simp]
theorem WithTop.map_coe {α : Type u_1} {β : Type u_2} (f : αβ) (a : α) :
WithTop.map f a = (f a)
theorem WithTop.map_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f₁ : αβ} {f₂ : αγ} {g₁ : βδ} {g₂ : γδ} (h : g₁ f₁ = g₂ f₂) (a : α) :
WithTop.map g₁ (WithTop.map f₁ a) = WithTop.map g₂ (WithTop.map f₂ a)
def WithTop.map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} :
(αβγ)

The image of a binary function f : α → β → γ as a function WithTop α → WithTop β → WithTop γ.

Mathematically this should be thought of as the image of the corresponding function α × β → γ.

Equations
• WithTop.map₂ = Option.map₂
Instances For
theorem WithTop.map₂_coe_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (a : α) (b : β) :
WithTop.map₂ f a b = (f a b)
@[simp]
theorem WithTop.map₂_top_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (b : ) :
@[simp]
theorem WithTop.map₂_top_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (a : ) :
@[simp]
theorem WithTop.map₂_coe_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (a : α) (b : ) :
WithTop.map₂ f (a) b = WithTop.map (fun (b : β) => f a b) b
@[simp]
theorem WithTop.map₂_coe_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (a : ) (b : β) :
WithTop.map₂ f a b = WithTop.map (fun (x : α) => f x b) a
@[simp]
theorem WithTop.map₂_eq_top_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβγ} {a : } {b : } :
theorem WithTop.map_toDual {α : Type u_1} {β : Type u_2} (f : αᵒᵈβᵒᵈ) (a : ) :
WithTop.map f (WithBot.toDual a) = WithBot.map (OrderDual.toDual f) a
theorem WithTop.map_ofDual {α : Type u_1} {β : Type u_2} (f : αβ) (a : ) :
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.toDual () = WithBot.map (OrderDual.toDual f OrderDual.ofDual) (WithTop.toDual a)
theorem WithTop.ofDual_map {α : Type u_1} {β : Type u_2} (f : αᵒᵈβᵒᵈ) (a : ) :
WithTop.ofDual () = WithBot.map (OrderDual.ofDual f OrderDual.toDual) (WithTop.ofDual a)
theorem WithTop.ne_top_iff_exists {α : Type u_1} {x : } :
x ∃ (a : α), a = x
theorem WithTop.forall_ne_iff_eq_top {α : Type u_1} {x : } :
(∀ (a : α), a x) x =
def WithTop.untop {α : Type u_1} (x : ) :
x α

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

Equations
• x✝.untop x = match x✝, x with | some x, x_1 => x
Instances For
@[simp]
theorem WithTop.coe_untop {α : Type u_1} (x : ) (hx : x ) :
(x.untop hx) = x
@[simp]
theorem WithTop.untop_coe {α : Type u_1} (x : α) (h : optParam (x ) ) :
(x).untop h = x
instance WithTop.canLift {α : Type u_1} :
CanLift () α WithTop.some fun (r : ) => r
Equations
• =
@[instance 10]
instance WithTop.le {α : Type u_1} [LE α] :
LE ()
Equations
• WithTop.le = { le := fun (o₁ o₂ : ) => ∀ (a : α), o₂ = a∃ (b : α), o₁ = b b a }
theorem WithTop.toDual_le_iff {α : Type u_1} [LE α] {a : } {b : } :
WithTop.toDual a b WithBot.ofDual b a
theorem WithTop.le_toDual_iff {α : Type u_1} [LE α] {a : } {b : } :
a WithTop.toDual b b WithBot.ofDual a
@[simp]
theorem WithTop.toDual_le_toDual_iff {α : Type u_1} [LE α] {a : } {b : } :
WithTop.toDual a WithTop.toDual b b a
theorem WithTop.ofDual_le_iff {α : Type u_1} [LE α] {a : } {b : } :
WithTop.ofDual a b WithBot.toDual b a
theorem WithTop.le_ofDual_iff {α : Type u_1} [LE α] {a : } {b : } :
a WithTop.ofDual b b WithBot.toDual a
@[simp]
theorem WithTop.ofDual_le_ofDual_iff {α : Type u_1} [LE α] {a : } {b : } :
WithTop.ofDual a WithTop.ofDual b b a
@[simp]
theorem WithTop.coe_le_coe {α : Type u_1} {a : α} {b : α} [LE α] :
a b a b
@[simp, deprecated WithTop.coe_le_coe]
theorem WithTop.some_le_some {α : Type u_1} {a : α} {b : α} [LE α] :
some a some b a b
instance WithTop.orderTop {α : Type u_1} [LE α] :
Equations
• WithTop.orderTop =
@[simp, deprecated le_top]
theorem WithTop.le_none {α : Type u_1} [LE α] {a : } :
a none
instance WithTop.instBot {α : Type u_1} [Bot α] :
Bot ()
Equations
• WithTop.instBot = { bot := }
@[simp]
theorem WithTop.coe_bot {α : Type u_1} [Bot α] :
=
@[simp]
theorem WithTop.coe_eq_bot {α : Type u_1} [Bot α] {a : α} :
a = a =
@[simp]
theorem WithTop.bot_eq_coe {α : Type u_1} [Bot α] {a : α} :
= a = a
instance WithTop.orderBot {α : Type u_1} [LE α] [] :
Equations
• WithTop.orderBot =
instance WithTop.boundedOrder {α : Type u_1} [LE α] [] :
Equations
• WithTop.boundedOrder = let __src := WithTop.orderTop; let __src_1 := WithTop.orderBot; BoundedOrder.mk
theorem WithTop.not_top_le_coe {α : Type u_1} [LE α] (a : α) :
¬ a
@[simp]
theorem WithTop.top_le_iff {α : Type u_1} [LE α] {a : } :

There is a general version top_le_iff, but this lemma does not require a PartialOrder.

theorem WithTop.le_coe {α : Type u_1} {a : α} {b : α} [LE α] {o : } :
a o(o b a b)
theorem WithTop.le_coe_iff {α : Type u_1} {b : α} [LE α] {x : } :
x b ∃ (a : α), x = a a b
theorem WithTop.coe_le_iff {α : Type u_1} {a : α} [LE α] {x : } :
a x ∀ (b : α), x = ba b
theorem IsMin.withTop {α : Type u_1} {a : α} [LE α] (h : ) :
IsMin a
theorem WithTop.untop_le_iff {α : Type u_1} [LE α] {a : } {b : α} (h : a ) :
a.untop h b a b
theorem WithTop.le_untop_iff {α : Type u_1} [LE α] {a : α} {b : } (h : b ) :
a b.untop h a b
theorem WithTop.le_untop'_iff {α : Type u_1} [LE α] {a : } {b : α} {c : α} (h : a = c b) :
c c a
@[instance 10]
instance WithTop.lt {α : Type u_1} [LT α] :
LT ()
Equations
• WithTop.lt = { lt := fun (o₁ o₂ : ) => ∃ (b : α), b o₁ ∀ (a : α), a o₂b < a }
theorem WithTop.toDual_lt_iff {α : Type u_1} [LT α] {a : } {b : } :
WithTop.toDual a < b WithBot.ofDual b < a
theorem WithTop.lt_toDual_iff {α : Type u_1} [LT α] {a : } {b : } :
a < WithTop.toDual b b < WithBot.ofDual a
@[simp]
theorem WithTop.toDual_lt_toDual_iff {α : Type u_1} [LT α] {a : } {b : } :
WithTop.toDual a < WithTop.toDual b b < a
theorem WithTop.ofDual_lt_iff {α : Type u_1} [LT α] {a : } {b : } :
WithTop.ofDual a < b WithBot.toDual b < a
theorem WithTop.lt_ofDual_iff {α : Type u_1} [LT α] {a : } {b : } :
a < WithTop.ofDual b b < WithBot.toDual a
@[simp]
theorem WithTop.ofDual_lt_ofDual_iff {α : Type u_1} [LT α] {a : } {b : } :
WithTop.ofDual a < WithTop.ofDual b b < a
theorem WithTop.lt_untop'_iff {α : Type u_1} [LT α] {a : } {b : α} {c : α} (h : a = c < b) :
c < c < a
@[simp]
theorem WithBot.toDual_symm_apply {α : Type u_1} (a : ) :
WithBot.toDual.symm a = WithTop.ofDual a
@[simp]
theorem WithBot.ofDual_symm_apply {α : Type u_1} (a : ) :
WithBot.ofDual.symm 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 : ) :
WithBot.map f (WithTop.toDual a) = WithTop.map (OrderDual.toDual f) a
theorem WithBot.map_ofDual {α : Type u_1} {β : Type u_2} (f : αβ) (a : ) :
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.toDual () = WithBot.map (OrderDual.toDual f OrderDual.ofDual) (WithBot.toDual a)
theorem WithBot.ofDual_map {α : Type u_1} {β : Type u_2} (f : αᵒᵈβᵒᵈ) (a : ) :
WithBot.ofDual () = WithBot.map (OrderDual.ofDual f OrderDual.toDual) (WithBot.ofDual a)
theorem WithBot.forall_lt_iff_eq_bot {α : Type u_1} [] {x : } :
(∀ (y : α), x < y) x =
theorem WithBot.toDual_le_iff {α : Type u_1} [LE α] {a : } {b : } :
WithBot.toDual a b WithTop.ofDual b a
theorem WithBot.le_toDual_iff {α : Type u_1} [LE α] {a : } {b : } :
a WithBot.toDual b b WithTop.ofDual a
@[simp]
theorem WithBot.toDual_le_toDual_iff {α : Type u_1} [LE α] {a : } {b : } :
WithBot.toDual a WithBot.toDual b b a
theorem WithBot.ofDual_le_iff {α : Type u_1} [LE α] {a : } {b : } :
WithBot.ofDual a b WithTop.toDual b a
theorem WithBot.le_ofDual_iff {α : Type u_1} [LE α] {a : } {b : } :
a WithBot.ofDual b b WithTop.toDual a
@[simp]
theorem WithBot.ofDual_le_ofDual_iff {α : Type u_1} [LE α] {a : } {b : } :
WithBot.ofDual a WithBot.ofDual b b a
theorem WithBot.toDual_lt_iff {α : Type u_1} [LT α] {a : } {b : } :
WithBot.toDual a < b WithTop.ofDual b < a
theorem WithBot.lt_toDual_iff {α : Type u_1} [LT α] {a : } {b : } :
a < WithBot.toDual b b < WithTop.ofDual a
@[simp]
theorem WithBot.toDual_lt_toDual_iff {α : Type u_1} [LT α] {a : } {b : } :
WithBot.toDual a < WithBot.toDual b b < a
theorem WithBot.ofDual_lt_iff {α : Type u_1} [LT α] {a : } {b : } :
WithBot.ofDual a < b WithTop.toDual b < a
theorem WithBot.lt_ofDual_iff {α : Type u_1} [LT α] {a : } {b : } :
a < WithBot.ofDual b b < WithTop.toDual a
@[simp]
theorem WithBot.ofDual_lt_ofDual_iff {α : Type u_1} [LT α] {a : } {b : } :
WithBot.ofDual a < WithBot.ofDual b b < a
@[simp]
theorem WithTop.coe_lt_coe {α : Type u_1} [LT α] {a : α} {b : α} :
a < b a < b
@[simp]
theorem WithTop.coe_lt_top {α : Type u_1} [LT α] (a : α) :
a <
@[simp]
theorem WithTop.not_top_lt {α : Type u_1} [LT α] (a : ) :
@[simp, deprecated WithTop.coe_lt_coe]
theorem WithTop.some_lt_some {α : Type u_1} [LT α] {a : α} {b : α} :
some a < some b a < b
@[simp, deprecated WithTop.coe_lt_top]
theorem WithTop.some_lt_none {α : Type u_1} [LT α] (a : α) :
some a < none
@[simp, deprecated not_top_lt]
theorem WithTop.not_none_lt {α : Type u_1} [LT α] (a : ) :
¬none < a
theorem WithTop.lt_iff_exists_coe {α : Type u_1} [LT α] {a : } {b : } :
a < b ∃ (p : α), a = p p < b
theorem WithTop.coe_lt_iff {α : Type u_1} [LT α] {a : α} {x : } :
a < x ∀ (b : α), x = ba < b
theorem WithTop.lt_top_iff_ne_top {α : Type u_1} [LT α] {x : } :

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

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

Alias of the reverse direction of WithTop.monotone_map_iff.

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

Alias of the reverse direction of WithTop.strictMono_map_iff.

theorem WithTop.map_le_iff {α : Type u_1} {β : Type u_2} [] [] (f : αβ) (a : ) (b : ) (mono_iff : ∀ {a b : α}, f a f b a b) :
a b
theorem WithTop.coe_untop'_le {α : Type u_1} [] (a : ) (b : α) :
() a
@[simp]
theorem WithTop.coe_top_lt {α : Type u_1} [] [] {x : } :
< x x =
theorem WithTop.forall_lt_iff_eq_top {α : Type u_1} [] {x : } :
(∀ (y : α), y < x) x =
instance WithTop.semilatticeInf {α : Type u_1} [] :
Equations
• WithTop.semilatticeInf = let __src := WithTop.partialOrder;
theorem WithTop.coe_inf {α : Type u_1} [] (a : α) (b : α) :
(a b) = a b
instance WithTop.semilatticeSup {α : Type u_1} [] :
Equations
• WithTop.semilatticeSup = let __src := WithTop.partialOrder;
theorem WithTop.coe_sup {α : Type u_1} [] (a : α) (b : α) :
(a b) = a b
instance WithTop.lattice {α : Type u_1} [] :
Equations
• WithTop.lattice = let __src := WithTop.semilatticeSup; let __src_1 := WithTop.semilatticeInf; Lattice.mk
instance WithTop.distribLattice {α : Type u_1} [] :
Equations
• WithTop.distribLattice = let __src := WithTop.lattice;
instance WithTop.decidableEq {α : Type u_1} [] :
Equations
• WithTop.decidableEq =
instance WithTop.decidableLE {α : Type u_1} [LE α] [DecidableRel fun (x x_1 : α) => x x_1] :
DecidableRel fun (x x_1 : ) => x x_1
Equations
• x✝.decidableLE x =
instance WithTop.decidableLT {α : Type u_1} [LT α] [DecidableRel fun (x x_1 : α) => x < x_1] :
DecidableRel fun (x x_1 : ) => x < x_1
Equations
• x✝.decidableLT x =
instance WithTop.isTotal_le {α : Type u_1} [LE α] [IsTotal α fun (x x_1 : α) => x x_1] :
IsTotal () fun (x x_1 : ) => x x_1
Equations
• =
instance WithTop.linearOrder {α : Type u_1} [] :
Equations
• WithTop.linearOrder =
@[simp]
theorem WithTop.coe_min {α : Type u_1} [] (x : α) (y : α) :
(min x y) = min x y
@[simp]
theorem WithTop.coe_max {α : Type u_1} [] (x : α) (y : α) :
(max x y) = max x y
instance WithTop.instWellFoundedLT {α : Type u_1} [LT α] [] :
Equations
• =
instance WithTop.instWellFoundedGT {α : Type u_1} [LT α] [] :
Equations
• =
instance WithTop.trichotomous.lt {α : Type u_1} [] [IsTrichotomous α fun (x x_1 : α) => x < x_1] :
IsTrichotomous () fun (x x_1 : ) => x < x_1
Equations
• =
instance WithTop.IsWellOrder.lt {α : Type u_1} [] [IsWellOrder α fun (x x_1 : α) => x < x_1] :
IsWellOrder () fun (x x_1 : ) => x < x_1
Equations
• =
instance WithTop.trichotomous.gt {α : Type u_1} [] [IsTrichotomous α fun (x x_1 : α) => x > x_1] :
IsTrichotomous () fun (x x_1 : ) => x > x_1
Equations
• =
instance WithTop.IsWellOrder.gt {α : Type u_1} [] [IsWellOrder α fun (x x_1 : α) => x > x_1] :
IsWellOrder () fun (x x_1 : ) => x > x_1
Equations
• =
instance WithBot.trichotomous.lt {α : Type u_1} [] [h : IsTrichotomous α fun (x x_1 : α) => x < x_1] :
IsTrichotomous () fun (x x_1 : ) => x < x_1
Equations
• =
instance WithBot.isWellOrder.lt {α : Type u_1} [] [IsWellOrder α fun (x x_1 : α) => x < x_1] :
IsWellOrder () fun (x x_1 : ) => x < x_1
Equations
• =
instance WithBot.trichotomous.gt {α : Type u_1} [] [h : IsTrichotomous α fun (x x_1 : α) => x > x_1] :
IsTrichotomous () fun (x x_1 : ) => x > x_1
Equations
• =
instance WithBot.isWellOrder.gt {α : Type u_1} [] [h : IsWellOrder α fun (x x_1 : α) => x > x_1] :
IsWellOrder () fun (x x_1 : ) => x > x_1
Equations
• =
instance WithTop.instDenselyOrderedOfNoMaxOrder {α : Type u_1} [LT α] [] [] :
Equations
• =
theorem WithTop.lt_iff_exists_coe_btwn {α : Type u_1} [] [] [] {a : } {b : } :
a < b ∃ (x : α), a < x x < b
instance WithTop.noBotOrder {α : Type u_1} [LE α] [] [] :
Equations
• =
instance WithTop.noMinOrder {α : Type u_1} [LT α] [] [] :
Equations
• =