Documentation

Mathlib.Data.Fintype.Order

Order structures on finite types #

This file provides order instances on fintypes.

Computable instances #

On a Fintype, we can construct

Those are marked as def to avoid defeqness issues.

Completion instances #

Those instances are noncomputable because the definitions of sSup and sInf use Set.toFinset and set membership is undecidable in general.

On a Fintype, we can promote:

Those are marked as def to avoid typeclass loops.

Concrete instances #

We provide a few instances for concrete types:

@[reducible, inline]
abbrev Fintype.toOrderBot (α : Type u_2) [Fintype α] [Nonempty α] [SemilatticeInf α] :

Constructs the of a finite nonempty SemilatticeInf.

Equations
Instances For
    @[reducible, inline]
    abbrev Fintype.toOrderTop (α : Type u_2) [Fintype α] [Nonempty α] [SemilatticeSup α] :

    Constructs the of a finite nonempty SemilatticeSup

    Equations
    Instances For
      @[reducible, inline]
      abbrev Fintype.toBoundedOrder (α : Type u_2) [Fintype α] [Nonempty α] [Lattice α] :

      Constructs the and of a finite nonempty Lattice.

      Equations
      Instances For
        @[reducible, inline]
        noncomputable abbrev Fintype.toCompleteLattice (α : Type u_2) [Fintype α] [Lattice α] [BoundedOrder α] :

        A finite bounded lattice is complete.

        Equations
        Instances For
          @[reducible, inline]

          A finite bounded distributive lattice is completely distributive.

          Equations
          Instances For
            @[reducible, inline]

            A finite bounded distributive lattice is completely distributive.

            Equations
            Instances For
              @[reducible, inline]
              noncomputable abbrev Fintype.toCompleteLinearOrder (α : Type u_2) [Fintype α] [LinearOrder α] [BoundedOrder α] :

              A finite bounded linear order is complete.

              Equations
              Instances For
                @[reducible, inline]

                A finite boolean algebra is complete.

                Equations
                Instances For
                  @[reducible, inline]

                  A finite boolean algebra is complete and atomic.

                  Equations
                  Instances For
                    @[reducible, inline]
                    noncomputable abbrev Fintype.toCompleteLatticeOfNonempty (α : Type u_2) [Fintype α] [Nonempty α] [Lattice α] :

                    A nonempty finite lattice is complete. If the lattice is already a BoundedOrder, then use Fintype.toCompleteLattice instead, as this gives definitional equality for and .

                    Equations
                    Instances For
                      @[reducible, inline]

                      A nonempty finite linear order is complete. If the linear order is already a BoundedOrder, then use Fintype.toCompleteLinearOrder instead, as this gives definitional equality for and .

                      Equations
                      Instances For

                        Properties for PartialOrders #

                        theorem Finite.exists_minimal_le {α : Type u_1} [PartialOrder α] {a : α} {p : αProp} [Finite α] (h : p a) :
                        ba, Minimal p b
                        @[deprecated Finite.exists_minimal_le]
                        theorem Finite.exists_ge_minimal {α : Type u_1} [PartialOrder α] {a : α} {p : αProp} [Finite α] (h : p a) :
                        ba, Minimal p b

                        Alias of Finite.exists_minimal_le.

                        theorem Finite.exists_le_maximal {α : Type u_1} [PartialOrder α] {a : α} {p : αProp} [Finite α] (h : p a) :
                        ∃ (b : α), a b Maximal p b
                        theorem Finset.exists_minimal_le {α : Type u_1} [PartialOrder α] {a : α} (s : Finset α) (h : a s) :
                        ba, Minimal (fun (x : α) => x s) b
                        theorem Finset.exists_le_maximal {α : Type u_1} [PartialOrder α] {a : α} (s : Finset α) (h : a s) :
                        ∃ (b : α), a b Maximal (fun (x : α) => x s) b
                        theorem Set.Finite.exists_minimal_le {α : Type u_1} [PartialOrder α] {a : α} {s : Set α} (hs : s.Finite) (h : a s) :
                        ba, Minimal (fun (x : α) => x s) b
                        theorem Set.Finite.exists_le_maximal {α : Type u_1} [PartialOrder α] {a : α} {s : Set α} (hs : s.Finite) (h : a s) :
                        ∃ (b : α), a b Maximal (fun (x : α) => x s) b

                        Concrete instances #

                        noncomputable instance Fin.completeLinearOrder {n : } [NeZero n] :
                        Equations

                        Directed Orders #

                        theorem Directed.finite_set_le {α : Type u_1} {r : ααProp} [IsTrans α r] {γ : Type u_3} [Nonempty γ] {f : γα} (D : Directed r f) {s : Set γ} (hs : s.Finite) :
                        ∃ (z : γ), is, r (f i) (f z)
                        theorem Directed.finite_le {α : Type u_1} {r : ααProp} [IsTrans α r] {β : Type u_2} {γ : Type u_3} [Nonempty γ] {f : γα} [Finite β] (D : Directed r f) (g : βγ) :
                        ∃ (z : γ), ∀ (i : β), r (f (g i)) (f z)
                        theorem Finite.exists_le {α : Type u_1} {β : Type u_2} [Finite β] [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] (f : βα) :
                        ∃ (M : α), ∀ (i : β), f i M
                        theorem Finite.exists_ge {α : Type u_1} {β : Type u_2} [Finite β] [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] (f : βα) :
                        ∃ (M : α), ∀ (i : β), M f i
                        theorem Set.Finite.exists_le {α : Type u_1} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {s : Set α} (hs : s.Finite) :
                        ∃ (M : α), is, i M
                        theorem Set.Finite.exists_ge {α : Type u_1} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {s : Set α} (hs : s.Finite) :
                        ∃ (M : α), is, M i
                        @[simp]
                        theorem Finite.bddAbove_range {α : Type u_1} {β : Type u_2} [Finite β] [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] (f : βα) :
                        @[simp]
                        theorem Finite.bddBelow_range {α : Type u_1} {β : Type u_2} [Finite β] [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] (f : βα) :
                        @[deprecated Directed.finite_le]
                        theorem Directed.fintype_le {α : Type u_1} {r : ααProp} [IsTrans α r] {β : Type u_2} {γ : Type u_3} [Nonempty γ] {f : γα} [Finite β] (D : Directed r f) (g : βγ) :
                        ∃ (z : γ), ∀ (i : β), r (f (g i)) (f z)

                        Alias of Directed.finite_le.

                        @[deprecated Finite.exists_le]
                        theorem Fintype.exists_le {α : Type u_1} {β : Type u_2} [Finite β] [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] (f : βα) :
                        ∃ (M : α), ∀ (i : β), f i M

                        Alias of Finite.exists_le.

                        @[deprecated Finite.exists_ge]
                        theorem Fintype.exists_ge {α : Type u_1} {β : Type u_2} [Finite β] [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] (f : βα) :
                        ∃ (M : α), ∀ (i : β), M f i

                        Alias of Finite.exists_ge.

                        @[deprecated Finite.bddAbove_range]
                        theorem Fintype.bddAbove_range {α : Type u_1} {β : Type u_2} [Finite β] [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] (f : βα) :

                        Alias of Finite.bddAbove_range.

                        @[deprecated Finite.bddBelow_range]
                        theorem Fintype.bddBelow_range {α : Type u_1} {β : Type u_2} [Finite β] [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] (f : βα) :

                        Alias of Finite.bddBelow_range.