LeanPool.Duality.ExtendedFields

This entire file is inspired by: https://github.com/leanprover-community/mathlib4/blob/333e2d79fdaee86489af73dee919bc4b66957a52/Mathlib/Data/Real/EReal.lean

source

def Extend (F : Type u_1) :

Type u_1

Extend F is the type of values in F ∪ {⊥, ⊤} where, informally speaking, ⊥ (negative infinity) is stronger than ⊤ (positive infinity).

Equations

Extend F = WithBot (WithTop F)

Instances For

source

@[implicit_reducible]

instance instAddCommMonoidExtend {F : Type u_1} [Field F] :

AddCommMonoid (Extend F)

Equations

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

source

@[implicit_reducible]

instance instLinearOrderExtend {F : Type u_1} [LinearOrder F] :

LinearOrder (Extend F)

Equations

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

source

instance instIsOrderedAddMonoidExtend {F : Type u_1} [Field F] [LinearOrder F] [IsStrictOrderedRing F] :

IsOrderedAddMonoid (Extend F)

source

@[implicit_reducible]

instance instAddCommMonoidWithOneExtend {F : Type u_1} [Field F] :

AddCommMonoidWithOne (Extend F)

Equations

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

source

instance instZeroLEOneClassExtend {F : Type u_1} [Field F] [LinearOrder F] [IsStrictOrderedRing F] :

ZeroLEOneClass (Extend F)

source

instance instCharZeroExtend {F : Type u_1} [Field F] [LinearOrder F] [IsStrictOrderedRing F] :

CharZero (Extend F)

source

@[implicit_reducible]

instance instBoundedOrderExtend {F : Type u_1} [LinearOrder F] :

BoundedOrder (Extend F)

Equations

instBoundedOrderExtend = { top := instBoundedOrderExtend._aux_1, le_top := ⋯, bot := instBoundedOrderExtend._aux_4, bot_le := ⋯ }

source

instance instDenselyOrderedExtend {F : Type u_1} [Field F] [LinearOrder F] [IsStrictOrderedRing F] :

DenselyOrdered (Extend F)

source

@[implicit_reducible]

instance instDecidableRelExtendLt {F : Type u_1} [LinearOrder F] :

DecidableRel fun (x1 x2 : Extend F) => x1 < x2

Equations

instDecidableRelExtendLt = WithBot.decidableLT

source

def toE {F : Type u_1} :

F → Extend F

The canonical inclusion from F to Extend F is registered as a coercion.

Equations

toE = some ∘ some

Instances For

source

@[implicit_reducible]

instance instCoeExtend {F : Type u_1} :

Coe F (Extend F)

Equations

instCoeExtend = { coe := toE }

Coercion #

source

theorem EF.coe_strictMono {F : Type u_1} [LinearOrder F] :

StrictMono toE

source

theorem EF.coe_injective {F : Type u_1} [LinearOrder F] :

Function.Injective toE

source

@[simp]

theorem EF.coe_le_coe_iff {F : Type u_1} [LinearOrder F] {x y : F} :

↑x ≤ ↑y ↔ x ≤ y

source

theorem EF.coe_le_coe_iff_F (F : Type) [Field F] [LinearOrder F] [IsStrictOrderedRing F] {x y : F} :

↑x ≤ ↑y ↔ x ≤ y

source

@[simp]

theorem EF.coe_lt_coe_iff {F : Type u_1} [LinearOrder F] {x y : F} :

↑x < ↑y ↔ x < y

source

@[simp]

theorem EF.coe_eq_coe_iff {F : Type u_1} [LinearOrder F] {x y : F} :

↑x = ↑y ↔ x = y

source

theorem EF.coe_neq_coe_iff {F : Type u_1} [LinearOrder F] {x y : F} :

↑x ≠ ↑y ↔ x ≠ y

source

@[simp]

theorem EF.coe_zero {F : Type u_1} [Field F] :

↑0 = 0

source

@[simp]

theorem EF.coe_one {F : Type u_1} [Field F] :

↑1 = 1

source

@[simp]

theorem EF.bot_lt_coe {F : Type u_1} [LinearOrder F] (x : F) :

⊥ < ↑x

source

@[simp]

theorem EF.coe_neq_bot {F : Type u_1} [LinearOrder F] (x : F) :

↑x ≠ ⊥

source

@[simp]

theorem EF.bot_neq_coe {F : Type u_1} [LinearOrder F] (x : F) :

⊥ ≠ ↑x

source

@[simp]

theorem EF.coe_lt_top {F : Type u_1} [LinearOrder F] (x : F) :

↑x < ⊤

source

@[simp]

theorem EF.coe_neq_top {F : Type u_1} [LinearOrder F] (x : F) :

↑x ≠ ⊤

source

@[simp]

theorem EF.top_neq_coe {F : Type u_1} [LinearOrder F] (x : F) :

⊤ ≠ ↑x

source

@[simp]

theorem EF.bot_lt_zero {F : Type u_1} [Field F] [LinearOrder F] :

⊥ < 0

source

@[simp]

