Documentation

Mathlib.Order.WithBot

WithBot, WithTop #

Adding a bot or a top to an order.

Main declarations #

@[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 : WithBot α), p x) p (x : α), p x
theorem WithBot.some_eq_coe {α : Type u_1} (a : α) :
Option.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.unbotD {α : Type u_1} (d : α) (x : WithBot α) :
α

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

Equations
@[deprecated WithBot.unbotD (since := "2025-02-06")]
def WithBot.unbot' {α : Type u_1} (d : α) (x : WithBot α) :
α

Alias of WithBot.unbotD.


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

Equations
@[simp]
theorem WithBot.unbotD_bot {α : Type u_5} (d : α) :
@[deprecated WithBot.unbotD_bot (since := "2025-02-06")]
theorem WithBot.unbot'_bot {α : Type u_5} (d : α) :

Alias of WithBot.unbotD_bot.

@[simp]
theorem WithBot.unbotD_coe {α : Type u_5} (d x : α) :
unbotD d x = x
@[deprecated WithBot.unbotD_coe (since := "2025-02-06")]
theorem WithBot.unbot'_coe {α : Type u_5} (d x : α) :
unbotD d x = x

Alias of WithBot.unbotD_coe.

theorem WithBot.coe_eq_coe {α : Type u_1} {a b : α} :
a = b a = b
theorem WithBot.unbotD_eq_iff {α : Type u_1} {d y : α} {x : WithBot α} :
unbotD d x = y x = y x = y = d
@[deprecated WithBot.unbotD_eq_iff (since := "2025-02-06")]
theorem WithBot.unbot'_eq_iff {α : Type u_1} {d y : α} {x : WithBot α} :
unbotD d x = y x = y x = y = d

Alias of WithBot.unbotD_eq_iff.

@[simp]
theorem WithBot.unbotD_eq_self_iff {α : Type u_1} {d : α} {x : WithBot α} :
unbotD d x = d x = d x =
@[deprecated WithBot.unbotD_eq_self_iff (since := "2025-02-06")]
theorem WithBot.unbot'_eq_self_iff {α : Type u_1} {d : α} {x : WithBot α} :
unbotD d x = d x = d x =

Alias of WithBot.unbotD_eq_self_iff.

theorem WithBot.unbotD_eq_unbotD_iff {α : Type u_1} {d : α} {x y : WithBot α} :
unbotD d x = unbotD d y x = y x = d y = x = y = d
@[deprecated WithBot.unbotD_eq_unbotD_iff (since := "2025-02-06")]
theorem WithBot.unbot'_eq_unbot'_iff {α : Type u_1} {d : α} {x y : WithBot α} :
unbotD d x = unbotD d y x = y x = d y = x = y = d

