Time.Interval

source

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

Prop

Reflexive relation of LE class

le_refl (a : α) : a ≤ a

Instances

source

instance Time.instLeReflNat :

LeRefl Nat

source

instance Time.instLeReflInt :

LeRefl Int

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 (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 (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 (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 (Icc a b) α

Equations

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

source

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

LeRefl (Icc a b)

source

instance Time.instCoeOutIccNatInt (a b : Nat) :

CoeOut (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 α] [LeRefl α] {a b : α} (h : a ≤ b) :

Nonempty (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 (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 (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 (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 (Ico a b) α

Equations

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

source

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

LeRefl (Ico a b)

source

instance Time.instCoeOutIcoNat (a b : Nat) :

CoeOut (Ico a b) Nat

Equations

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

source

instance Time.instCoeOutIcoNatInt (a b : Nat) :

CoeOut (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 α] [LeRefl α] {a b : α} (h : a < b) :

Nonempty (Ico a b)

source

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

Type

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

Instances For

source

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

Coe (NonemptyIcc a b) (Icc a b)

Equations

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

source

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

Type

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

Instances For

source

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

Coe (NonemptyIco a b) (Ico a b)

Equations

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

source

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

NonemptyIcc a b

Equations

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

Instances For

source

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

NonemptyIco a b

Equations

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

Instances For

source

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

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

source

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

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

source

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

Fin (m + 1 - n)

Equations

x.toFin = ⟨x.icc.val - n, ⋯⟩

Instances For

source

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

Coe (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 (NonemptyIcc 1 m) (Fin m)

Equations

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

source

theorem Time.Icc.Nat.val_eq_mem_of_range {n : Nat} (m : Icc 1 n) :

m.val ∈ List.range' 1 n

source

theorem Time.Icc.Nat.mem_of_range_exists_val {n m : Nat} (h : m ∈ List.range' 1 n) :

∃ (x : Icc 1 n), m = x.val