WithBot, WithTop

Adding a bot or a top to an order.

Main declarations

• With α: 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

• WithBot α = Option α

instance WithBot.instReprWithBot {α : Type u_1} [Repr α] : Repr (WithBot α)

Equations

• WithBot.instReprWithBot = { reprPrec := fun o x => match o with | none => Std.Format.text "⊥" | some a => Std.Format.text "↑" ++ repr a }

@[match_pattern]

def WithBot.some {α : Type u_1} : α → WithBot α

The canonical map from α into WithBot α

Equations

• WithBot.some = some

instance WithBot.coe {α : Type u_1} : Coe α (WithBot α)

Equations

• WithBot.coe = { coe := WithBot.some }

instance WithBot.bot {α : Type u_1} : Bot (WithBot α)

Equations

• WithBot.bot = { bot := none }

instance WithBot.inhabited {α : Type u_1} : Inhabited (WithBot α)

Equations

• WithBot.inhabited = { default := ⊥ }

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

Equations

• (_ : Nontrivial (WithBot α)) = (_ : Nontrivial (Option α))

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 : WithBot α → Prop} : ((x : WithBot α) → p x) ↔ p ⊥ ∧ ((x : α) → p ↑x)

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

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

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

@[simp]

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

@[simp]

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

def WithBot.recBotCoe {α : Type u_1} {C : WithBot α → Sort u_5} (bot : C ⊥) (coe : (a : α) → C ↑a) (n : WithBot α) : C n

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

Equations

• WithBot.recBotCoe bot coe x = match x with | none => bot | some a => coe a

@[simp]

theorem WithBot.recBotCoe_bot {α : Type u_1} {C : WithBot α → Sort u_5} (d : C ⊥) (f : (a : α) → C ↑a) : WithBot.recBotCoe d f ⊥ = d

@[simp]

theorem WithBot.recBotCoe_coe {α : Type u_1} {C : WithBot α → Sort u_5} (d : C ⊥) (f : (a : α) → C ↑a) (x : α) : WithBot.recBotCoe d f ↑x = f x

def WithBot.unbot' {α : Type u_1} (d : α) (x : WithBot α) : α

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

Equations

• WithBot.unbot' d x = WithBot.recBotCoe d id x

@[simp]

theorem WithBot.unbot'_bot {α : Type u_5} (d : α) : WithBot.unbot' d ⊥ = d

@[simp]

theorem WithBot.unbot'_coe {α : Type u_5} (d : α) (x : α) : WithBot.unbot' d ↑x = x

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

theorem WithBot.unbot'_eq_iff {α : Type u_1} {d : α} {y : α} {x : WithBot α} : WithBot.unbot' d x = y ↔ x = ↑y ∨ x = ⊥ ∧ y = d

@[simp]

theorem WithBot.unbot'_eq_self_iff {α : Type u_1} {d : α} {x : WithBot α} : WithBot.unbot' d x = d ↔ x = ↑d ∨ x = ⊥

theorem WithBot.unbot'_eq_unbot'_iff {α : Type u_1} {d : α} {x : WithBot α} {y : WithBot α} : WithBot.unbot' d x = WithBot.unbot' d y ↔ x = y ∨ x = ↑d ∧ y = ⊥ ∨ x = ⊥ ∧ y = ↑d

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

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

Equations

• WithBot.map f = Option.map f

@[simp]

theorem WithBot.map_bot {α : Type u_1} {β : Type u_2} (f : α → β) : WithBot.map 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)

theorem WithBot.ne_bot_iff_exists {α : Type u_1} {x : WithBot α} : x ≠ ⊥ ↔ ∃ a, ↑a = x

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

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

Equations

• WithBot.unbot x x = match x, x with | none, h => absurd (_ : ⊥ = ⊥) h | some x, x_1 => x

@[simp]

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

@[simp]

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

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

Equations

• @WithBot.canLift = @WithBot.canLift.proof_1

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

Equations

• WithBot.le = { le := fun o₁ o₂ => ∀ (a : α), a ∈ o₁ → ∃ b, b ∈ o₂ ∧ a ≤ b }

@[simp]

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

@[simp]

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

@[simp]

theorem WithBot.none_le {α : Type u_1} [LE α] {a : WithBot α} : none ≤ a

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

Equations

