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.

instance WithBot.nontrivial {α : Type u_1} [Nonempty α] : Nontrivial (WithBot α)

instance WithTop.nontrivial {α : Type u_1} [Nonempty α] : Nontrivial (WithTop α)

instance WithBot.instUniqueOfIsEmpty {α : Type u_1} [IsEmpty α] : Unique (WithBot α)

instance WithTop.instUniqueOfIsEmpty {α : Type u_1} [IsEmpty α] : Unique (WithTop α)

theorem WithBot.coe_injective {α : Type u_1} : Function.Injective some

theorem WithTop.coe_injective {α : Type u_1} : Function.Injective some

@[simp]

theorem WithBot.coe_inj {α : Type u_1} {a b : α} : ↑a = ↑b ↔ a = b

@[simp]

theorem WithTop.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 WithTop.forall {α : Type u_1} {p : WithTop α → Prop} : (∀ (x : WithTop α), p x) ↔ p ⊤ ∧ ∀ (x : α), p ↑x

theorem WithBot.exists {α : Type u_1} {p : WithBot α → Prop} : (∃ (x : WithBot α), p x) ↔ p ⊥ ∨ ∃ (x : α), p ↑x

theorem WithTop.exists {α : Type u_1} {p : WithTop α → Prop} : (∃ (x : WithTop α), p x) ↔ p ⊤ ∨ ∃ (x : α), p ↑x

theorem WithBot.none_eq_bot {α : Type u_1} : none = ⊥

theorem WithTop.none_eq_top {α : Type u_1} : none = ⊤

theorem WithBot.some_eq_coe {α : Type u_1} (a : α) : Option.some a = ↑a

theorem WithTop.some_eq_coe {α : Type u_1} (a : α) : Option.some a = ↑a

@[simp]

theorem WithBot.bot_ne_coe {α : Type u_1} {a : α} : ⊥ ≠ ↑a

@[simp]

theorem WithTop.top_ne_coe {α : Type u_1} {a : α} : ⊤ ≠ ↑a

@[simp]

theorem WithBot.coe_ne_bot {α : Type u_1} {a : α} : ↑a ≠ ⊥

@[simp]

theorem WithTop.coe_ne_top {α : 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.

def WithTop.untopD {α : Type u_1} (d : α) (x : WithTop α) : α

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

@[simp]

theorem WithBot.unbotD_bot {α : Type u_5} (d : α) : unbotD d ⊥ = d

@[simp]

theorem WithTop.untopD_top {α : Type u_5} (d : α) : untopD d ⊤ = d

@[simp]

theorem WithBot.unbotD_coe {α : Type u_5} (d x : α) : unbotD d ↑x = x

@[simp]

theorem WithTop.untopD_coe {α : Type u_5} (d x : α) : untopD d ↑x = x

theorem WithBot.coe_eq_coe {α : Type u_1} {a b : α} : ↑a = ↑b ↔ a = b

theorem WithTop.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

theorem WithTop.untopD_eq_iff {α : Type u_1} {d y : α} {x : WithTop α} : untopD d x = y ↔ x = ↑y ∨ x = ⊤ ∧ y = d

@[simp]

theorem WithBot.unbotD_eq_self_iff {α : Type u_1} {d : α} {x : WithBot α} : unbotD d x = d ↔ x = ↑d ∨ x = ⊥

@[simp]

theorem WithTop.untopD_eq_self_iff {α : Type u_1} {d : α} {x : WithTop α} : untopD d x = d ↔ x = ↑d ∨ x = ⊤

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

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

def WithBot.map {α : Type u_1} {β : Type u_2} (f : α → β) : WithBot α → WithBot β

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

def WithTop.map {α : Type u_1} {β : Type u_2} (f : α → β) : WithTop α → WithTop β

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

@[simp]

theorem WithBot.map_bot {α : Type u_1} {β : Type u_2} (f : α → β) : map f ⊥ = ⊥

@[simp]

theorem WithTop.map_top {α : Type u_1} {β : Type u_2} (f : α → β) : map f ⊤ = ⊤

@[simp]

theorem WithBot.map_coe {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) : map f ↑a = ↑(f a)

@[simp]

theorem WithTop.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 = ⊥

@[simp]

theorem WithTop.map_eq_top_iff {α : Type u_1} {β : Type u_2} {f : α → β} {a : WithTop α} : 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 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 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 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

@[simp]

theorem WithBot.map_id {α : Type u_1} : map id = id

@[simp]

theorem WithTop.map_id {α : Type u_1} : map id = id

@[simp]

theorem WithBot.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : β → γ) (g : α → β) (a : WithBot α) : map h (map g a) = map (h ∘ g) a

@[simp]

theorem WithTop.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : β → γ) (g : α → β) (a : WithTop α) : map h (map g a) = map (h ∘ g) a

theorem WithBot.comp_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : β → γ) (g : α → β) (x : WithBot α) : map (h ∘ g) x = map h (map g x)

theorem WithTop.comp_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : β → γ) (g : α → β) (x : WithTop α) : map (h ∘ g) x = map h (map g x)

@[simp]

theorem WithBot.map_comp_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → γ) : map g ∘ map f = map (g ∘ f)

@[simp]

theorem WithTop.map_comp_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → γ) : map g ∘ map f = map (g ∘ f)

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)

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)

theorem WithBot.map_injective {α : Type u_1} {β : Type u_2} {f : α → β} (Hf : Function.Injective f) : Function.Injective (map f)

theorem WithTop.map_injective {α : Type u_1} {β : Type u_2} {f : α → β} (Hf : Function.Injective f) : Function.Injective (map f)

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 α × β → γ.

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 α × β → γ.

theorem WithBot.map₂_coe_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : α) (b : β) : map₂ f ↑a ↑b = ↑(f a b)

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 WithBot.map₂_bot_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (b : WithBot β) : map₂ f ⊥ b = ⊥

@[simp]

theorem WithTop.map₂_top_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (b : WithTop β) : map₂ f ⊤ b = ⊤

@[simp]

theorem WithBot.map₂_bot_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : WithBot α) : map₂ f a ⊥ = ⊥

@[simp]

theorem WithTop.map₂_top_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : WithTop α) : map₂ 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 = map (fun (b : β) => f a b) b

