Documentation

Mathlib.Order.Interval.Basic

Order intervals #

This file defines (nonempty) closed intervals in an order (see Set.Icc). This is a prototype for interval arithmetic.

Main declarations #

theorem NonemptyInterval.ext {α : Type u_7} :
∀ {inst : LE α} (x y : NonemptyInterval α), x.toProd = y.toProdx = y
theorem NonemptyInterval.ext_iff {α : Type u_7} :
∀ {inst : LE α} (x y : NonemptyInterval α), x = y x.toProd = y.toProd
structure NonemptyInterval (α : Type u_7) [LE α] extends Prod :
Type u_7

The nonempty closed intervals in an order.

We define intervals by the pair of endpoints fst, snd. To convert intervals to the set of elements between these endpoints, use the coercion NonemptyInterval α → Set α.

  • fst : α
  • snd : α
  • fst_le_snd : self.toProd.1 self.toProd.2

    The starting point of an interval is smaller than the endpoint.

Instances For
    theorem NonemptyInterval.fst_le_snd {α : Type u_7} [LE α] (self : NonemptyInterval α) :
    self.toProd.1 self.toProd.2

    The starting point of an interval is smaller than the endpoint.

    theorem NonemptyInterval.toProd_injective {α : Type u_1} [LE α] :
    Function.Injective NonemptyInterval.toProd
    def NonemptyInterval.toDualProd {α : Type u_1} [LE α] :

    The injection that induces the order on intervals.

    Equations
    • NonemptyInterval.toDualProd = NonemptyInterval.toProd
    Instances For
      @[simp]
      theorem NonemptyInterval.toDualProd_apply {α : Type u_1} [LE α] (s : NonemptyInterval α) :
      s.toDualProd = (OrderDual.toDual s.toProd.1, s.toProd.2)
      theorem NonemptyInterval.toDualProd_injective {α : Type u_1} [LE α] :
      Function.Injective NonemptyInterval.toDualProd
      Equations
      • =
      Equations
      • =
      instance NonemptyInterval.le {α : Type u_1} [LE α] :
      Equations
      theorem NonemptyInterval.le_def {α : Type u_1} [LE α] {s : NonemptyInterval α} {t : NonemptyInterval α} :
      s t t.toProd.1 s.toProd.1 s.toProd.2 t.toProd.2
      @[simp]
      theorem NonemptyInterval.toDualProdHom_apply {α : Type u_1} [LE α] :
      ∀ (a : NonemptyInterval α), NonemptyInterval.toDualProdHom a = a.toDualProd

      toDualProd as an order embedding.

      Equations
      • NonemptyInterval.toDualProdHom = { toFun := NonemptyInterval.toDualProd, inj' := , map_rel_iff' := }
      Instances For

        Turn an interval into an interval in the dual order.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem NonemptyInterval.fst_dual {α : Type u_1} [LE α] (s : NonemptyInterval α) :
          (NonemptyInterval.dual s).toProd.1 = OrderDual.toDual s.toProd.2
          @[simp]
          theorem NonemptyInterval.snd_dual {α : Type u_1} [LE α] (s : NonemptyInterval α) :
          (NonemptyInterval.dual s).toProd.2 = OrderDual.toDual s.toProd.1
          Equations
          • NonemptyInterval.instPreorder = Preorder.lift NonemptyInterval.toDualProd
          instance NonemptyInterval.instCoeSet {α : Type u_1} [Preorder α] :
          Equations
          @[instance 100]
          Equations
          @[simp]
          theorem NonemptyInterval.mem_mk {α : Type u_1} [Preorder α] {x : α × α} {a : α} {hx : x.1 x.2} :
          a { toProd := x, fst_le_snd := hx } x.1 a a x.2
          theorem NonemptyInterval.mem_def {α : Type u_1} [Preorder α] {s : NonemptyInterval α} {a : α} :
          a s s.toProd.1 a a s.toProd.2
          theorem NonemptyInterval.coe_nonempty {α : Type u_1} [Preorder α] (s : NonemptyInterval α) :
          (Set.Icc s.toProd.1 s.toProd.2).Nonempty
          @[simp]
          theorem NonemptyInterval.pure_snd {α : Type u_1} [Preorder α] (a : α) :
          (NonemptyInterval.pure a).toProd.2 = a
          @[simp]
          theorem NonemptyInterval.pure_fst {α : Type u_1} [Preorder α] (a : α) :
          (NonemptyInterval.pure a).toProd.1 = a
          def NonemptyInterval.pure {α : Type u_1} [Preorder α] (a : α) :

          {a} as an interval.

          Equations
          Instances For
            theorem NonemptyInterval.pure_injective {α : Type u_1} [Preorder α] :
            Function.Injective NonemptyInterval.pure
            @[simp]
            theorem NonemptyInterval.dual_pure {α : Type u_1} [Preorder α] (a : α) :
            NonemptyInterval.dual (NonemptyInterval.pure a) = NonemptyInterval.pure (OrderDual.toDual a)
            Equations
            Equations
            • =
            Equations
            • =
            @[simp]
            theorem NonemptyInterval.map_snd {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α →o β) (a : NonemptyInterval α) :
            (NonemptyInterval.map f a).toProd.2 = f a.1.2
            @[simp]
            theorem NonemptyInterval.map_fst {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α →o β) (a : NonemptyInterval α) :
            (NonemptyInterval.map f a).toProd.1 = f a.1.1
            def NonemptyInterval.map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α →o β) (a : NonemptyInterval α) :

            Pushforward of nonempty intervals.

            Equations
            Instances For
              @[simp]
              theorem NonemptyInterval.map_pure {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α →o β) (a : α) :
              @[simp]
              theorem NonemptyInterval.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] (g : β →o γ) (f : α →o β) (a : NonemptyInterval α) :
              @[simp]
              theorem NonemptyInterval.dual_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α →o β) (a : NonemptyInterval α) :
              NonemptyInterval.dual (NonemptyInterval.map f a) = NonemptyInterval.map (OrderHom.dual f) (NonemptyInterval.dual a)
              @[simp]
              theorem NonemptyInterval.map₂_snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] (f : αβγ) (h₀ : ∀ (b : β), Monotone fun (a : α) => f a b) (h₁ : ∀ (a : α), Monotone (f a)) :
              ∀ (a : NonemptyInterval α) (a_1 : NonemptyInterval β), (NonemptyInterval.map₂ f h₀ h₁ a a_1).toProd.2 = f a.toProd.2 a_1.toProd.2
              @[simp]
              theorem NonemptyInterval.map₂_fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] (f : αβγ) (h₀ : ∀ (b : β), Monotone fun (a : α) => f a b) (h₁ : ∀ (a : α), Monotone (f a)) :
              ∀ (a : NonemptyInterval α) (a_1 : NonemptyInterval β), (NonemptyInterval.map₂ f h₀ h₁ a a_1).toProd.1 = f a.toProd.1 a_1.toProd.1
              def NonemptyInterval.map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] (f : αβγ) (h₀ : ∀ (b : β), Monotone fun (a : α) => f a b) (h₁ : ∀ (a : α), Monotone (f a)) :

              Binary pushforward of nonempty intervals.

              Equations
              • NonemptyInterval.map₂ f h₀ h₁ s t = { toProd := (f s.toProd.1 t.toProd.1, f s.toProd.2 t.toProd.2), fst_le_snd := }
              Instances For
                @[simp]
                theorem NonemptyInterval.map₂_pure {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] (f : αβγ) (h₀ : ∀ (b : β), Monotone fun (a : α) => f a b) (h₁ : ∀ (a : α), Monotone (f a)) (a : α) (b : β) :
                @[simp]
                theorem NonemptyInterval.dual_map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] (f : αβγ) (h₀ : ∀ (b : β), Monotone fun (a : α) => f a b) (h₁ : ∀ (a : α), Monotone (f a)) (s : NonemptyInterval α) (t : NonemptyInterval β) :
                NonemptyInterval.dual (NonemptyInterval.map₂ f h₀ h₁ s t) = NonemptyInterval.map₂ (fun (a : αᵒᵈ) (b : βᵒᵈ) => OrderDual.toDual (f (OrderDual.ofDual a) (OrderDual.ofDual b))) (NonemptyInterval.dual s) (NonemptyInterval.dual t)
                Equations
                @[simp]
                theorem NonemptyInterval.dual_top {α : Type u_1} [Preorder α] [BoundedOrder α] :
                NonemptyInterval.dual =
                Equations

                Consider a nonempty interval [a, b] as the set [a, b].

                Equations
                Instances For
                  Equations
                  • NonemptyInterval.setLike = { coe := fun (s : NonemptyInterval α) => Set.Icc s.toProd.1 s.toProd.2, coe_injective' := }
                  theorem NonemptyInterval.coe_subset_coe {α : Type u_1} [PartialOrder α] {s : NonemptyInterval α} {t : NonemptyInterval α} :
                  s t s t
                  theorem NonemptyInterval.coe_ssubset_coe {α : Type u_1} [PartialOrder α] {s : NonemptyInterval α} {t : NonemptyInterval α} :
                  s t s < t
                  @[simp]
                  theorem NonemptyInterval.coe_coeHom {α : Type u_1} [PartialOrder α] :
                  NonemptyInterval.coeHom = SetLike.coe
                  theorem NonemptyInterval.coe_def {α : Type u_1} [PartialOrder α] (s : NonemptyInterval α) :
                  s = Set.Icc s.toProd.1 s.toProd.2
                  @[simp]
                  theorem NonemptyInterval.coe_pure {α : Type u_1} [PartialOrder α] (a : α) :
                  @[simp]
                  theorem NonemptyInterval.mem_pure {α : Type u_1} [PartialOrder α] {a : α} {b : α} :
                  @[simp]
                  theorem NonemptyInterval.coe_top {α : Type u_1} [PartialOrder α] [BoundedOrder α] :
                  = Set.univ
                  @[simp]
                  theorem NonemptyInterval.coe_dual {α : Type u_1} [PartialOrder α] (s : NonemptyInterval α) :
                  (NonemptyInterval.dual s) = OrderDual.ofDual ⁻¹' s
                  theorem NonemptyInterval.subset_coe_map {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (f : α →o β) (s : NonemptyInterval α) :
                  f '' s (NonemptyInterval.map f s)
                  Equations
                  • NonemptyInterval.instSup = { sup := fun (s t : NonemptyInterval α) => { toProd := (s.toProd.1 t.toProd.1, s.toProd.2 t.toProd.2), fst_le_snd := } }
                  Equations
                  @[simp]
                  theorem NonemptyInterval.fst_sup {α : Type u_1} [Lattice α] (s : NonemptyInterval α) (t : NonemptyInterval α) :
                  (s t).toProd.1 = s.toProd.1 t.toProd.1
                  @[simp]
                  theorem NonemptyInterval.snd_sup {α : Type u_1} [Lattice α] (s : NonemptyInterval α) (t : NonemptyInterval α) :
                  (s t).toProd.2 = s.toProd.2 t.toProd.2
                  @[reducible, inline]
                  abbrev Interval (α : Type u_7) [LE α] :
                  Type u_7

                  The closed intervals in an order.

                  We represent intervals either as or a nonempty interval given by its endpoints fst, snd. To convert intervals to the set of elements between these endpoints, use the coercion Interval α → Set α.

                  Equations
                  Instances For
                    instance Interval.instInhabited {α : Type u_1} [LE α] :
                    Equations
                    • Interval.instInhabited = WithBot.inhabited
                    instance Interval.instLE {α : Type u_1} [LE α] :
                    Equations
                    • Interval.instLE = WithBot.le
                    instance Interval.instOrderBot {α : Type u_1} [LE α] :
                    Equations
                    • Interval.instOrderBot = WithBot.orderBot
                    Equations
                    • Interval.instCoeNonemptyInterval = WithBot.coe
                    instance Interval.canLift {α : Type u_1} [LE α] :
                    CanLift (Interval α) (NonemptyInterval α) WithBot.some fun (r : Interval α) => r
                    Equations
                    • =
                    def Interval.recBotCoe {α : Type u_1} [LE α] {C : Interval αSort u_7} (bot : C ) (coe : (a : NonemptyInterval α) → C a) (n : Interval α) :
                    C n

                    Recursor for Interval using the preferred forms and ↑a.

                    Equations
                    Instances For
                      theorem Interval.coe_injective {α : Type u_1} [LE α] :
                      Function.Injective WithBot.some
                      theorem Interval.coe_inj {α : Type u_1} [LE α] {s : NonemptyInterval α} {t : NonemptyInterval α} :
                      s = t s = t
                      theorem Interval.forall {α : Type u_1} [LE α] {p : Interval αProp} :
                      (∀ (s : Interval α), p s) p ∀ (s : NonemptyInterval α), p s
                      theorem Interval.exists {α : Type u_1} [LE α] {p : Interval αProp} :
                      (∃ (s : Interval α), p s) p ∃ (s : NonemptyInterval α), p s
                      instance Interval.instUniqueOfIsEmpty {α : Type u_1} [LE α] [IsEmpty α] :
                      Equations
                      def Interval.dual {α : Type u_1} [LE α] :

                      Turn an interval into an interval in the dual order.

                      Equations
                      • Interval.dual = NonemptyInterval.dual.optionCongr
                      Instances For
                        instance Interval.instPreorder {α : Type u_1} [Preorder α] :
                        Equations
                        • Interval.instPreorder = WithBot.preorder
                        def Interval.pure {α : Type u_1} [Preorder α] (a : α) :

                        {a} as an interval.

                        Equations
                        Instances For
                          theorem Interval.pure_injective {α : Type u_1} [Preorder α] :
                          Function.Injective Interval.pure
                          @[simp]
                          theorem Interval.dual_pure {α : Type u_1} [Preorder α] (a : α) :
                          Interval.dual (Interval.pure a) = Interval.pure (OrderDual.toDual a)
                          @[simp]
                          theorem Interval.dual_bot {α : Type u_1} [Preorder α] :
                          Interval.dual =
                          @[simp]
                          theorem Interval.pure_ne_bot {α : Type u_1} [Preorder α] {a : α} :
                          @[simp]
                          theorem Interval.bot_ne_pure {α : Type u_1} [Preorder α] {a : α} :
                          Equations
                          • =
                          def Interval.map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α →o β) :
                          Interval αInterval β

                          Pushforward of intervals.

                          Equations
                          Instances For
                            @[simp]
                            theorem Interval.map_pure {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α →o β) (a : α) :
                            @[simp]
                            theorem Interval.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] (g : β →o γ) (f : α →o β) (s : Interval α) :
                            @[simp]
                            theorem Interval.dual_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α →o β) (s : Interval α) :
                            Interval.dual (Interval.map f s) = Interval.map (OrderHom.dual f) (Interval.dual s)
                            Equations
                            • Interval.boundedOrder = WithBot.instBoundedOrder
                            @[simp]
                            theorem Interval.dual_top {α : Type u_1} [Preorder α] [BoundedOrder α] :
                            Interval.dual =
                            Equations
                            • Interval.partialOrder = WithBot.partialOrder
                            def Interval.coeHom {α : Type u_1} [PartialOrder α] :

                            Consider an interval [a, b] as the set [a, b].

                            Equations
                            Instances For
                              instance Interval.setLike {α : Type u_1} [PartialOrder α] :
                              Equations
                              • Interval.setLike = { coe := Interval.coeHom, coe_injective' := }
                              theorem Interval.coe_subset_coe {α : Type u_1} [PartialOrder α] {s : Interval α} {t : Interval α} :
                              s t s t
                              theorem Interval.coe_sSubset_coe {α : Type u_1} [PartialOrder α] {s : Interval α} {t : Interval α} :
                              s t s < t
                              @[simp]
                              theorem Interval.coe_pure {α : Type u_1} [PartialOrder α] (a : α) :
                              (Interval.pure a) = {a}
                              @[simp]
                              theorem Interval.coe_coe {α : Type u_1} [PartialOrder α] (s : NonemptyInterval α) :
                              s = s
                              @[simp]
                              theorem Interval.coe_bot {α : Type u_1} [PartialOrder α] :
                              =
                              @[simp]
                              theorem Interval.coe_top {α : Type u_1} [PartialOrder α] [BoundedOrder α] :
                              = Set.univ
                              @[simp]
                              theorem Interval.coe_dual {α : Type u_1} [PartialOrder α] (s : Interval α) :
                              (Interval.dual s) = OrderDual.ofDual ⁻¹' s
                              theorem Interval.subset_coe_map {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (f : α →o β) (s : Interval α) :
                              f '' s (Interval.map f s)
                              @[simp]
                              theorem Interval.mem_pure {α : Type u_1} [PartialOrder α] {a : α} {b : α} :
                              theorem Interval.mem_pure_self {α : Type u_1} [PartialOrder α] (a : α) :
                              Equations
                              • Interval.semilatticeSup = WithBot.semilatticeSup
                              instance Interval.lattice {α : Type u_1} [Lattice α] [DecidableRel fun (x x_1 : α) => x x_1] :
                              Equations
                              • Interval.lattice = let __src := Interval.semilatticeSup; Lattice.mk
                              @[simp]
                              theorem Interval.coe_inf {α : Type u_1} [Lattice α] [DecidableRel fun (x x_1 : α) => x x_1] (s : Interval α) (t : Interval α) :
                              (s t) = s t
                              @[simp]
                              theorem Interval.disjoint_coe {α : Type u_1} [Lattice α] (s : Interval α) (t : Interval α) :
                              Disjoint s t Disjoint s t
                              @[simp]
                              @[simp]
                              @[simp]
                              theorem NonemptyInterval.mem_coe_interval {α : Type u_1} [PartialOrder α] {s : NonemptyInterval α} {x : α} :
                              x s x s
                              @[simp]
                              theorem NonemptyInterval.coe_sup_interval {α : Type u_1} [Lattice α] (s : NonemptyInterval α) (t : NonemptyInterval α) :
                              (s t) = s t
                              noncomputable instance Interval.completeLattice {α : Type u_1} [CompleteLattice α] [DecidableRel fun (x x_1 : α) => x x_1] :
                              Equations
                              • Interval.completeLattice = let __src := Interval.lattice; let __src_1 := Interval.boundedOrder; CompleteLattice.mk
                              @[simp]
                              theorem Interval.coe_sInf {α : Type u_1} [CompleteLattice α] [DecidableRel fun (x x_1 : α) => x x_1] (S : Set (Interval α)) :
                              (sInf S) = sS, s
                              @[simp]
                              theorem Interval.coe_iInf {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] [DecidableRel fun (x x_1 : α) => x x_1] (f : ιInterval α) :
                              (⨅ (i : ι), f i) = ⋂ (i : ι), (f i)
                              theorem Interval.coe_iInf₂ {α : Type u_1} {ι : Sort u_5} {κ : ιSort u_6} [CompleteLattice α] [DecidableRel fun (x x_1 : α) => x x_1] (f : (i : ι) → κ iInterval α) :
                              (⨅ (i : ι), ⨅ (j : κ i), f i j) = ⋂ (i : ι), ⋂ (j : κ i), (f i j)