Alias of WithBot.unbotD_eq_unbotD_iff.

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_1} {β : Type u_2} (f : αβ) :
@[simp]
theorem WithBot.map_coe {α : Type u_1} {β : Type u_2} (f : αβ) (a : α) :
map f a = (f a)
@[simp]
theorem WithBot.map_eq_bot_iff {α : Type u_1} {β : Type u_2} {f : αβ} {a : WithBot α} :
map f a = a =
theorem WithBot.map_eq_some_iff {α : Type u_1} {β : Type u_2} {f : αβ} {y : β} {v : WithBot α} :
map f v = y (x : α), v = x f x = y
theorem WithBot.some_eq_map_iff {α : Type u_1} {β : Type u_2} {f : αβ} {y : β} {v : WithBot α} :
y = map f v (x : α), v = x f x = y
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 : α) :
map g₁ (map f₁ a) = map g₂ (map f₂ a)
def WithBot.map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} :
(αβγ)WithBot αWithBot βWithBot γ

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
theorem WithBot.map₂_coe_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (a : α) (b : β) :
map₂ f a b = (f a b)
@[simp]
theorem WithBot.map₂_bot_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (b : WithBot β) :
@[simp]
theorem WithBot.map₂_bot_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (a : WithBot α) :
@[simp]
theorem WithBot.map₂_coe_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (a : α) (b : WithBot β) :
map₂ f (↑a) b = map (fun (b : β) => f a b) b
@[simp]
theorem WithBot.map₂_coe_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (a : WithBot α) (b : β) :
map₂ f a b = 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 : WithBot α} {b : WithBot β} :
map₂ f a b = a = b =
theorem WithBot.ne_bot_iff_exists {α : Type u_1} {x : WithBot α} :
x (a : α), a = x
theorem WithBot.forall_ne_iff_eq_bot {α : Type u_1} {x : WithBot α} :
(∀ (a : α), a x) 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 α) (hx : x ) :
(x.unbot hx) = x
@[simp]
theorem WithBot.unbot_coe {α : Type u_1} (x : α) (h : x := ) :
(↑x).unbot h = x
instance WithBot.canLift {α : Type u_1} :
CanLift (WithBot α) α some fun (r : WithBot α) => r
instance WithBot.instTop {α : Type u_1} [Top α] :
Equations
@[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
theorem WithBot.unbot_eq_iff {α : Type u_1} {a : WithBot α} {b : α} (h : a ) :
a.unbot h = b a = b
theorem WithBot.eq_unbot_iff {α : Type u_1} {a : α} {b : WithBot α} (h : b ) :
a = b.unbot h a = b
def Equiv.withBotSubtypeNe {α : Type u_1} :
{ y : WithBot α // y } α

The equivalence between the non-bottom elements of WithBot α and α.

Equations
@[simp]
theorem Equiv.withBotSubtypeNe_symm_apply_coe {α : Type u_1} (x : α) :
(withBotSubtypeNe.symm x) = x
@[simp]
theorem Equiv.withBotSubtypeNe_apply {α : Type u_1} (x✝ : { y : WithBot α // y }) :
withBotSubtypeNe x✝ = match x✝ with | x, h => x.unbot h
@[instance 10]
instance WithBot.le {α : Type u_1} [LE α] :
LE (WithBot α)
Equations
theorem WithBot.le_def {α : Type u_1} [LE α] {x y : WithBot α} :
x y ∀ (a : α), x = a (b : α), y = b a b
@[simp]
theorem WithBot.coe_le_coe {α : Type u_1} {a b : α} [LE α] :
a b a b
theorem WithBot.not_coe_le_bot {α : Type u_1} [LE α] (a : α) :
¬a
instance WithBot.orderBot {α : Type u_1} [LE α] :
Equations
@[simp, deprecated WithBot.coe_le_coe "Don't mix Option and WithBot" (since := "2024-05-27")]
theorem WithBot.some_le_some {α : Type u_1} {a b : α} [LE α] :
@[simp, deprecated bot_le "Don't mix Option and WithBot" (since := "2024-05-27")]
theorem WithBot.none_le {α : Type u_1} [LE α] {a : WithBot α} :
instance WithBot.orderTop {α : Type u_1} [LE α] [OrderTop α] :
Equations
@[simp]
theorem WithBot.le_bot_iff {α : Type u_1} [LE α] {a : WithBot α} :

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 : Option α} :
b o → (a o a b)
theorem WithBot.coe_le_iff {α : Type u_1} {a : α} [LE α] {x : WithBot α} :
a x (b : α), x = b a b
theorem WithBot.le_coe_iff {α : Type u_1} {b : α} [LE α] {x : WithBot α} :
x b ∀ (a : α), x = aa b
theorem IsMax.withBot {α : Type u_1} {a : α} [LE α] (h : IsMax a) :
IsMax a
theorem WithBot.le_unbot_iff {α : Type u_1} {a : α} [LE α] {y : WithBot α} (hy : y ) :
a y.unbot hy a y
theorem WithBot.unbot_le_iff {α : Type u_1} {b : α} [LE α] {x : WithBot α} (hx : x ) :
x.unbot hx b x b
theorem WithBot.unbotD_le_iff {α : Type u_1} {a b : α} [LE α] {x : WithBot α} (hx : x = a b) :
unbotD a x b x b
@[deprecated WithBot.unbotD_le_iff (since := "2025-02-06")]
theorem WithBot.unbot'_le_iff {α : Type u_1} {a b : α} [LE α] {x : WithBot α} (hx : x = a b) :
unbotD a x b x b

Alias of WithBot.unbotD_le_iff.

@[instance 10]
instance WithBot.lt {α : Type u_1} [LT α] :
LT (WithBot α)
Equations
theorem WithBot.lt_def {α : Type u_1} [LT α] {x y : WithBot α} :
x < y (b : α), y = b ∀ (a : α), x = 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 : WithBot α) :
@[simp, deprecated WithBot.coe_lt_coe "Don't mix Option and WithBot" (since := "2024-05-27")]
theorem WithBot.some_lt_some {α : Type u_1} {a b : α} [LT α] :
@[simp, deprecated WithBot.bot_lt_coe "Don't mix Option and WithBot" (since := "2024-05-27")]
theorem WithBot.none_lt_some {α : Type u_1} [LT α] (a : α) :
none < a
@[simp, deprecated not_lt_bot "Don't mix Option and WithBot" (since := "2024-05-27")]
theorem WithBot.not_lt_none {α : Type u_1} [LT α] (a : WithBot α) :
theorem WithBot.lt_iff_exists_coe {α : Type u_1} [LT α] {x y : WithBot α} :
x < y (b : α), y = b x < b
theorem WithBot.lt_coe_iff {α : Type u_1} {b : α} [LT α] {x : WithBot α} :
x < b ∀ (a : α), x = aa < b
theorem WithBot.bot_lt_iff_ne_bot {α : Type u_1} [LT α] {x : WithBot α} :

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

theorem WithBot.lt_unbot_iff {α : Type u_1} {a : α} [LT α] {y : WithBot α} (hy : y ) :
a < y.unbot hy a < y
theorem WithBot.unbot_lt_iff {α : Type u_1} {b : α} [LT α] {x : WithBot α} (hx : x ) :
x.unbot hx < b x < b
theorem WithBot.unbotD_lt_iff {α : Type u_1} {a b : α} [LT α] {x : WithBot α} (hx : x = a < b) :
unbotD a x < b x < b
@[deprecated WithBot.unbotD_lt_iff (since := "2025-02-06")]
theorem WithBot.unbot'_lt_iff {α : Type u_1} {a b : α} [LT α] {x : WithBot α} (hx : x = a < b) :
unbotD a x < b x < b

Alias of WithBot.unbotD_lt_iff.

instance WithBot.preorder {α : Type u_1} [Preorder α] :
Equations
theorem WithBot.coe_strictMono {α : Type u_1} [Preorder α] :
StrictMono fun (a : α) => a
theorem WithBot.coe_mono {α : Type u_1} [Preorder α] :
Monotone fun (a : α) => a
theorem WithBot.monotone_iff {α : Type u_1} {β : Type u_2} [Preorder α] [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} [Preorder α] [Preorder β] {f : αβ} :
theorem Monotone.withBot_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : αβ} :

Alias of the reverse direction of WithBot.monotone_map_iff.

theorem WithBot.strictMono_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : WithBot αβ} :
StrictMono f (StrictMono fun (a : α) => f a) ∀ (x : α), f < f x
theorem WithBot.strictAnti_iff {α : Type u_1} {β : Type u_2} [Preorder α] [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} [Preorder α] [Preorder β] {f : αβ} :
theorem StrictMono.withBot_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : αβ} :

