order.with_bot

`with_bot`, `with_top`#

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Adding a `bot` or a `top` to an order.

Main declarations #

• `with_<top/bot> α`: Equips `option α` with the order on `α` plus `none` as the top/bottom element.
def with_bot (α : Type u_1) :
Type u_1

Attach `⊥` to a type.

Equations
Instances for `with_bot`
@[protected, instance]
meta def with_bot.has_to_format {α : Type u_1}  :
@[protected, instance]
def with_bot.has_repr {α : Type u_1} [has_repr α] :
Equations
@[protected, instance]
def with_bot.has_coe_t {α : Type u_1} :
(with_bot α)
Equations
@[protected, instance]
def with_bot.has_bot {α : Type u_1} :
Equations
@[protected, instance]
meta def with_bot.has_reflect {α : Type} [ α] [has_reflect α] :
@[protected, instance]
def with_bot.inhabited {α : Type u_1} :
Equations
@[protected, instance]
def with_bot.nontrivial {α : Type u_1} [nonempty α] :
theorem with_bot.coe_injective {α : Type u_1} :
@[norm_cast]
theorem with_bot.coe_inj {α : Type u_1} {a b : α} :
a = b a = b
@[protected]
theorem with_bot.forall {α : Type u_1} {p : Prop} :
( (x : with_bot α), p x) p (x : α), p x
@[protected]
theorem with_bot.exists {α : Type u_1} {p : Prop} :
( (x : with_bot α), p x) p (x : α), p x
theorem with_bot.none_eq_bot {α : Type u_1} :
theorem with_bot.some_eq_coe {α : Type u_1} (a : α) :
@[simp]
theorem with_bot.bot_ne_coe {α : Type u_1} {a : α} :
@[simp]
theorem with_bot.coe_ne_bot {α : Type u_1} {a : α} :
def with_bot.rec_bot_coe {α : Type u_1} {C : Sort u_2} (h₁ : C ) (h₂ : Π (a : α), C a) (n : with_bot α) :
C n

Recursor for `with_bot` using the preferred forms `⊥` and `↑a`.

Equations
• h₂ = option.rec h₁ h₂
@[simp]
theorem with_bot.rec_bot_coe_bot {α : Type u_1} {C : Sort u_2} (d : C ) (f : Π (a : α), C a) :
= d
@[simp]
theorem with_bot.rec_bot_coe_coe {α : Type u_1} {C : Sort u_2} (d : C ) (f : Π (a : α), C a) (x : α) :
= f x
def with_bot.unbot' {α : Type u_1} (d : α) (x : with_bot α) :
α

Specialization of `option.get_or_else` to values in `with_bot α` that respects API boundaries.

Equations
@[simp]
theorem with_bot.unbot'_bot {α : Type u_1} (d : α) :
@[simp]
theorem with_bot.unbot'_coe {α : Type u_1} (d x : α) :
= x
@[norm_cast]
theorem with_bot.coe_eq_coe {α : Type u_1} {a b : α} :
a = b a = b
theorem with_bot.unbot'_eq_iff {α : Type u_1} {d y : α} {x : with_bot α} :
= y x = y x = y = d
@[simp]
theorem with_bot.unbot'_eq_self_iff {α : Type u_1} {d : α} {x : with_bot α} :
= d x = d x =
theorem with_bot.unbot'_eq_unbot'_iff {α : Type u_1} {d : α} {x y : with_bot α} :
= x = y x = d y = x = y = d
def with_bot.map {α : Type u_1} {β : Type u_2} (f : α β) :

Lift a map `f : α → β` to `with_bot α → with_bot β`. Implemented using `option.map`.

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

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