@[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 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 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 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 = ⊥

@[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 WithBot.ne_bot_iff_exists {α : Type u_1} {x : WithBot α} : x ≠ ⊥ ↔ ∃ (a : α), ↑a = x

theorem WithTop.ne_top_iff_exists {α : Type u_1} {x : WithTop α} : x ≠ ⊤ ↔ ∃ (a : α), ↑a = x

theorem WithBot.eq_bot_iff_forall_ne {α : Type u_1} {x : WithBot α} : x = ⊥ ↔ ∀ (a : α), ↑a ≠ x

theorem WithTop.eq_top_iff_forall_ne {α : Type u_1} {x : WithTop α} : x = ⊤ ↔ ∀ (a : α), ↑a ≠ x

theorem WithBot.forall_ne_bot {α : Type u_1} {p : WithBot α → Prop} : (∀ (x : WithBot α), x ≠ ⊥ → p x) ↔ ∀ (x : α), p ↑x

theorem WithTop.forall_ne_top {α : Type u_1} {p : WithTop α → Prop} : (∀ (x : WithTop α), x ≠ ⊤ → p x) ↔ ∀ (x : α), p ↑x

theorem WithBot.exists_ne_bot {α : Type u_1} {p : WithBot α → Prop} : (∃ (x : WithBot α), x ≠ ⊥ ∧ p x) ↔ ∃ (x : α), p ↑x

theorem WithTop.exists_ne_top {α : Type u_1} {p : WithTop α → Prop} : (∃ (x : WithTop α), x ≠ ⊤ ∧ p x) ↔ ∃ (x : α), p ↑x

def WithBot.unbot {α : Type u_1} (x : WithBot α) : x ≠ ⊥ → α

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

def WithTop.untop {α : Type u_1} (x : WithTop α) : x ≠ ⊤ → α

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

@[simp]

theorem WithBot.coe_unbot {α : Type u_1} (x : WithBot α) (hx : x ≠ ⊥) : ↑(x.unbot hx) = x

@[simp]

theorem WithTop.coe_untop {α : Type u_1} (x : WithTop α) (hx : x ≠ ⊤) : ↑(x.untop hx) = x

@[simp]

theorem WithBot.unbot_coe {α : Type u_1} (x : α) (h : ↑x ≠ ⊥ := ⋯) : (↑x).unbot h = x

@[simp]

theorem WithTop.untop_coe {α : Type u_1} (x : α) (h : ↑x ≠ ⊤ := ⋯) : (↑x).untop h = x

instance WithBot.canLift {α : Type u_1} : CanLift (WithBot α) α some fun (r : WithBot α) => r ≠ ⊥

instance WithTop.canLift {α : Type u_1} : CanLift (WithTop α) α some fun (r : WithTop α) => r ≠ ⊤

instance WithBot.instTop {α : Type u_1} [Top α] : Top (WithBot α)

instance WithTop.instBot {α : Type u_1} [Bot α] : Bot (WithTop α)

@[simp]

theorem WithBot.coe_top {α : Type u_1} [Top α] : ↑⊤ = ⊤

@[simp]

theorem WithTop.coe_bot {α : Type u_1} [Bot α] : ↑⊥ = ⊥

@[simp]

theorem WithBot.coe_eq_top {α : Type u_1} [Top α] {a : α} : ↑a = ⊤ ↔ a = ⊤

@[simp]

theorem WithTop.coe_eq_bot {α : Type u_1} [Bot α] {a : α} : ↑a = ⊥ ↔ a = ⊥

@[simp]

theorem WithBot.top_eq_coe {α : Type u_1} [Top α] {a : α} : ⊤ = ↑a ↔ ⊤ = a

@[simp]

theorem WithTop.bot_eq_coe {α : Type u_1} [Bot α] {a : α} : ⊥ = ↑a ↔ ⊥ = a

theorem WithBot.unbot_eq_iff {α : Type u_1} {a : WithBot α} {b : α} (h : a ≠ ⊥) : a.unbot h = b ↔ a = ↑b

theorem WithTop.untop_eq_iff {α : Type u_1} {a : WithTop α} {b : α} (h : a ≠ ⊤) : a.untop h = b ↔ a = ↑b

theorem WithBot.eq_unbot_iff {α : Type u_1} {a : α} {b : WithBot α} (h : b ≠ ⊥) : a = b.unbot h ↔ ↑a = b

theorem WithTop.eq_untop_iff {α : Type u_1} {a : α} {b : WithTop α} (h : b ≠ ⊤) : a = b.untop h ↔ ↑a = b

def Equiv.withBotSubtypeNe {α : Type u_1} : { y : WithBot α // y ≠ ⊥ } ≃ α

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

def Equiv.withTopSubtypeNe {α : Type u_1} : { y : WithTop α // y ≠ ⊤ } ≃ α

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

@[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.withBotSubtypeNe_symm_apply_coe {α : Type u_1} (x : α) : ↑(withBotSubtypeNe.symm x) = ↑x

@[simp]

theorem Equiv.withTopSubtypeNe_symm_apply_coe {α : Type u_1} (x : α) : ↑(withTopSubtypeNe.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

@[reducible, inline]

noncomputable abbrev WithBot.unbotA {α : Type u_1} [Nonempty α] : WithBot α → α

Function that sends an element of WithBot α to α, with an arbitrary default value for ⊥.

@[reducible, inline]

noncomputable abbrev WithTop.untopA {α : Type u_1} [Nonempty α] : WithTop α → α

Function that sends an element of WithTop α to α, with an arbitrary default value for ⊤.

theorem WithBot.unbotA_eq_unbot {α : Type u_1} [Nonempty α] {a : WithBot α} (ha : a ≠ ⊥) : a.unbotA = a.unbot ha

theorem WithTop.untopA_eq_untop {α : Type u_1} [Nonempty α] {a : WithTop α} (ha : a ≠ ⊤) : a.untopA = a.untop ha

def Equiv.withBotCongr {α : Type u_1} {β : Type u_2} (e : α ≃ β) : WithBot α ≃ WithBot β

A universe-polymorphic version of EquivFunctor.mapEquiv WithBot e.

def Equiv.withTopCongr {α : Type u_1} {β : Type u_2} (e : α ≃ β) : WithTop α ≃ WithTop β

A universe-polymorphic version of EquivFunctor.mapEquiv WithTop e.

@[simp]

theorem Equiv.withTopCongr_apply {α : Type u_1} {β : Type u_2} (e : α ≃ β) (a✝ : WithTop α) : e.withTopCongr a✝ = WithTop.map (⇑e) a✝

@[simp]

theorem Equiv.withBotCongr_apply {α : Type u_1} {β : Type u_2} (e : α ≃ β) (a✝ : WithBot α) : e.withBotCongr a✝ = WithBot.map (⇑e) a✝

@[simp]

theorem Equiv.withBotCongr_refl {α : Type u_1} : (Equiv.refl α).withBotCongr = Equiv.refl (WithBot α)

@[simp]

theorem Equiv.withTopCongr_refl {α : Type u_1} : (Equiv.refl α).withTopCongr = Equiv.refl (WithTop α)

@[simp]

theorem Equiv.withBotCongr_symm {α : Type u_1} {β : Type u_2} (e : α ≃ β) : e.symm.withBotCongr = e.withBotCongr.symm

@[simp]

theorem Equiv.withTopCongr_symm {α : Type u_1} {β : Type u_2} (e : α ≃ β) : e.symm.withTopCongr = e.withTopCongr.symm

@[simp]

theorem Equiv.withBotCongr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e₁ : α ≃ β) (e₂ : β ≃ γ) : (e₁.trans e₂).withBotCongr = e₁.withBotCongr.trans e₂.withBotCongr

@[simp]

theorem Equiv.withTopCongr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e₁ : α ≃ β) (e₂ : β ≃ γ) : (e₁.trans e₂).withTopCongr = e₁.withTopCongr.trans e₂.withTopCongr

inductive WithBot.LE {α : Type u_1} [LE α] : WithBot α → WithBot α → Prop

Auxiliary definition for the order on WithBot.

• bot_le {α : Type u_1} [LE α] (x : WithBot α) : ⊥.LE x
• coe_le_coe {α : Type u_1} [LE α] {a b : α} : a ≤ b → (↑a).LE ↑b

theorem WithBot.le_def_aux {α : Type u_1} [LE α] (a✝ a✝¹ : WithBot α) : a✝.LE a✝¹ ↔ a✝ = ⊥ ∨ ∃ (a : α) (b : α), a ≤ b ∧ a✝ = ↑a ∧ a✝¹ = ↑b

@[instance 10]

instance WithBot.instLE {α : Type u_1} [LE α] : LE (WithBot α)

The order on WithBot α, defined by ⊥ ≤ y and a ≤ b → ↑a ≤ ↑b.

Equivalently, x ≤ y can be defined as ∀ a : α, x = ↑a → ∃ b : α, y = ↑b ∧ a ≤ b, see le_iff_forall. The definition as an inductive predicate is preferred since it cannot be accidentally unfolded too far.

@[instance 10]

instance WithTop.instLE {α : Type u_1} [LE α] : LE (WithTop α)

The order on WithTop α, defined by x ≤ ⊤ and a ≤ b → ↑a ≤ ↑b.

Equivalently, x ≤ y can be defined as ∀ b : α, y = ↑b → ∃ a : α, x = ↑a ∧ a ≤ b, see le_iff_forall. The definition as an inductive predicate is preferred since it cannot be accidentally unfolded too far.

theorem WithBot.le_def {α : Type u_1} [LE α] {x y : WithBot α} : x ≤ y ↔ x = ⊥ ∨ ∃ (a : α) (b : α), a ≤ b ∧ x = ↑a ∧ y = ↑b

theorem WithTop.le_def' {α : Type u_1} [LE α] {x y : WithTop α} : x ≤ y ↔ y = ⊤ ∨ ∃ (b : α), ∃ a ≤ b, y = ↑b ∧ x = ↑a

theorem WithTop.le_def {α : Type u_1} [LE α] {x y : WithTop α} : x ≤ y ↔ y = ⊤ ∨ ∃ (a : α) (b : α), a ≤ b ∧ x = ↑a ∧ y = ↑b

theorem WithBot.le_def' {α : Type u_1} [LE α] {x y : WithBot α} : y ≤ x ↔ y = ⊥ ∨ ∃ (a : α), ∃ b ≤ a, x = ↑a ∧ y = ↑b

inductive WithBot.LT {α : Type u_1} [LT α] : WithBot α → WithBot α → Prop

Auxiliary definition for the order on WithBot.

• bot_lt {α : Type u_1} [LT α] (b : α) : ⊥.LT ↑b
• coe_lt_coe {α : Type u_1} [LT α] {a b : α} : a < b → (↑a).LT ↑b

theorem WithBot.lt_def_aux {α : Type u_1} [LT α] (a✝ a✝¹ : WithBot α) : a✝.LT a✝¹ ↔ (∃ (b : α), a✝ = ⊥ ∧ a✝¹ = ↑b) ∨ ∃ (a : α) (b : α), a < b ∧ a✝ = ↑a ∧ a✝¹ = ↑b

@[instance 10]

instance WithBot.instLT {α : Type u_1} [LT α] : LT (WithBot α)

The order on WithBot α, defined by ⊥ < ↑a and a < b → ↑a < ↑b.

Equivalently, x < y can be defined as ∃ b : α, y = ↑b ∧ ∀ a : α, x = ↑a → a < b, see lt_iff_exists. The definition as an inductive predicate is preferred since it cannot be accidentally unfolded too far.

@[instance 10]

instance WithTop.instLT {α : Type u_1} [LT α] : LT (WithTop α)

The order on WithTop α, defined by ↑a < ⊤ and a < b → ↑a < ↑b.

Equivalently, x < y can be defined as ∃ a : α, x = ↑a ∧ ∀ b : α, y = ↑b → a < b, see le_if_forall. The definition as an inductive predicate is preferred since it cannot be accidentally unfolded too far.

theorem WithBot.lt_def {α : Type u_1} [LT α] {x y : WithBot α} : x < y ↔ (x = ⊥ ∧ ∃ (b : α), y = ↑b) ∨ ∃ (a : α) (b : α), a < b ∧ x = ↑a ∧ y = ↑b

theorem WithTop.lt_def' {α : Type u_1} [LT α] {x y : WithTop α} : x < y ↔ (y = ⊤ ∧ ∃ (a : α), x = ↑a) ∨ ∃ (b : α), ∃ a < b, y = ↑b ∧ x = ↑a

theorem WithTop.lt_def {α : Type u_1} [LT α] {x y : WithTop α} : x < y ↔ (∃ (a : α), x = ↑a) ∧ y = ⊤ ∨ ∃ (a : α) (b : α), a < b ∧ x = ↑a ∧ y = ↑b

theorem WithBot.lt_def' {α : Type u_1} [LT α] {x y : WithBot α} : y < x ↔ (∃ (a : α), x = ↑a) ∧ y = ⊥ ∨ ∃ (a : α), ∃ b < a, x = ↑a ∧ y = ↑b

theorem WithBot.le_iff_forall {α : Type u_1} [LE α] {x y : WithBot α} : x ≤ y ↔ ∀ (a : α), x = ↑a → ∃ (b : α), y = ↑b ∧ a ≤ b

theorem WithTop.le_iff_forall {α : Type u_1} [LE α] {x y : WithTop α} : y ≤ x ↔ ∀ (a : α), x = ↑a → ∃ (b : α), y = ↑b ∧ b ≤ a

@[simp]

theorem WithBot.coe_le_coe {α : Type u_1} {a b : α} [LE α] : ↑a ≤ ↑b ↔ a ≤ b

@[simp]

theorem WithTop.coe_le_coe {α : Type u_1} {a b : α} [LE α] : ↑b ≤ ↑a ↔ b ≤ a

theorem WithBot.not_coe_le_bot {α : Type u_1} [LE α] (a : α) : ¬↑a ≤ ⊥

theorem WithTop.not_top_le_coe {α : Type u_1} [LE α] (a : α) : ¬⊤ ≤ ↑a

instance WithBot.instOrderBot {α : Type u_1} [LE α] : OrderBot (WithBot α)

instance WithTop.instOrderTop {α : Type u_1} [LE α] : OrderTop (WithTop α)

instance WithBot.instOrderTop {α : Type u_1} [LE α] [OrderTop α] : OrderTop (WithBot α)

instance WithTop.instOrderBot {α : Type u_1} [LE α] [OrderBot α] : OrderBot (WithTop α)

instance WithBot.instBoundedOrder {α : Type u_1} [LE α] [OrderTop α] : BoundedOrder (WithBot α)

instance WithTop.instBoundedOrder {α : Type u_1} [LE α] [OrderBot α] : BoundedOrder (WithTop α)

@[simp]

theorem WithBot.le_bot_iff {α : Type u_1} [LE α] {x : WithBot α} : x ≤ ⊥ ↔ x = ⊥

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

@[simp]

theorem WithTop.top_le_iff {α : Type u_1} [LE α] {x : WithTop α} : ⊤ ≤ x ↔ x = ⊤

There is a general version top_le_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 WithTop.le_coe {α : Type u_1} {a b : α} [LE α] {o : Option α} : b ∈ o → (o ≤ ↑a ↔ b ≤ a)

theorem WithBot.coe_le_iff {α : Type u_1} {a : α} [LE α] {x : WithBot α} : ↑a ≤ x ↔ ∃ (b : α), x = ↑b ∧ a ≤ b

theorem WithTop.le_coe_iff {α : Type u_1} {a : α} [LE α] {x : WithTop α} : x ≤ ↑a ↔ ∃ (b : α), x = ↑b ∧ b ≤ a

theorem WithBot.le_coe_iff {α : Type u_1} {b : α} [LE α] {x : WithBot α} : x ≤ ↑b ↔ ∀ (a : α), x = ↑a → a ≤ b

theorem WithTop.coe_le_iff {α : Type u_1} {b : α} [LE α] {x : WithTop α} : ↑b ≤ x ↔ ∀ (a : α), x = ↑a → b ≤ a

theorem IsMax.withBot {α : Type u_1} {a : α} [LE α] (h : IsMax a) : IsMax ↑a

theorem IsMin.withTop {α : Type u_1} {a : α} [LE α] (h : IsMin a) : IsMin ↑a

@[simp]

theorem WithBot.le_unbot_iff {α : Type u_1} {a : α} [LE α] {x : WithBot α} (hx : x ≠ ⊥) : a ≤ x.unbot hx ↔ ↑a ≤ x

@[simp]

theorem WithTop.untop_le_iff {α : Type u_1} {a : α} [LE α] {x : WithTop α} (hx : x ≠ ⊤) : x.untop hx ≤ a ↔ x ≤ ↑a

@[simp]

theorem WithBot.unbot_le_iff {α : Type u_1} {a : α} [LE α] {x : WithBot α} (hx : x ≠ ⊥) : x.unbot hx ≤ a ↔ x ≤ ↑a

@[simp]

theorem WithTop.le_untop_iff {α : Type u_1} {a : α} [LE α] {x : WithTop α} (hx : x ≠ ⊤) : a ≤ x.untop hx ↔ ↑a ≤ x

theorem WithBot.unbot_le_unbot_iff {α : Type u_1} [LE α] {x y : WithBot α} (hx : x ≠ ⊥) (hy : y ≠ ⊥) : x.unbot hx ≤ y.unbot hy ↔ x ≤ y

theorem WithTop.untop_le_untop_iff {α : Type u_1} [LE α] {x y : WithTop α} (hy : y ≠ ⊤) (hx : x ≠ ⊤) : y.untop hy ≤ x.untop hx ↔ y ≤ x

theorem WithBot.unbot_mono {α : Type u_1} [LE α] {x y : WithBot α} (hx : x ≠ ⊥) (hy : y ≠ ⊥) : x ≤ y → x.unbot hx ≤ y.unbot hy

Alias of the reverse direction of WithBot.unbot_le_unbot_iff.

theorem WithTop.untop_mono {α : Type u_1} [LE α] {x y : WithTop α} (hx : x ≠ ⊤) (hy : y ≠ ⊤) : y ≤ x → y.untop hy ≤ x.untop hx

@[deprecated WithBot.unbot_le_unbot_iff (since := "2025-12-05")]

theorem WithBot.unbot_le_unbot {α : Type u_1} [LE α] {x y : WithBot α} (hx : x ≠ ⊥) (hy : y ≠ ⊥) : x.unbot hx ≤ y.unbot hy ↔ x ≤ y

Alias of WithBot.unbot_le_unbot_iff.

theorem WithBot.le_unbotD_iff {α : Type u_1} {a b : α} [LE α] {x : WithBot α} (hx : x ≠ ⊥) : b ≤ unbotD a x ↔ ↑b ≤ x

theorem WithTop.untopD_le_iff {α : Type u_1} {a b : α} [LE α] {x : WithTop α} (hx : x ≠ ⊤) : untopD a x ≤ 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

theorem WithTop.le_untopD_iff {α : Type u_1} {a b : α} [LE α] {x : WithTop α} (hx : x = ⊤ → b ≤ a) : b ≤ untopD a x ↔ ↑b ≤ x

theorem WithBot.unbotD_mono {α : Type u_1} {a : α} [LE α] {x y : WithBot α} (hx : x ≠ ⊥) (h : x ≤ y) : unbotD a x ≤ unbotD a y

theorem WithTop.untopD_mono {α : Type u_1} {a : α} [LE α] {x y : WithTop α} (hx : x ≠ ⊤) (h : y ≤ x) : untopD a y ≤ untopD a x

theorem WithBot.le_unbotA_iff {α : Type u_1} {a : α} [LE α] {x : WithBot α} [Nonempty α] (hx : x ≠ ⊥) : a ≤ x.unbotA ↔ ↑a ≤ x

theorem WithTop.untopA_le_iff {α : Type u_1} {a : α} [LE α] {x : WithTop α} [Nonempty α] (hx : x ≠ ⊤) : x.untopA ≤ a ↔ x ≤ ↑a

theorem WithBot.unbotA_le_iff {α : Type u_1} {a : α} [LE α] {x : WithBot α} [Nonempty α] (hx : x ≠ ⊥) : x.unbotA ≤ a ↔ x ≤ ↑a

theorem WithTop.le_untopA_iff {α : Type u_1} {a : α} [LE α] {x : WithTop α} [Nonempty α] (hx : x ≠ ⊤) : a ≤ x.untopA ↔ ↑a ≤ x

theorem WithBot.unbotA_mono {α : Type u_1} [LE α] {x y : WithBot α} [Nonempty α] (hy : x ≠ ⊥) (h : x ≤ y) : x.unbotA ≤ y.unbotA

theorem WithTop.untopA_mono {α : Type u_1} [LE α] {x y : WithTop α} [Nonempty α] (hy : x ≠ ⊤) (h : y ≤ x) : y.untopA ≤ x.untopA

theorem WithBot.lt_iff_exists {α : Type u_1} [LT α] {x y : WithBot α} : x < y ↔ ∃ (b : α), y = ↑b ∧ ∀ (a : α), x = ↑a → a < b

theorem WithTop.lt_iff_exists {α : Type u_1} [LT α] {x y : WithTop α} : y < x ↔ ∃ (b : α), y = ↑b ∧ ∀ (a : α), x = ↑a → b < a

@[simp]

theorem WithBot.coe_lt_coe {α : Type u_1} {a b : α} [LT α] : ↑a < ↑b ↔ a < b

@[simp]

theorem WithTop.coe_lt_coe {α : Type u_1} {a b : α} [LT α] : ↑b < ↑a ↔ b < a

@[simp]

theorem WithBot.bot_lt_coe {α : Type u_1} [LT α] (a : α) : ⊥ < ↑a

@[simp]

theorem WithTop.coe_lt_top {α : Type u_1} [LT α] (a : α) : ↑a < ⊤

@[simp]

theorem WithBot.not_lt_bot {α : Type u_1} [LT α] (a : WithBot α) : ¬a < ⊥

@[simp]

theorem WithTop.not_top_lt {α : Type u_1} [LT α] (a : WithTop α) : ¬⊤ < a

theorem WithBot.lt_iff_exists_coe {α : Type u_1} [LT α] {x y : WithBot α} : x < y ↔ ∃ (b : α), y = ↑b ∧ x < ↑b

theorem WithTop.lt_iff_exists_coe {α : Type u_1} [LT α] {x y : WithTop α} : y < x ↔ ∃ (b : α), y = ↑b ∧ ↑b < x

theorem WithBot.lt_coe_iff {α : Type u_1} {b : α} [LT α] {x : WithBot α} : x < ↑b ↔ ∀ (a : α), x = ↑a → a < b

theorem WithTop.coe_lt_iff {α : Type u_1} {b : α} [LT α] {x : WithTop α} : ↑b < x ↔ ∀ (a : α), x = ↑a → b < a

theorem WithBot.bot_lt_iff_ne_bot {α : Type u_1} [LT α] {x : WithBot α} : ⊥ < x ↔ x ≠ ⊥

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

theorem WithTop.lt_top_iff_ne_top {α : Type u_1} [LT α] {x : WithTop α} : x < ⊤ ↔ x ≠ ⊤

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

@[simp]

theorem WithBot.lt_unbot_iff {α : Type u_1} {a : α} [LT α] {x : WithBot α} (hx : x ≠ ⊥) : a < x.unbot hx ↔ ↑a < x

@[simp]

theorem WithTop.untop_lt_iff {α : Type u_1} {a : α} [LT α] {x : WithTop α} (hx : x ≠ ⊤) : x.untop hx < a ↔ x < ↑a

@[simp]

theorem WithBot.unbot_lt_iff {α : Type u_1} {b : α} [LT α] {x : WithBot α} (hx : x ≠ ⊥) : x.unbot hx < b ↔ x < ↑b

@[simp]

theorem WithTop.lt_untop_iff {α : Type u_1} {b : α} [LT α] {x : WithTop α} (hx : x ≠ ⊤) : b < x.untop hx ↔ ↑b < x

theorem WithBot.unbot_lt_unbot_iff {α : Type u_1} [LT α] {x y : WithBot α} (hx : x ≠ ⊥) (hy : y ≠ ⊥) : x.unbot hx < y.unbot hy ↔ x < y

theorem WithTop.untop_lt_untop_iff {α : Type u_1} [LT α] {x y : WithTop α} (hy : y ≠ ⊤) (hx : x ≠ ⊤) : y.untop hy < x.untop hx ↔ y < x

@[deprecated WithBot.unbot_lt_unbot_iff (since := "2025-12-05")]

theorem WithBot.unbot_lt_unbot {α : Type u_1} [LT α] {x y : WithBot α} (hx : x ≠ ⊥) (hy : y ≠ ⊥) : x.unbot hx < y.unbot hy ↔ x < y

Alias of WithBot.unbot_lt_unbot_iff.

theorem WithBot.lt_unbotD_iff {α : Type u_1} {a b : α} [LT α] {x : WithBot α} (hx : x ≠ ⊥) : b < unbotD a x ↔ ↑b < x

theorem WithTop.untopD_lt_iff {α : Type u_1} {a b : α} [LT α] {x : WithTop α} (hx : x ≠ ⊤) : untopD a x < 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

theorem WithTop.lt_untopD_iff {α : Type u_1} {a b : α} [LT α] {x : WithTop α} (hx : x = ⊤ → b < a) : b < untopD a x ↔ ↑b < x

theorem WithBot.lt_unbotA_iff {α : Type u_1} {a : α} [LT α] {x : WithBot α} [Nonempty α] (hx : x ≠ ⊥) : a < x.unbotA ↔ ↑a < x

theorem WithTop.untopA_lt_iff {α : Type u_1} {a : α} [LT α] {x : WithTop α} [Nonempty α] (hx : x ≠ ⊤) : x.untopA < a ↔ x < ↑a

theorem WithBot.unbotA_lt_iff {α : Type u_1} {a : α} [LT α] {x : WithBot α} [Nonempty α] (hx : x ≠ ⊥) : x.unbotA < a ↔ x < ↑a

theorem WithTop.lt_untopA_iff {α : Type u_1} {a : α} [LT α] {x : WithTop α} [Nonempty α] (hx : x ≠ ⊤) : a < x.untopA ↔ ↑a < x

instance WithBot.instPreorder {α : Type u_1} [Preorder α] : Preorder (WithBot α)

instance WithTop.instPreorder {α : Type u_1} [Preorder α] : Preorder (WithTop α)

theorem WithBot.coe_strictMono {α : Type u_1} [Preorder α] : StrictMono fun (a : α) => ↑a

theorem WithTop.coe_strictMono {α : Type u_1} [Preorder α] : StrictMono fun (a : α) => ↑a

theorem WithBot.coe_mono {α : Type u_1} [Preorder α] : Monotone fun (a : α) => ↑a

theorem WithTop.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

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 WithBot.monotone_map_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} : Monotone (map f) ↔ Monotone f

@[simp]

theorem WithTop.monotone_map_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} : Monotone (map f) ↔ Monotone f

theorem Monotone.withBot_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} : Monotone f → Monotone (WithBot.map f)

Alias of the reverse direction of WithBot.monotone_map_iff.

theorem Monotone.withTop_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} : Monotone f → Monotone (WithTop.map f)

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 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 WithBot.strictAnti_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : WithBot α → β} : StrictAnti f ↔ (StrictAnti 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 WithBot.strictMono_map_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} : StrictMono (map f) ↔ StrictMono f