Alias of the reverse direction of WithBot.strictMono_map_iff.

theorem WithBot.map_le_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x y : WithBot α} (f : αβ) (mono_iff : ∀ {a b : α}, f a f b a b) :
map f x map f y x y
theorem WithBot.le_coe_unbotD {α : Type u_1} [Preorder α] (x : WithBot α) (b : α) :
x (unbotD b x)
@[deprecated WithBot.le_coe_unbotD (since := "2025-02-06")]
theorem WithBot.le_coe_unbot' {α : Type u_1} [Preorder α] (x : WithBot α) (b : α) :
x (unbotD b x)

Alias of WithBot.le_coe_unbotD.

@[simp]
theorem WithBot.lt_coe_bot {α : Type u_1} [Preorder α] {x : WithBot α} [OrderBot α] :
x < x =
theorem WithBot.forall_lt_iff_eq_bot {α : Type u_1} [Preorder α] {x : WithBot α} :
(∀ (b : α), x < b) x =
theorem WithBot.forall_le_iff_eq_bot {α : Type u_1} [Preorder α] {x : WithBot α} [NoMinOrder α] :
(∀ (b : α), x b) x =
Equations
  • One or more equations did not get rendered due to their size.
theorem WithBot.coe_sup {α : Type u_1} [SemilatticeSup α] (a b : α) :
↑(a b) = a b
Equations
theorem WithBot.coe_inf {α : Type u_1} [SemilatticeInf α] (a b : α) :
↑(a b) = a b
instance WithBot.decidableLE {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 x2] :
DecidableRel fun (x1 x2 : WithBot α) => x1 x2
Equations
instance WithBot.decidableLT {α : Type u_1} [LT α] [DecidableRel fun (x1 x2 : α) => x1 < x2] :
DecidableRel fun (x1 x2 : WithBot α) => x1 < x2
Equations
instance WithBot.isTotal_le {α : Type u_1} [LE α] [IsTotal α fun (x1 x2 : α) => x1 x2] :
IsTotal (WithBot α) fun (x1 x2 : WithBot α) => x1 x2
@[simp]
theorem WithBot.coe_min {α : Type u_1} [LinearOrder α] (a b : α) :
↑(a b) = a b
@[simp]
theorem WithBot.coe_max {α : Type u_1} [LinearOrder α] (a b : α) :
↑(a b) = a b
theorem WithBot.le_of_forall_lt_iff_le {α : Type u_1} [LinearOrder α] {x y : WithBot α} [DenselyOrdered α] [NoMinOrder α] :
(∀ (z : α), x < zy z) y x
theorem WithBot.ge_of_forall_gt_iff_ge {α : Type u_1} [LinearOrder α] {x y : WithBot α} [DenselyOrdered α] [NoMinOrder α] :
(∀ (z : α), z < xz y) x y
theorem WithBot.lt_iff_exists_coe_btwn {α : Type u_1} [Preorder α] [DenselyOrdered α] [NoMinOrder α] {a b : WithBot α} :
a < b (x : α), a < x x < b
instance WithBot.noTopOrder {α : Type u_1} [LE α] [NoTopOrder α] [Nonempty α] :
instance WithBot.noMaxOrder {α : Type u_1} [LT α] [NoMaxOrder α] [Nonempty α] :
theorem WithTop.coe_inj {α : Type u_1} {a b : α} :
a = b a = b
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 : WithTop α), p x) p (x : α), p x
theorem WithTop.some_eq_coe {α : Type u_1} (a : α) :
Option.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

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_apply_coe {α : Type u_1} (a : α) :
@[simp]
theorem WithTop.ofDual_apply_coe {α : Type u_1} (a : αᵒᵈ) :
def WithTop.untopD {α : Type u_1} (d : α) (x : WithTop α) :
α

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

