Time.Interval

source

class Time.LeRefl (α : Type u) [LE α] :

Type

Reflexive relation of LE class

le_refl : ∀ (a : α), a ≤ a

Instances

source

theorem Time.LeRefl.le_refl {α : Type u} [LE α] [self : Time.LeRefl α] (a : α) :

a ≤ a

source

instance Time.instLeReflNat :

Time.LeRefl Nat

Equations

Time.instLeReflNat = { le_refl := Nat.le_refl }

source

instance Time.instLeReflInt :

Time.LeRefl Int

Equations

Time.instLeReflInt = { le_refl := Int.le_refl }

source

def Time.Icc {α : Type} [LE α] (a : α) (b : α) :

Type

Left-closed right-closed interval

Equations

Time.Icc a b = { x : α // a ≤ x ∧ x ≤ b }

Instances For

source

instance Time.instLEIcc {α : Type} [LE α] {a : α} {b : α} :

LE (Time.Icc a b)

Equations

Time.instLEIcc = { le := fun (a_1 b_1 : Time.Icc a b) => a_1.val ≤ b_1.val }

source

instance Time.instReprIcc {α : Type} [Repr α] [LE α] {a : α} {b : α} :

Repr (Time.Icc a b)

Equations

Time.instReprIcc = { reprPrec := fun (s : Time.Icc a b) (x : Nat) => repr s.val }

source

instance Time.instBEqIcc {α : Type} [BEq α] [LE α] {a : α} {b : α} :

BEq (Time.Icc a b)

Equations

Time.instBEqIcc = { beq := fun (a_1 b_1 : Time.Icc a b) => a_1.val == b_1.val }

source

instance Time.instCoeOutIcc {α : Type} [LE α] {a : α} {b : α} :

CoeOut (Time.Icc a b) α

Equations

Time.instCoeOutIcc = { coe := fun (n : Time.Icc a b) => n.val }

source

instance Time.instLeReflIcc {α : Type} [LE α] [Time.LeRefl α] {a : α} {b : α} :

Time.LeRefl (Time.Icc a b)

Equations

Time.instLeReflIcc = { le_refl := ⋯ }

source

instance Time.instCoeOutIccNatInt (a : Nat) (b : Nat) :

CoeOut (Time.Icc a b) Int

Equations

Time.instCoeOutIccNatInt a b = { coe := fun (n : Time.Icc a b) => ↑n.val }

source

theorem Time.Icc.nonempty {α : Type} [LE α] [Time.LeRefl α] {a : α} {b : α} (h : a ≤ b) :

Nonempty (Time.Icc a b)

source

def Time.Ico {α : Type} [LE α] [LT α] (a : α) (b : α) :

Type

Left-closed right-open interval

Equations

Time.Ico a b = { x : α // a ≤ x ∧ x < b }

Instances For

source

instance Time.instLEIco {α : Type} [LE α] [LT α] {a : α} {b : α} :

LE (Time.Ico a b)

Equations

Time.instLEIco = { le := fun (a_1 b_1 : Time.Ico a b) => a_1.val ≤ b_1.val }

source

instance Time.instReprIco {α : Type} [Repr α] [LE α] [LT α] {a : α} {b : α} :

Repr (Time.Ico a b)

Equations

Time.instReprIco = { reprPrec := fun (s : Time.Ico a b) (x : Nat) => repr s.val }

source

instance Time.instBEqIco {α : Type} [BEq α] [LE α] [LT α] {a : α} {b : α} :

BEq (Time.Ico a b)

Equations

Time.instBEqIco = { beq := fun (a_1 b_1 : Time.Ico a b) => a_1.val == b_1.val }

source

instance Time.instCoeOutIco {α : Type} [LE α] [LT α] (a : α) (b : α) :

CoeOut (Time.Ico a b) α

Equations

Time.instCoeOutIco a b = { coe := fun (n : Time.Ico a b) => n.val }

source

instance Time.instLeReflIco {α : Type} [LE α] [LT α] [Time.LeRefl α] {a : α} {b : α} :

Time.LeRefl (Time.Ico a b)

Equations

Time.instLeReflIco = { le_refl := ⋯ }

source

instance Time.instCoeOutIcoNat (a : Nat) (b : Nat) :

CoeOut (Time.Ico a b) Nat

Equations

Time.instCoeOutIcoNat a b = { coe := fun (n : Time.Ico a b) => n.val }

source

instance Time.instCoeOutIcoNatInt (a : Nat) (b : Nat) :

CoeOut (Time.Ico a b) Int

Equations

Time.instCoeOutIcoNatInt a b = { coe := fun (n : Time.Ico a b) => ↑n.val }

source

theorem Time.Ico.nonempty {α : Type} [LE α] [LT α] [Time.LeRefl α] {a : α} {b : α} (h : a < b) :

Nonempty (Time.Ico a b)

source

structure Time.NonemptyIcc {α : Type} [LE α] [Time.LeRefl α] (a : α) (b : α) :

Type

icc : Time.Icc a b
isNonempty : Nonempty (Time.Icc a b)

Instances For

source

theorem Time.NonemptyIcc.isNonempty {α : Type} [LE α] [Time.LeRefl α] {a : α} {b : α} (self : Time.NonemptyIcc a b) :

Nonempty (Time.Icc a b)

source

instance Time.instCoeNonemptyIccIcc {α : Type} [LE α] [Time.LeRefl α] (a : α) (b : α) :

Coe (Time.NonemptyIcc a b) (Time.Icc a b)

Equations

Time.instCoeNonemptyIccIcc a b = { coe := fun (n : Time.NonemptyIcc a b) => n.icc }

source

structure Time.NonemptyIco {α : Type} [LE α] [LT α] [Time.LeRefl α] (a : α) (b : α) :

Type

ico : Time.Ico a b
isNonempty : Nonempty (Time.Ico a b)

Instances For

source

theorem Time.NonemptyIco.isNonempty {α : Type} [LE α] [LT α] [Time.LeRefl α] {a : α} {b : α} (self : Time.NonemptyIco a b) :

Nonempty (Time.Ico a b)

source

instance Time.instCoeNonemptyIcoIco {α : Type} [LE α] [LT α] [Time.LeRefl α] (a : α) (b : α) :

Coe (Time.NonemptyIco a b) (Time.Ico a b)

Equations

Time.instCoeNonemptyIcoIco a b = { coe := fun (n : Time.NonemptyIco a b) => n.ico }

source

def Time.toNonemptyIcc {α : Type} [LE α] [Time.LeRefl α] {a : α} {b : α} (v : Time.Icc a b) (h : a ≤ b) :

Time.NonemptyIcc a b

Equations

Time.toNonemptyIcc v h = { icc := v, isNonempty := ⋯ }

Instances For

source

def Time.toNonemptyIco {α : Type} [LE α] [LT α] [Time.LeRefl α] {a : α} {b : α} (v : Time.Ico a b) (h : a < b) :

Time.NonemptyIco a b

Equations

Time.toNonemptyIco v h = { ico := v, isNonempty := ⋯ }

Instances For

source

theorem Time.NonemptyIcc.sub_lt_sub {n : Nat} {x : Nat} {m : Nat} :

n ≤ x → x < m → n < m → x - n < m - n

source

theorem Time.NonemptyIcc.sub_lt_sub_of_succ {n : Nat} {x : Nat} {m : Nat} :

n ≤ x → x ≤ m → n ≤ m → x - n < m + 1 - n

source

def Time.NonemptyIcc.toFin {n : Nat} {m : Nat} (x : Time.NonemptyIcc n m) :

Fin (m + 1 - n)

Equations

x.toFin = let_fun h1 := ⋯; let_fun h2 := ⋯; let_fun h := ⋯; ⟨x.icc.val - n, ⋯⟩

Instances For

source

instance Time.NonemptyIcc.instCoeNatFinHSubHAddOfNat {n : Nat} {m : Nat} :

Coe (Time.NonemptyIcc n m) (Fin (m + 1 - n))

Equations

Time.NonemptyIcc.instCoeNatFinHSubHAddOfNat = { coe := fun (x : Time.NonemptyIcc n m) => x.toFin }

source

instance Time.NonemptyIcc.instCoeNatOfNatFin {m : Nat} :

Coe (Time.NonemptyIcc 1 m) (Fin m)

Equations

Time.NonemptyIcc.instCoeNatOfNatFin = { coe := fun (x : Time.NonemptyIcc 1 m) => Fin.cast ⋯ x.toFin }