@[simp]

theorem WithTop.strictMono_map_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} : StrictMono (map f) ↔ StrictMono f

theorem StrictMono.withBot_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} : StrictMono f → StrictMono (WithBot.map f)

Alias of the reverse direction of WithBot.strictMono_map_iff.

theorem StrictMono.withTop_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} : StrictMono f → StrictMono (WithTop.map f)

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 WithTop.map_le_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x y : WithTop α} (f : α → β) (mono_iff : ∀ {a b : α}, f b ≤ f a ↔ b ≤ a) : map f y ≤ map f x ↔ y ≤ x

theorem WithBot.le_coe_unbotD {α : Type u_1} [Preorder α] (x : WithBot α) (b : α) : x ≤ ↑(unbotD b x)

theorem WithTop.coe_untopD_le {α : Type u_1} [Preorder α] (x : WithTop α) (b : α) : ↑(untopD b x) ≤ x

@[simp]

theorem WithBot.lt_coe_bot {α : Type u_1} [Preorder α] {x : WithBot α} [OrderBot α] : x < ↑⊥ ↔ x = ⊥

@[simp]

theorem WithTop.coe_top_lt {α : Type u_1} [Preorder α] {x : WithTop α} [OrderTop α] : ↑⊤ < x ↔ x = ⊤