Equations
@[deprecated WithTop.untopD (since := "2025-02-06")]
def WithTop.untop' {α : Type u_1} (d : α) (x : WithTop α) :
α

Alias of WithTop.untopD.


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

Equations
@[simp]
theorem WithTop.untopD_top {α : Type u_5} (d : α) :
@[deprecated WithTop.untopD_top (since := "2025-02-06")]
theorem WithTop.untop'_top {α : Type u_5} (d : α) :

Alias of WithTop.untopD_top.

@[simp]
theorem WithTop.untopD_coe {α : Type u_5} (d x : α) :
untopD d x = x
@[deprecated WithTop.untopD_coe (since := "2025-02-06")]
theorem WithTop.untop'_coe {α : Type u_5} (d x : α) :
untopD d x = x

Alias of WithTop.untopD_coe.

@[simp]
theorem WithTop.coe_eq_coe {α : Type u_1} {a b : α} :
a = b a = b
theorem WithTop.untopD_eq_iff {α : Type u_1} {d y : α} {x : WithTop α} :
untopD d x = y x = y x = y = d
@[deprecated WithTop.untopD_eq_iff (since := "2025-02-06")]
theorem WithTop.untop'_eq_iff {α : Type u_1} {d y : α} {x : WithTop α} :
untopD d x = y x = y x = y = d

Alias of WithTop.untopD_eq_iff.

@[simp]
theorem WithTop.untopD_eq_self_iff {α : Type u_1} {d : α} {x : WithTop α} :
untopD d x = d x = d x =
@[deprecated WithTop.untopD_eq_self_iff (since := "2025-02-06")]
theorem WithTop.untop'_eq_self_iff {α : Type u_1} {d : α} {x : WithTop α} :
untopD d x = d x = d x =

Alias of WithTop.untopD_eq_self_iff.

theorem WithTop.untopD_eq_untopD_iff {α : Type u_1} {d : α} {x y : WithTop α} :
untopD d x = untopD d y x = y x = d y = x = y = d
@[deprecated WithTop.untopD_eq_untopD_iff (since := "2025-02-06")]
theorem WithTop.untop'_eq_untop'_iff {α : Type u_1} {d : α} {x y : WithTop α} :
untopD d x = untopD d y x = y x = d y = x = y = d

