Mathlib.Order.WithBot

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)

source

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

WithBot.map₂ = Option.map₂

source

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

WithBot.map₂ f ↑a ↑b = ↑(f a b)

source

@[simp]

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

WithBot.map₂ f ⊥ b = ⊥

source

@[simp]

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

WithBot.map₂ f a ⊥ = ⊥

source

@[simp]

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

WithBot.map₂ f (↑a) b = WithBot.map (fun (b : β) => f a b) b

source

@[simp]

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

WithBot.map₂ f a ↑b = WithBot.map (fun (x : α) => f x b) a

source

@[simp]

theorem WithBot.map₂_eq_bot_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {a : WithBot α} {b : WithBot β} :

WithBot.map₂ f a b = ⊥ ↔ a = ⊥ ∨ b = ⊥

source

theorem WithBot.ne_bot_iff_exists {α : Type u_1} {x : WithBot α} :

x ≠ ⊥ ↔ ∃ (a : α), ↑a = x

source

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 | some x, x_1 => x

source

@[simp]

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

↑(WithBot.unbot x hx) = x

source

@[simp]

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

WithBot.unbot (↑x) h = x

source

instance WithBot.canLift {α : Type u_1} :

CanLift (WithBot α) α WithBot.some fun (r : WithBot α) => r ≠ ⊥

Equations

⋯ = ⋯

source

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

LE (WithBot α)

Equations

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

source

@[simp]

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

some a ≤ some b ↔ a ≤ b

source

@[simp]

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

↑a ≤ ↑b ↔ a ≤ b

source

@[simp]

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

none ≤ a

source

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

OrderBot (WithBot α)

Equations

WithBot.orderBot = let __src := WithBot.bot; OrderBot.mk ⋯

source

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

OrderTop (WithBot α)

Equations

WithBot.orderTop = OrderTop.mk ⋯

source

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

BoundedOrder (WithBot α)

Equations

WithBot.instBoundedOrder = let __src := WithBot.orderBot; let __src_1 := WithBot.orderTop; BoundedOrder.mk

source

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

¬↑a ≤ ⊥

source

@[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.

source

theorem WithBot.coe_le {α : Type u_1} {a : α} {b : α} [LE α] {o : Option α} :

b ∈ o → (↑a ≤ o ↔ a ≤ b)

source

theorem WithBot.coe_le_iff {α : Type u_1} {a : α} [LE α] {x : WithBot α} :

↑a ≤ x ↔ ∃ (b : α), x = ↑b ∧ a ≤ b

source

theorem WithBot.le_coe_iff {α : Type u_1} {b : α} [LE α] {x : WithBot α} :

x ≤ ↑b ↔ ∀ (a : α), x = ↑a → a ≤ b

source

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

IsMax ↑a

source

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

a ≤ WithBot.unbot b h ↔ ↑a ≤ b

source

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

WithBot.unbot a h ≤ b ↔ a ≤ ↑b

source

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

WithBot.unbot' b a ≤ c ↔ a ≤ ↑c

source

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

LT (WithBot α)

Equations

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

source

@[simp]

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

some a < some b ↔ a < b

source

@[simp]

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

↑a < ↑b ↔ a < b

source

@[simp]

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

none < ↑a

source

@[simp]

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

⊥ < ↑a

source

@[simp]

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

¬a < none

source

theorem WithBot.lt_iff_exists_coe {α : Type u_1} [LT α] {a : WithBot α} {b : WithBot α} :

a < b ↔ ∃ (p : α), b = ↑p ∧ a < ↑p

source

theorem WithBot.lt_coe_iff {α : Type u_1} {b : α} [LT α] {x : WithBot α} :

x < ↑b ↔ ∀ (a : α), x = ↑a → a < b

source

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

source

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

WithBot.unbot' b a < c ↔ a < ↑c

source

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

Preorder (WithBot α)

Equations

WithBot.preorder = Preorder.mk ⋯ ⋯ ⋯

source

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

PartialOrder (WithBot α)

Equations

WithBot.partialOrder = let __src := WithBot.preorder; PartialOrder.mk ⋯

source

theorem WithBot.coe_strictMono {α : Type u_1} [Preorder α] :

StrictMono fun (a : α) => ↑a

source

theorem WithBot.coe_mono {α : Type u_1} [Preorder α] :

Monotone fun (a : α) => ↑a

source

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

source

@[simp]

theorem WithBot.monotone_map_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} :

Monotone (WithBot.map f) ↔ Monotone f

source

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.

source

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

source

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 ⊥

source

@[simp]