theorem WithBot.eq_bot_iff_forall_lt {α : Type u_1} [Preorder α] {x : WithBot α} : x = ⊥ ↔ ∀ (b : α), x < ↑b

theorem WithTop.eq_top_iff_forall_gt {α : Type u_1} [Preorder α] {x : WithTop α} : x = ⊤ ↔ ∀ (b : α), ↑b < x

theorem WithBot.eq_bot_iff_forall_le {α : Type u_1} [Preorder α] {x : WithBot α} [NoBotOrder α] : x = ⊥ ↔ ∀ (b : α), x ≤ ↑b

theorem WithTop.eq_top_iff_forall_ge {α : Type u_1} [Preorder α] {x : WithTop α} [NoTopOrder α] : x = ⊤ ↔ ∀ (b : α), ↑b ≤ x

theorem WithBot.forall_coe_le_iff_le {α : Type u_1} [Preorder α] {x y : WithBot α} [NoBotOrder α] : (∀ (a : α), ↑a ≤ x → ↑a ≤ y) ↔ x ≤ y

theorem WithTop.forall_le_coe_iff_le {α : Type u_1} [Preorder α] {x y : WithTop α} [NoTopOrder α] : (∀ (a : α), x ≤ ↑a → y ≤ ↑a) ↔ y ≤ x

