Documentation

Mathlib.Order.Lattice

(Semi-)lattices #

Semilattices are partially ordered sets with join (greatest lower bound, or sup) or meet (least upper bound, or inf) operations. Lattices are posets that are both join-semilattices and meet-semilattices.

Distributive lattices are lattices which satisfy any of four equivalent distributivity properties, of sup over inf, on the left or on the right.

Main declarations #

Notations #

TODO #

Tags #

semilattice, lattice

See if the term is a ⊂ b and the goal is a ⊆ b.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    Join-semilattices #

    class SemilatticeSup (α : Type u) extends Sup , PartialOrder :

    A SemilatticeSup is a join-semilattice, that is, a partial order with a join (a.k.a. lub / least upper bound, sup / supremum) operation which is the least element larger than both factors.

    • sup : ααα
    • le : ααProp
    • lt : ααProp
    • le_refl : ∀ (a : α), a a
    • le_trans : ∀ (a b c : α), a bb ca c
    • lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
    • le_antisymm : ∀ (a b : α), a bb aa = b
    • le_sup_left : ∀ (a b : α), a a b

      The supremum is an upper bound on the first argument

    • le_sup_right : ∀ (a b : α), b a b

      The supremum is an upper bound on the second argument

    • sup_le : ∀ (a b c : α), a cb ca b c

      The supremum is the least upper bound

    Instances
      def SemilatticeSup.mk' {α : Type u_1} [Sup α] (sup_comm : ∀ (a b : α), a b = b a) (sup_assoc : ∀ (a b c : α), a b c = a (b c)) (sup_idem : ∀ (a : α), a a = a) :

      A type with a commutative, associative and idempotent binary sup operation has the structure of a join-semilattice.

      The partial order is defined so that a ≤ b unfolds to a ⊔ b = b; cf. sup_eq_right.

      Equations
      Instances For
        instance OrderDual.instSup (α : Type u_1) [Inf α] :
        Equations
        instance OrderDual.instInf (α : Type u_1) [Sup α] :
        Equations
        @[simp]
        theorem le_sup_left {α : Type u} [SemilatticeSup α] {a : α} {b : α} :
        a a b
        theorem le_sup_left' {α : Type u} [SemilatticeSup α] {a : α} {b : α} :
        a a b
        @[simp]
        theorem le_sup_right {α : Type u} [SemilatticeSup α] {a : α} {b : α} :
        b a b
        theorem le_sup_right' {α : Type u} [SemilatticeSup α] {a : α} {b : α} :
        b a b
        theorem le_sup_of_le_left {α : Type u} [SemilatticeSup α] {a : α} {b : α} {c : α} (h : c a) :
        c a b
        theorem le_sup_of_le_right {α : Type u} [SemilatticeSup α] {a : α} {b : α} {c : α} (h : c b) :
        c a b
        theorem lt_sup_of_lt_left {α : Type u} [SemilatticeSup α] {a : α} {b : α} {c : α} (h : c < a) :
        c < a b
        theorem lt_sup_of_lt_right {α : Type u} [SemilatticeSup α] {a : α} {b : α} {c : α} (h : c < b) :
        c < a b
        theorem sup_le {α : Type u} [SemilatticeSup α] {a : α} {b : α} {c : α} :
        a cb ca b c
        @[simp]
        theorem sup_le_iff {α : Type u} [SemilatticeSup α] {a : α} {b : α} {c : α} :
        a b c a c b c
        @[simp]
        theorem sup_eq_left {α : Type u} [SemilatticeSup α] {a : α} {b : α} :
        a b = a b a
        @[simp]
        theorem sup_eq_right {α : Type u} [SemilatticeSup α] {a : α} {b : α} :
        a b = b a b
        @[simp]
        theorem left_eq_sup {α : Type u} [SemilatticeSup α] {a : α} {b : α} :
        a = a b b a
        @[simp]
        theorem right_eq_sup {α : Type u} [SemilatticeSup α] {a : α} {b : α} :
        b = a b a b
        @[simp]
        theorem sup_of_le_left {α : Type u} [SemilatticeSup α] {a : α} {b : α} :
        b aa b = a

        Alias of the reverse direction of sup_eq_left.

        theorem le_of_sup_eq {α : Type u} [SemilatticeSup α] {a : α} {b : α} :
        a b = ba b

        Alias of the forward direction of sup_eq_right.

        @[simp]
        theorem sup_of_le_right {α : Type u} [SemilatticeSup α] {a : α} {b : α} :
        a ba b = b

        Alias of the reverse direction of sup_eq_right.

        @[simp]
        theorem left_lt_sup {α : Type u} [SemilatticeSup α] {a : α} {b : α} :
        a < a b ¬b a
        @[simp]
        theorem right_lt_sup {α : Type u} [SemilatticeSup α] {a : α} {b : α} :
        b < a b ¬a b
        theorem left_or_right_lt_sup {α : Type u} [SemilatticeSup α] {a : α} {b : α} (h : a b) :
        a < a b b < a b
        theorem le_iff_exists_sup {α : Type u} [SemilatticeSup α] {a : α} {b : α} :
        a b ∃ (c : α), b = a c
        theorem sup_le_sup {α : Type u} [SemilatticeSup α] {a : α} {b : α} {c : α} {d : α} (h₁ : a b) (h₂ : c d) :
        a c b d
        theorem sup_le_sup_left {α : Type u} [SemilatticeSup α] {a : α} {b : α} (h₁ : a b) (c : α) :
        c a c b
        theorem sup_le_sup_right {α : Type u} [SemilatticeSup α] {a : α} {b : α} (h₁ : a b) (c : α) :
        a c b c
        theorem sup_idem {α : Type u} [SemilatticeSup α] (a : α) :
        a a = a
        instance instIdempotentOpSupToSup {α : Type u} [SemilatticeSup α] :
        Std.IdempotentOp fun (x x_1 : α) => x x_1
        Equations
        • =
        theorem sup_comm {α : Type u} [SemilatticeSup α] (a : α) (b : α) :
        a b = b a
        instance instCommutativeSupToSup {α : Type u} [SemilatticeSup α] :
        Std.Commutative fun (x x_1 : α) => x x_1
        Equations
        • =
        theorem sup_assoc {α : Type u} [SemilatticeSup α] (a : α) (b : α) (c : α) :
        a b c = a (b c)
        instance instAssociativeSupToSup {α : Type u} [SemilatticeSup α] :
        Std.Associative fun (x x_1 : α) => x x_1
        Equations
        • =
        theorem sup_left_right_swap {α : Type u} [SemilatticeSup α] (a : α) (b : α) (c : α) :
        a b c = c b a
        theorem sup_left_idem {α : Type u} [SemilatticeSup α] (a : α) (b : α) :
        a (a b) = a b
        theorem sup_right_idem {α : Type u} [SemilatticeSup α] (a : α) (b : α) :
        a b b = a b
        theorem sup_left_comm {α : Type u} [SemilatticeSup α] (a : α) (b : α) (c : α) :
        a (b c) = b (a c)
        theorem sup_right_comm {α : Type u} [SemilatticeSup α] (a : α) (b : α) (c : α) :
        a b c = a c b
        theorem sup_sup_sup_comm {α : Type u} [SemilatticeSup α] (a : α) (b : α) (c : α) (d : α) :
        a b (c d) = a c (b d)
        theorem sup_sup_distrib_left {α : Type u} [SemilatticeSup α] (a : α) (b : α) (c : α) :
        a (b c) = a b (a c)
        theorem sup_sup_distrib_right {α : Type u} [SemilatticeSup α] (a : α) (b : α) (c : α) :
        a b c = a c (b c)
        theorem sup_congr_left {α : Type u} [SemilatticeSup α] {a : α} {b : α} {c : α} (hb : b a c) (hc : c a b) :
        a b = a c
        theorem sup_congr_right {α : Type u} [SemilatticeSup α] {a : α} {b : α} {c : α} (ha : a b c) (hb : b a c) :
        a c = b c
        theorem sup_eq_sup_iff_left {α : Type u} [SemilatticeSup α] {a : α} {b : α} {c : α} :
        a b = a c b a c c a b
        theorem sup_eq_sup_iff_right {α : Type u} [SemilatticeSup α] {a : α} {b : α} {c : α} :
        a c = b c a b c b a c
        theorem Ne.lt_sup_or_lt_sup {α : Type u} [SemilatticeSup α] {a : α} {b : α} (hab : a b) :
        a < a b b < a b
        theorem Monotone.forall_le_of_antitone {α : Type u} [SemilatticeSup α] {β : Type u_1} [Preorder β] {f : αβ} {g : αβ} (hf : Monotone f) (hg : Antitone g) (h : f g) (m : α) (n : α) :
        f m g n

        If f is monotone, g is antitone, and f ≤ g, then for all a, b we have f a ≤ g b.

        theorem SemilatticeSup.ext_sup {α : Type u_1} {A : SemilatticeSup α} {B : SemilatticeSup α} (H : ∀ (x y : α), x y x y) (x : α) (y : α) :
        x y = x y
        theorem SemilatticeSup.ext {α : Type u_1} {A : SemilatticeSup α} {B : SemilatticeSup α} (H : ∀ (x y : α), x y x y) :
        A = B
        theorem ite_le_sup {α : Type u} [SemilatticeSup α] (s : α) (s' : α) (P : Prop) [Decidable P] :
        (if P then s else s') s s'

        Meet-semilattices #

        class SemilatticeInf (α : Type u) extends Inf , PartialOrder :

        A SemilatticeInf is a meet-semilattice, that is, a partial order with a meet (a.k.a. glb / greatest lower bound, inf / infimum) operation which is the greatest element smaller than both factors.

        • inf : ααα
        • le : ααProp
        • lt : ααProp
        • le_refl : ∀ (a : α), a a
        • le_trans : ∀ (a b c : α), a bb ca c
        • lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
        • le_antisymm : ∀ (a b : α), a bb aa = b
        • inf_le_left : ∀ (a b : α), a b a

          The infimum is a lower bound on the first argument

        • inf_le_right : ∀ (a b : α), a b b

          The infimum is a lower bound on the second argument

        • le_inf : ∀ (a b c : α), a ba ca b c

          The infimum is the greatest lower bound

        Instances
          @[simp]
          theorem inf_le_left {α : Type u} [SemilatticeInf α] {a : α} {b : α} :
          a b a
          theorem inf_le_left' {α : Type u} [SemilatticeInf α] {a : α} {b : α} :
          a b a
          @[simp]
          theorem inf_le_right {α : Type u} [SemilatticeInf α] {a : α} {b : α} :
          a b b
          theorem inf_le_right' {α : Type u} [SemilatticeInf α] {a : α} {b : α} :
          a b b
          theorem le_inf {α : Type u} [SemilatticeInf α] {a : α} {b : α} {c : α} :
          a ba ca b c
          theorem inf_le_of_left_le {α : Type u} [SemilatticeInf α] {a : α} {b : α} {c : α} (h : a c) :
          a b c
          theorem inf_le_of_right_le {α : Type u} [SemilatticeInf α] {a : α} {b : α} {c : α} (h : b c) :
          a b c
          theorem inf_lt_of_left_lt {α : Type u} [SemilatticeInf α] {a : α} {b : α} {c : α} (h : a < c) :
          a b < c
          theorem inf_lt_of_right_lt {α : Type u} [SemilatticeInf α] {a : α} {b : α} {c : α} (h : b < c) :
          a b < c
          @[simp]
          theorem le_inf_iff {α : Type u} [SemilatticeInf α] {a : α} {b : α} {c : α} :
          a b c a b a c
          @[simp]
          theorem inf_eq_left {α : Type u} [SemilatticeInf α] {a : α} {b : α} :
          a b = a a b
          @[simp]
          theorem inf_eq_right {α : Type u} [SemilatticeInf α] {a : α} {b : α} :
          a b = b b a
          @[simp]
          theorem left_eq_inf {α : Type u} [SemilatticeInf α] {a : α} {b : α} :
          a = a b a b
          @[simp]
          theorem right_eq_inf {α : Type u} [SemilatticeInf α] {a : α} {b : α} :
          b = a b b a
          theorem le_of_inf_eq {α : Type u} [SemilatticeInf α] {a : α} {b : α} :
          a b = aa b

          Alias of the forward direction of inf_eq_left.

          @[simp]
          theorem inf_of_le_left {α : Type u} [SemilatticeInf α] {a : α} {b : α} :
          a ba b = a

          Alias of the reverse direction of inf_eq_left.

          @[simp]
          theorem inf_of_le_right {α : Type u} [SemilatticeInf α] {a : α} {b : α} :
          b aa b = b

          Alias of the reverse direction of inf_eq_right.

          @[simp]
          theorem inf_lt_left {α : Type u} [SemilatticeInf α] {a : α} {b : α} :
          a b < a ¬a b
          @[simp]
          theorem inf_lt_right {α : Type u} [SemilatticeInf α] {a : α} {b : α} :
          a b < b ¬b a
          theorem inf_lt_left_or_right {α : Type u} [SemilatticeInf α] {a : α} {b : α} (h : a b) :
          a b < a a b < b
          theorem inf_le_inf {α : Type u} [SemilatticeInf α] {a : α} {b : α} {c : α} {d : α} (h₁ : a b) (h₂ : c d) :
          a c b d
          theorem inf_le_inf_right {α : Type u} [SemilatticeInf α] (a : α) {b : α} {c : α} (h : b c) :
          b a c a
          theorem inf_le_inf_left {α : Type u} [SemilatticeInf α] (a : α) {b : α} {c : α} (h : b c) :
          a b a c
          theorem inf_idem {α : Type u} [SemilatticeInf α] (a : α) :
          a a = a
          instance instIdempotentOpInfToInf {α : Type u} [SemilatticeInf α] :
          Std.IdempotentOp fun (x x_1 : α) => x x_1
          Equations
          • =
          theorem inf_comm {α : Type u} [SemilatticeInf α] (a : α) (b : α) :
          a b = b a
          instance instCommutativeInfToInf {α : Type u} [SemilatticeInf α] :
          Std.Commutative fun (x x_1 : α) => x x_1
          Equations
          • =
          theorem inf_assoc {α : Type u} [SemilatticeInf α] (a : α) (b : α) (c : α) :
          a b c = a (b c)
          instance instAssociativeInfToInf {α : Type u} [SemilatticeInf α] :
          Std.Associative fun (x x_1 : α) => x x_1
          Equations
          • =
          theorem inf_left_right_swap {α : Type u} [SemilatticeInf α] (a : α) (b : α) (c : α) :
          a b c = c b a
          theorem inf_left_idem {α : Type u} [SemilatticeInf α] (a : α) (b : α) :
          a (a b) = a b
          theorem inf_right_idem {α : Type u} [SemilatticeInf α] (a : α) (b : α) :
          a b b = a b
          theorem inf_left_comm {α : Type u} [SemilatticeInf α] (a : α) (b : α) (c : α) :
          a (b c) = b (a c)
          theorem inf_right_comm {α : Type u} [SemilatticeInf α] (a : α) (b : α) (c : α) :
          a b c = a c b
          theorem inf_inf_inf_comm {α : Type u} [SemilatticeInf α] (a : α) (b : α) (c : α) (d : α) :
          a b (c d) = a c (b d)
          theorem inf_inf_distrib_left {α : Type u} [SemilatticeInf α] (a : α) (b : α) (c : α) :
          a (b c) = a b (a c)
          theorem inf_inf_distrib_right {α : Type u} [SemilatticeInf α] (a : α) (b : α) (c : α) :
          a b c = a c (b c)
          theorem inf_congr_left {α : Type u} [SemilatticeInf α] {a : α} {b : α} {c : α} (hb : a c b) (hc : a b c) :
          a b = a c
          theorem inf_congr_right {α : Type u} [SemilatticeInf α] {a : α} {b : α} {c : α} (h1 : b c a) (h2 : a c b) :
          a c = b c
          theorem inf_eq_inf_iff_left {α : Type u} [SemilatticeInf α] {a : α} {b : α} {c : α} :
          a b = a c a c b a b c
          theorem inf_eq_inf_iff_right {α : Type u} [SemilatticeInf α] {a : α} {b : α} {c : α} :
          a c = b c b c a a c b
          theorem Ne.inf_lt_or_inf_lt {α : Type u} [SemilatticeInf α] {a : α} {b : α} :
          a ba b < a a b < b
          theorem SemilatticeInf.ext_inf {α : Type u_1} {A : SemilatticeInf α} {B : SemilatticeInf α} (H : ∀ (x y : α), x y x y) (x : α) (y : α) :
          x y = x y
          theorem SemilatticeInf.ext {α : Type u_1} {A : SemilatticeInf α} {B : SemilatticeInf α} (H : ∀ (x y : α), x y x y) :
          A = B
          theorem inf_le_ite {α : Type u} [SemilatticeInf α] (s : α) (s' : α) (P : Prop) [Decidable P] :
          s s' if P then s else s'
          def SemilatticeInf.mk' {α : Type u_1} [Inf α] (inf_comm : ∀ (a b : α), a b = b a) (inf_assoc : ∀ (a b c : α), a b c = a (b c)) (inf_idem : ∀ (a : α), a a = a) :

          A type with a commutative, associative and idempotent binary inf operation has the structure of a meet-semilattice.

          The partial order is defined so that a ≤ b unfolds to b ⊓ a = a; cf. inf_eq_right.

          Equations
          Instances For

            Lattices #

            class Lattice (α : Type u) extends SemilatticeSup , Inf :

            A lattice is a join-semilattice which is also a meet-semilattice.

            • sup : ααα
            • le : ααProp
            • lt : ααProp
            • le_refl : ∀ (a : α), a a
            • le_trans : ∀ (a b c : α), a bb ca c
            • lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
            • le_antisymm : ∀ (a b : α), a bb aa = b
            • le_sup_left : ∀ (a b : α), a a b
            • le_sup_right : ∀ (a b : α), b a b
            • sup_le : ∀ (a b c : α), a cb ca b c
            • inf : ααα
            • inf_le_left : ∀ (a b : α), a b a

              The infimum is a lower bound on the first argument

            • inf_le_right : ∀ (a b : α), a b b

              The infimum is a lower bound on the second argument

            • le_inf : ∀ (a b c : α), a ba ca b c

              The infimum is the greatest lower bound

            Instances
              instance OrderDual.instLattice (α : Type u_1) [Lattice α] :
              Equations
              theorem semilatticeSup_mk'_partialOrder_eq_semilatticeInf_mk'_partialOrder {α : Type u_1} [Sup α] [Inf α] (sup_comm : ∀ (a b : α), a b = b a) (sup_assoc : ∀ (a b c : α), a b c = a (b c)) (sup_idem : ∀ (a : α), a a = a) (inf_comm : ∀ (a b : α), a b = b a) (inf_assoc : ∀ (a b c : α), a b c = a (b c)) (inf_idem : ∀ (a : α), a a = a) (sup_inf_self : ∀ (a b : α), a a b = a) (inf_sup_self : ∀ (a b : α), a (a b) = a) :
              SemilatticeSup.toPartialOrder = SemilatticeInf.toPartialOrder

              The partial orders from SemilatticeSup_mk' and SemilatticeInf_mk' agree if sup and inf satisfy the lattice absorption laws sup_inf_self (a ⊔ a ⊓ b = a) and inf_sup_self (a ⊓ (a ⊔ b) = a).

              def Lattice.mk' {α : Type u_1} [Sup α] [Inf α] (sup_comm : ∀ (a b : α), a b = b a) (sup_assoc : ∀ (a b c : α), a b c = a (b c)) (inf_comm : ∀ (a b : α), a b = b a) (inf_assoc : ∀ (a b c : α), a b c = a (b c)) (sup_inf_self : ∀ (a b : α), a a b = a) (inf_sup_self : ∀ (a b : α), a (a b) = a) :

              A type with a pair of commutative and associative binary operations which satisfy two absorption laws relating the two operations has the structure of a lattice.

              The partial order is defined so that a ≤ b unfolds to a ⊔ b = b; cf. sup_eq_right.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                theorem inf_le_sup {α : Type u} [Lattice α] {a : α} {b : α} :
                a b a b
                theorem sup_le_inf {α : Type u} [Lattice α] {a : α} {b : α} :
                a b a b a = b
                @[simp]
                theorem inf_eq_sup {α : Type u} [Lattice α] {a : α} {b : α} :
                a b = a b a = b
                @[simp]
                theorem sup_eq_inf {α : Type u} [Lattice α] {a : α} {b : α} :
                a b = a b a = b
                @[simp]
                theorem inf_lt_sup {α : Type u} [Lattice α] {a : α} {b : α} :
                a b < a b a b
                theorem inf_eq_and_sup_eq_iff {α : Type u} [Lattice α] {a : α} {b : α} {c : α} :
                a b = c a b = c a = c b = c

                Distributivity laws #

                theorem sup_inf_le {α : Type u} [Lattice α] {a : α} {b : α} {c : α} :
                a b c (a b) (a c)
                theorem le_inf_sup {α : Type u} [Lattice α] {a : α} {b : α} {c : α} :
                a b a c a (b c)
                theorem inf_sup_self {α : Type u} [Lattice α] {a : α} {b : α} :
                a (a b) = a
                theorem sup_inf_self {α : Type u} [Lattice α] {a : α} {b : α} :
                a a b = a
                theorem sup_eq_iff_inf_eq {α : Type u} [Lattice α] {a : α} {b : α} :
                a b = b a b = a
                theorem Lattice.ext {α : Type u_1} {A : Lattice α} {B : Lattice α} (H : ∀ (x y : α), x y x y) :
                A = B

                Distributive lattices #

                class DistribLattice (α : Type u_1) extends Lattice :
                Type u_1

                A distributive lattice is a lattice that satisfies any of four equivalent distributive properties (of sup over inf or inf over sup, on the left or right).

                The definition here chooses le_sup_inf: (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ (y ⊓ z). To prove distributivity from the dual law, use DistribLattice.of_inf_sup_le.

                A classic example of a distributive lattice is the lattice of subsets of a set, and in fact this example is generic in the sense that every distributive lattice is realizable as a sublattice of a powerset lattice.

                • sup : ααα
                • le : ααProp
                • lt : ααProp
                • le_refl : ∀ (a : α), a a
                • le_trans : ∀ (a b c : α), a bb ca c
                • lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
                • le_antisymm : ∀ (a b : α), a bb aa = b
                • le_sup_left : ∀ (a b : α), a a b
                • le_sup_right : ∀ (a b : α), b a b
                • sup_le : ∀ (a b c : α), a cb ca b c
                • inf : ααα
                • inf_le_left : ∀ (a b : α), a b a
                • inf_le_right : ∀ (a b : α), a b b
                • le_inf : ∀ (a b c : α), a ba ca b c
                • le_sup_inf : ∀ (x y z : α), (x y) (x z) x y z

                  The infimum distributes over the supremum

                Instances
                  theorem le_sup_inf {α : Type u} [DistribLattice α] {x : α} {y : α} {z : α} :
                  (x y) (x z) x y z
                  theorem sup_inf_left {α : Type u} [DistribLattice α] (a : α) (b : α) (c : α) :
                  a b c = (a b) (a c)
                  theorem sup_inf_right {α : Type u} [DistribLattice α] (a : α) (b : α) (c : α) :
                  a b c = (a c) (b c)
                  theorem inf_sup_left {α : Type u} [DistribLattice α] (a : α) (b : α) (c : α) :
                  a (b c) = a b a c
                  theorem inf_sup_right {α : Type u} [DistribLattice α] (a : α) (b : α) (c : α) :
                  (a b) c = a c b c
                  theorem le_of_inf_le_sup_le {α : Type u} [DistribLattice α] {x : α} {y : α} {z : α} (h₁ : x z y z) (h₂ : x z y z) :
                  x y
                  theorem eq_of_inf_eq_sup_eq {α : Type u} [DistribLattice α] {a : α} {b : α} {c : α} (h₁ : b a = c a) (h₂ : b a = c a) :
                  b = c
                  @[reducible]
                  def DistribLattice.ofInfSupLe {α : Type u} [Lattice α] (inf_sup_le : ∀ (a b c : α), a (b c) a b a c) :

                  Prove distributivity of an existing lattice from the dual distributive law.

                  Equations
                  Instances For

                    Lattices derived from linear orders #

                    instance LinearOrder.toLattice {α : Type u} [o : LinearOrder α] :
                    Equations
                    • LinearOrder.toLattice = let __spread.0 := o; Lattice.mk
                    theorem sup_eq_max {α : Type u} [LinearOrder α] {a : α} {b : α} :
                    a b = max a b
                    theorem inf_eq_min {α : Type u} [LinearOrder α] {a : α} {b : α} :
                    a b = min a b
                    theorem sup_ind {α : Type u} [LinearOrder α] (a : α) (b : α) {p : αProp} (ha : p a) (hb : p b) :
                    p (a b)
                    @[simp]
                    theorem le_sup_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} :
                    a b c a b a c
                    @[simp]
                    theorem lt_sup_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} :
                    a < b c a < b a < c
                    @[simp]
                    theorem sup_lt_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} :
                    b c < a b < a c < a
                    theorem inf_ind {α : Type u} [LinearOrder α] (a : α) (b : α) {p : αProp} :
                    p ap bp (a b)
                    @[simp]
                    theorem inf_le_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} :
                    b c a b a c a
                    @[simp]
                    theorem inf_lt_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} :
                    b c < a b < a c < a
                    @[simp]
                    theorem lt_inf_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} :
                    a < b c a < b a < c
                    theorem max_max_max_comm {α : Type u} [LinearOrder α] (a : α) (b : α) (c : α) (d : α) :
                    max (max a b) (max c d) = max (max a c) (max b d)
                    theorem min_min_min_comm {α : Type u} [LinearOrder α] (a : α) (b : α) (c : α) (d : α) :
                    min (min a b) (min c d) = min (min a c) (min b d)
                    theorem sup_eq_maxDefault {α : Type u} [SemilatticeSup α] [DecidableRel fun (x x_1 : α) => x x_1] [IsTotal α fun (x x_1 : α) => x x_1] :
                    (fun (x x_1 : α) => x x_1) = maxDefault
                    theorem inf_eq_minDefault {α : Type u} [SemilatticeInf α] [DecidableRel fun (x x_1 : α) => x x_1] [IsTotal α fun (x x_1 : α) => x x_1] :
                    (fun (x x_1 : α) => x x_1) = minDefault
                    @[reducible]
                    def Lattice.toLinearOrder (α : Type u) [Lattice α] [DecidableEq α] [DecidableRel fun (x x_1 : α) => x x_1] [DecidableRel fun (x x_1 : α) => x < x_1] [IsTotal α fun (x x_1 : α) => x x_1] :

                    A lattice with total order is a linear order.

                    See note [reducible non-instances].

                    Equations
                    Instances For
                      Equations
                      Equations

                      Dual order #

                      @[simp]
                      theorem ofDual_inf {α : Type u} [Sup α] (a : αᵒᵈ) (b : αᵒᵈ) :
                      OrderDual.ofDual (a b) = OrderDual.ofDual a OrderDual.ofDual b
                      @[simp]
                      theorem ofDual_sup {α : Type u} [Inf α] (a : αᵒᵈ) (b : αᵒᵈ) :
                      OrderDual.ofDual (a b) = OrderDual.ofDual a OrderDual.ofDual b
                      @[simp]
                      theorem toDual_inf {α : Type u} [Inf α] (a : α) (b : α) :
                      OrderDual.toDual (a b) = OrderDual.toDual a OrderDual.toDual b
                      @[simp]
                      theorem toDual_sup {α : Type u} [Sup α] (a : α) (b : α) :
                      OrderDual.toDual (a b) = OrderDual.toDual a OrderDual.toDual b
                      @[simp]
                      theorem ofDual_min {α : Type u} [LinearOrder α] (a : αᵒᵈ) (b : αᵒᵈ) :
                      OrderDual.ofDual (min a b) = max (OrderDual.ofDual a) (OrderDual.ofDual b)
                      @[simp]
                      theorem ofDual_max {α : Type u} [LinearOrder α] (a : αᵒᵈ) (b : αᵒᵈ) :
                      OrderDual.ofDual (max a b) = min (OrderDual.ofDual a) (OrderDual.ofDual b)
                      @[simp]
                      theorem toDual_min {α : Type u} [LinearOrder α] (a : α) (b : α) :
                      OrderDual.toDual (min a b) = max (OrderDual.toDual a) (OrderDual.toDual b)
                      @[simp]
                      theorem toDual_max {α : Type u} [LinearOrder α] (a : α) (b : α) :
                      OrderDual.toDual (max a b) = min (OrderDual.toDual a) (OrderDual.toDual b)

                      Function lattices #

                      instance Pi.instSupForAll {ι : Type u_1} {α' : ιType u_2} [(i : ι) → Sup (α' i)] :
                      Sup ((i : ι) → α' i)
                      Equations
                      • Pi.instSupForAll = { sup := fun (f g : (i : ι) → α' i) (i : ι) => f i g i }
                      @[simp]
                      theorem Pi.sup_apply {ι : Type u_1} {α' : ιType u_2} [(i : ι) → Sup (α' i)] (f : (i : ι) → α' i) (g : (i : ι) → α' i) (i : ι) :
                      (f g) i = f i g i
                      theorem Pi.sup_def {ι : Type u_1} {α' : ιType u_2} [(i : ι) → Sup (α' i)] (f : (i : ι) → α' i) (g : (i : ι) → α' i) :
                      f g = fun (i : ι) => f i g i
                      instance Pi.instInfForAll {ι : Type u_1} {α' : ιType u_2} [(i : ι) → Inf (α' i)] :
                      Inf ((i : ι) → α' i)
                      Equations
                      • Pi.instInfForAll = { inf := fun (f g : (i : ι) → α' i) (i : ι) => f i g i }
                      @[simp]
                      theorem Pi.inf_apply {ι : Type u_1} {α' : ιType u_2} [(i : ι) → Inf (α' i)] (f : (i : ι) → α' i) (g : (i : ι) → α' i) (i : ι) :
                      (f g) i = f i g i
                      theorem Pi.inf_def {ι : Type u_1} {α' : ιType u_2} [(i : ι) → Inf (α' i)] (f : (i : ι) → α' i) (g : (i : ι) → α' i) :
                      f g = fun (i : ι) => f i g i
                      instance Pi.instSemilatticeSup {ι : Type u_1} {α' : ιType u_2} [(i : ι) → SemilatticeSup (α' i)] :
                      SemilatticeSup ((i : ι) → α' i)
                      Equations
                      instance Pi.instSemilatticeInf {ι : Type u_1} {α' : ιType u_2} [(i : ι) → SemilatticeInf (α' i)] :
                      SemilatticeInf ((i : ι) → α' i)
                      Equations
                      instance Pi.instLattice {ι : Type u_1} {α' : ιType u_2} [(i : ι) → Lattice (α' i)] :
                      Lattice ((i : ι) → α' i)
                      Equations
                      instance Pi.instDistribLattice {ι : Type u_1} {α' : ιType u_2} [(i : ι) → DistribLattice (α' i)] :
                      DistribLattice ((i : ι) → α' i)
                      Equations
                      theorem Function.update_sup {ι : Type u_1} {π : ιType u_2} [DecidableEq ι] [(i : ι) → SemilatticeSup (π i)] (f : (i : ι) → π i) (i : ι) (a : π i) (b : π i) :
                      theorem Function.update_inf {ι : Type u_1} {π : ιType u_2} [DecidableEq ι] [(i : ι) → SemilatticeInf (π i)] (f : (i : ι) → π i) (i : ι) (a : π i) (b : π i) :

                      Monotone functions and lattices #

                      theorem Monotone.sup {α : Type u} {β : Type v} [Preorder α] [SemilatticeSup β] {f : αβ} {g : αβ} (hf : Monotone f) (hg : Monotone g) :

                      Pointwise supremum of two monotone functions is a monotone function.

                      theorem Monotone.inf {α : Type u} {β : Type v} [Preorder α] [SemilatticeInf β] {f : αβ} {g : αβ} (hf : Monotone f) (hg : Monotone g) :

                      Pointwise infimum of two monotone functions is a monotone function.

                      theorem Monotone.max {α : Type u} {β : Type v} [Preorder α] [LinearOrder β] {f : αβ} {g : αβ} (hf : Monotone f) (hg : Monotone g) :
                      Monotone fun (x : α) => max (f x) (g x)

                      Pointwise maximum of two monotone functions is a monotone function.

                      theorem Monotone.min {α : Type u} {β : Type v} [Preorder α] [LinearOrder β] {f : αβ} {g : αβ} (hf : Monotone f) (hg : Monotone g) :
                      Monotone fun (x : α) => min (f x) (g x)

                      Pointwise minimum of two monotone functions is a monotone function.

                      theorem Monotone.le_map_sup {α : Type u} {β : Type v} [SemilatticeSup α] [SemilatticeSup β] {f : αβ} (h : Monotone f) (x : α) (y : α) :
                      f x f y f (x y)
                      theorem Monotone.map_inf_le {α : Type u} {β : Type v} [SemilatticeInf α] [SemilatticeInf β] {f : αβ} (h : Monotone f) (x : α) (y : α) :
                      f (x y) f x f y
                      theorem Monotone.of_map_inf {α : Type u} {β : Type v} [SemilatticeInf α] [SemilatticeInf β] {f : αβ} (h : ∀ (x y : α), f (x y) = f x f y) :
                      theorem Monotone.of_map_sup {α : Type u} {β : Type v} [SemilatticeSup α] [SemilatticeSup β] {f : αβ} (h : ∀ (x y : α), f (x y) = f x f y) :
                      theorem Monotone.map_sup {α : Type u} {β : Type v} [LinearOrder α] [SemilatticeSup β] {f : αβ} (hf : Monotone f) (x : α) (y : α) :
                      f (x y) = f x f y
                      theorem Monotone.map_inf {α : Type u} {β : Type v} [LinearOrder α] [SemilatticeInf β] {f : αβ} (hf : Monotone f) (x : α) (y : α) :
                      f (x y) = f x f y
                      theorem MonotoneOn.sup {α : Type u} {β : Type v} [Preorder α] [SemilatticeSup β] {f : αβ} {g : αβ} {s : Set α} (hf : MonotoneOn f s) (hg : MonotoneOn g s) :
                      MonotoneOn (f g) s

                      Pointwise supremum of two monotone functions is a monotone function.

                      theorem MonotoneOn.inf {α : Type u} {β : Type v} [Preorder α] [SemilatticeInf β] {f : αβ} {g : αβ} {s : Set α} (hf : MonotoneOn f s) (hg : MonotoneOn g s) :
                      MonotoneOn (f g) s

                      Pointwise infimum of two monotone functions is a monotone function.

                      theorem MonotoneOn.max {α : Type u} {β : Type v} [Preorder α] [LinearOrder β] {f : αβ} {g : αβ} {s : Set α} (hf : MonotoneOn f s) (hg : MonotoneOn g s) :
                      MonotoneOn (fun (x : α) => max (f x) (g x)) s

                      Pointwise maximum of two monotone functions is a monotone function.

                      theorem MonotoneOn.min {α : Type u} {β : Type v} [Preorder α] [LinearOrder β] {f : αβ} {g : αβ} {s : Set α} (hf : MonotoneOn f s) (hg : MonotoneOn g s) :
                      MonotoneOn (fun (x : α) => min (f x) (g x)) s

                      Pointwise minimum of two monotone functions is a monotone function.

                      theorem MonotoneOn.of_map_inf {α : Type u} {β : Type v} {f : αβ} {s : Set α} [SemilatticeInf α] [SemilatticeInf β] (h : ∀ (x : α), x s∀ (y : α), y sf (x y) = f x f y) :
                      theorem MonotoneOn.of_map_sup {α : Type u} {β : Type v} {f : αβ} {s : Set α} [SemilatticeSup α] [SemilatticeSup β] (h : ∀ (x : α), x s∀ (y : α), y sf (x y) = f x f y) :
                      theorem MonotoneOn.map_sup {α : Type u} {β : Type v} {f : αβ} {s : Set α} {x : α} {y : α} [LinearOrder α] [SemilatticeSup β] (hf : MonotoneOn f s) (hx : x s) (hy : y s) :
                      f (x y) = f x f y
                      theorem MonotoneOn.map_inf {α : Type u} {β : Type v} {f : αβ} {s : Set α} {x : α} {y : α} [LinearOrder α] [SemilatticeInf β] (hf : MonotoneOn f s) (hx : x s) (hy : y s) :
                      f (x y) = f x f y
                      theorem Antitone.sup {α : Type u} {β : Type v} [Preorder α] [SemilatticeSup β] {f : αβ} {g : αβ} (hf : Antitone f) (hg : Antitone g) :

                      Pointwise supremum of two monotone functions is a monotone function.

                      theorem Antitone.inf {α : Type u} {β : Type v} [Preorder α] [SemilatticeInf β] {f : αβ} {g : αβ} (hf : Antitone f) (hg : Antitone g) :

                      Pointwise infimum of two monotone functions is a monotone function.

                      theorem Antitone.max {α : Type u} {β : Type v} [Preorder α] [LinearOrder β] {f : αβ} {g : αβ} (hf : Antitone f) (hg : Antitone g) :
                      Antitone fun (x : α) => max (f x) (g x)

                      Pointwise maximum of two monotone functions is a monotone function.

                      theorem Antitone.min {α : Type u} {β : Type v} [Preorder α] [LinearOrder β] {f : αβ} {g : αβ} (hf : Antitone f) (hg : Antitone g) :
                      Antitone fun (x : α) => min (f x) (g x)

                      Pointwise minimum of two monotone functions is a monotone function.

                      theorem Antitone.map_sup_le {α : Type u} {β : Type v} [SemilatticeSup α] [SemilatticeInf β] {f : αβ} (h : Antitone f) (x : α) (y : α) :
                      f (x y) f x f y
                      theorem Antitone.le_map_inf {α : Type u} {β : Type v} [SemilatticeInf α] [SemilatticeSup β] {f : αβ} (h : Antitone f) (x : α) (y : α) :
                      f x f y f (x y)
                      theorem Antitone.map_sup {α : Type u} {β : Type v} [LinearOrder α] [SemilatticeInf β] {f : αβ} (hf : Antitone f) (x : α) (y : α) :
                      f (x y) = f x f y
                      theorem Antitone.map_inf {α : Type u} {β : Type v} [LinearOrder α] [SemilatticeSup β] {f : αβ} (hf : Antitone f) (x : α) (y : α) :
                      f (x y) = f x f y
                      theorem AntitoneOn.sup {α : Type u} {β : Type v} [Preorder α] [SemilatticeSup β] {f : αβ} {g : αβ} {s : Set α} (hf : AntitoneOn f s) (hg : AntitoneOn g s) :
                      AntitoneOn (f g) s

                      Pointwise supremum of two antitone functions is an antitone function.

                      theorem AntitoneOn.inf {α : Type u} {β : Type v} [Preorder α] [SemilatticeInf β] {f : αβ} {g : αβ} {s : Set α} (hf : AntitoneOn f s) (hg : AntitoneOn g s) :
                      AntitoneOn (f g) s

                      Pointwise infimum of two antitone functions is an antitone function.

                      theorem AntitoneOn.max {α : Type u} {β : Type v} [Preorder α] [LinearOrder β] {f : αβ} {g : αβ} {s : Set α} (hf : AntitoneOn f s) (hg : AntitoneOn g s) :
                      AntitoneOn (fun (x : α) => max (f x) (g x)) s

                      Pointwise maximum of two antitone functions is an antitone function.

                      theorem AntitoneOn.min {α : Type u} {β : Type v} [Preorder α] [LinearOrder β] {f : αβ} {g : αβ} {s : Set α} (hf : AntitoneOn f s) (hg : AntitoneOn g s) :
                      AntitoneOn (fun (x : α) => min (f x) (g x)) s

                      Pointwise minimum of two antitone functions is an antitone function.

                      theorem AntitoneOn.of_map_inf {α : Type u} {β : Type v} {f : αβ} {s : Set α} [SemilatticeInf α] [SemilatticeSup β] (h : ∀ (x : α), x s∀ (y : α), y sf (x y) = f x f y) :
                      theorem AntitoneOn.of_map_sup {α : Type u} {β : Type v} {f : αβ} {s : Set α} [SemilatticeSup α] [SemilatticeInf β] (h : ∀ (x : α), x s∀ (y : α), y sf (x y) = f x f y) :
                      theorem AntitoneOn.map_sup {α : Type u} {β : Type v} {f : αβ} {s : Set α} {x : α} {y : α} [LinearOrder α] [SemilatticeInf β] (hf : AntitoneOn f s) (hx : x s) (hy : y s) :
                      f (x y) = f x f y
                      theorem AntitoneOn.map_inf {α : Type u} {β : Type v} {f : αβ} {s : Set α} {x : α} {y : α} [LinearOrder α] [SemilatticeSup β] (hf : AntitoneOn f s) (hx : x s) (hy : y s) :
                      f (x y) = f x f y

                      Products of (semi-)lattices #

                      instance Prod.instSupProd (α : Type u) (β : Type v) [Sup α] [Sup β] :
                      Sup (α × β)
                      Equations
                      instance Prod.instInfProd (α : Type u) (β : Type v) [Inf α] [Inf β] :
                      Inf (α × β)
                      Equations
                      @[simp]
                      theorem Prod.mk_sup_mk (α : Type u) (β : Type v) [Sup α] [Sup β] (a₁ : α) (a₂ : α) (b₁ : β) (b₂ : β) :
                      (a₁, b₁) (a₂, b₂) = (a₁ a₂, b₁ b₂)
                      @[simp]
                      theorem Prod.mk_inf_mk (α : Type u) (β : Type v) [Inf α] [Inf β] (a₁ : α) (a₂ : α) (b₁ : β) (b₂ : β) :
                      (a₁, b₁) (a₂, b₂) = (a₁ a₂, b₁ b₂)
                      @[simp]
                      theorem Prod.fst_sup (α : Type u) (β : Type v) [Sup α] [Sup β] (p : α × β) (q : α × β) :
                      (p q).1 = p.1 q.1
                      @[simp]
                      theorem Prod.fst_inf (α : Type u) (β : Type v) [Inf α] [Inf β] (p : α × β) (q : α × β) :
                      (p q).1 = p.1 q.1
                      @[simp]
                      theorem Prod.snd_sup (α : Type u) (β : Type v) [Sup α] [Sup β] (p : α × β) (q : α × β) :
                      (p q).2 = p.2 q.2
                      @[simp]
                      theorem Prod.snd_inf (α : Type u) (β : Type v) [Inf α] [Inf β] (p : α × β) (q : α × β) :
                      (p q).2 = p.2 q.2
                      @[simp]
                      theorem Prod.swap_sup (α : Type u) (β : Type v) [Sup α] [Sup β] (p : α × β) (q : α × β) :
                      @[simp]
                      theorem Prod.swap_inf (α : Type u) (β : Type v) [Inf α] [Inf β] (p : α × β) (q : α × β) :
                      theorem Prod.sup_def (α : Type u) (β : Type v) [Sup α] [Sup β] (p : α × β) (q : α × β) :
                      p q = (p.1 q.1, p.2 q.2)
                      theorem Prod.inf_def (α : Type u) (β : Type v) [Inf α] [Inf β] (p : α × β) (q : α × β) :
                      p q = (p.1 q.1, p.2 q.2)
                      instance Prod.instSemilatticeSup (α : Type u) (β : Type v) [SemilatticeSup α] [SemilatticeSup β] :
                      Equations
                      instance Prod.instSemilatticeInf (α : Type u) (β : Type v) [SemilatticeInf α] [SemilatticeInf β] :
                      Equations
                      instance Prod.instLattice (α : Type u) (β : Type v) [Lattice α] [Lattice β] :
                      Lattice (α × β)
                      Equations
                      instance Prod.instDistribLattice (α : Type u) (β : Type v) [DistribLattice α] [DistribLattice β] :
                      Equations

                      Subtypes of (semi-)lattices #

                      @[reducible]
                      def Subtype.semilatticeSup {α : Type u} [SemilatticeSup α] {P : αProp} (Psup : ∀ ⦃x y : α⦄, P xP yP (x y)) :
                      SemilatticeSup { x : α // P x }

                      A subtype forms a -semilattice if preserves the property. See note [reducible non-instances].

                      Equations
                      Instances For
                        @[reducible]
                        def Subtype.semilatticeInf {α : Type u} [SemilatticeInf α] {P : αProp} (Pinf : ∀ ⦃x y : α⦄, P xP yP (x y)) :
                        SemilatticeInf { x : α // P x }

                        A subtype forms a -semilattice if preserves the property. See note [reducible non-instances].

                        Equations
                        Instances For
                          @[reducible]
                          def Subtype.lattice {α : Type u} [Lattice α] {P : αProp} (Psup : ∀ ⦃x y : α⦄, P xP yP (x y)) (Pinf : ∀ ⦃x y : α⦄, P xP yP (x y)) :
                          Lattice { x : α // P x }

                          A subtype forms a lattice if and preserve the property. See note [reducible non-instances].

                          Equations
                          Instances For
                            @[simp]
                            theorem Subtype.coe_sup {α : Type u} [SemilatticeSup α] {P : αProp} (Psup : ∀ ⦃x y : α⦄, P xP yP (x y)) (x : Subtype P) (y : Subtype P) :
                            (x y) = x y
                            @[simp]
                            theorem Subtype.coe_inf {α : Type u} [SemilatticeInf α] {P : αProp} (Pinf : ∀ ⦃x y : α⦄, P xP yP (x y)) (x : Subtype P) (y : Subtype P) :
                            (x y) = x y
                            @[simp]
                            theorem Subtype.mk_sup_mk {α : Type u} [SemilatticeSup α] {P : αProp} (Psup : ∀ ⦃x y : α⦄, P xP yP (x y)) {x : α} {y : α} (hx : P x) (hy : P y) :
                            { val := x, property := hx } { val := y, property := hy } = { val := x y, property := }
                            @[simp]
                            theorem Subtype.mk_inf_mk {α : Type u} [SemilatticeInf α] {P : αProp} (Pinf : ∀ ⦃x y : α⦄, P xP yP (x y)) {x : α} {y : α} (hx : P x) (hy : P y) :
                            { val := x, property := hx } { val := y, property := hy } = { val := x y, property := }
                            @[reducible]
                            def Function.Injective.semilatticeSup {α : Type u} {β : Type v} [Sup α] [SemilatticeSup β] (f : αβ) (hf_inj : Function.Injective f) (map_sup : ∀ (a b : α), f (a b) = f a f b) :

                            A type endowed with is a SemilatticeSup, if it admits an injective map that preserves to a SemilatticeSup. See note [reducible non-instances].

                            Equations
                            Instances For
                              @[reducible]
                              def Function.Injective.semilatticeInf {α : Type u} {β : Type v} [Inf α] [SemilatticeInf β] (f : αβ) (hf_inj : Function.Injective f) (map_inf : ∀ (a b : α), f (a b) = f a f b) :

                              A type endowed with is a SemilatticeInf, if it admits an injective map that preserves to a SemilatticeInf. See note [reducible non-instances].

                              Equations
                              Instances For
                                @[reducible]
                                def Function.Injective.lattice {α : Type u} {β : Type v} [Sup α] [Inf α] [Lattice β] (f : αβ) (hf_inj : Function.Injective f) (map_sup : ∀ (a b : α), f (a b) = f a f b) (map_inf : ∀ (a b : α), f (a b) = f a f b) :

                                A type endowed with and is a Lattice, if it admits an injective map that preserves and to a Lattice. See note [reducible non-instances].

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  @[reducible]
                                  def Function.Injective.distribLattice {α : Type u} {β : Type v} [Sup α] [Inf α] [DistribLattice β] (f : αβ) (hf_inj : Function.Injective f) (map_sup : ∀ (a b : α), f (a b) = f a f b) (map_inf : ∀ (a b : α), f (a b) = f a f b) :

                                  A type endowed with and is a DistribLattice, if it admits an injective map that preserves and to a DistribLattice. See note [reducible non-instances].

                                  Equations
                                  Instances For
                                    Equations
                                    Equations
                                    Equations
                                    Equations
                                    Equations