Alias of WithTop.untopD_eq_untopD_iff.

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_1} {β : Type u_2} (f : αβ) :
@[simp]
theorem WithTop.map_coe {α : Type u_1} {β : Type u_2} (f : αβ) (a : α) :
map f a = (f a)
@[simp]
theorem WithTop.map_eq_top_iff {α : Type u_1} {β : Type u_2} {f : αβ} {a : WithTop α} :
map f a = a =
theorem WithTop.map_eq_some_iff {α : Type u_1} {β : Type u_2} {f : αβ} {y : β} {v : WithTop α} :
map f v = y (x : α), v = x f x = y
theorem WithTop.some_eq_map_iff {α : Type u_1} {β : Type u_2} {f : αβ} {y : β} {v : WithTop α} :
y = map f v (x : α), v = x f x = y
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 : α) :
map g₁ (map f₁ a) = map g₂ (map f₂ a)
def WithTop.map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} :
(αβγ)WithTop αWithTop βWithTop γ

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
theorem WithTop.map₂_coe_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (a : α) (b : β) :
map₂ f a b = (f a b)
@[simp]
theorem WithTop.map₂_top_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (b : WithTop β) :
@[simp]
theorem WithTop.map₂_top_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (a : WithTop α) :
@[simp]
theorem WithTop.map₂_coe_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (a : α) (b : WithTop β) :
map₂ f (↑a) b = map (fun (b : β) => f a b) b
@[simp]
theorem WithTop.map₂_coe_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (a : WithTop α) (b : β) :
map₂ f a b = 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 : WithTop α} {b : WithTop β} :
map₂ f a b = a = b =
theorem WithTop.map_toDual {α : Type u_1} {β : Type u_2} (f : αᵒᵈβᵒᵈ) (a : WithBot α) :
theorem WithTop.map_ofDual {α : Type u_1} {β : Type u_2} (f : αβ) (a : WithBot αᵒᵈ) :
theorem WithTop.toDual_map {α : Type u_1} {β : Type u_2} (f : αβ) (a : WithTop α) :
theorem WithTop.ne_top_iff_exists {α : Type u_1} {x : WithTop α} :
x (a : α), a = x
theorem WithTop.forall_ne_iff_eq_top {α : Type u_1} {x : WithTop α} :
(∀ (a : α), a x) 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
@[simp]
theorem WithTop.coe_untop {α : Type u_1} (x : WithTop α) (hx : x ) :
(x.untop hx) = x
@[simp]
theorem WithTop.untop_coe {α : Type u_1} (x : α) (h : x := ) :
(↑x).untop h = x
instance WithTop.canLift {α : Type u_1} :
CanLift (WithTop α) α some fun (r : WithTop α) => r
instance WithTop.instBot {α : Type u_1} [Bot α] :
Equations
@[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
theorem WithTop.untop_eq_iff {α : Type u_1} {a : WithTop α} {b : α} (h : a ) :
a.untop h = b a = b
theorem WithTop.eq_untop_iff {α : Type u_1} {a : α} {b : WithTop α} (h : b ) :
a = b.untop h a = b
def Equiv.withTopSubtypeNe {α : Type u_1} :
{ y : WithTop α // y } α

The equivalence between the non-top elements of WithTop α and α.

Equations
@[simp]
theorem Equiv.withTopSubtypeNe_apply {α : Type u_1} (x✝ : { y : WithTop α // y }) :
withTopSubtypeNe x✝ = match x✝ with | x, h => x.untop h
@[simp]
theorem Equiv.withTopSubtypeNe_symm_apply_coe {α : Type u_1} (x : α) :
(withTopSubtypeNe.symm x) = x
@[instance 10]
instance WithTop.le {α : Type u_1} [LE α] :
LE (WithTop α)
Equations
theorem WithTop.le_def {α : Type u_1} [LE α] {x y : WithTop α} :
x y ∀ (b : α), y = b (a : α), x = a a b
@[simp]
theorem WithTop.coe_le_coe {α : Type u_1} {a b : α} [LE α] :
a b a b
theorem WithTop.not_top_le_coe {α : Type u_1} [LE α] (a : α) :
¬ a
@[simp, deprecated WithTop.coe_le_coe "Don't mix Option and WithTop" (since := "2024-05-27")]
theorem WithTop.some_le_some {α : Type u_1} {a b : α} [LE α] :
instance WithTop.orderTop {α : Type u_1} [LE α] :
Equations
@[simp, deprecated le_top "Don't mix Option and WithTop" (since := "2024-05-27")]
theorem WithTop.le_none {α : Type u_1} [LE α] {a : WithTop α} :
instance WithTop.orderBot {α : Type u_1} [LE α] [OrderBot α] :
Equations
@[simp]
theorem WithTop.top_le_iff {α : Type u_1} [LE α] {a : WithTop α} :

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 : Option α} :
a o → (o b a b)
theorem WithTop.le_coe_iff {α : Type u_1} {b : α} [LE α] {x : WithTop α} :
x b (a : α), x = a a b
theorem WithTop.coe_le_iff {α : Type u_1} {a : α} [LE α] {x : WithTop α} :
a x ∀ (b : α), x = ba b
theorem IsMin.withTop {α : Type u_1} {a : α} [LE α] (h : IsMin a) :
IsMin a
theorem WithTop.untop_le_iff {α : Type u_1} {b : α} [LE α] {x : WithTop α} (hx : x ) :
x.untop hx b x b
theorem WithTop.le_untop_iff {α : Type u_1} {a : α} [LE α] {y : WithTop α} (hy : y ) :
a y.untop hy a y
theorem WithTop.le_untopD_iff {α : Type u_1} {a b : α} [LE α] {y : WithTop α} (hy : y = a b) :
a untopD b y a y
@[deprecated WithTop.le_untopD_iff (since := "2025-02-11")]
theorem WithTop.le_untop'_iff {α : Type u_1} {a b : α} [LE α] {y : WithTop α} (hy : y = a b) :
a untopD b y a y

Alias of WithTop.le_untopD_iff.

@[instance 10]
instance WithTop.lt {α : Type u_1} [LT α] :
LT (WithTop α)
Equations
theorem WithTop.lt_def {α : Type u_1} [LT α] {x y : WithTop α} :
x < y (a : α), x = a ∀ (b : α), y = ba < b
@[simp]
theorem WithTop.coe_lt_coe {α : Type u_1} {a b : α} [LT α] :
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 : WithTop α) :
@[simp, deprecated WithTop.coe_lt_coe "Don't mix Option and WithTop" (since := "2024-05-27")]
theorem WithTop.some_lt_some {α : Type u_1} {a b : α} [LT α] :
@[simp, deprecated WithTop.coe_lt_top "Don't mix Option and WithTop" (since := "2024-05-27")]
theorem WithTop.some_lt_none {α : Type u_1} [LT α] (a : α) :
@[simp, deprecated not_top_lt "Don't mix Option and WithTop" (since := "2024-05-27")]
theorem WithTop.not_none_lt {α : Type u_1} [LT α] (a : WithTop α) :
theorem WithTop.lt_iff_exists_coe {α : Type u_1} [LT α] {x y : WithTop α} :
x < y (a : α), x = a a < y
theorem WithTop.coe_lt_iff {α : Type u_1} {a : α} [LT α] {y : WithTop α} :
a < y ∀ (b : α), y = ba < b
theorem WithTop.lt_top_iff_ne_top {α : Type u_1} [LT α] {x : WithTop α} :

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

theorem WithTop.lt_untop_iff {α : Type u_1} {a : α} [LT α] {y : WithTop α} (hy : y ) :
a < y.untop hy a < y
theorem WithTop.untop_lt_iff {α : Type u_1} {b : α} [LT α] {x : WithTop α} (hx : x ) :
x.untop hx < b x < b
theorem WithTop.lt_untopD_iff {α : Type u_1} {a b : α} [LT α] {y : WithTop α} (hy : y = a < b) :
a < untopD b y a < y
@[deprecated WithTop.lt_untopD_iff (since := "2025-02-11")]
theorem WithTop.lt_untop'_iff {α : Type u_1} {a b : α} [LT α] {y : WithTop α} (hy : y = a < b) :
a < untopD b y a < y

Alias of WithTop.lt_untopD_iff.

instance WithTop.preorder {α : Type u_1} [Preorder α] :
Equations
theorem WithTop.coe_strictMono {α : Type u_1} [Preorder α] :
StrictMono fun (a : α) => a
theorem WithTop.coe_mono {α : Type u_1} [Preorder α] :
Monotone fun (a : α) => a
theorem WithTop.monotone_iff {α : Type u_1} {β : Type u_2} [Preorder α] [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} [Preorder α] [Preorder β] {f : αβ} :
theorem Monotone.withTop_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : αβ} :

Alias of the reverse direction of WithTop.monotone_map_iff.

theorem WithTop.strictMono_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : WithTop αβ} :
StrictMono f (StrictMono fun (a : α) => f a) ∀ (x : α), f x < f
theorem WithTop.strictAnti_iff {α : Type u_1} {β : Type u_2} [Preorder α] [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} [Preorder α] [Preorder β] {f : αβ} :
theorem StrictMono.withTop_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : αβ} :