theorem WithBot.forall_le_coe_iff_le {α : Type u_1} [Preorder α] {x y : WithBot α} [NoBotOrder α] : (∀ (a : α), y ≤ ↑a → x ≤ ↑a) ↔ x ≤ y

theorem WithTop.forall_coe_le_iff_le {α : Type u_1} [Preorder α] {x y : WithTop α} [NoTopOrder α] : (∀ (a : α), ↑a ≤ y → ↑a ≤ x) ↔ y ≤ x

@[simp]

theorem WithBot.forall_coe_lt {α : Type u_1} {a : α} [Preorder α] {p : WithBot α → Prop} : (∀ (x : WithBot α), ↑a < x → p x) ↔ ∀ (b : α), a < b → p ↑b

@[simp]

theorem WithTop.forall_lt_coe {α : Type u_1} {a : α} [Preorder α] {p : WithTop α → Prop} : (∀ x < ↑a, p x) ↔ ∀ b < a, p ↑b

@[simp]

theorem WithBot.exists_coe_lt {α : Type u_1} {a : α} [Preorder α] {p : WithBot α → Prop} : (∃ (x : WithBot α), ↑a < x ∧ p x) ↔ ∃ (b : α), a < b ∧ p ↑b

@[simp]

theorem WithTop.exists_lt_coe {α : Type u_1} {a : α} [Preorder α] {p : WithTop α → Prop} : (∃ x < ↑a, p x) ↔ ∃ b < a, p ↑b

@[simp]

theorem WithBot.forall_coe_le {α : Type u_1} {a : α} [Preorder α] {p : WithBot α → Prop} : (∀ (x : WithBot α), ↑a ≤ x → p x) ↔ ∀ (b : α), a ≤ b → p ↑b

@[simp]

theorem WithTop.forall_le_coe {α : Type u_1} {a : α} [Preorder α] {p : WithTop α → Prop} : (∀ x ≤ ↑a, p x) ↔ ∀ b ≤ a, p ↑b

@[simp]

theorem WithBot.exists_coe_le {α : Type u_1} {a : α} [Preorder α] {p : WithBot α → Prop} : (∃ (x : WithBot α), ↑a ≤ x ∧ p x) ↔ ∃ (b : α), a ≤ b ∧ p ↑b