Equations
@[simp]
theorem with_bot.coe_unbot {α : Type u_1} (x : with_bot α) (h : x ) :
(x.unbot h) = x
@[simp]
theorem with_bot.unbot_coe {α : Type u_1} (x : α) (h : x := with_bot.coe_ne_bot) :
x.unbot h = x
@[protected, instance]
def with_bot.can_lift {α : Type u_1} :
can_lift (with_bot α) α coe (λ (r : with_bot α), r )
Equations
@[protected, instance]
def with_bot.has_le {α : Type u_1} [has_le α] :
Equations
@[simp]
theorem with_bot.some_le_some {α : Type u_1} {a b : α} [has_le α] :
a b
@[simp, norm_cast]
theorem with_bot.coe_le_coe {α : Type u_1} {a b : α} [has_le α] :
a b a b
@[simp]
theorem with_bot.none_le {α : Type u_1} [has_le α] {a : with_bot α} :
@[protected, instance]
def with_bot.order_bot {α : Type u_1} [has_le α] :
Equations
@[protected, instance]
def with_bot.order_top {α : Type u_1} [has_le α] [order_top α] :
Equations
@[protected, instance]
def with_bot.bounded_order {α : Type u_1} [has_le α] [order_top α] :
Equations
theorem with_bot.not_coe_le_bot {α : Type u_1} [has_le α] (a : α) :
theorem with_bot.coe_le {α : Type u_1} {a b : α} [has_le α] {o : option α} :
b o (a o a b)
theorem with_bot.coe_le_iff {α : Type u_1} {a : α} [has_le α] {x : with_bot α} :
a x (b : α), x = b a b
theorem with_bot.le_coe_iff {α : Type u_1} {b : α} [has_le α] {x : with_bot α} :
x b (a : α), x = a a b
@[protected]
theorem is_max.with_bot {α : Type u_1} {a : α} [has_le α] (h : is_max a) :
@[protected, instance]
def with_bot.has_lt {α : Type u_1} [has_lt α] :
Equations
@[simp]
theorem with_bot.some_lt_some {α : Type u_1} {a b : α} [has_lt α] :
a < b
@[simp, norm_cast]
theorem with_bot.coe_lt_coe {α : Type u_1} {a b : α} [has_lt α] :
a < b a < b
@[simp]
theorem with_bot.none_lt_some {α : Type u_1} [has_lt α] (a : α) :
theorem with_bot.bot_lt_coe {α : Type u_1} [has_lt α] (a : α) :
@[simp]
theorem with_bot.not_lt_none {α : Type u_1} [has_lt α] (a : with_bot α) :
theorem with_bot.lt_iff_exists_coe {α : Type u_1} [has_lt α] {a b : with_bot α} :
a < b (p : α), b = p a < p
theorem with_bot.lt_coe_iff {α : Type u_1} {b : α} [has_lt α] {x : with_bot α} :
x < b (a : α), x = a a < b
@[protected]
theorem with_bot.bot_lt_iff_ne_bot {α : Type u_1} [has_lt α] {x : with_bot α} :

A version of `bot_lt_iff_ne_bot` for `with_bot` that only requires `has_lt α`, not `partial_order α`.

@[protected, instance]
def with_bot.preorder {α : Type u_1} [preorder α] :
Equations
@[protected, instance]
def with_bot.partial_order {α : Type u_1}  :
Equations
theorem with_bot.coe_strict_mono {α : Type u_1} [preorder α] :
theorem with_bot.coe_mono {α : Type u_1} [preorder α] :
theorem with_bot.monotone_iff {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : β} :
monotone (f coe) (x : α), f f x
@[simp]
theorem with_bot.monotone_map_iff {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α β} :
theorem monotone.with_bot_map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α β} :

Alias of the reverse direction of `with_bot.monotone_map_iff`.

theorem with_bot.strict_mono_iff {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : β} :
strict_mono (f coe) (x : α), f < f x
@[simp]
theorem with_bot.strict_mono_map_iff {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α β} :
theorem strict_mono.with_bot_map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α β} :

Alias of the reverse direction of `with_bot.strict_mono_map_iff`.