Alias of the reverse direction of WithTop.strictMono_map_iff.

theorem WithTop.map_le_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x y : WithTop α} (f : αβ) (mono_iff : ∀ {a b : α}, f a f b a b) :
map f x map f y x y
theorem WithTop.coe_untopD_le {α : Type u_1} [Preorder α] (y : WithTop α) (a : α) :
(untopD a y) y
@[deprecated WithTop.coe_untopD_le (since := "2025-02-11")]
theorem WithTop.coe_untop'_le {α : Type u_1} [Preorder α] (y : WithTop α) (a : α) :
(untopD a y) y

Alias of WithTop.coe_untopD_le.

@[simp]
theorem WithTop.coe_top_lt {α : Type u_1} [Preorder α] {x : WithTop α} [OrderTop α] :
< x x =
theorem WithTop.forall_gt_iff_eq_top {α : Type u_1} [Preorder α] {y : WithTop α} :
(∀ (a : α), a < y) y =
theorem WithTop.forall_ge_iff_eq_top {α : Type u_1} [Preorder α] {y : WithTop α} [NoMaxOrder α] :
(∀ (a : α), a y) y =
Equations
  • One or more equations did not get rendered due to their size.
theorem WithTop.coe_inf {α : Type u_1} [SemilatticeInf α] (a b : α) :
↑(a b) = a b
Equations
theorem WithTop.coe_sup {α : Type u_1} [SemilatticeSup α] (a b : α) :
↑(a b) = a b
instance WithTop.decidableLE {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 x2] :
DecidableRel fun (x1 x2 : WithTop α) => x1 x2
Equations
instance WithTop.decidableLT {α : Type u_1} [LT α] [DecidableRel fun (x1 x2 : α) => x1 < x2] :
DecidableRel fun (x1 x2 : WithTop α) => x1 < x2
Equations
instance WithTop.isTotal_le {α : Type u_1} [LE α] [IsTotal α fun (x1 x2 : α) => x1 x2] :
IsTotal (WithTop α) fun (x1 x2 : WithTop α) => x1 x2
@[simp]
theorem WithTop.coe_min {α : Type u_1} [LinearOrder α] (a b : α) :
↑(a b) = a b
@[simp]
theorem WithTop.coe_max {α : Type u_1} [LinearOrder α] (a b : α) :
↑(a b) = a b
theorem WithTop.le_of_forall_lt_iff_le {α : Type u_1} [LinearOrder α] {x y : WithTop α} [DenselyOrdered α] [NoMaxOrder α] :
(∀ (b : α), x < by b) y x
theorem WithTop.ge_of_forall_gt_iff_ge {α : Type u_1} [LinearOrder α] {x y : WithTop α} [DenselyOrdered α] [NoMaxOrder α] :
(∀ (a : α), a < xa y) x y
instance WithTop.trichotomous.lt {α : Type u_1} [Preorder α] [IsTrichotomous α fun (x1 x2 : α) => x1 < x2] :
IsTrichotomous (WithTop α) fun (x1 x2 : WithTop α) => x1 < x2
instance WithTop.IsWellOrder.lt {α : Type u_1} [Preorder α] [IsWellOrder α fun (x1 x2 : α) => x1 < x2] :
IsWellOrder (WithTop α) fun (x1 x2 : WithTop α) => x1 < x2
instance WithTop.trichotomous.gt {α : Type u_1} [Preorder α] [IsTrichotomous α fun (x1 x2 : α) => x1 > x2] :
IsTrichotomous (WithTop α) fun (x1 x2 : WithTop α) => x1 > x2
instance WithTop.IsWellOrder.gt {α : Type u_1} [Preorder α] [IsWellOrder α fun (x1 x2 : α) => x1 > x2] :
IsWellOrder (WithTop α) fun (x1 x2 : WithTop α) => x1 > x2
instance WithBot.trichotomous.lt {α : Type u_1} [Preorder α] [h : IsTrichotomous α fun (x1 x2 : α) => x1 < x2] :
IsTrichotomous (WithBot α) fun (x1 x2 : WithBot α) => x1 < x2
instance WithBot.isWellOrder.lt {α : Type u_1} [Preorder α] [IsWellOrder α fun (x1 x2 : α) => x1 < x2] :
IsWellOrder (WithBot α) fun (x1 x2 : WithBot α) => x1 < x2
instance WithBot.trichotomous.gt {α : Type u_1} [Preorder α] [h : IsTrichotomous α fun (x1 x2 : α) => x1 > x2] :
IsTrichotomous (WithBot α) fun (x1 x2 : WithBot α) => x1 > x2
instance WithBot.isWellOrder.gt {α : Type u_1} [Preorder α] [h : IsWellOrder α fun (x1 x2 : α) => x1 > x2] :
IsWellOrder (WithBot α) fun (x1 x2 : WithBot α) => x1 > x2
theorem WithTop.lt_iff_exists_coe_btwn {α : Type u_1} [Preorder α] [DenselyOrdered α] [NoMaxOrder α] {a b : WithTop α} :
a < b (x : α), a < x x < b
instance WithTop.noBotOrder {α : Type u_1} [LE α] [NoBotOrder α] [Nonempty α] :
instance WithTop.noMinOrder {α : Type u_1} [LT α] [NoMinOrder α] [Nonempty α] :