theorem WithBot.strictMono_map_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} :

StrictMono (WithBot.map f) ↔ StrictMono f

source

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.

source

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

source

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

a ≤ ↑(WithBot.unbot' b a)

source

@[simp]

theorem WithBot.lt_coe_bot {α : Type u_1} [Preorder α] [OrderBot α] {x : WithBot α} :

x < ↑⊥ ↔ x = ⊥

source

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

SemilatticeSup (WithBot α)

Equations

WithBot.semilatticeSup = let __src := WithBot.partialOrder; let __src_1 := WithBot.orderBot; SemilatticeSup.mk ⋯ ⋯ ⋯

source

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

↑(a ⊔ b) = ↑a ⊔ ↑b

source

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

SemilatticeInf (WithBot α)

Equations

WithBot.semilatticeInf = let __src := WithBot.partialOrder; let __src_1 := WithBot.orderBot; SemilatticeInf.mk ⋯ ⋯ ⋯

source

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

↑(a ⊓ b) = ↑a ⊓ ↑b

source

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

Lattice (WithBot α)

Equations

WithBot.lattice = let __src := WithBot.semilatticeSup; let __src_1 := WithBot.semilatticeInf; Lattice.mk ⋯ ⋯ ⋯

source

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

DistribLattice (WithBot α)

Equations

WithBot.distribLattice = let __src := WithBot.lattice; DistribLattice.mk ⋯

source

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

DecidableEq (WithBot α)

Equations

WithBot.decidableEq = inferInstanceAs (DecidableEq (Option α))

source

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

DecidableRel fun (x x_1 : WithBot α) => x ≤ x_1

Equations

WithBot.decidableLE x✝ x = match x✝, x with | none, x => isTrue ⋯ | some x, some y => if h : x ≤ y then isTrue ⋯ else isFalse ⋯ | some x, none => isFalse ⋯

source

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

DecidableRel fun (x x_1 : WithBot α) => x < x_1

Equations

WithBot.decidableLT x✝ x = match x✝, x with | none, some x => isTrue ⋯ | some x, some y => if h : x < y then isTrue ⋯ else isFalse ⋯ | x, none => isFalse ⋯

source

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

IsTotal (WithBot α) fun (x x_1 : WithBot α) => x ≤ x_1

Equations

⋯ = ⋯

source

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

LinearOrder (WithBot α)

Equations

WithBot.linearOrder = Lattice.toLinearOrder (WithBot α)

source

@[simp]

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

↑(min x y) = min ↑x ↑y

source

@[simp]

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

↑(max x y) = max ↑x ↑y

source

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

WellFoundedLT (WithBot α)

Equations

⋯ = ⋯

source

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

WellFoundedGT (WithBot α)

Equations

⋯ = ⋯

source

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

DenselyOrdered (WithBot α)

Equations

⋯ = ⋯

source

theorem WithBot.lt_iff_exists_coe_btwn {α : Type u_1} [Preorder α] [DenselyOrdered α] [NoMinOrder α] {a : WithBot α} {b : WithBot α} :

a < b ↔ ∃ (x : α), a < ↑x ∧ ↑x < b

source

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

NoTopOrder (WithBot α)

Equations

⋯ = ⋯

source

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

NoMaxOrder (WithBot α)

Equations

⋯ = ⋯

source

def WithTop (α : Type u_5) :

Type u_5

Attach ⊤ to a type.

Equations

WithTop α = Option α

Instances For

source

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

Repr (WithTop α)

Equations

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

source

@[match_pattern]

def WithTop.some {α : Type u_1} :

α → WithTop α

The canonical map from α into WithTop α

Equations

WithTop.some = some

Instances For

WithTop.canLift

source

instance WithTop.coeTC {α : Type u_1} :

CoeTC α (WithTop α)

Equations

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

source

instance WithTop.top {α : Type u_1} :

Top (WithTop α)

Equations

WithTop.top = { top := none }

source

instance WithTop.inhabited {α : Type u_1} :

Inhabited (WithTop α)

Equations

WithTop.inhabited = { default := ⊤ }

source

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

Nontrivial (WithTop α)

Equations

⋯ = ⋯

source

theorem WithTop.coe_injective {α : Type u_1} :

Function.Injective WithTop.some

source

theorem WithTop.coe_inj {α : Type u_1} {a : α} {b : α} :

↑a = ↑b ↔ a = b

source

theorem WithTop.forall {α : Type u_1} {p : WithTop α → Prop} :

(∀ (x : WithTop α), p x) ↔ p ⊤ ∧ ∀ (x : α), p ↑x

source

theorem WithTop.exists {α : Type u_1} {p : WithTop α → Prop} :

(∃ (x : WithTop α), p x) ↔ p ⊤ ∨ ∃ (x : α), p ↑x

source

theorem WithTop.none_eq_top {α : Type u_1} :

none = ⊤

source

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

some a = ↑a

source

@[simp]

theorem WithTop.top_ne_coe {α : Type u_1} {a : α} :

⊤ ≠ ↑a

source

@[simp]

theorem WithTop.coe_ne_top {α : Type u_1} {a : α} :

↑a ≠ ⊤

source

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

source

@[simp]

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

WithTop.recTopCoe d f ⊤ = d

source

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

source

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

source

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 αᵒᵈ)