• WithBot.orderBot = let src := WithBot.bot; OrderBot.mk (_ : ∀ (x : WithBot α), none ≤ x)

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

Equations

• WithBot.orderTop = OrderTop.mk (_ : ∀ (o : WithBot α) (a : α), a ∈ o → ∃ b, b ∈ ⊤ ∧ a ≤ b)

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

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 : WithBot α} : a ≤ ⊥ ↔ 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 : 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 = ↑a → a ≤ b

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

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

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

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

Equations

• WithBot.lt = { lt := fun o₁ o₂ => ∃ b, b ∈ o₂ ∧ ∀ (a : α), a ∈ o₁ → a < b }

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

theorem WithBot.lt_iff_exists_coe {α : Type u_1} [LT α] {a : WithBot α} {b : WithBot α} : a < b ↔ ∃ p, b = ↑p ∧ a < ↑p

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

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 α.

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

Equations

• WithBot.preorder = Preorder.mk (_ : ∀ (o : WithBot α) (a : α), a ∈ o → ∃ b, b ∈ o ∧ a ≤ b) (_ : ∀ (o₁ o₂ o₃ : WithBot α), o₁ ≤ o₂ → o₂ ≤ o₃ → ∀ (a : α), a ∈ o₁ → ∃ b, b ∈ o₃ ∧ a ≤ b)

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

Equations

• WithBot.partialOrder = let src := WithBot.preorder; PartialOrder.mk (_ : ∀ (o₁ o₂ : WithBot α), o₁ ≤ o₂ → o₂ ≤ o₁ → o₁ = o₂)

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

theorem WithBot.le_coe_unbot' {α : Type u_1} [Preorder α] (a : WithBot α) (b : α) : a ≤ ↑(WithBot.unbot' b a)

theorem WithBot.unbot'_le_iff {α : Type u_1} [LE α] {a : WithBot α} {b : α} {c : α} (h : a = ⊥ → b ≤ c) : WithBot.unbot' b a ≤ c ↔ a ≤ ↑c

theorem WithBot.unbot'_lt_iff {α : Type u_1} [LT α] {a : WithBot α} {b : α} {c : α} (h : a = ⊥ → b < c) : WithBot.unbot' b a < c ↔ a < ↑c

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

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• WithBot.distribLattice = let src := WithBot.lattice; DistribLattice.mk (_ : ∀ (o₁ o₂ o₃ : WithBot α), (o₁ ⊔ o₂) ⊓ (o₁ ⊔ o₃) ≤ o₁ ⊔ o₂ ⊓ o₃)

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

Equations

• WithBot.decidableEq = instDecidableEqOption

instance WithBot.decidableLE {α : Type u_1} [LE α] [DecidableRel fun x x_1 => x ≤ x_1] : DecidableRel fun x x_1 => x ≤ x_1

Equations

• One or more equations did not get rendered due to their size.

instance WithBot.decidableLT {α : Type u_1} [LT α] [DecidableRel fun x x_1 => x < x_1] : DecidableRel fun x x_1 => x < x_1

Equations

• One or more equations did not get rendered due to their size.

instance WithBot.isTotal_le {α : Type u_1} [LE α] [IsTotal α fun x x_1 => x ≤ x_1] : IsTotal (WithBot α) fun x x_1 => x ≤ x_1

Equations

• @WithBot.isTotal_le = @WithBot.isTotal_le.proof_1

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

Equations

• WithBot.linearOrder = Lattice.toLinearOrder (WithBot α)

@[simp]

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

@[simp]

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

theorem WithBot.wellFounded_lt {α : Type u_1} [LT α] (h : WellFounded fun x x_1 => x < x_1) : WellFounded fun x x_1 => x < x_1

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

Equations

• @WithBot.denselyOrdered = @WithBot.denselyOrdered.proof_1

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

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

Equations

• @WithBot.noTopOrder = @WithBot.noTopOrder.proof_1

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

Equations

• @WithBot.noMaxOrder = @WithBot.noMaxOrder.proof_1

def WithTop (α : Type u_5) : Type u_5

Attach ⊤ to a type.

Equations

• WithTop α = Option α

instance WithTop.instReprWithTop {α : Type u_1} [Repr α] : Repr (WithTop α)

Equations