theorem EF.bot_neq_zero {F : Type u_1} [Field F] [LinearOrder F] :

⊥ ≠ 0

source

@[simp]

theorem EF.zero_neq_bot {F : Type u_1} [Field F] [LinearOrder F] :

0 ≠ ⊥

source

@[simp]

theorem EF.zero_lt_top {F : Type u_1} [Field F] [LinearOrder F] :

0 < ⊤

source

@[simp]

theorem EF.zero_neq_top {F : Type u_1} [Field F] [LinearOrder F] :

0 ≠ ⊤

source

@[simp]

theorem EF.top_neq_zero {F : Type u_1} [Field F] [LinearOrder F] :

⊤ ≠ 0

source

@[simp]

theorem EF.coe_add {F : Type u_1} [Field F] (x y : F) :

↑(x + y) = ↑x + ↑y

source

@[simp]

theorem EF.coe_eq_zero {F : Type u_1} [Field F] [LinearOrder F] {x : F} :

↑x = 0 ↔ x = 0

source

@[simp]

theorem EF.coe_eq_one {F : Type u_1} [Field F] [LinearOrder F] {x : F} :

↑x = 1 ↔ x = 1

source

theorem EF.coe_neq_zero {F : Type u_1} [Field F] [LinearOrder F] {x : F} :

↑x ≠ 0 ↔ x ≠ 0

source

theorem EF.coe_neq_one {F : Type u_1} [Field F] [LinearOrder F] {x : F} :

↑x ≠ 1 ↔ x ≠ 1

source

@[simp]

theorem EF.coe_nonneg {F : Type u_1} [Field F] [LinearOrder F] {x : F} :

0 ≤ ↑x ↔ 0 ≤ x

source

@[simp]

theorem EF.coe_nonpos {F : Type u_1} [Field F] [LinearOrder F] {x : F} :

↑x ≤ 0 ↔ x ≤ 0

source

@[simp]

theorem EF.coe_pos {F : Type u_1} [Field F] [LinearOrder F] {x : F} :

0 < ↑x ↔ 0 < x

source

@[simp]

theorem EF.coe_neg' {F : Type u_1} [Field F] [LinearOrder F] {x : F} :

↑x < 0 ↔ x < 0

Addition #

source

@[simp]

theorem EF.add_bot {F : Type u_1} [Field F] [LinearOrder F] (x : Extend F) :

x + ⊥ = ⊥

source

@[simp]

theorem EF.bot_add {F : Type u_1} [Field F] [LinearOrder F] (x : Extend F) :

⊥ + x = ⊥

source

@[simp]

theorem EF.add_eq_bot_iff {F : Type u_1} [Field F] [LinearOrder F] {x y : Extend F} :

x + y = ⊥ ↔ x = ⊥ ∨ y = ⊥

source

@[simp]

theorem EF.top_add_top {F : Type u_1} [Field F] [LinearOrder F] :

⊤ + ⊤ = ⊤

source

@[simp]

theorem EF.top_add_coe {F : Type u_1} [Field F] [LinearOrder F] (x : F) :

⊤ + ↑x = ⊤

source

@[simp]

theorem EF.coe_add_top {F : Type u_1} [Field F] [LinearOrder F] (x : F) :

↑x + ⊤ = ⊤

Negation #

source

def EF.neg {F : Type u_1} [Field F] [LinearOrder F] :

Extend F → Extend F

Negation on Extend F.

Equations

Instances For

source

@[implicit_reducible]

instance EF.instNegExtend {F : Type u_1} [Field F] [LinearOrder F] :

Neg (Extend F)

Equations

EF.instNegExtend = { neg := EF.neg }

source

@[implicit_reducible]

instance EF.instSubNegZeroMonoidExtend {F : Type u_1} [Field F] [LinearOrder F] :

SubNegZeroMonoid (Extend F)

Equations

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

source

@[simp]

theorem EF.neg_top {F : Type u_1} [Field F] [LinearOrder F] :

-⊤ = ⊥

source

@[simp]

theorem EF.neg_bot {F : Type u_1} [Field F] [LinearOrder F] :

-⊥ = ⊤

source

@[simp]

theorem EF.coe_neg {F : Type u_1} [Field F] [LinearOrder F] (x : F) :

↑(-x) = -↑x

source

@[implicit_reducible]

instance EF.instInvolutiveNegExtend {F : Type u_1} [Field F] [LinearOrder F] :

InvolutiveNeg (Extend F)

Equations

EF.instInvolutiveNegExtend = { toNeg := EF.instNegExtend, neg_neg := ⋯ }

source

@[simp]

theorem EF.neg_eq_top_iff {F : Type u_1} [Field F] [LinearOrder F] {x : Extend F} :

-x = ⊤ ↔ x = ⊥

source

@[simp]

theorem EF.neg_eq_bot_iff {F : Type u_1} [Field F] [LinearOrder F] {x : Extend F} :

-x = ⊥ ↔ x = ⊤

source

@[simp]

theorem EF.neg_eq_zero_iff {F : Type u_1} [Field F] [LinearOrder F] {x : Extend F} :

-x = 0 ↔ x = 0