source

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

source

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 αᵒᵈ)

source

@[simp]

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

WithTop.toDual.symm a = WithBot.ofDual a

source

@[simp]

theorem WithTop.ofDual_symm_apply {α : Type u_1} (a : WithBot α) :

WithTop.ofDual.symm a = WithBot.toDual a

source

@[simp]

theorem WithTop.toDual_apply_top {α : Type u_1} :

WithTop.toDual ⊤ = ⊥

source

@[simp]

theorem WithTop.ofDual_apply_top {α : Type u_1} :

WithTop.ofDual ⊤ = ⊥

source

@[simp]

theorem WithTop.toDual_apply_coe {α : Type u_1} (a : α) :

WithTop.toDual ↑a = ↑(OrderDual.toDual a)

source

@[simp]

theorem WithTop.ofDual_apply_coe {α : Type u_1} (a : αᵒᵈ) :

WithTop.ofDual ↑a = ↑(OrderDual.ofDual a)

source

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

source

@[simp]

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

WithTop.untop' d ⊤ = d

source

@[simp]

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

WithTop.untop' d ↑x = x

source

@[simp]

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

↑a = ↑b ↔ a = b

source

theorem WithTop.untop'_eq_iff {α : Type u_1} {d : α} {y : α} {x : WithTop α} :

WithTop.untop' d x = y ↔ x = ↑y ∨ x = ⊤ ∧ y = d

source

@[simp]

theorem WithTop.untop'_eq_self_iff {α : Type u_1} {d : α} {x : WithTop α} :

WithTop.untop' d x = d ↔ x = ↑d ∨ x = ⊤

source

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

source

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

source

@[simp]

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

WithTop.map f ⊤ = ⊤

source

@[simp]

theorem WithTop.map_coe {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) :

WithTop.map f ↑a = ↑(f a)

source

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)

source

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

WithTop.map₂ = Option.map₂

source

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

WithTop.map₂ f ↑a ↑b = ↑(f a b)

source

@[simp]

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

WithTop.map₂ f ⊤ b = ⊤

source

@[simp]

theorem WithTop.map₂_top_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : WithTop α) :

WithTop.map₂ f a ⊤ = ⊤

source

@[simp]

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

WithTop.map₂ f (↑a) b = WithTop.map (fun (b : β) => f a b) b

source

@[simp]

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

WithTop.map₂ f a ↑b = WithTop.map (fun (x : α) => f x b) a

source

@[simp]

theorem WithTop.map₂_eq_top_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {a : WithTop α} {b : WithTop β} :

WithTop.map₂ f a b = ⊤ ↔ a = ⊤ ∨ b = ⊤

source

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

source

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

source

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)

source

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)

source

theorem WithTop.ne_top_iff_exists {α : Type u_1} {x : WithTop α} :

x ≠ ⊤ ↔ ∃ (a : α), ↑a = x

source

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 x✝ x = match x✝, x with | some x, x_1 => x

source

@[simp]

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

↑(WithTop.untop x hx) = x

source

@[simp]

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

WithTop.untop (↑x) h = x

source

instance WithTop.canLift {α : Type u_1} :

CanLift (WithTop α) α WithTop.some fun (r : WithTop α) => r ≠ ⊤

Equations

⋯ = ⋯

source

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

LE (WithTop α)

Equations

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

source

theorem WithTop.toDual_le_iff {α : Type u_1} [LE α] {a : WithTop α} {b : WithBot αᵒᵈ} :

WithTop.toDual a ≤ b ↔ WithBot.ofDual b ≤ a

source

theorem WithTop.le_toDual_iff {α : Type u_1} [LE α] {a : WithBot αᵒᵈ} {b : WithTop α} :

a ≤ WithTop.toDual b ↔ b ≤ WithBot.ofDual a

source

@[simp]