theorem with_bot.map_le_iff {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α β) (mono_iff : {a b : α}, f a f b a b) (a b : with_bot α) :
a b a b
theorem with_bot.le_coe_unbot' {α : Type u_1} [preorder α] (a : with_bot α) (b : α) :
a a)
theorem with_bot.unbot'_bot_le_iff {α : Type u_1} [has_le α] [order_bot α] {a : with_bot α} {b : α} :
a b
theorem with_bot.unbot'_lt_iff {α : Type u_1} [has_lt α] {a : with_bot α} {b c : α} (ha : a ) :
< c a < c
@[protected, instance]
def with_bot.semilattice_sup {α : Type u_1}  :
Equations
theorem with_bot.coe_sup {α : Type u_1} (a b : α) :
(a b) = a b
@[protected, instance]
def with_bot.semilattice_inf {α : Type u_1}  :
Equations
theorem with_bot.coe_inf {α : Type u_1} (a b : α) :
(a b) = a b
@[protected, instance]
def with_bot.lattice {α : Type u_1} [lattice α] :
Equations
@[protected, instance]
def with_bot.distrib_lattice {α : Type u_1}  :
Equations
@[protected, instance]
def with_bot.decidable_le {α : Type u_1} [has_le α]  :
Equations
@[protected, instance]
def with_bot.decidable_lt {α : Type u_1} [has_lt α]  :
Equations
@[protected, instance]
def with_bot.is_total_le {α : Type u_1} [has_le α]  :
@[protected, instance]
def with_bot.linear_order {α : Type u_1} [linear_order α] :
Equations
@[norm_cast]
theorem with_bot.coe_min {α : Type u_1} [linear_order α] (x y : α) :
y) =
@[norm_cast]
theorem with_bot.coe_max {α : Type u_1} [linear_order α] (x y : α) :
y) =
theorem with_bot.well_founded_lt {α : Type u_1} [preorder α]  :
@[protected, instance]
def with_bot.densely_ordered {α : Type u_1} [has_lt α] [no_min_order α] :
theorem with_bot.lt_iff_exists_coe_btwn {α : Type u_1} [preorder α] [no_min_order α] {a b : with_bot α} :
a < b (x : α), a < x x < b
@[protected, instance]
def with_bot.no_top_order {α : Type u_1} [has_le α] [no_top_order α] [nonempty α] :
@[protected, instance]
def with_bot.no_max_order {α : Type u_1} [has_lt α] [no_max_order α] [nonempty α] :
def with_top (α : Type u_1) :
Type u_1

Attach `⊤` to a type.

Equations
Instances for `with_top`
@[protected, instance]
meta def with_top.has_to_format {α : Type u_1}  :
@[protected, instance]
def with_top.has_repr {α : Type u_1} [has_repr α] :
Equations
@[protected, instance]
def with_top.has_coe_t {α : Type u_1} :
(with_top α)
Equations
@[protected, instance]
def with_top.has_top {α : Type u_1} :
Equations
@[protected, instance]
meta def with_top.has_reflect {α : Type} [ α] [has_reflect α] :
@[protected, instance]
def with_top.inhabited {α : Type u_1} :
Equations
@[protected, instance]
def with_top.nontrivial {α : Type u_1} [nonempty α] :
@[protected]
theorem with_top.forall {α : Type u_1} {p : Prop} :
( (x : with_top α), p x) p (x : α), p x
@[protected]
theorem with_top.exists {α : Type u_1} {p : Prop} :
( (x : with_top α), p x) p (x : α), p x
theorem with_top.none_eq_top {α : Type u_1} :
theorem with_top.some_eq_coe {α : Type u_1} (a : α) :
@[simp]
theorem with_top.top_ne_coe {α : Type u_1} {a : α} :
@[simp]
theorem with_top.coe_ne_top {α : Type u_1} {a : α} :
def with_top.rec_top_coe {α : Type u_1} {C : Sort u_2} (h₁ : C ) (h₂ : Π (a : α), C a) (n : with_top α) :
C n

Recursor for `with_top` using the preferred forms `⊤` and `↑a`.

Equations
• h₂ = option.rec h₁ h₂
@[simp]
theorem with_top.rec_top_coe_top {α : Type u_1} {C : Sort u_2} (d : C ) (f : Π (a : α), C a) :
= d
@[simp]
theorem with_top.rec_top_coe_coe {α : Type u_1} {C : Sort u_2} (d : C ) (f : Π (a : α), C a) (x : α) :
= f x
@[protected]
def with_top.to_dual {α : Type u_1} :

