order.with_bot - scilib docs

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 g₁ (with_bot.map f₁ ↑a) = with_bot.map g₂ (with_bot.map f₂ ↑a)

source

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

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

source

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

with_bot.unbot (option.some x) h = x
⊥.unbot h = absurd with_bot.unbot._main._proof_1 h

source

@[simp]

theorem with_bot.coe_unbot {α : Type u_1} (x : with_bot α) (h : x ≠ ⊥) :

↑(x.unbot h) = x

source

@[simp]

theorem with_bot.unbot_coe {α : Type u_1} (x : α) (h : ↑x ≠ ⊥ := with_bot.coe_ne_bot) :

↑x.unbot h = x

source

@[protected, instance]

def with_bot.can_lift {α : Type u_1} :

can_lift (with_bot α) α coe (λ (r : with_bot α), r ≠ ⊥)

Equations

with_bot.can_lift = {prf := _}

source

@[protected, instance]

def with_bot.has_le {α : Type u_1} [has_le α] :

has_le (with_bot α)

Equations

with_bot.has_le = {le := λ (o₁ o₂ : option α), ∀ (a : α), a ∈ o₁ → (∃ (b : α) (H : b ∈ o₂), a ≤ b)}

source

@[simp]

theorem with_bot.some_le_some {α : Type u_1} {a b : α} [has_le α] :

option.some a ≤ option.some b ↔ a ≤ b

source

@[simp, norm_cast]

theorem with_bot.coe_le_coe {α : Type u_1} {a b : α} [has_le α] :

↑a ≤ ↑b ↔ a ≤ b

source

@[simp]

theorem with_bot.none_le {α : Type u_1} [has_le α] {a : with_bot α} :

option.none ≤ a

source

@[protected, instance]

def with_bot.order_bot {α : Type u_1} [has_le α] :

order_bot (with_bot α)

Equations

with_bot.order_bot = {bot := ⊥, bot_le := _}

source

@[protected, instance]

def with_bot.order_top {α : Type u_1} [has_le α] [order_top α] :

order_top (with_bot α)

Equations

with_bot.order_top = {top := option.some ⊤, le_top := _}

source

@[protected, instance]

def with_bot.bounded_order {α : Type u_1} [has_le α] [order_top α] :

bounded_order (with_bot α)

Equations

with_bot.bounded_order = {top := order_top.top with_bot.order_top, le_top := _, bot := order_bot.bot with_bot.order_bot, bot_le := _}

source

theorem with_bot.not_coe_le_bot {α : Type u_1} [has_le α] (a : α) :

¬↑a ≤ ⊥

source

theorem with_bot.coe_le {α : Type u_1} {a b : α} [has_le α] {o : option α} :

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

source

theorem with_bot.coe_le_iff {α : Type u_1} {a : α} [has_le α] {x : with_bot α} :

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

source

theorem with_bot.le_coe_iff {α : Type u_1} {b : α} [has_le α] {x : with_bot α} :

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

source

@[protected]

theorem is_max.with_bot {α : Type u_1} {a : α} [has_le α] (h : is_max a) :

is_max ↑a

source

@[protected, instance]

def with_bot.has_lt {α : Type u_1} [has_lt α] :

has_lt (with_bot α)

Equations

with_bot.has_lt = {lt := λ (o₁ o₂ : option α), ∃ (b : α) (H : b ∈ o₂), ∀ (a : α), a ∈ o₁ → a < b}

source

@[simp]

theorem with_bot.some_lt_some {α : Type u_1} {a b : α} [has_lt α] :

option.some a < option.some b ↔ a < b

source

@[simp, norm_cast]

theorem with_bot.coe_lt_coe {α : Type u_1} {a b : α} [has_lt α] :

↑a < ↑b ↔ a < b

source

@[simp]

theorem with_bot.none_lt_some {α : Type u_1} [has_lt α] (a : α) :

option.none < option.some a

source

theorem with_bot.bot_lt_coe {α : Type u_1} [has_lt α] (a : α) :

⊥ < ↑a

source

@[simp]