• WithTop.instReprWithTop = { reprPrec := fun o x => match o with | none => Std.Format.text "⊤" | some a => Std.Format.text "↑" ++ repr a }

@[match_pattern]

def WithTop.some {α : Type u_1} : α → WithTop α

The canonical map from α into WithTop α

Equations

• WithTop.some = some

instance WithTop.coeTC {α : Type u_1} : CoeTC α (WithTop α)

Equations

• WithTop.coeTC = { coe := WithTop.some }

instance WithTop.top {α : Type u_1} : Top (WithTop α)

Equations

• WithTop.top = { top := none }

instance WithTop.inhabited {α : Type u_1} : Inhabited (WithTop α)

Equations

• WithTop.inhabited = { default := ⊤ }

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

Equations

• (_ : Nontrivial (WithTop α)) = (_ : Nontrivial (Option α))

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 : WithTop α → Prop} : ((x : WithTop α) → p x) ↔ p ⊤ ∧ ((x : α) → p ↑x)

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

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

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

@[simp]

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

@[simp]

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

def WithTop.recTopCoe {α : Type u_1} {C : WithTop α → Sort u_5} (top : C ⊤) (coe : (a : α) → C ↑a) (n : WithTop α) : C n

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

Equations

• WithTop.recTopCoe top coe x = match x with | none => top | some a => coe a

@[simp]

theorem WithTop.recTopCoe_top {α : Type u_1} {C : WithTop α → Sort u_5} (d : C ⊤) (f : (a : α) → C ↑a) : WithTop.recTopCoe d f ⊤ = d

@[simp]

theorem WithTop.recTopCoe_coe {α : Type u_1} {C : WithTop α → Sort u_5} (d : C ⊤) (f : (a : α) → C ↑a) (x : α) : WithTop.recTopCoe d f ↑x = f x

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.

Equations

• WithTop.toDual = Equiv.refl (WithTop α)

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.

Equations

• WithTop.ofDual = Equiv.refl (WithTop αᵒᵈ)

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

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 = Equiv.refl (WithBot α)

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

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 = Equiv.refl (WithBot αᵒᵈ)

@[simp]

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

@[simp]

theorem WithTop.ofDual_symm_apply {α : Type u_1} (a : WithBot α) : ↑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 : WithTop α) : α

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

Equations

• WithTop.untop' d x = WithTop.recTopCoe d id x

@[simp]

theorem WithTop.untop'_top {α : Type u_5} (d : α) : WithTop.untop' d ⊤ = d

@[simp]

theorem WithTop.untop'_coe {α : Type u_5} (d : α) (x : α) : WithTop.untop' d ↑x = x

@[simp]

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

theorem WithTop.untop'_eq_iff {α : Type u_1} {d : α} {y : α} {x : WithTop α} : WithTop.untop' d x = y ↔ x = ↑y ∨ x = ⊤ ∧ y = d

@[simp]

theorem WithTop.untop'_eq_self_iff {α : Type u_1} {d : α} {x : WithTop α} : WithTop.untop' d x = d ↔ x = ↑d ∨ x = ⊤

theorem WithTop.untop'_eq_untop'_iff {α : Type u_1} {d : α} {x : WithTop α} {y : WithTop α} : WithTop.untop' d x = WithTop.untop' d y ↔ x = y ∨ x = ↑d ∧ y = ⊤ ∨ x = ⊤ ∧ y = ↑d

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

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

Equations

• WithTop.map f = Option.map f

@[simp]

theorem WithTop.map_top {α : Type u_1} {β : Type u_2} (f : α → β) : WithTop.map 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)

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

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

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

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

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

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

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

Equations

• WithTop.untop = WithBot.unbot

@[simp]

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

@[simp]

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

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

Equations

• @WithTop.canLift = @WithTop.canLift.proof_1

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

Equations

• WithTop.le = { le := fun o₁ o₂ => ∀ (a : α), a ∈ o₂ → ∃ b, b ∈ o₁ ∧ b ≤ a }

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

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

@[simp]

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

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

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

@[simp]

theorem WithTop.ofDual_le_ofDual_iff {α : Type u_1} [LE α] {a : WithTop αᵒᵈ} {b : WithTop αᵒᵈ} : ↑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]

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

@[simp]

theorem WithTop.le_none {α : Type u_1} [LE α] {a : WithTop α} : a ≤ none

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

Equations