`with_top.to_dual` is the equivalence sending `⊤` to `⊥` and any `a : α` to `to_dual a : αᵒᵈ`. See `with_top.to_dual_bot_equiv` for the related order-iso.

Equations
@[protected]
def with_top.of_dual {α : Type u_1} :

`with_top.of_dual` is the equivalence sending `⊤` to `⊥` and any `a : αᵒᵈ` to `of_dual a : α`. See `with_top.to_dual_bot_equiv` for the related order-iso.

Equations
@[protected]
def with_bot.to_dual {α : Type u_1} :

`with_bot.to_dual` is the equivalence sending `⊥` to `⊤` and any `a : α` to `to_dual a : αᵒᵈ`. See `with_bot.to_dual_top_equiv` for the related order-iso.

Equations
@[protected]
def with_bot.of_dual {α : Type u_1} :

`with_bot.of_dual` is the equivalence sending `⊥` to `⊤` and any `a : αᵒᵈ` to `of_dual a : α`. See `with_bot.to_dual_top_equiv` for the related order-iso.

Equations
@[simp]
theorem with_top.to_dual_symm_apply {α : Type u_1} (a : with_bot αᵒᵈ) :
@[simp]
theorem with_top.of_dual_symm_apply {α : Type u_1} (a : with_bot α) :
@[simp]
theorem with_top.to_dual_apply_top {α : Type u_1} :
@[simp]
theorem with_top.of_dual_apply_top {α : Type u_1} :
@[simp]
theorem with_top.to_dual_apply_coe {α : Type u_1} (a : α) :
@[simp]
theorem with_top.of_dual_apply_coe {α : Type u_1} (a : αᵒᵈ) :
def with_top.untop' {α : Type u_1} (d : α) (x : with_top α) :
α

Specialization of `option.get_or_else` to values in `with_top α` that respects API boundaries.

Equations
@[simp]
theorem with_top.untop'_top {α : Type u_1} (d : α) :
@[simp]
theorem with_top.untop'_coe {α : Type u_1} (d x : α) :
= x
@[norm_cast]
theorem with_top.coe_eq_coe {α : Type u_1} {a b : α} :
a = b a = b
theorem with_top.untop'_eq_iff {α : Type u_1} {d y : α} {x : with_top α} :
= y x = y x = y = d
@[simp]
theorem with_top.untop'_eq_self_iff {α : Type u_1} {d : α} {x : with_top α} :
= d x = d x =
theorem with_top.untop'_eq_untop'_iff {α : Type u_1} {d : α} {x y : with_top α} :
= x = y x = d y = x = y = d
def with_top.map {α : Type u_1} {β : Type u_2} (f : α β) :

Lift a map `f : α → β` to `with_top α → with_top β`. Implemented using `option.map`.

Equations
@[simp]
theorem with_top.map_top {α : Type u_1} {β : Type u_2} (f : α β) :
@[simp]
theorem with_top.map_coe {α : Type u_1} {β : Type u_2} (f : α β) (a : α) :
= (f a)
theorem with_top.map_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f₁ : α β} {f₂ : α γ} {g₁ : β δ} {g₂ : γ δ} (h : g₁ f₁ = g₂ f₂) (a : α) :
(with_top.map f₁ a) = (with_top.map f₂ a)
theorem with_top.map_to_dual {α : Type u_1} {β : Type u_2} (f : αᵒᵈ βᵒᵈ) (a : with_bot α) :
theorem with_top.map_of_dual {α : Type u_1} {β : Type u_2} (f : α β) (a : with_bot αᵒᵈ) :
theorem with_top.to_dual_map {α : Type u_1} {β : Type u_2} (f : α β) (a : with_top α) :
theorem with_top.of_dual_map {α : Type u_1} {β : Type u_2} (f : αᵒᵈ βᵒᵈ) (a : with_top αᵒᵈ) :
theorem with_top.ne_top_iff_exists {α : Type u_1} {x : with_top α} :
x (a : α), a = x
def with_top.untop {α : Type u_1} (x : with_top α) :
x α

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