@[simp]

theorem WithTop.exists_le_coe {α : Type u_1} {a : α} [Preorder α] {p : WithTop α → Prop} : (∃ x ≤ ↑a, p x) ↔ ∃ b ≤ a, p ↑b

instance WithBot.instPartialOrder {α : Type u_1} [PartialOrder α] : PartialOrder (WithBot α)

instance WithTop.instPartialOrder {α : Type u_1} [PartialOrder α] : PartialOrder (WithTop α)

theorem WithBot.le_unbotD {α : Type u_1} [PartialOrder α] {y : WithBot α} {a b : α} (hy : ↑b ≤ y) : b ≤ unbotD a y

theorem WithTop.untopD_le {α : Type u_1} [PartialOrder α] {y : WithTop α} {a b : α} (hy : y ≤ ↑b) : untopD a y ≤ b

theorem WithBot.le_unbotA {α : Type u_1} [PartialOrder α] {y : WithBot α} {b : α} [Nonempty α] (hy : ↑b ≤ y) : b ≤ y.unbotA

theorem WithTop.untopA_le {α : Type u_1} [PartialOrder α] {y : WithTop α} {b : α} [Nonempty α] (hy : y ≤ ↑b) : y.untopA ≤ b

theorem WithBot.eq_top_iff_forall_ge {α : Type u_1} [PartialOrder α] [Nonempty α] [NoTopOrder α] {x : WithBot (WithTop α)} : x = ⊤ ↔ ∀ (a : α), ↑↑a ≤ x

theorem WithTop.eq_bot_iff_forall_le {α : Type u_1} [PartialOrder α] [Nonempty α] [NoBotOrder α] {x : WithTop (WithBot α)} : x = ⊥ ↔ ∀ (a : α), x ≤ ↑↑a

theorem WithBot.eq_of_forall_coe_le_iff {α : Type u_1} [PartialOrder α] {x y : WithBot α} [NoBotOrder α] (h : ∀ (a : α), ↑a ≤ x ↔ ↑a ≤ y) : x = y

theorem WithTop.eq_of_forall_le_coe_iff {α : Type u_1} [PartialOrder α] {x y : WithTop α} [NoTopOrder α] (h : ∀ (a : α), x ≤ ↑a ↔ y ≤ ↑a) : x = y

theorem WithBot.eq_of_forall_le_coe_iff {α : Type u_1} [PartialOrder α] {x y : WithBot α} [NoBotOrder α] (h : ∀ (a : α), x ≤ ↑a ↔ y ≤ ↑a) : x = y

theorem WithTop.eq_of_forall_coe_le_iff {α : Type u_1} [PartialOrder α] {x y : WithTop α} [NoTopOrder α] (h : ∀ (a : α), ↑a ≤ x ↔ ↑a ≤ y) : x = y

instance WithBot.semilatticeSup {α : Type u_1} [SemilatticeSup α] : SemilatticeSup (WithBot α)

instance WithTop.semilatticeInf {α : Type u_1} [SemilatticeInf α] : SemilatticeInf (WithTop α)

instance WithBot.semilatticeInf {α : Type u_1} [SemilatticeInf α] : SemilatticeInf (WithBot α)

instance WithTop.semilatticeSup {α : Type u_1} [SemilatticeSup α] : SemilatticeSup (WithTop α)

@[simp]

theorem WithBot.coe_sup {α : Type u_1} [SemilatticeSup α] (a b : α) : ↑(a ⊔ b) = ↑a ⊔ ↑b

@[simp]

theorem WithTop.coe_inf {α : Type u_1} [SemilatticeInf α] (a b : α) : ↑(a ⊓ b) = ↑a ⊓ ↑b

@[simp]

theorem WithBot.coe_inf {α : Type u_1} [SemilatticeInf α] (a b : α) : ↑(a ⊓ b) = ↑a ⊓ ↑b

@[simp]

theorem WithTop.coe_sup {α : Type u_1} [SemilatticeSup α] (a b : α) : ↑(a ⊔ b) = ↑a ⊔ ↑b

instance WithBot.lattice {α : Type u_1} [Lattice α] : Lattice (WithBot α)

instance WithTop.lattice {α : Type u_1} [Lattice α] : Lattice (WithTop α)

instance WithBot.distribLattice {α : Type u_1} [DistribLattice α] : DistribLattice (WithBot α)

instance WithTop.distribLattice {α : Type u_1} [DistribLattice α] : DistribLattice (WithTop α)

instance WithBot.decidableEq {α : Type u_1} [DecidableEq α] : DecidableEq (WithBot α)

instance WithTop.decidableEq {α : Type u_1} [DecidableEq α] : DecidableEq (WithTop α)

instance WithBot.decidableLE {α : Type u_1} [LE α] [DecidableLE α] : DecidableLE (WithBot α)

instance WithTop.decidableLE {α : Type u_1} [LE α] [DecidableLE α] : DecidableLE (WithTop α)

instance WithBot.decidableLT {α : Type u_1} [LT α] [DecidableLT α] : DecidableLT (WithBot α)

instance WithTop.decidableLT {α : Type u_1} [LT α] [DecidableLT α] : DecidableLT (WithTop α)

instance WithBot.total_le {α : Type u_1} [LE α] [Std.Total fun (x1 x2 : α) => x1 ≤ x2] : Std.Total fun (x1 x2 : WithBot α) => x1 ≤ x2

instance WithTop.total_le {α : Type u_1} [LE α] [Std.Total fun (x1 x2 : α) => x1 ≤ x2] : Std.Total fun (x1 x2 : WithTop α) => x1 ≤ x2

instance WithBot.linearOrder {α : Type u_1} [LinearOrder α] : LinearOrder (WithBot α)

instance WithTop.linearOrder {α : Type u_1} [LinearOrder α] : LinearOrder (WithTop α)

instance WithBot.instWellFoundedLT {α : Type u_1} [LT α] [WellFoundedLT α] : WellFoundedLT (WithBot α)

instance WithTop.instWellFoundedGT {α : Type u_1} [LT α] [WellFoundedGT α] : WellFoundedGT (WithTop α)

instance WithBot.instWellFoundedGT {α : Type u_1} [LT α] [WellFoundedGT α] : WellFoundedGT (WithBot α)

instance WithTop.instWellFoundedLT {α : Type u_1} [LT α] [WellFoundedLT α] : WellFoundedLT (WithTop α)

theorem WithBot.denselyOrdered_iff {α : Type u_1} [LT α] [NoMinOrder α] : DenselyOrdered (WithBot α) ↔ DenselyOrdered α

theorem WithTop.denselyOrdered_iff {α : Type u_1} [LT α] [NoMaxOrder α] : DenselyOrdered (WithTop α) ↔ DenselyOrdered α

instance WithBot.denselyOrdered {α : Type u_1} [LT α] [DenselyOrdered α] [NoMinOrder α] : DenselyOrdered (WithBot α)

instance WithTop.denselyOrdered {α : Type u_1} [LT α] [DenselyOrdered α] [NoMaxOrder α] : DenselyOrdered (WithTop α)

instance WithBot.trichotomous.lt {α : Type u_1} [Preorder α] [Std.Trichotomous fun (x1 x2 : α) => x1 < x2] : Std.Trichotomous fun (x1 x2 : WithBot α) => x1 < x2

instance WithTop.trichotomous.lt {α : Type u_1} [Preorder α] [Std.Trichotomous fun (x1 x2 : α) => x1 < x2] : Std.Trichotomous fun (x1 x2 : WithTop α) => 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 WithTop.IsWellOrder.lt {α : Type u_1} [Preorder α] [IsWellOrder α fun (x1 x2 : α) => x1 < x2] : IsWellOrder (WithTop α) fun (x1 x2 : WithTop α) => x1 < x2