• WithTop.orderTop = let src := WithTop.top; OrderTop.mk (_ : ∀ (x : WithTop α), x ≤ none)

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

Equations

• WithTop.orderBot = OrderBot.mk (_ : ∀ (o : WithTop α) (a : α), a ∈ o → ∃ b, b ∈ ⊥ ∧ b ≤ a)

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

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 : WithTop α} : ⊤ ≤ a ↔ 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 : 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 = ↑b → a ≤ b

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

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

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

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

Equations

• WithTop.lt = { lt := fun o₁ o₂ => ∃ b, b ∈ o₁ ∧ ∀ (a : α), a ∈ o₂ → b < a }

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

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

@[simp]

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

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

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

@[simp]

theorem WithTop.ofDual_lt_ofDual_iff {α : Type u_1} [LT α] {a : WithTop αᵒᵈ} {b : WithTop αᵒᵈ} : ↑WithTop.ofDual a < ↑WithTop.ofDual b ↔ b < a

@[simp]

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

@[simp]

theorem WithBot.ofDual_symm_apply {α : Type u_1} (a : WithTop α) : ↑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 : WithTop α) : WithBot.map f (↑WithTop.toDual a) = WithTop.map (↑OrderDual.toDual ∘ f) a

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

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

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

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

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

@[simp]

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

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

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

@[simp]

theorem WithBot.ofDual_le_ofDual_iff {α : Type u_1} [LE α] {a : WithBot αᵒᵈ} {b : WithBot αᵒᵈ} : ↑WithBot.ofDual a ≤ ↑WithBot.ofDual b ↔ b ≤ a

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

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

@[simp]

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

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

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

@[simp]

theorem WithBot.ofDual_lt_ofDual_iff {α : Type u_1} [LT α] {a : WithBot αᵒᵈ} {b : WithBot αᵒᵈ} : ↑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.some_lt_some {α : Type u_1} [LT α] {a : α} {b : α} : some a < some b ↔ a < b

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

@[simp]

theorem WithTop.some_lt_none {α : Type u_1} [LT α] (a : α) : some a < none

@[simp]

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

theorem WithTop.lt_iff_exists_coe {α : Type u_1} [LT α] {a : WithTop α} {b : WithTop α} : a < b ↔ ∃ p, a = ↑p ∧ ↑p < b

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

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 α.

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

Equations

• WithTop.preorder = Preorder.mk (_ : ∀ (x : WithTop α), x ≤ x) (_ : ∀ (x x_1 x_2 : WithTop α), x ≤ x_1 → x_1 ≤ x_2 → x ≤ x_2)

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

Equations

• WithTop.partialOrder = let src := WithTop.preorder; PartialOrder.mk (_ : ∀ (x x_1 : WithTop α), x ≤ x_1 → x_1 ≤ x → x = x_1)

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 : α → β} : Monotone (WithTop.map f) ↔ Monotone f

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

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

Alias of the reverse direction of WithTop.strictMono_map_iff.

theorem WithTop.map_le_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α → β) (a : WithTop α) (b : WithTop α) (mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b) : WithTop.map f a ≤ WithTop.map f b ↔ a ≤ b

theorem WithTop.coe_untop'_le {α : Type u_1} [Preorder α] (a : WithTop α) (b : α) : ↑(WithTop.untop' b a) ≤ a

theorem WithTop.le_untop'_iff {α : Type u_1} [LE α] {a : WithTop α} {b : α} {c : α} (h : a = ⊤ → c ≤ b) : c ≤ WithTop.untop' b a ↔ ↑c ≤ a

theorem WithTop.lt_untop'_iff {α : Type u_1} [LT α] {a : WithTop α} {b : α} {c : α} (h : a = ⊤ → c < b) : c < WithTop.untop' b a ↔ ↑c < a

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

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• WithTop.distribLattice = let src := WithTop.lattice; DistribLattice.mk (_ : ∀ (o₁ o₂ o₃ : WithTop α), (o₁ ⊔ o₂) ⊓ (o₁ ⊔ o₃) ≤ o₁ ⊔ o₂ ⊓ o₃)

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

Equations

• WithTop.decidableEq = instDecidableEqOption

instance WithTop.decidableLE {α : Type u_1} [LE α] [DecidableRel fun x x_1 => x ≤ x_1] : DecidableRel fun x x_1 => x ≤ x_1

