Adding both ⊥ and ⊤ to a type

This files defines an abbreviation WithBotTop ι for WithBot (WithTop ι). We also introduce an abbreviation EInt for WithBotTop ℤ.

@[reducible, inline]

abbrev WithBotTop (ι : Type u_1) : Type u_1

The type obtained by adding both ⊥ and ⊤ to a type.

Equations

• WithBotTop ι = WithBot (WithTop ι)

@[reducible, inline]

abbrev WithTopBot (ι : Type u_1) : Type u_1

The type obtained by adding both ⊤ and ⊥ to a type.

Equations

• WithTopBot ι = WithTop (WithBot ι)

def WithBotTop.coe {ι : Type u_1} : ι → WithBotTop ι

The canonical inclusion ι → WithBotTop ι. Registered as a coercion.

Equations

• WithBotTop.coe = WithBot.some ∘ WithTop.some

@[instance_reducible]

instance WithBotTop.instCoe {ι : Type u_1} : Coe ι (WithBotTop ι)

Equations

• WithBotTop.instCoe = { coe := WithBotTop.coe }

theorem WithBotTop.coe_injective {ι : Type u_1} : Function.Injective coe

@[simp]

theorem WithBotTop.coe_ne_bot {ι : Type u_1} (a : ι) : coe a ≠ ⊥

@[simp]

theorem WithBotTop.coe_ne_top {ι : Type u_1} (a : ι) : coe a ≠ ⊤

@[simp]

theorem WithBotTop.top_ne_bot {ι : Type u_1} : ⊤ ≠ ⊥

def WithBotTop.rec {ι : Type u_1} {motive : WithBotTop ι → Sort u_2} (bot : motive ⊥) (coe : (a : ι) → motive (coe a)) (top : motive ⊤) (a : WithBotTop ι) : motive a

A recursor for WithBotTop in terms of the coercion.

Equations

• WithBotTop.rec bot coe top none = bot
• WithBotTop.rec bot coe top (some (some a)) = coe a
• WithBotTop.rec bot coe top (some none) = top

@[simp]

theorem WithBotTop.rec_bot {ι : Type u_1} {motive : WithBotTop ι → Sort u_2} (bot : motive ⊥) (coe : (a : ι) → motive (coe a)) (top : motive ⊤) : WithBotTop.rec bot coe top ⊥ = bot

@[simp]

theorem WithBotTop.rec_coe {ι : Type u_1} {motive : WithBotTop ι → Sort u_2} (bot : motive ⊥) (coe : (a : ι) → motive (coe a)) (top : motive ⊤) (a : ι) : WithBotTop.rec bot coe top (WithBotTop.coe a) = coe a

@[simp]

theorem WithBotTop.rec_top {ι : Type u_1} {motive : WithBotTop ι → Sort u_2} (bot : motive ⊥) (coe : (a : ι) → motive (coe a)) (top : motive ⊤) : WithBotTop.rec bot coe top ⊤ = top

@[simp]

theorem WithBotTop.coe_le_coe {ι : Type u_1} [LE ι] {a b : ι} : coe a ≤ coe b ↔ a ≤ b

@[simp]

theorem WithBotTop.coe_lt_coe {ι : Type u_1} [LT ι] {a b : ι} : coe a < coe b ↔ a < b

@[simp]

theorem WithBotTop.coe_strictMono {ι : Type u_1} [Preorder ι] : StrictMono coe

theorem WithBotTop.coe_monotone {ι : Type u_1} [Preorder ι] : Monotone coe

@[reducible, inline]

abbrev EInt : Type

The type of extended integers [-∞, ∞], constructed as WithBot (WithTop ℤ).

Equations

• EInt = WithBotTop ℤ