(WithBot α)ᵒᵈ ≃ WithTop αᵒᵈ, (WithTop α)ᵒᵈ ≃ WithBot αᵒᵈ #

@[simp]
theorem WithBot.toDual_apply_coe {α : Type u_1} (a : α) :
@[simp]
theorem WithBot.ofDual_apply_coe {α : Type u_1} (a : αᵒᵈ) :
theorem WithBot.map_toDual {α : Type u_1} {β : Type u_2} (f : αᵒᵈβᵒᵈ) (a : WithTop α) :
theorem WithBot.map_ofDual {α : Type u_1} {β : Type u_2} (f : αβ) (a : WithTop αᵒᵈ) :
theorem WithBot.toDual_map {α : Type u_1} {β : Type u_2} (f : αβ) (a : WithBot α) :
theorem WithBot.ofDual_map {α : Type u_1} {β : Type u_2} (f : αᵒᵈβᵒᵈ) (a : WithBot αᵒᵈ) :
theorem WithBot.toDual_le_iff {α : Type u_1} [LE α] {x : WithBot α} {y : WithTop αᵒᵈ} :
theorem WithBot.le_toDual_iff {α : Type u_1} [LE α] {x : WithTop αᵒᵈ} {y : WithBot α} :
@[simp]
theorem WithBot.toDual_le_toDual_iff {α : Type u_1} [LE α] {x y : WithBot α} :
theorem WithBot.ofDual_le_iff {α : Type u_1} [LE α] {x : WithBot αᵒᵈ} {y : WithTop α} :
theorem WithBot.le_ofDual_iff {α : Type u_1} [LE α] {x : WithTop α} {y : WithBot αᵒᵈ} :
@[simp]
theorem WithTop.toDual_le_iff {α : Type u_1} [LE α] {x : WithTop α} {y : WithBot αᵒᵈ} :
theorem WithTop.le_toDual_iff {α : Type u_1} [LE α] {x : WithBot αᵒᵈ} {y : WithTop α} :
@[simp]
theorem WithTop.toDual_le_toDual_iff {α : Type u_1} [LE α] {x y : WithTop α} :
theorem WithTop.ofDual_le_iff {α : Type u_1} [LE α] {x : WithTop αᵒᵈ} {y : WithBot α} :
theorem WithTop.le_ofDual_iff {α : Type u_1} [LE α] {x : WithBot α} {y : WithTop αᵒᵈ} :
@[simp]
theorem WithBot.toDual_lt_iff {α : Type u_1} [LT α] {x : WithBot α} {y : WithTop αᵒᵈ} :
theorem WithBot.lt_toDual_iff {α : Type u_1} [LT α] {x : WithTop αᵒᵈ} {y : WithBot α} :
@[simp]
theorem WithBot.toDual_lt_toDual_iff {α : Type u_1} [LT α] {x y : WithBot α} :
theorem WithBot.ofDual_lt_iff {α : Type u_1} [LT α] {x : WithBot αᵒᵈ} {y : WithTop α} :
theorem WithBot.lt_ofDual_iff {α : Type u_1} [LT α] {x : WithTop α} {y : WithBot αᵒᵈ} :
@[simp]
theorem WithTop.toDual_lt_iff {α : Type u_1} [LT α] {x : WithTop α} {y : WithBot αᵒᵈ} :
theorem WithTop.lt_toDual_iff {α : Type u_1} [LT α] {x : WithBot αᵒᵈ} {y : WithTop α} :
@[simp]
theorem WithTop.toDual_lt_toDual_iff {α : Type u_1} [LT α] {x y : WithTop α} :
theorem WithTop.ofDual_lt_iff {α : Type u_1} [LT α] {x : WithTop αᵒᵈ} {y : WithBot α} :
theorem WithTop.lt_ofDual_iff {α : Type u_1} [LT α] {x : WithBot α} {y : WithTop αᵒᵈ} :
@[simp]