Equations
@[simp]
theorem with_top.coe_untop {α : Type u_1} (x : with_top α) (h : x ) :
(x.untop h) = x
@[simp]
theorem with_top.untop_coe {α : Type u_1} (x : α) (h : x := with_top.coe_ne_top) :
x.untop h = x
@[protected, instance]
def with_top.can_lift {α : Type u_1} :
can_lift (with_top α) α coe (λ (r : with_top α), r )
Equations
@[protected, instance]
def with_top.has_le {α : Type u_1} [has_le α] :
Equations
theorem with_top.to_dual_le_iff {α : Type u_1} [has_le α] {a : with_top α} {b : with_bot αᵒᵈ} :
theorem with_top.le_to_dual_iff {α : Type u_1} [has_le α] {a : with_bot αᵒᵈ} {b : with_top α} :
@[simp]
theorem with_top.to_dual_le_to_dual_iff {α : Type u_1} [has_le α] {a b : with_top α} :
b a
theorem with_top.of_dual_le_iff {α : Type u_1} [has_le α] {a : with_top αᵒᵈ} {b : with_bot α} :
theorem with_top.le_of_dual_iff {α : Type u_1} [has_le α] {a : with_bot α} {b : with_top αᵒᵈ} :
@[simp]
theorem with_top.of_dual_le_of_dual_iff {α : Type u_1} [has_le α] {a b : with_top αᵒᵈ} :
b a
@[simp, norm_cast]
theorem with_top.coe_le_coe {α : Type u_1} {a b : α} [has_le α] :
a b a b
@[simp]
theorem with_top.some_le_some {α : Type u_1} {a b : α} [has_le α] :
a b
@[simp]
theorem with_top.le_none {α : Type u_1} [has_le α] {a : with_top α} :
@[protected, instance]
def with_top.order_top {α : Type u_1} [has_le α] :
Equations
@[protected, instance]
def with_top.order_bot {α : Type u_1} [has_le α] [order_bot α] :
Equations
@[protected, instance]
def with_top.bounded_order {α : Type u_1} [has_le α] [order_bot α] :
Equations
theorem with_top.not_top_le_coe {α : Type u_1} [has_le α] (a : α) :
theorem with_top.le_coe {α : Type u_1} {a b : α} [has_le α] {o : option α} :
a o (o b a b)
theorem with_top.le_coe_iff {α : Type u_1} {b : α} [has_le α] {x : with_top α} :
x b (a : α), x = a a b
theorem with_top.coe_le_iff {α : Type u_1} {a : α} [has_le α] {x : with_top α} :
a x (b : α), x = b a b
@[protected]
theorem is_min.with_top {α : Type u_1} {a : α} [has_le α] (h : is_min a) :
@[protected, instance]
def with_top.has_lt {α : Type u_1} [has_lt α] :
Equations
theorem with_top.to_dual_lt_iff {α : Type u_1} [has_lt α] {a : with_top α} {b : with_bot αᵒᵈ} :
theorem with_top.lt_to_dual_iff {α : Type u_1} [has_lt α] {a : with_bot αᵒᵈ} {b : with_top α} :
@[simp]
theorem with_top.to_dual_lt_to_dual_iff {α : Type u_1} [has_lt α] {a b : with_top α} :
b < a
theorem with_top.of_dual_lt_iff {α : Type u_1} [has_lt α] {a : with_top αᵒᵈ} {b : with_bot α} :
theorem with_top.lt_of_dual_iff {α : Type u_1} [has_lt α] {a : with_bot α} {b : with_top αᵒᵈ} :
@[simp]
theorem with_top.of_dual_lt_of_dual_iff {α : Type u_1} [has_lt α] {a b : with_top αᵒᵈ} :
b < a
@[simp]
theorem with_bot.to_dual_symm_apply {α : Type u_1} (a : with_top αᵒᵈ) :
@[simp]
theorem with_bot.of_dual_symm_apply {α : Type u_1} (a : with_top α) :
@[simp]
theorem with_bot.to_dual_apply_bot {α : Type u_1} :
@[simp]
theorem with_bot.of_dual_apply_bot {α : Type u_1} :
@[simp]
theorem with_bot.to_dual_apply_coe {α : Type u_1} (a : α) :
@[simp]
theorem with_bot.of_dual_apply_coe {α : Type u_1} (a : αᵒᵈ) :
theorem with_bot.map_to_dual {α : Type u_1} {β : Type u_2} (f : αᵒᵈ βᵒᵈ) (a : with_top α) :
theorem with_bot.map_of_dual {α : Type u_1} {β : Type u_2} (f : α β) (a : with_top αᵒᵈ) :
theorem with_bot.to_dual_map {α : Type u_1} {β : Type u_2} (f : α β) (a : with_bot α) :
theorem with_bot.of_dual_map {α : Type u_1} {β : Type u_2} (f : αᵒᵈ βᵒᵈ) (a : with_bot αᵒᵈ) :
theorem with_bot.to_dual_le_iff {α : Type u_1} [has_le α] {a : with_bot α} {b : with_top αᵒᵈ} :
theorem with_bot.le_to_dual_iff {α : Type u_1} [has_le α] {a : with_top αᵒᵈ} {b : with_bot α} :
@[simp]
theorem with_bot.to_dual_le_to_dual_iff {α : Type u_1} [has_le α] {a b : with_bot α} :
b a
theorem with_bot.of_dual_le_iff {α : Type u_1} [has_le α] {a : with_bot αᵒᵈ} {b : with_top α} :
theorem with_bot.le_of_dual_iff {α : Type u_1} [has_le α] {a : with_top α} {b : with_bot αᵒᵈ} :
@[simp]
theorem with_bot.of_dual_le_of_dual_iff {α : Type u_1} [has_le α] {a b : with_bot αᵒᵈ} :
b a
theorem with_bot.to_dual_lt_iff {α : Type u_1} [has_lt α] {a : with_bot α} {b : with_top αᵒᵈ} :
theorem with_bot.lt_to_dual_iff {α : Type u_1} [has_lt α] {a : with_top αᵒᵈ} {b : with_bot α} :
@[simp]
theorem with_bot.to_dual_lt_to_dual_iff {α : Type u_1} [has_lt α] {a b : with_bot α} :
b < a
theorem with_bot.of_dual_lt_iff {α : Type u_1} [has_lt α] {a : with_bot αᵒᵈ} {b : with_top α} :
theorem with_bot.lt_of_dual_iff {α : Type u_1} [has_lt α] {a : with_top α} {b : with_bot αᵒᵈ} :
@[simp]
theorem with_bot.of_dual_lt_of_dual_iff {α : Type u_1} [has_lt α] {a b : with_bot αᵒᵈ} :
b < a
@[simp, norm_cast]
theorem with_top.coe_lt_coe {α : Type u_1} [has_lt α] {a b : α} :
a < b a < b
@[simp]
theorem with_top.some_lt_some {α : Type u_1} [has_lt α] {a b : α} :
a < b
theorem with_top.coe_lt_top {α : Type u_1} [has_lt α] (a : α) :
@[simp]
theorem with_top.some_lt_none {α : Type u_1} [has_lt α] (a : α) :
@[simp]
theorem with_top.not_none_lt {α : Type u_1} [has_lt α] (a : with_top α) :
theorem with_top.lt_iff_exists_coe {α : Type u_1} [has_lt α] {a b : with_top α} :
a < b (p : α), a = p p < b
theorem with_top.coe_lt_iff {α : Type u_1} [has_lt α] {a : α} {x : with_top α} :
a < x (b : α), x = b a < b
@[protected]
theorem with_top.lt_top_iff_ne_top {α : Type u_1} [has_lt α] {x : with_top α} :