theorem WithTop.toDual_le_toDual_iff {α : Type u_1} [LE α] {a : WithTop α} {b : WithTop α} :

WithTop.toDual a ≤ WithTop.toDual b ↔ b ≤ a

source

theorem WithTop.ofDual_le_iff {α : Type u_1} [LE α] {a : WithTop αᵒᵈ} {b : WithBot α} :

WithTop.ofDual a ≤ b ↔ WithBot.toDual b ≤ a

source

theorem WithTop.le_ofDual_iff {α : Type u_1} [LE α] {a : WithBot α} {b : WithTop αᵒᵈ} :

a ≤ WithTop.ofDual b ↔ b ≤ WithBot.toDual a

source

@[simp]

theorem WithTop.ofDual_le_ofDual_iff {α : Type u_1} [LE α] {a : WithTop αᵒᵈ} {b : WithTop αᵒᵈ} :

WithTop.ofDual a ≤ WithTop.ofDual b ↔ b ≤ a

source

@[simp]

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

↑a ≤ ↑b ↔ a ≤ b

source

@[simp]

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

some a ≤ some b ↔ a ≤ b

source

@[simp]

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

a ≤ none

source

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

OrderTop (WithTop α)

Equations

WithTop.orderTop = let __src := WithTop.top; OrderTop.mk ⋯

source

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

OrderBot (WithTop α)

Equations

WithTop.orderBot = OrderBot.mk ⋯

source

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

BoundedOrder (WithTop α)

Equations

WithTop.boundedOrder = let __src := WithTop.orderTop; let __src_1 := WithTop.orderBot; BoundedOrder.mk

source

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

¬⊤ ≤ ↑a

source

@[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.

source

theorem WithTop.le_coe {α : Type u_1} {a : α} {b : α} [LE α] {o : Option α} :

a ∈ o → (o ≤ ↑b ↔ a ≤ b)

source

theorem WithTop.le_coe_iff {α : Type u_1} {b : α} [LE α] {x : WithTop α} :

x ≤ ↑b ↔ ∃ (a : α), x = ↑a ∧ a ≤ b

source

theorem WithTop.coe_le_iff {α : Type u_1} {a : α} [LE α] {x : WithTop α} :

↑a ≤ x ↔ ∀ (b : α), x = ↑b → a ≤ b

source

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

IsMin ↑a

source

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

WithTop.untop a h ≤ b ↔ a ≤ ↑b

source

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

a ≤ WithTop.untop b h ↔ ↑a ≤ b

source

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

c ≤ WithTop.untop' b a ↔ ↑c ≤ a

source

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

LT (WithTop α)

Equations

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

source

theorem WithTop.toDual_lt_iff {α : Type u_1} [LT α] {a : WithTop α} {b : WithBot αᵒᵈ} :

WithTop.toDual a < b ↔ WithBot.ofDual b < a

source

theorem WithTop.lt_toDual_iff {α : Type u_1} [LT α] {a : WithBot αᵒᵈ} {b : WithTop α} :

a < WithTop.toDual b ↔ b < WithBot.ofDual a

source

@[simp]

theorem WithTop.toDual_lt_toDual_iff {α : Type u_1} [LT α] {a : WithTop α} {b : WithTop α} :

WithTop.toDual a < WithTop.toDual b ↔ b < a

source

theorem WithTop.ofDual_lt_iff {α : Type u_1} [LT α] {a : WithTop αᵒᵈ} {b : WithBot α} :

WithTop.ofDual a < b ↔ WithBot.toDual b < a

source

theorem WithTop.lt_ofDual_iff {α : Type u_1} [LT α] {a : WithBot α} {b : WithTop αᵒᵈ} :

a < WithTop.ofDual b ↔ b < WithBot.toDual a

source

@[simp]

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

WithTop.ofDual a < WithTop.ofDual b ↔ b < a

source

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

c < WithTop.untop' b a ↔ ↑c < a

source

@[simp]

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

WithBot.toDual.symm a = WithTop.ofDual a

source

@[simp]

theorem WithBot.ofDual_symm_apply {α : Type u_1} (a : WithTop α) :

WithBot.ofDual.symm a = WithTop.toDual a

source

@[simp]

theorem WithBot.toDual_apply_bot {α : Type u_1} :

WithBot.toDual ⊥ = ⊤

source

@[simp]

theorem WithBot.ofDual_apply_bot {α : Type u_1} :

WithBot.ofDual ⊥ = ⊤

source

@[simp]

theorem WithBot.toDual_apply_coe {α : Type u_1} (a : α) :

WithBot.toDual ↑a = ↑(OrderDual.toDual a)

source

@[simp]

theorem WithBot.ofDual_apply_coe {α : Type u_1} (a : αᵒᵈ) :

WithBot.ofDual ↑a = ↑(OrderDual.ofDual a)

source

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

source

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

source

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)