Equations

• WithTop.decidableLE x x = decidable_of_decidable_of_iff (_ : ↑WithTop.toDual x ≤ ↑WithTop.toDual x ↔ x ≤ 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

• WithTop.decidableLT x x = decidable_of_decidable_of_iff (_ : ↑WithTop.toDual x < ↑WithTop.toDual x ↔ x < x)

instance WithTop.isTotal_le {α : Type u_1} [LE α] [IsTotal α fun x x_1 => x ≤ x_1] : IsTotal (WithTop α) fun x x_1 => x ≤ x_1

Equations

• @WithTop.isTotal_le = @WithTop.isTotal_le.proof_1

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

Equations

• WithTop.linearOrder = Lattice.toLinearOrder (WithTop α)

@[simp]

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

@[simp]

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

theorem WithTop.wellFounded_lt {α : Type u_1} [LT α] (h : WellFounded fun x x_1 => x < x_1) : WellFounded fun x x_1 => x < x_1

theorem WithTop.wellFounded_gt {α : Type u_1} [LT α] (h : WellFounded fun x x_1 => x > x_1) : WellFounded fun x x_1 => x > x_1

theorem WithBot.wellFounded_gt {α : Type u_1} [LT α] (h : WellFounded fun x x_1 => x > x_1) : WellFounded fun x x_1 => x > x_1

instance WithTop.trichotomous.lt {α : Type u_1} [Preorder α] [IsTrichotomous α fun x x_1 => x < x_1] : IsTrichotomous (WithTop α) fun x x_1 => x < x_1

Equations

• @WithTop.trichotomous.lt = @WithTop.trichotomous.lt.proof_1

instance WithTop.IsWellOrder.lt {α : Type u_1} [Preorder α] [h : IsWellOrder α fun x x_1 => x < x_1] : IsWellOrder (WithTop α) fun x x_1 => x < x_1

Equations

• @WithTop.IsWellOrder.lt = @WithTop.IsWellOrder.lt.proof_1

instance WithTop.trichotomous.gt {α : Type u_1} [Preorder α] [IsTrichotomous α fun x x_1 => x > x_1] : IsTrichotomous (WithTop α) fun x x_1 => x > x_1

Equations

• @WithTop.trichotomous.gt = @WithTop.trichotomous.gt.proof_1

instance WithTop.IsWellOrder.gt {α : Type u_1} [Preorder α] [h : IsWellOrder α fun x x_1 => x > x_1] : IsWellOrder (WithTop α) fun x x_1 => x > x_1

Equations

• @WithTop.IsWellOrder.gt = @WithTop.IsWellOrder.gt.proof_1

instance WithBot.trichotomous.lt {α : Type u_1} [Preorder α] [h : IsTrichotomous α fun x x_1 => x < x_1] : IsTrichotomous (WithBot α) fun x x_1 => x < x_1

Equations

• @WithBot.trichotomous.lt = @WithBot.trichotomous.lt.proof_1

instance WithBot.isWellOrder.lt {α : Type u_1} [Preorder α] [h : IsWellOrder α fun x x_1 => x < x_1] : IsWellOrder (WithBot α) fun x x_1 => x < x_1

Equations

• @WithBot.isWellOrder.lt = @WithBot.isWellOrder.lt.proof_1

instance WithBot.trichotomous.gt {α : Type u_1} [Preorder α] [h : IsTrichotomous α fun x x_1 => x > x_1] : IsTrichotomous (WithBot α) fun x x_1 => x > x_1

Equations

• @WithBot.trichotomous.gt = @WithBot.trichotomous.gt.proof_1

instance WithBot.isWellOrder.gt {α : Type u_1} [Preorder α] [h : IsWellOrder α fun x x_1 => x > x_1] : IsWellOrder (WithBot α) fun x x_1 => x > x_1

Equations

• @WithBot.isWellOrder.gt = @WithBot.isWellOrder.gt.proof_1

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

Equations

• @WithTop.instDenselyOrderedWithTopLt = @WithTop.instDenselyOrderedWithTopLt.proof_1

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

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

Equations

• @WithTop.noBotOrder = @WithTop.noBotOrder.proof_1

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

Equations

• @WithTop.noMinOrder = @WithTop.noMinOrder.proof_1