theorem with_bot.not_lt_none {α : Type u_1} [has_lt α] (a : with_bot α) :

¬a < option.none

source

theorem with_bot.lt_iff_exists_coe {α : Type u_1} [has_lt α] {a b : with_bot α} :

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

source

theorem with_bot.lt_coe_iff {α : Type u_1} {b : α} [has_lt α] {x : with_bot α} :

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

source

@[protected]

theorem with_bot.bot_lt_iff_ne_bot {α : Type u_1} [has_lt α] {x : with_bot α} :

⊥ < x ↔ x ≠ ⊥

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

source

@[protected, instance]

def with_bot.preorder {α : Type u_1} [preorder α] :

preorder (with_bot α)

Equations

with_bot.preorder = {le := has_le.le with_bot.has_le, lt := has_lt.lt with_bot.has_lt, le_refl := _, le_trans := _, lt_iff_le_not_le := _}

source

@[protected, instance]

def with_bot.partial_order {α : Type u_1} [partial_order α] :

partial_order (with_bot α)

Equations

with_bot.partial_order = {le := preorder.le with_bot.preorder, lt := preorder.lt with_bot.preorder, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

source

theorem with_bot.coe_strict_mono {α : Type u_1} [preorder α] :

strict_mono coe

source

theorem with_bot.coe_mono {α : Type u_1} [preorder α] :

monotone coe

source

theorem with_bot.monotone_iff {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : with_bot α → β} :

monotone f ↔ monotone (f ∘ coe) ∧ ∀ (x : α), f ⊥ ≤ f ↑x

source

@[simp]

theorem with_bot.monotone_map_iff {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α → β} :

monotone (with_bot.map f) ↔ monotone f

source

theorem monotone.with_bot_map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α → β} :

monotone f → monotone (with_bot.map f)

Alias of the reverse direction of with_bot.monotone_map_iff.

source

theorem with_bot.strict_mono_iff {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : with_bot α → β} :

strict_mono f ↔ strict_mono (f ∘ coe) ∧ ∀ (x : α), f ⊥ < f ↑x

source

@[simp]

theorem with_bot.strict_mono_map_iff {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α → β} :

strict_mono (with_bot.map f) ↔ strict_mono f

source

theorem strict_mono.with_bot_map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α → β} :

strict_mono f → strict_mono (with_bot.map f)

Alias of the reverse direction of with_bot.strict_mono_map_iff.

source

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

with_bot.map f a ≤ with_bot.map f b ↔ a ≤ b

source

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