A version of `lt_top_iff_ne_top` for `with_top` that only requires `has_lt α`, not `partial_order α`.

@[protected, instance]
def with_top.preorder {α : Type u_1} [preorder α] :
Equations
@[protected, instance]
def with_top.partial_order {α : Type u_1}  :
Equations
theorem with_top.coe_strict_mono {α : Type u_1} [preorder α] :
theorem with_top.coe_mono {α : Type u_1} [preorder α] :
theorem with_top.monotone_iff {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : β} :
monotone (f coe) (x : α), f x f
@[simp]
theorem with_top.monotone_map_iff {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α β} :
theorem monotone.with_top_map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α β} :

Alias of the reverse direction of `with_top.monotone_map_iff`.

theorem with_top.strict_mono_iff {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : β} :
strict_mono (f coe) (x : α), f x < f
@[simp]
theorem with_top.strict_mono_map_iff {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α β} :
theorem strict_mono.with_top_map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α β} :

Alias of the reverse direction of `with_top.strict_mono_map_iff`.

theorem with_top.map_le_iff {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α β) (a b : with_top α) (mono_iff : {a b : α}, f a f b a b) :
a b a b
@[protected, instance]
def with_top.semilattice_inf {α : Type u_1}  :
Equations
theorem with_top.coe_inf {α : Type u_1} (a b : α) :
(a b) = a b
@[protected, instance]
def with_top.semilattice_sup {α : Type u_1}  :
Equations
theorem with_top.coe_sup {α : Type u_1} (a b : α) :
(a b) = a b
@[protected, instance]
def with_top.lattice {α : Type u_1} [lattice α] :
Equations
@[protected, instance]
def with_top.distrib_lattice {α : Type u_1}  :
Equations
@[protected, instance]
def with_top.decidable_le {α : Type u_1} [has_le α]  :
Equations
@[protected, instance]
def with_top.decidable_lt {α : Type u_1} [has_lt α]  :
Equations
@[protected, instance]
def with_top.is_total_le {α : Type u_1} [has_le α]  :
@[protected, instance]
def with_top.linear_order {α : Type u_1} [linear_order α] :
Equations
@[simp, norm_cast]
theorem with_top.coe_min {α : Type u_1} [linear_order α] (x y : α) :
y) =
@[simp, norm_cast]
theorem with_top.coe_max {α : Type u_1} [linear_order α] (x y : α) :
y) =
theorem with_top.well_founded_lt {α : Type u_1} [preorder α]  :
theorem with_top.well_founded_gt {α : Type u_1} [preorder α] (h : well_founded gt) :
theorem with_bot.well_founded_gt {α : Type u_1} [preorder α] (h : well_founded gt) :
@[protected, instance]
def with_top.trichotomous.lt {α : Type u_1} [preorder α]  :
@[protected, instance]
def with_top.is_well_order.lt {α : Type u_1} [preorder α] [h : has_lt.lt] :
@[protected, instance]
def with_top.trichotomous.gt {α : Type u_1} [preorder α]  :
@[protected, instance]
def with_top.is_well_order.gt {α : Type u_1} [preorder α] [h : gt] :
@[protected, instance]
def with_bot.trichotomous.lt {α : Type u_1} [preorder α] [h : has_lt.lt] :
@[protected, instance]
def with_bot.is_well_order.lt {α : Type u_1} [preorder α] [h : has_lt.lt] :
@[protected, instance]
def with_bot.trichotomous.gt {α : Type u_1} [preorder α] [h : gt] :
@[protected, instance]
def with_bot.is_well_order.gt {α : Type u_1} [preorder α] [h : gt] :
@[protected, instance]
def with_top.densely_ordered {α : Type u_1} [has_lt α] [no_max_order α] :
theorem with_top.lt_iff_exists_coe_btwn {α : Type u_1} [preorder α] [no_max_order α] {a b : with_top α} :
a < b (x : α), a < x x < b
@[protected, instance]
def with_top.no_bot_order {α : Type u_1} [has_le α] [no_bot_order α] [nonempty α] :
@[protected, instance]
def with_top.no_min_order {α : Type u_1} [has_lt α] [no_min_order α] [nonempty α] :