Documentation

Time.Interval

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

Reflexive relation of LE class

  • le_refl : ∀ (a : α), a a
Instances
    def Time.Icc {α : Type} [LE α] (a b : α) :

    Left-closed right-closed interval

    Equations
    Instances For
      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 }
      instance Time.instReprIcc {α : Type} [Repr α] [LE α] {a b : α} :
      Equations
      • Time.instReprIcc = { reprPrec := fun (s : Time.Icc a b) (x : Nat) => repr s.val }
      instance Time.instBEqIcc {α : Type} [BEq α] [LE α] {a b : α} :
      Equations
      • Time.instBEqIcc = { beq := fun (a_1 b_1 : Time.Icc a b) => a_1.val == b_1.val }
      instance Time.instCoeOutIcc {α : Type} [LE α] {a b : α} :
      CoeOut (Time.Icc a b) α
      Equations
      • Time.instCoeOutIcc = { coe := fun (n : Time.Icc a b) => n.val }
      instance Time.instLeReflIcc {α : Type} [LE α] [Time.LeRefl α] {a b : α} :
      Equations
      • =
      Equations
      theorem Time.Icc.nonempty {α : Type} [LE α] [Time.LeRefl α] {a b : α} (h : a b) :
      def Time.Ico {α : Type} [LE α] [LT α] (a b : α) :

      Left-closed right-open interval

      Equations
      Instances For
        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 }
        instance Time.instReprIco {α : Type} [Repr α] [LE α] [LT α] {a b : α} :
        Equations
        • Time.instReprIco = { reprPrec := fun (s : Time.Ico a b) (x : Nat) => repr s.val }
        instance Time.instBEqIco {α : Type} [BEq α] [LE α] [LT α] {a b : α} :
        Equations
        • Time.instBEqIco = { beq := fun (a_1 b_1 : Time.Ico a b) => a_1.val == b_1.val }
        instance Time.instCoeOutIco {α : Type} [LE α] [LT α] (a b : α) :
        CoeOut (Time.Ico a b) α
        Equations
        instance Time.instLeReflIco {α : Type} [LE α] [LT α] [Time.LeRefl α] {a b : α} :
        Equations
        • =
        instance Time.instCoeOutIcoNat (a b : Nat) :
        Equations
        Equations
        theorem Time.Ico.nonempty {α : Type} [LE α] [LT α] [Time.LeRefl α] {a b : α} (h : a < b) :
        structure Time.NonemptyIcc {α : Type} [LE α] [Time.LeRefl α] (a b : α) :
        Instances For
          instance Time.instCoeNonemptyIccIcc {α : Type} [LE α] [Time.LeRefl α] (a b : α) :
          Equations
          structure Time.NonemptyIco {α : Type} [LE α] [LT α] [Time.LeRefl α] (a b : α) :
          Instances For
            instance Time.instCoeNonemptyIcoIco {α : Type} [LE α] [LT α] [Time.LeRefl α] (a b : α) :
            Equations
            def Time.toNonemptyIcc {α : Type} [LE α] [Time.LeRefl α] {a b : α} (v : Time.Icc a b) (h : a b) :
            Equations
            Instances For
              def Time.toNonemptyIco {α : Type} [LE α] [LT α] [Time.LeRefl α] {a b : α} (v : Time.Ico a b) (h : a < b) :
              Equations
              Instances For
                theorem Time.NonemptyIcc.sub_lt_sub {n x m : Nat} :
                n xx < mn < mx - n < m - n
                theorem Time.NonemptyIcc.sub_lt_sub_of_succ {n x m : Nat} :
                n xx mn mx - n < m + 1 - n
                def Time.NonemptyIcc.toFin {n m : Nat} (x : Time.NonemptyIcc n m) :
                Fin (m + 1 - n)
                Equations
                • x.toFin = x.icc.val - n,
                Instances For
                  Equations
                  • Time.NonemptyIcc.instCoeNatFinHSubHAddOfNat = { coe := fun (x : Time.NonemptyIcc n m) => x.toFin }
                  Equations
                  theorem Time.Icc.Nat.mem_of_range_exists_val {n m : Nat} (h : m List.range' 1 n) :
                  ∃ (x : Time.Icc 1 n), m = x.val