a ≤ ↑(with_bot.unbot' b a)

source

theorem with_bot.unbot'_bot_le_iff {α : Type u_1} [has_le α] [order_bot α] {a : with_bot α} {b : α} :

with_bot.unbot' ⊥ a ≤ b ↔ a ≤ ↑b

source

theorem with_bot.unbot'_lt_iff {α : Type u_1} [has_lt α] {a : with_bot α} {b c : α} (ha : a ≠ ⊥) :

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

source

@[protected, instance]

def with_bot.semilattice_sup {α : Type u_1} [semilattice_sup α] :

semilattice_sup (with_bot α)

Equations

with_bot.semilattice_sup = {sup := option.lift_or_get has_sup.sup, le := partial_order.le with_bot.partial_order, lt := partial_order.lt with_bot.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _}

source

theorem with_bot.coe_sup {α : Type u_1} [semilattice_sup α] (a b : α) :

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

source

@[protected, instance]

def with_bot.semilattice_inf {α : Type u_1} [semilattice_inf α] :

semilattice_inf (with_bot α)

Equations

with_bot.semilattice_inf = {inf := option.map₂ has_inf.inf, le := partial_order.le with_bot.partial_order, lt := partial_order.lt with_bot.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, inf_le_left := _, inf_le_right := _, le_inf := _}

source

theorem with_bot.coe_inf {α : Type u_1} [semilattice_inf α] (a b : α) :

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

source

@[protected, instance]

def with_bot.lattice {α : Type u_1} [lattice α] :

lattice (with_bot α)

Equations

with_bot.lattice = {sup := semilattice_sup.sup with_bot.semilattice_sup, le := semilattice_sup.le with_bot.semilattice_sup, lt := semilattice_sup.lt with_bot.semilattice_sup, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf.inf with_bot.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[protected, instance]

def with_bot.distrib_lattice {α : Type u_1} [distrib_lattice α] :

distrib_lattice (with_bot α)

Equations

with_bot.distrib_lattice = {sup := lattice.sup with_bot.lattice, le := lattice.le with_bot.lattice, lt := lattice.lt with_bot.lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf with_bot.lattice, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _}

source

@[protected, instance]

def with_bot.decidable_le {α : Type u_1} [has_le α] [decidable_rel has_le.le] :

decidable_rel has_le.le

Equations

with_bot.decidable_le (option.some x) (option.some y) = dite (x ≤ y) (λ (h : x ≤ y), decidable.is_true _) (λ (h : ¬x ≤ y), decidable.is_false _)
with_bot.decidable_le (option.some x) option.none = decidable.is_false _
with_bot.decidable_le option.none x = decidable.is_true _

source

@[protected, instance]

def with_bot.decidable_lt {α : Type u_1} [has_lt α] [decidable_rel has_lt.lt] :

decidable_rel has_lt.lt

Equations

with_bot.decidable_lt (option.some x) (option.some y) = dite (x < y) (λ (h : x < y), decidable.is_true _) (λ (h : ¬x < y), decidable.is_false _)
with_bot.decidable_lt (option.some val) option.none = decidable.is_false _
with_bot.decidable_lt option.none (option.some x) = decidable.is_true _
with_bot.decidable_lt option.none option.none = decidable.is_false with_bot.decidable_lt._main._proof_1

source

@[protected, instance]

def with_bot.is_total_le {α : Type u_1} [has_le α] [is_total α has_le.le] :

is_total (with_bot α) has_le.le

source

@[protected, instance]

def with_bot.linear_order {α : Type u_1} [linear_order α] :

linear_order (with_bot α)

Equations

with_bot.linear_order = lattice.to_linear_order (with_bot α)

source

@[norm_cast]

theorem with_bot.coe_min {α : Type u_1} [linear_order α] (x y : α) :

↑(linear_order.min x y) = linear_order.min ↑x ↑y

source

@[norm_cast]

theorem with_bot.coe_max {α : Type u_1} [linear_order α] (x y : α) :

↑(linear_order.max x y) = linear_order.max ↑x ↑y

source

theorem with_bot.well_founded_lt {α : Type u_1} [preorder α] (h : well_founded has_lt.lt) :

well_founded has_lt.lt

source

@[protected, instance]

def with_bot.densely_ordered {α : Type u_1} [has_lt α] [densely_ordered α] [no_min_order α] :

densely_ordered (with_bot α)

source

theorem with_bot.lt_iff_exists_coe_btwn {α : Type u_1} [preorder α] [densely_ordered α] [no_min_order α] {a b : with_bot α} :

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

source

@[protected, instance]

def with_bot.no_top_order {α : Type u_1} [has_le α] [no_top_order α] [nonempty α] :

no_top_order (with_bot α)

source

@[protected, instance]

def with_bot.no_max_order {α : Type u_1} [has_lt α] [no_max_order α] [nonempty α] :

no_max_order (with_bot α)

source

def with_top (α : Type u_1) :

Type u_1

Attach ⊤ to a type.

Equations

with_top α = option α

Instances for with_top

source

@[protected, instance]

meta def with_top.has_to_format {α : Type u_1} [has_to_format α] :

has_to_format (with_top α)

source

@[protected, instance]

def with_top.has_repr {α : Type u_1} [has_repr α] :

has_repr (with_top α)

Equations

with_top.has_repr = {repr := λ (o : with_top α), with_top.has_repr._match_1 o}
with_top.has_repr._match_1 (option.some a) = "↑" ++ repr a
with_top.has_repr._match_1 option.none = "⊤"

source

@[protected, instance]

def with_top.has_coe_t {α : Type u_1} :

has_coe_t α (with_top α)

Equations

with_top.has_coe_t = {coe := option.some α}

source

@[protected, instance]

def with_top.has_top {α : Type u_1} :

has_top (with_top α)

Equations

with_top.has_top = {top := option.none α}

source

@[protected, instance]

meta def with_top.has_reflect {α : Type} [reflected Type α] [has_reflect α] :

has_reflect (with_top α)

source

@[protected, instance]

def with_top.inhabited {α : Type u_1} :

inhabited (with_top α)

Equations

with_top.inhabited = {default := ⊤}

source

@[protected, instance]

def with_top.nontrivial {α : Type u_1} [nonempty α] :

nontrivial (with_top α)

source

@[protected]

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

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

source

@[protected]

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

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

source

theorem with_top.none_eq_top {α : Type u_1} :

option.none = ⊤

source

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

option.some a = ↑a

source

@[simp]

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

⊤ ≠ ↑a

source

@[simp]

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

↑a ≠ ⊤

source

def with_top.rec_top_coe {α : Type u_1} {C : with_top α → 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

with_top.rec_top_coe h₁ h₂ = option.rec h₁ h₂

source

@[simp]

theorem with_top.rec_top_coe_top {α : Type u_1} {C : with_top α → Sort u_2} (d : C ⊤) (f : Π (a : α), C ↑a) :

with_top.rec_top_coe d f ⊤ = d

source

@[simp]

theorem with_top.rec_top_coe_coe {α : Type u_1} {C : with_top α → Sort u_2} (d : C ⊤) (f : Π (a : α), C ↑a) (x : α) :

with_top.rec_top_coe d f ↑x = f x

source

@[protected]

def with_top.to_dual {α : Type u_1} :

with_top α ≃ with_bot αᵒᵈ

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

with_top.to_dual = equiv.refl (with_top α)

source

@[protected]

def with_top.of_dual {α : Type u_1} :

with_top αᵒᵈ ≃ with_bot α

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

with_top.of_dual = equiv.refl (with_top αᵒᵈ)

source

@[protected]

def with_bot.to_dual {α : Type u_1} :

with_bot α ≃ with_top αᵒᵈ

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

with_bot.to_dual = equiv.refl (with_bot α)

source

@[protected]

def with_bot.of_dual {α : Type u_1} :

with_bot αᵒᵈ ≃ with_top α

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

with_bot.of_dual = equiv.refl (with_bot αᵒᵈ)

source

@[simp]

theorem with_top.to_dual_symm_apply {α : Type u_1} (a : with_bot αᵒᵈ) :

⇑(with_top.to_dual.symm) a = ⇑with_bot.of_dual a

source

@[simp]

theorem with_top.of_dual_symm_apply {α : Type u_1} (a : with_bot α) :

⇑(with_top.of_dual.symm) a = ⇑with_bot.to_dual a

source

@[simp]

theorem with_top.to_dual_apply_top {α : Type u_1} :

⇑with_top.to_dual ⊤ = ⊥

source

@[simp]

theorem with_top.of_dual_apply_top {α : Type u_1} :

⇑with_top.of_dual ⊤ = ⊥

source

@[simp]

theorem with_top.to_dual_apply_coe {α : Type u_1} (a : α) :

⇑with_top.to_dual ↑a = ↑(⇑order_dual.to_dual a)

source

@[simp]

theorem with_top.of_dual_apply_coe {α : Type u_1} (a : αᵒᵈ) :

⇑with_top.of_dual ↑a = ↑(⇑order_dual.of_dual a)

source

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

with_top.untop' d x = with_top.rec_top_coe d id x

source

@[simp]

theorem with_top.untop'_top {α : Type u_1} (d : α) :

with_top.untop' d ⊤ = d

source

@[simp]

theorem with_top.untop'_coe {α : Type u_1} (d x : α) :

with_top.untop' d ↑x = x

source

@[norm_cast]

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

↑a = ↑b ↔ a = b

source

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

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

source

@[simp]

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

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

source

theorem with_top.untop'_eq_untop'_iff {α : Type u_1} {d : α} {x y : with_top α} :

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

source

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

with_top α → with_top β

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

Equations

with_top.map f = option.map f

source

@[simp]

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

with_top.map f ⊤ = ⊤

source

@[simp]

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

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

source

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 g₁ (with_top.map f₁ ↑a) = with_top.map g₂ (with_top.map f₂ ↑a)

source

theorem with_top.map_to_dual {α : Type u_1} {β : Type u_2} (f : αᵒᵈ → βᵒᵈ) (a : with_bot α) :

with_top.map f (⇑with_bot.to_dual a) = with_bot.map (⇑order_dual.to_dual ∘ f) a

source

theorem with_top.map_of_dual {α : Type u_1} {β : Type u_2} (f : α → β) (a : with_bot αᵒᵈ) :

with_top.map f (⇑with_bot.of_dual a) = with_bot.map (⇑order_dual.of_dual ∘ f) a

source

theorem with_top.to_dual_map {α : Type u_1} {β : Type u_2} (f : α → β) (a : with_top α) :

⇑with_top.to_dual (with_top.map f a) = with_bot.map (⇑order_dual.to_dual ∘ f ∘ ⇑order_dual.of_dual) (⇑with_top.to_dual a)

source

theorem with_top.of_dual_map {α : Type u_1} {β : Type u_2} (f : αᵒᵈ → βᵒᵈ) (a : with_top αᵒᵈ) :

⇑with_top.of_dual (with_top.map f a) = with_bot.map (⇑order_dual.of_dual ∘ f ∘ ⇑order_dual.to_dual) (⇑with_top.of_dual a)

source

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

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

source

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

with_top.untop = with_bot.unbot

source

@[simp]

theorem with_top.coe_untop {α : Type u_1} (x : with_top α) (h : x ≠ ⊤) :

↑(x.untop h) = x

source

@[simp]

theorem with_top.untop_coe {α : Type u_1} (x : α) (h : ↑x ≠ ⊤ := with_top.coe_ne_top) :

↑x.untop h = x

source

@[protected, instance]

def with_top.can_lift {α : Type u_1} :

can_lift (with_top α) α coe (λ (r : with_top α), r ≠ ⊤)

Equations

with_top.can_lift = {prf := _}

source

@[protected, instance]

def with_top.has_le {α : Type u_1} [has_le α] :

has_le (with_top α)

Equations

with_top.has_le = {le := λ (o₁ o₂ : option α), ∀ (a : α), a ∈ o₂ → (∃ (b : α) (H : b ∈ o₁), b ≤ a)}

source

theorem with_top.to_dual_le_iff {α : Type u_1} [has_le α] {a : with_top α} {b : with_bot αᵒᵈ} :

⇑with_top.to_dual a ≤ b ↔ ⇑with_bot.of_dual b ≤ a

source

theorem with_top.le_to_dual_iff {α : Type u_1} [has_le α] {a : with_bot αᵒᵈ} {b : with_top α} :

a ≤ ⇑with_top.to_dual b ↔ b ≤ ⇑with_bot.of_dual a

source

@[simp]

theorem with_top.to_dual_le_to_dual_iff {α : Type u_1} [has_le α] {a b : with_top α} :

⇑with_top.to_dual a ≤ ⇑with_top.to_dual b ↔ b ≤ a

source

theorem with_top.of_dual_le_iff {α : Type u_1} [has_le α] {a : with_top αᵒᵈ} {b : with_bot α} :

⇑with_top.of_dual a ≤ b ↔ ⇑with_bot.to_dual b ≤ a

source

theorem with_top.le_of_dual_iff {α : Type u_1} [has_le α] {a : with_bot α} {b : with_top αᵒᵈ} :

a ≤ ⇑with_top.of_dual b ↔ b ≤ ⇑with_bot.to_dual a

source

@[simp]

theorem with_top.of_dual_le_of_dual_iff {α : Type u_1} [has_le α] {a b : with_top αᵒᵈ} :

⇑with_top.of_dual a ≤ ⇑with_top.of_dual b ↔ b ≤ a

source

@[simp, norm_cast]

theorem with_top.coe_le_coe {α : Type u_1} {a b : α} [has_le α] :

↑a ≤ ↑b ↔ a ≤ b

source

@[simp]

theorem with_top.some_le_some {α : Type u_1} {a b : α} [has_le α] :

option.some a ≤ option.some b ↔ a ≤ b

source

@[simp]

theorem with_top.le_none {α : Type u_1} [has_le α] {a : with_top α} :

a ≤ option.none

source

@[protected, instance]

def with_top.order_top {α : Type u_1} [has_le α] :

order_top (with_top α)

Equations

with_top.order_top = {top := ⊤, le_top := _}

source

@[protected, instance]

def with_top.order_bot {α : Type u_1} [has_le α] [order_bot α] :

order_bot (with_top α)

Equations

with_top.order_bot = {bot := option.some ⊥, bot_le := _}

source

@[protected, instance]

def with_top.bounded_order {α : Type u_1} [has_le α] [order_bot α] :

bounded_order (with_top α)

Equations

with_top.bounded_order = {top := order_top.top with_top.order_top, le_top := _, bot := order_bot.bot with_top.order_bot, bot_le := _}

source

theorem with_top.not_top_le_coe {α : Type u_1} [has_le α] (a : α) :

¬⊤ ≤ ↑a

source

theorem with_top.le_coe {α : Type u_1} {a b : α} [has_le α] {o : option α} :

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

source

theorem with_top.le_coe_iff {α : Type u_1} {b : α} [has_le α] {x : with_top α} :

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

source

theorem with_top.coe_le_iff {α : Type u_1} {a : α} [has_le α] {x : with_top α} :

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

source

@[protected]

theorem is_min.with_top {α : Type u_1} {a : α} [has_le α] (h : is_min a) :

is_min ↑a

source

@[protected, instance]

def with_top.has_lt {α : Type u_1} [has_lt α] :

has_lt (with_top α)

Equations

with_top.has_lt = {lt := λ (o₁ o₂ : option α), ∃ (b : α) (H : b ∈ o₁), ∀ (a : α), a ∈ o₂ → b < a}

source

theorem with_top.to_dual_lt_iff {α : Type u_1} [has_lt α] {a : with_top α} {b : with_bot αᵒᵈ} :

⇑with_top.to_dual a < b ↔ ⇑with_bot.of_dual b < a

source

theorem with_top.lt_to_dual_iff {α : Type u_1} [has_lt α] {a : with_bot αᵒᵈ} {b : with_top α} :

a < ⇑with_top.to_dual b ↔ b < ⇑with_bot.of_dual a

source

@[simp]

theorem with_top.to_dual_lt_to_dual_iff {α : Type u_1} [has_lt α] {a b : with_top α} :

⇑with_top.to_dual a < ⇑with_top.to_dual b ↔ b < a

source

theorem with_top.of_dual_lt_iff {α : Type u_1} [has_lt α] {a : with_top αᵒᵈ} {b : with_bot α} :

⇑with_top.of_dual a < b ↔ ⇑with_bot.to_dual b < a

source

theorem with_top.lt_of_dual_iff {α : Type u_1} [has_lt α] {a : with_bot α} {b : with_top αᵒᵈ} :

a < ⇑with_top.of_dual b ↔ b < ⇑with_bot.to_dual a

source

@[simp]

theorem with_top.of_dual_lt_of_dual_iff {α : Type u_1} [has_lt α] {a b : with_top αᵒᵈ} :

⇑with_top.of_dual a < ⇑with_top.of_dual b ↔ b < a

source

@[simp]

theorem with_bot.to_dual_symm_apply {α : Type u_1} (a : with_top αᵒᵈ) :

⇑(with_bot.to_dual.symm) a = ⇑with_top.of_dual a

source

@[simp]

theorem with_bot.of_dual_symm_apply {α : Type u_1} (a : with_top α) :

⇑(with_bot.of_dual.symm) a = ⇑with_top.to_dual a

source

@[simp]

theorem with_bot.to_dual_apply_bot {α : Type u_1} :

⇑with_bot.to_dual ⊥ = ⊤

source

@[simp]

theorem with_bot.of_dual_apply_bot {α : Type u_1} :

⇑with_bot.of_dual ⊥ = ⊤

source

@[simp]

theorem with_bot.to_dual_apply_coe {α : Type u_1} (a : α) :

⇑with_bot.to_dual ↑a = ↑(⇑order_dual.to_dual a)

source

@[simp]

theorem with_bot.of_dual_apply_coe {α : Type u_1} (a : αᵒᵈ) :

⇑with_bot.of_dual ↑a = ↑(⇑order_dual.of_dual a)

source

theorem with_bot.map_to_dual {α : Type u_1} {β : Type u_2} (f : αᵒᵈ → βᵒᵈ) (a : with_top α) :

with_bot.map f (⇑with_top.to_dual a) = with_top.map (⇑order_dual.to_dual ∘ f) a

source

theorem with_bot.map_of_dual {α : Type u_1} {β : Type u_2} (f : α → β) (a : with_top αᵒᵈ) :

with_bot.map f (⇑with_top.of_dual a) = with_top.map (⇑order_dual.of_dual ∘ f) a

source

theorem with_bot.to_dual_map {α : Type u_1} {β : Type u_2} (f : α → β) (a : with_bot α) :

⇑with_bot.to_dual (with_bot.map f a) = with_bot.map (⇑order_dual.to_dual ∘ f ∘ ⇑order_dual.of_dual) (⇑with_bot.to_dual a)

source

theorem with_bot.of_dual_map {α : Type u_1} {β : Type u_2} (f : αᵒᵈ → βᵒᵈ) (a : with_bot αᵒᵈ) :

⇑with_bot.of_dual (with_bot.map f a) = with_bot.map (⇑order_dual.of_dual ∘ f ∘ ⇑order_dual.to_dual) (⇑with_bot.of_dual a)

source

theorem with_bot.to_dual_le_iff {α : Type u_1} [has_le α] {a : with_bot α} {b : with_top αᵒᵈ} :

⇑with_bot.to_dual a ≤ b ↔ ⇑with_top.of_dual b ≤ a

source

theorem with_bot.le_to_dual_iff {α : Type u_1} [has_le α] {a : with_top αᵒᵈ} {b : with_bot α} :

a ≤ ⇑with_bot.to_dual b ↔ b ≤ ⇑with_top.of_dual a

source

@[simp]

theorem with_bot.to_dual_le_to_dual_iff {α : Type u_1} [has_le α] {a b : with_bot α} :

⇑with_bot.to_dual a ≤ ⇑with_bot.to_dual b ↔ b ≤ a

source

theorem with_bot.of_dual_le_iff {α : Type u_1} [has_le α] {a : with_bot αᵒᵈ} {b : with_top α} :

⇑with_bot.of_dual a ≤ b ↔ ⇑with_top.to_dual b ≤ a

source

theorem with_bot.le_of_dual_iff {α : Type u_1} [has_le α] {a : with_top α} {b : with_bot αᵒᵈ} :

a ≤ ⇑with_bot.of_dual b ↔ b ≤ ⇑with_top.to_dual a

source

@[simp]

theorem with_bot.of_dual_le_of_dual_iff {α : Type u_1} [has_le α] {a b : with_bot αᵒᵈ} :

⇑with_bot.of_dual a ≤ ⇑with_bot.of_dual b ↔ b ≤ a

source

theorem with_bot.to_dual_lt_iff {α : Type u_1} [has_lt α] {a : with_bot α} {b : with_top αᵒᵈ} :

⇑with_bot.to_dual a < b ↔ ⇑with_top.of_dual b < a

source

theorem with_bot.lt_to_dual_iff {α : Type u_1} [has_lt α] {a : with_top αᵒᵈ} {b : with_bot α} :

a < ⇑with_bot.to_dual b ↔ b < ⇑with_top.of_dual a

source

@[simp]

theorem with_bot.to_dual_lt_to_dual_iff {α : Type u_1} [has_lt α] {a b : with_bot α} :

⇑with_bot.to_dual a < ⇑with_bot.to_dual b ↔ b < a

source

theorem with_bot.of_dual_lt_iff {α : Type u_1} [has_lt α] {a : with_bot αᵒᵈ} {b : with_top α} :

⇑with_bot.of_dual a < b ↔ ⇑with_top.to_dual b < a

source

theorem with_bot.lt_of_dual_iff {α : Type u_1} [has_lt α] {a : with_top α} {b : with_bot αᵒᵈ} :

a < ⇑with_bot.of_dual b ↔ b < ⇑with_top.to_dual a

source

@[simp]

theorem with_bot.of_dual_lt_of_dual_iff {α : Type u_1} [has_lt α] {a b : with_bot αᵒᵈ} :

⇑with_bot.of_dual a < ⇑with_bot.of_dual b ↔ b < a

source

@[simp, norm_cast]

theorem with_top.coe_lt_coe {α : Type u_1} [has_lt α] {a b : α} :

↑a < ↑b ↔ a < b

source

@[simp]

theorem with_top.some_lt_some {α : Type u_1} [has_lt α] {a b : α} :

option.some a < option.some b ↔ a < b

source

theorem with_top.coe_lt_top {α : Type u_1} [has_lt α] (a : α) :

↑a < ⊤

source

@[simp]

theorem with_top.some_lt_none {α : Type u_1} [has_lt α] (a : α) :

option.some a < option.none

source

@[simp]

theorem with_top.not_none_lt {α : Type u_1} [has_lt α] (a : with_top α) :

¬option.none < a

source

theorem with_top.lt_iff_exists_coe {α : Type u_1} [has_lt α] {a b : with_top α} :

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

source

theorem with_top.coe_lt_iff {α : Type u_1} [has_lt α] {a : α} {x : with_top α} :

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

source

@[protected]

theorem with_top.lt_top_iff_ne_top {α : Type u_1} [has_lt α] {x : with_top α} :

x < ⊤ ↔ x ≠ ⊤

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

source

@[protected, instance]

def with_top.preorder {α : Type u_1} [preorder α] :

preorder (with_top α)

Equations

with_top.preorder = {le := has_le.le with_top.has_le, lt := has_lt.lt with_top.has_lt, le_refl := _, le_trans := _, lt_iff_le_not_le := _}

source

@[protected, instance]

def with_top.partial_order {α : Type u_1} [partial_order α] :

partial_order (with_top α)

Equations

with_top.partial_order = {le := preorder.le with_top.preorder, lt := preorder.lt with_top.preorder, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

source

theorem with_top.coe_strict_mono {α : Type u_1} [preorder α] :

strict_mono coe

source

theorem with_top.coe_mono {α : Type u_1} [preorder α] :

monotone coe

source

theorem with_top.monotone_iff {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : with_top α → β} :

monotone f ↔ monotone (f ∘ coe) ∧ ∀ (x : α), f ↑x ≤ f ⊤

source

@[simp]

theorem with_top.monotone_map_iff {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α → β} :

monotone (with_top.map f) ↔ monotone f

source

theorem monotone.with_top_map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α → β} :

monotone f → monotone (with_top.map f)

Alias of the reverse direction of with_top.monotone_map_iff.

source

theorem with_top.strict_mono_iff {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : with_top α → β} :

strict_mono f ↔ strict_mono (f ∘ coe) ∧ ∀ (x : α), f ↑x < f ⊤

source

@[simp]

theorem with_top.strict_mono_map_iff {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α → β} :

strict_mono (with_top.map f) ↔ strict_mono f

source

theorem strict_mono.with_top_map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α → β} :

strict_mono f → strict_mono (with_top.map f)

Alias of the reverse direction of with_top.strict_mono_map_iff.

source

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

with_top.map f a ≤ with_top.map f b ↔ a ≤ b

source

@[protected, instance]

def with_top.semilattice_inf {α : Type u_1} [semilattice_inf α] :

semilattice_inf (with_top α)

Equations