instance WithBot.trichotomous.gt {α : Type u_1} [Preorder α] [Std.Trichotomous fun (x1 x2 : α) => x1 > x2] : Std.Trichotomous fun (x1 x2 : WithBot α) => x1 > x2

instance WithTop.trichotomous.gt {α : Type u_1} [Preorder α] [Std.Trichotomous fun (x1 x2 : α) => x1 > x2] : Std.Trichotomous fun (x1 x2 : WithTop α) => x1 > x2

instance WithBot.IsWellOrder.gt {α : Type u_1} [Preorder α] [IsWellOrder α fun (x1 x2 : α) => x1 > x2] : IsWellOrder (WithBot α) fun (x1 x2 : WithBot α) => x1 > x2

instance WithTop.IsWellOrder.gt {α : Type u_1} [Preorder α] [IsWellOrder α fun (x1 x2 : α) => x1 > x2] : IsWellOrder (WithTop α) fun (x1 x2 : WithTop α) => x1 > x2

theorem WithBot.coe_min {α : Type u_1} [LinearOrder α] (a b : α) : ↑(min a b) = min ↑a ↑b

theorem WithTop.coe_max {α : Type u_1} [LinearOrder α] (a b : α) : ↑(max a b) = max ↑a ↑b

theorem WithBot.coe_max {α : Type u_1} [LinearOrder α] (a b : α) : ↑(max a b) = max ↑a ↑b

theorem WithTop.coe_min {α : Type u_1} [LinearOrder α] (a b : α) : ↑(min a b) = min ↑a ↑b

theorem WithBot.le_of_forall_lt_iff_le {α : Type u_1} [LinearOrder α] {x y : WithBot α} [DenselyOrdered α] [NoMinOrder α] : (∀ (z : α), x < ↑z → y ≤ ↑z) ↔ y ≤ x

theorem WithTop.ge_of_forall_gt_iff_ge {α : Type u_1} [LinearOrder α] {x y : WithTop α} [DenselyOrdered α] [NoMaxOrder α] : (∀ (z : α), ↑z < x → ↑z ≤ y) ↔ x ≤ y

theorem WithBot.ge_of_forall_gt_iff_ge {α : Type u_1} [LinearOrder α] {x y : WithBot α} [DenselyOrdered α] [NoMinOrder α] : (∀ (z : α), ↑z < x → ↑z ≤ y) ↔ x ≤ y

theorem WithTop.le_of_forall_lt_iff_le {α : Type u_1} [LinearOrder α] {x y : WithTop α} [DenselyOrdered α] [NoMaxOrder α] : (∀ (z : α), x < ↑z → y ≤ ↑z) ↔ y ≤ x

theorem WithBot.lt_iff_exists_coe_btwn {α : Type u_1} [Preorder α] [DenselyOrdered α] [NoMinOrder α] {a b : WithBot α} : a < b ↔ ∃ (x : α), a < ↑x ∧ ↑x < b

theorem WithTop.lt_iff_exists_coe_btwn' {α : Type u_1} [Preorder α] [DenselyOrdered α] [NoMaxOrder α] {a b : WithTop α} : b < a ↔ ∃ (x : α), ↑x < a ∧ b < ↑x

theorem WithBot.lt_iff_exists_coe_btwn' {α : Type u_1} [Preorder α] [DenselyOrdered α] [NoMinOrder α] {a b : WithBot α} : a < b ↔ ∃ (x : α), ↑x < b ∧ a < ↑x

theorem WithTop.lt_iff_exists_coe_btwn {α : Type u_1} [Preorder α] [DenselyOrdered α] [NoMaxOrder α] {a b : WithTop α} : b < a ↔ ∃ (x : α), b < ↑x ∧ ↑x < a

instance WithBot.noTopOrder {α : Type u_1} [LE α] [NoTopOrder α] [Nonempty α] : NoTopOrder (WithBot α)

instance WithTop.noBotOrder {α : Type u_1} [LE α] [NoBotOrder α] [Nonempty α] : NoBotOrder (WithTop α)

instance WithBot.noMaxOrder {α : Type u_1} [LT α] [NoMaxOrder α] [Nonempty α] : NoMaxOrder (WithBot α)

instance WithTop.noMinOrder {α : Type u_1} [LT α] [NoMinOrder α] [Nonempty α] : NoMinOrder (WithTop α)

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

def WithBot.toDual {α : Type u_1} : WithBot α ≃ WithTop αᵒᵈ

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

def WithTop.toDual {α : Type u_1} : WithTop α ≃ WithBot αᵒᵈ

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

def WithBot.ofDual {α : Type u_1} : WithBot αᵒᵈ ≃ WithTop α

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

def WithTop.ofDual {α : Type u_1} : WithTop αᵒᵈ ≃ WithBot α

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

@[simp]

theorem WithBot.toDual_symm {α : Type u_1} : WithBot.toDual.symm = WithTop.ofDual

@[simp]

theorem WithTop.toDual_symm {α : Type u_1} : WithTop.toDual.symm = WithBot.ofDual

@[deprecated WithBot.toDual_symm (since := "2025-12-30")]

theorem WithBot.toDual_symm_apply {α : Type u_1} (a : WithTop αᵒᵈ) : WithBot.toDual.symm a = WithTop.ofDual a

@[deprecated WithTop.toDual_symm (since := "2025-12-30")]

theorem WithTop.toDual_symm_apply {α : Type u_1} (a : WithBot αᵒᵈ) : WithTop.toDual.symm a = WithBot.ofDual a

@[simp]

theorem WithBot.ofDual_symm {α : Type u_1} : WithBot.ofDual.symm = WithTop.toDual

@[simp]

theorem WithTop.ofDual_symm {α : Type u_1} : WithTop.ofDual.symm = WithBot.toDual

@[deprecated WithBot.ofDual_symm (since := "2025-12-30")]

theorem WithBot.ofDual_symm_apply {α : Type u_1} (a : WithTop α) : WithBot.ofDual.symm a = WithTop.toDual a

@[deprecated WithTop.ofDual_symm (since := "2025-12-30")]

theorem WithTop.ofDual_symm_apply {α : Type u_1} (a : WithBot α) : WithTop.ofDual.symm a = WithBot.toDual a

@[simp]

theorem WithBot.toDual_bot {α : Type u_1} : WithBot.toDual ⊥ = ⊤

@[simp]

theorem WithTop.toDual_top {α : Type u_1} : WithTop.toDual ⊤ = ⊥

@[deprecated WithBot.toDual_bot (since := "2025-12-30")]

theorem WithBot.toDual_apply_bot {α : Type u_1} : WithBot.toDual ⊥ = ⊤

Alias of WithBot.toDual_bot.

@[deprecated WithTop.toDual_top (since := "2025-12-30")]

theorem WithTop.toDual_apply_top {α : Type u_1} : WithTop.toDual ⊤ = ⊥

Alias of WithTop.toDual_top.

@[simp]

theorem WithBot.ofDual_bot {α : Type u_1} : WithBot.ofDual ⊥ = ⊤

@[simp]

theorem WithTop.ofDual_top {α : Type u_1} : WithTop.ofDual ⊤ = ⊥

@[deprecated WithBot.ofDual_bot (since := "2025-12-30")]

theorem WithBot.ofDual_apply_bot {α : Type u_1} : WithBot.ofDual ⊥ = ⊤

Alias of WithBot.ofDual_bot.

@[deprecated WithTop.ofDual_top (since := "2025-12-30")]

theorem WithTop.ofDual_apply_top {α : Type u_1} : WithTop.ofDual ⊤ = ⊥

Alias of WithTop.ofDual_top.

@[simp]

theorem WithBot.toDual_apply_coe {α : Type u_1} (a : α) : WithBot.toDual ↑a = ↑(OrderDual.toDual a)

@[simp]