source

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)

source

theorem WithBot.toDual_le_iff {α : Type u_1} [LE α] {a : WithBot α} {b : WithTop αᵒᵈ} :

WithBot.toDual a ≤ b ↔ WithTop.ofDual b ≤ a

source

theorem WithBot.le_toDual_iff {α : Type u_1} [LE α] {a : WithTop αᵒᵈ} {b : WithBot α} :

a ≤ WithBot.toDual b ↔ b ≤ WithTop.ofDual a

source

@[simp]

theorem WithBot.toDual_le_toDual_iff {α : Type u_1} [LE α] {a : WithBot α} {b : WithBot α} :

WithBot.toDual a ≤ WithBot.toDual b ↔ b ≤ a

source

theorem WithBot.ofDual_le_iff {α : Type u_1} [LE α] {a : WithBot αᵒᵈ} {b : WithTop α} :

WithBot.ofDual a ≤ b ↔ WithTop.toDual b ≤ a

source

theorem WithBot.le_ofDual_iff {α : Type u_1} [LE α] {a : WithTop α} {b : WithBot αᵒᵈ} :

a ≤ WithBot.ofDual b ↔ b ≤ WithTop.toDual a

source

@[simp]

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

WithBot.ofDual a ≤ WithBot.ofDual b ↔ b ≤ a

source

theorem WithBot.toDual_lt_iff {α : Type u_1} [LT α] {a : WithBot α} {b : WithTop αᵒᵈ} :

WithBot.toDual a < b ↔ WithTop.ofDual b < a

source

theorem WithBot.lt_toDual_iff {α : Type u_1} [LT α] {a : WithTop αᵒᵈ} {b : WithBot α} :

a < WithBot.toDual b ↔ b < WithTop.ofDual a

source

@[simp]

theorem WithBot.toDual_lt_toDual_iff {α : Type u_1} [LT α] {a : WithBot α} {b : WithBot α} :

WithBot.toDual a < WithBot.toDual b ↔ b < a

source

theorem WithBot.ofDual_lt_iff {α : Type u_1} [LT α] {a : WithBot αᵒᵈ} {b : WithTop α} :

WithBot.ofDual a < b ↔ WithTop.toDual b < a

source

theorem WithBot.lt_ofDual_iff {α : Type u_1} [LT α] {a : WithTop α} {b : WithBot αᵒᵈ} :

a < WithBot.ofDual b ↔ b < WithTop.toDual a

source

@[simp]

theorem WithBot.ofDual_lt_ofDual_iff {α : Type u_1} [LT α] {a : WithBot αᵒᵈ} {b : WithBot αᵒᵈ} :

WithBot.ofDual a < WithBot.ofDual b ↔ b < a

source

@[simp]

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

↑a < ↑b ↔ a < b

source

@[simp]

theorem WithTop.some_lt_some {α : Type u_1} [LT α] {a : α} {b : α} :

some a < some b ↔ a < b

source

@[simp]

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

↑a < ⊤

source

@[simp]

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

some a < none

source

@[simp]

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

¬none < a

source

theorem WithTop.lt_iff_exists_coe {α : Type u_1} [LT α] {a : WithTop α} {b : WithTop α} :

a < b ↔ ∃ (p : α), a = ↑p ∧ ↑p < b

source

theorem WithTop.coe_lt_iff {α : Type u_1} [LT α] {a : α} {x : WithTop α} :

↑a < x ↔ ∀ (b : α), x = ↑b → a < b

source

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

source

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

Preorder (WithTop α)

Equations

WithTop.preorder = Preorder.mk ⋯ ⋯ ⋯

source

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

PartialOrder (WithTop α)

Equations

WithTop.partialOrder = PartialOrder.mk ⋯

source

theorem WithTop.coe_strictMono {α : Type u_1} [Preorder α] :

StrictMono fun (a : α) => ↑a

source

theorem WithTop.coe_mono {α : Type u_1} [Preorder α] :

Monotone fun (a : α) => ↑a

source

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 ⊤

source

@[simp]

theorem WithTop.monotone_map_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} :

Monotone (WithTop.map f) ↔ Monotone f

source

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.

source

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 ⊤

source

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

source

@[simp]

theorem WithTop.strictMono_map_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} :

StrictMono (WithTop.map f) ↔ StrictMono f

source

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.

source

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) :