theorem WithTop.toDual_apply_coe {α : Type u_1} (a : α) : WithTop.toDual ↑a = ↑(OrderDual.toDual a)

@[simp]

theorem WithBot.ofDual_apply_coe {α : Type u_1} (a : αᵒᵈ) : WithBot.ofDual ↑a = ↑(OrderDual.ofDual a)

@[simp]

theorem WithTop.ofDual_apply_coe {α : Type u_1} (a : αᵒᵈ) : WithTop.ofDual ↑a = ↑(OrderDual.ofDual a)

theorem WithBot.map_toDual {α : Type u_1} {β : Type u_2} (f : αᵒᵈ → βᵒᵈ) (a : WithBot α) : map f (WithBot.toDual a) = map (⇑OrderDual.toDual ∘ f) a

theorem WithTop.map_toDual {α : Type u_1} {β : Type u_2} (f : αᵒᵈ → βᵒᵈ) (a : WithTop α) : map f (WithTop.toDual a) = map (⇑OrderDual.toDual ∘ f) a

theorem WithBot.map_ofDual {α : Type u_1} {β : Type u_2} (f : α → β) (a : WithBot αᵒᵈ) : map f (WithBot.ofDual a) = map (⇑OrderDual.ofDual ∘ f) a

theorem WithTop.map_ofDual {α : Type u_1} {β : Type u_2} (f : α → β) (a : WithTop αᵒᵈ) : map f (WithTop.ofDual a) = map (⇑OrderDual.ofDual ∘ f) a

theorem WithBot.toDual_map {α : Type u_1} {β : Type u_2} (f : α → β) (a : WithBot α) : WithBot.toDual (map f a) = WithTop.map (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) (WithBot.toDual a)

theorem WithTop.toDual_map {α : Type u_1} {β : Type u_2} (f : α → β) (a : WithTop α) : WithTop.toDual (map f a) = WithBot.map (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) (WithTop.toDual a)

theorem WithBot.ofDual_map {α : Type u_1} {β : Type u_2} (f : αᵒᵈ → βᵒᵈ) (a : WithBot αᵒᵈ) : WithBot.ofDual (map f a) = WithTop.map (⇑OrderDual.ofDual ∘ f ∘ ⇑OrderDual.toDual) (WithBot.ofDual a)

theorem WithTop.ofDual_map {α : Type u_1} {β : Type u_2} (f : αᵒᵈ → βᵒᵈ) (a : WithTop αᵒᵈ) : WithTop.ofDual (map f a) = WithBot.map (⇑OrderDual.ofDual ∘ f ∘ ⇑OrderDual.toDual) (WithTop.ofDual a)

theorem WithBot.toDual_le_iff {α : Type u_1} [LE α] {x : WithBot α} {y : WithTop αᵒᵈ} : WithBot.toDual x ≤ y ↔ WithTop.ofDual y ≤ x

theorem WithTop.le_toDual_iff {α : Type u_1} [LE α] {x : WithTop α} {y : WithBot αᵒᵈ} : y ≤ WithTop.toDual x ↔ x ≤ WithBot.ofDual y

theorem WithBot.le_toDual_iff {α : Type u_1} [LE α] {x : WithTop αᵒᵈ} {y : WithBot α} : x ≤ WithBot.toDual y ↔ y ≤ WithTop.ofDual x

theorem WithTop.toDual_le_iff {α : Type u_1} [LE α] {x : WithBot αᵒᵈ} {y : WithTop α} : WithTop.toDual y ≤ x ↔ WithBot.ofDual x ≤ y

@[simp]

theorem WithBot.toDual_le_toDual_iff {α : Type u_1} [LE α] {x y : WithBot α} : WithBot.toDual x ≤ WithBot.toDual y ↔ y ≤ x

@[simp]

theorem WithTop.toDual_le_toDual_iff {α : Type u_1} [LE α] {x y : WithTop α} : WithTop.toDual y ≤ WithTop.toDual x ↔ x ≤ y

theorem WithBot.ofDual_le_iff {α : Type u_1} [LE α] {x : WithBot αᵒᵈ} {y : WithTop α} : WithBot.ofDual x ≤ y ↔ WithTop.toDual y ≤ x

theorem WithTop.le_ofDual_iff {α : Type u_1} [LE α] {x : WithTop αᵒᵈ} {y : WithBot α} : y ≤ WithTop.ofDual x ↔ x ≤ WithBot.toDual y

theorem WithBot.le_ofDual_iff {α : Type u_1} [LE α] {x : WithTop α} {y : WithBot αᵒᵈ} : x ≤ WithBot.ofDual y ↔ y ≤ WithTop.toDual x

theorem WithTop.ofDual_le_iff {α : Type u_1} [LE α] {x : WithBot α} {y : WithTop αᵒᵈ} : WithTop.ofDual y ≤ x ↔ WithBot.toDual x ≤ y

@[simp]

theorem WithBot.ofDual_le_ofDual_iff {α : Type u_1} [LE α] {x y : WithBot αᵒᵈ} : WithBot.ofDual x ≤ WithBot.ofDual y ↔ y ≤ x

@[simp]

theorem WithTop.ofDual_le_ofDual_iff {α : Type u_1} [LE α] {x y : WithTop αᵒᵈ} : WithTop.ofDual y ≤ WithTop.ofDual x ↔ x ≤ y

theorem WithBot.toDual_lt_iff {α : Type u_1} [LT α] {x : WithBot α} {y : WithTop αᵒᵈ} : WithBot.toDual x < y ↔ WithTop.ofDual y < x

theorem WithTop.lt_toDual_iff {α : Type u_1} [LT α] {x : WithTop α} {y : WithBot αᵒᵈ} : y < WithTop.toDual x ↔ x < WithBot.ofDual y

theorem WithBot.lt_toDual_iff {α : Type u_1} [LT α] {x : WithTop αᵒᵈ} {y : WithBot α} : x < WithBot.toDual y ↔ y < WithTop.ofDual x

theorem WithTop.toDual_lt_iff {α : Type u_1} [LT α] {x : WithBot αᵒᵈ} {y : WithTop α} : WithTop.toDual y < x ↔ WithBot.ofDual x < y

@[simp]

theorem WithBot.toDual_lt_toDual_iff {α : Type u_1} [LT α] {x y : WithBot α} : WithBot.toDual x < WithBot.toDual y ↔ y < x

@[simp]

theorem WithTop.toDual_lt_toDual_iff {α : Type u_1} [LT α] {x y : WithTop α} : WithTop.toDual y < WithTop.toDual x ↔ x < y

theorem WithBot.ofDual_lt_iff {α : Type u_1} [LT α] {x : WithBot αᵒᵈ} {y : WithTop α} : WithBot.ofDual x < y ↔ WithTop.toDual y < x

theorem WithTop.lt_ofDual_iff {α : Type u_1} [LT α] {x : WithTop αᵒᵈ} {y : WithBot α} : y < WithTop.ofDual x ↔ x < WithBot.toDual y

theorem WithBot.lt_ofDual_iff {α : Type u_1} [LT α] {x : WithTop α} {y : WithBot αᵒᵈ} : x < WithBot.ofDual y ↔ y < WithTop.toDual x

theorem WithTop.ofDual_lt_iff {α : Type u_1} [LT α] {x : WithBot α} {y : WithTop αᵒᵈ} : WithTop.ofDual y < x ↔ WithBot.toDual x < y

@[simp]

theorem WithBot.ofDual_lt_ofDual_iff {α : Type u_1} [LT α] {x y : WithBot αᵒᵈ} : WithBot.ofDual x < WithBot.ofDual y ↔ y < x

@[simp]

theorem WithTop.ofDual_lt_ofDual_iff {α : Type u_1} [LT α] {x y : WithTop αᵒᵈ} : WithTop.ofDual y < WithTop.ofDual x ↔ x < y