Documentation

Mathlib.Order.Lattice

(Semi-)lattices #

Semilattices are partially ordered sets with join (least upper bound, or sup) or meet (greatest lower 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
Instances For

    Join-semilattices #

    class SemilatticeSup (α : Type u) extends 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.

    • 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
    • sup : ααα

      The binary supremum, used to derive Max α

    • le_sup_left (a b : α) : a sup a b

      The supremum is an upper bound on the first argument

    • le_sup_right (a b : α) : b sup a b

      The supremum is an upper bound on the second argument

    • sup_le (a b c : α) : a cb csup a b c

      The supremum is the least upper bound

    Instances
      instance SemilatticeSup.toMax {α : Type u} [SemilatticeSup α] :
      Max α
      Equations
      def SemilatticeSup.mk' {α : Type u_1} [Max α] (sup_comm : ∀ (a b : α), ab = ba) (sup_assoc : ∀ (a b c : α), abc = a(bc)) (sup_idem : ∀ (a : α), aa = 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
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem le_sup_left {α : Type u} [SemilatticeSup α] {a b : α} :
        a ab
        @[simp]
        theorem le_sup_right {α : Type u} [SemilatticeSup α] {a b : α} :
        b ab
        theorem le_sup_of_le_left {α : Type u} [SemilatticeSup α] {a b c : α} (h : c a) :
        c ab
        theorem le_sup_of_le_right {α : Type u} [SemilatticeSup α] {a b c : α} (h : c b) :
        c ab
        theorem lt_sup_of_lt_left {α : Type u} [SemilatticeSup α] {a b c : α} (h : c < a) :
        c < ab
        theorem lt_sup_of_lt_right {α : Type u} [SemilatticeSup α] {a b c : α} (h : c < b) :
        c < ab
        theorem sup_le {α : Type u} [SemilatticeSup α] {a b c : α} :
        a cb cab c
        @[simp]
        theorem sup_le_iff {α : Type u} [SemilatticeSup α] {a b c : α} :
        ab c a c b c
        @[simp]
        theorem sup_eq_left {α : Type u} [SemilatticeSup α] {a b : α} :
        ab = a b a
        @[simp]
        theorem sup_eq_right {α : Type u} [SemilatticeSup α] {a b : α} :
        ab = b a b
        @[simp]
        theorem left_eq_sup {α : Type u} [SemilatticeSup α] {a b : α} :
        a = ab b a
        @[simp]
        theorem right_eq_sup {α : Type u} [SemilatticeSup α] {a b : α} :
        b = ab a b
        @[simp]
        theorem sup_of_le_left {α : Type u} [SemilatticeSup α] {a b : α} :
        b aab = a

        Alias of the reverse direction of sup_eq_left.

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

        Alias of the reverse direction of sup_eq_right.

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

        Alias of the forward direction of sup_eq_right.

        @[simp]
        theorem left_lt_sup {α : Type u} [SemilatticeSup α] {a b : α} :
        a < ab ¬b a
        @[simp]
        theorem right_lt_sup {α : Type u} [SemilatticeSup α] {a b : α} :
        b < ab ¬a b
        theorem left_or_right_lt_sup {α : Type u} [SemilatticeSup α] {a b : α} (h : a b) :
        a < ab b < ab
        theorem le_iff_exists_sup {α : Type u} [SemilatticeSup α] {a b : α} :
        a b (c : α), b = ac
        theorem sup_le_sup {α : Type u} [SemilatticeSup α] {a b c d : α} (h₁ : a b) (h₂ : c d) :
        ac bd
        theorem sup_le_sup_left {α : Type u} [SemilatticeSup α] {a b : α} (h₁ : a b) (c : α) :
        ca cb
        theorem sup_le_sup_right {α : Type u} [SemilatticeSup α] {a b : α} (h₁ : a b) (c : α) :
        ac bc
        theorem sup_idem {α : Type u} [SemilatticeSup α] (a : α) :
        aa = a
        instance instIdempotentOpMax_mathlib {α : Type u} [SemilatticeSup α] :
        Std.IdempotentOp fun (x1 x2 : α) => x1x2
        theorem sup_comm {α : Type u} [SemilatticeSup α] (a b : α) :
        ab = ba
        instance instCommutativeMax_mathlib {α : Type u} [SemilatticeSup α] :
        Std.Commutative fun (x1 x2 : α) => x1x2
        theorem sup_assoc {α : Type u} [SemilatticeSup α] (a b c : α) :
        abc = a(bc)
        instance instAssociativeMax_mathlib {α : Type u} [SemilatticeSup α] :
        Std.Associative fun (x1 x2 : α) => x1x2
        theorem sup_left_right_swap {α : Type u} [SemilatticeSup α] (a b c : α) :
        abc = cba
        theorem sup_left_idem {α : Type u} [SemilatticeSup α] (a b : α) :
        a(ab) = ab
        theorem sup_right_idem {α : Type u} [SemilatticeSup α] (a b : α) :
        abb = ab
        theorem sup_left_comm {α : Type u} [SemilatticeSup α] (a b c : α) :
        a(bc) = b(ac)
        theorem sup_right_comm {α : Type u} [SemilatticeSup α] (a b c : α) :
        abc = acb
        theorem sup_sup_sup_comm {α : Type u} [SemilatticeSup α] (a b c d : α) :
        ab(cd) = ac(bd)
        theorem sup_sup_distrib_left {α : Type u} [SemilatticeSup α] (a b c : α) :
        a(bc) = ab(ac)
        theorem sup_sup_distrib_right {α : Type u} [SemilatticeSup α] (a b c : α) :
        abc = ac(bc)
        theorem sup_congr_left {α : Type u} [SemilatticeSup α] {a b c : α} (hb : b ac) (hc : c ab) :
        ab = ac
        theorem sup_congr_right {α : Type u} [SemilatticeSup α] {a b c : α} (ha : a bc) (hb : b ac) :
        ac = bc
        theorem sup_eq_sup_iff_left {α : Type u} [SemilatticeSup α] {a b c : α} :
        ab = ac b ac c ab
        theorem sup_eq_sup_iff_right {α : Type u} [SemilatticeSup α] {a b c : α} :
        ac = bc a bc b ac
        theorem Ne.lt_sup_or_lt_sup {α : Type u} [SemilatticeSup α] {a b : α} (hab : a b) :
        a < ab b < ab
        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 B : SemilatticeSup α} (H : ∀ (x y : α), x y x y) (x y : α) :
        xy = xy
        theorem SemilatticeSup.ext {α : Type u_1} {A 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') ss'

        Meet-semilattices #

        class SemilatticeInf (α : Type u) extends 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.

        • 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 : ααα

          The binary infimum, used to derive Min α

        • inf_le_left (a b : α) : inf a b a

          The infimum is a lower bound on the first argument

        • inf_le_right (a b : α) : inf a b b

          The infimum is a lower bound on the second argument

        • le_inf (a b c : α) : a ba ca inf b c

          The infimum is the greatest lower bound

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

          Alias of the forward direction of inf_eq_left.

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

          Alias of the reverse direction of inf_eq_left.

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

          Alias of the reverse direction of inf_eq_right.

          @[simp]
          theorem inf_lt_left {α : Type u} [SemilatticeInf α] {a b : α} :
          ab < a ¬a b
          @[simp]
          theorem inf_lt_right {α : Type u} [SemilatticeInf α] {a b : α} :
          ab < b ¬b a
          theorem inf_lt_left_or_right {α : Type u} [SemilatticeInf α] {a b : α} (h : a b) :
          ab < a ab < b
          theorem inf_le_inf {α : Type u} [SemilatticeInf α] {a b c d : α} (h₁ : a b) (h₂ : c d) :
          ac bd
          theorem inf_le_inf_right {α : Type u} [SemilatticeInf α] (a : α) {b c : α} (h : b c) :
          ba ca
          theorem inf_le_inf_left {α : Type u} [SemilatticeInf α] (a : α) {b c : α} (h : b c) :
          ab ac
          theorem inf_idem {α : Type u} [SemilatticeInf α] (a : α) :
          aa = a
          instance instIdempotentOpMin_mathlib {α : Type u} [SemilatticeInf α] :
          Std.IdempotentOp fun (x1 x2 : α) => x1x2
          theorem inf_comm {α : Type u} [SemilatticeInf α] (a b : α) :
          ab = ba
          instance instCommutativeMin_mathlib {α : Type u} [SemilatticeInf α] :
          Std.Commutative fun (x1 x2 : α) => x1x2
          theorem inf_assoc {α : Type u} [SemilatticeInf α] (a b c : α) :
          abc = a(bc)
          instance instAssociativeMin_mathlib {α : Type u} [SemilatticeInf α] :
          Std.Associative fun (x1 x2 : α) => x1x2
          theorem inf_left_right_swap {α : Type u} [SemilatticeInf α] (a b c : α) :
          abc = cba
          theorem inf_left_idem {α : Type u} [SemilatticeInf α] (a b : α) :
          a(ab) = ab
          theorem inf_right_idem {α : Type u} [SemilatticeInf α] (a b : α) :
          abb = ab
          theorem inf_left_comm {α : Type u} [SemilatticeInf α] (a b c : α) :
          a(bc) = b(ac)
          theorem inf_right_comm {α : Type u} [SemilatticeInf α] (a b c : α) :
          abc = acb
          theorem inf_inf_inf_comm {α : Type u} [SemilatticeInf α] (a b c d : α) :
          ab(cd) = ac(bd)
          theorem inf_inf_distrib_left {α : Type u} [SemilatticeInf α] (a b c : α) :
          a(bc) = ab(ac)
          theorem inf_inf_distrib_right {α : Type u} [SemilatticeInf α] (a b c : α) :
          abc = ac(bc)
          theorem inf_congr_left {α : Type u} [SemilatticeInf α] {a b c : α} (hb : ac b) (hc : ab c) :
          ab = ac
          theorem inf_congr_right {α : Type u} [SemilatticeInf α] {a b c : α} (h1 : bc a) (h2 : ac b) :
          ac = bc
          theorem inf_eq_inf_iff_left {α : Type u} [SemilatticeInf α] {a b c : α} :
          ab = ac ac b ab c
          theorem inf_eq_inf_iff_right {α : Type u} [SemilatticeInf α] {a b c : α} :
          ac = bc bc a ac b
          theorem Ne.inf_lt_or_inf_lt {α : Type u} [SemilatticeInf α] {a b : α} :
          a bab < a ab < b
          theorem SemilatticeInf.ext_inf {α : Type u_1} {A B : SemilatticeInf α} (H : ∀ (x y : α), x y x y) (x y : α) :
          xy = xy
          theorem SemilatticeInf.ext {α : Type u_1} {A B : SemilatticeInf α} (H : ∀ (x y : α), x y x y) :
          A = B
          theorem inf_le_ite {α : Type u} [SemilatticeInf α] (s s' : α) (P : Prop) [Decidable P] :
          ss' if P then s else s'
          def SemilatticeInf.mk' {α : Type u_1} [Min α] (inf_comm : ∀ (a b : α), ab = ba) (inf_assoc : ∀ (a b c : α), abc = a(bc)) (inf_idem : ∀ (a : α), aa = 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 α, SemilatticeInf α :

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

            Instances
              instance OrderDual.instLattice (α : Type u_1) [Lattice α] :
              Equations
              theorem semilatticeSup_mk'_partialOrder_eq_semilatticeInf_mk'_partialOrder {α : Type u_1} [Max α] [Min α] (sup_comm : ∀ (a b : α), ab = ba) (sup_assoc : ∀ (a b c : α), abc = a(bc)) (sup_idem : ∀ (a : α), aa = a) (inf_comm : ∀ (a b : α), ab = ba) (inf_assoc : ∀ (a b c : α), abc = a(bc)) (inf_idem : ∀ (a : α), aa = a) (sup_inf_self : ∀ (a b : α), aab = a) (inf_sup_self : ∀ (a b : α), a(ab) = a) :

              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} [Max α] [Min α] (sup_comm : ∀ (a b : α), ab = ba) (sup_assoc : ∀ (a b c : α), abc = a(bc)) (inf_comm : ∀ (a b : α), ab = ba) (inf_assoc : ∀ (a b c : α), abc = a(bc)) (sup_inf_self : ∀ (a b : α), aab = a) (inf_sup_self : ∀ (a b : α), a(ab) = 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 : α} :
                ab ab
                theorem sup_le_inf {α : Type u} [Lattice α] {a b : α} :
                ab ab a = b
                @[simp]
                theorem inf_eq_sup {α : Type u} [Lattice α] {a b : α} :
                ab = ab a = b
                @[simp]
                theorem sup_eq_inf {α : Type u} [Lattice α] {a b : α} :
                ab = ab a = b
                @[simp]
                theorem inf_lt_sup {α : Type u} [Lattice α] {a b : α} :
                ab < ab a b
                theorem inf_eq_and_sup_eq_iff {α : Type u} [Lattice α] {a b c : α} :
                ab = c ab = c a = c b = c

                Distributivity laws #

                theorem sup_inf_le {α : Type u} [Lattice α] {a b c : α} :
                abc (ab)(ac)
                theorem le_inf_sup {α : Type u} [Lattice α] {a b c : α} :
                abac a(bc)
                theorem inf_sup_self {α : Type u} [Lattice α] {a b : α} :
                a(ab) = a
                theorem sup_inf_self {α : Type u} [Lattice α] {a b : α} :
                aab = a
                theorem sup_eq_iff_inf_eq {α : Type u} [Lattice α] {a b : α} :
                ab = b ab = a
                theorem Lattice.ext {α : Type u_1} {A 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.

                Instances
                  theorem le_sup_inf {α : Type u} [DistribLattice α] {x y z : α} :
                  (xy)(xz) xyz
                  theorem sup_inf_left {α : Type u} [DistribLattice α] (a b c : α) :
                  abc = (ab)(ac)
                  theorem sup_inf_right {α : Type u} [DistribLattice α] (a b c : α) :
                  abc = (ac)(bc)
                  theorem inf_sup_left {α : Type u} [DistribLattice α] (a b c : α) :
                  a(bc) = abac
                  Equations
                  theorem inf_sup_right {α : Type u} [DistribLattice α] (a b c : α) :
                  (ab)c = acbc
                  theorem le_of_inf_le_sup_le {α : Type u} [DistribLattice α] {x y z : α} (h₁ : xz yz) (h₂ : xz yz) :
                  x y
                  theorem eq_of_inf_eq_sup_eq {α : Type u} [DistribLattice α] {a b c : α} (h₁ : ba = ca) (h₂ : ba = ca) :
                  b = c
                  @[reducible, inline]
                  abbrev DistribLattice.ofInfSupLe {α : Type u} [Lattice α] (inf_sup_le : ∀ (a b c : α), a(bc) abac) :

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

                  Equations
                  Instances For

                    Lattices derived from linear orders #

                    @[instance 100]
                    instance LinearOrder.toLattice {α : Type u} [LinearOrder α] :
                    Equations
                    • One or more equations did not get rendered due to their size.
                    @[deprecated "is syntactical" (since := "2024-11-13")]
                    theorem sup_eq_max {α : Type u} [LinearOrder α] {a b : α} :
                    max a b = max a b
                    @[deprecated "is syntactical" (since := "2024-11-13")]
                    theorem inf_eq_min {α : Type u} [LinearOrder α] {a b : α} :
                    min a b = min a b
                    theorem sup_ind {α : Type u} [LinearOrder α] (a b : α) {p : αProp} (ha : p a) (hb : p b) :
                    p (max a b)
                    @[simp]
                    theorem le_sup_iff {α : Type u} [LinearOrder α] {a b c : α} :
                    a max b c a b a c
                    @[simp]
                    theorem lt_sup_iff {α : Type u} [LinearOrder α] {a b c : α} :
                    a < max b c a < b a < c
                    @[simp]
                    theorem sup_lt_iff {α : Type u} [LinearOrder α] {a b c : α} :
                    max b c < a b < a c < a
                    theorem inf_ind {α : Type u} [LinearOrder α] (a b : α) {p : αProp} :
                    p ap bp (min a b)
                    @[simp]
                    theorem inf_le_iff {α : Type u} [LinearOrder α] {a b c : α} :
                    min b c a b a c a
                    @[simp]
                    theorem inf_lt_iff {α : Type u} [LinearOrder α] {a b c : α} :
                    min b c < a b < a c < a
                    @[simp]
                    theorem lt_inf_iff {α : Type u} [LinearOrder α] {a b c : α} :
                    a < min 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 α] [DecidableLE α] [IsTotal α fun (x1 x2 : α) => x1 x2] :
                    (fun (x1 x2 : α) => x1x2) = maxDefault
                    theorem inf_eq_minDefault {α : Type u} [SemilatticeInf α] [DecidableLE α] [IsTotal α fun (x1 x2 : α) => x1 x2] :
                    (fun (x1 x2 : α) => x1x2) = minDefault
                    @[reducible, inline]
                    abbrev Lattice.toLinearOrder (α : Type u) [Lattice α] [DecidableEq α] [DecidableLE α] [DecidableLT α] [IsTotal α fun (x1 x2 : α) => x1 x2] :

                    A lattice with total order is a linear order.

                    See note [reducible non-instances].

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[instance 100]
                      Equations

                      Dual order #

                      @[simp]
                      theorem ofDual_inf {α : Type u} [Max α] (a b : αᵒᵈ) :
                      @[simp]
                      theorem ofDual_sup {α : Type u} [Min α] (a b : αᵒᵈ) :
                      @[simp]
                      theorem toDual_inf {α : Type u} [Min α] (a b : α) :
                      @[simp]
                      theorem toDual_sup {α : Type u} [Max α] (a b : α) :
                      @[simp]
                      @[simp]
                      @[simp]
                      theorem toDual_min {α : Type u} [LinearOrder α] (a b : α) :
                      @[simp]
                      theorem toDual_max {α : Type u} [LinearOrder α] (a b : α) :

                      Function lattices #

                      instance Pi.instMaxForall_mathlib {ι : Type u_1} {α' : ιType u_2} [(i : ι) → Max (α' i)] :
                      Max ((i : ι) → α' i)
                      Equations
                      @[simp]
                      theorem Pi.sup_apply {ι : Type u_1} {α' : ιType u_2} [(i : ι) → Max (α' i)] (f g : (i : ι) → α' i) (i : ι) :
                      max f g i = f ig i
                      theorem Pi.sup_def {ι : Type u_1} {α' : ιType u_2} [(i : ι) → Max (α' i)] (f g : (i : ι) → α' i) :
                      fg = fun (i : ι) => f ig i
                      instance Pi.instMinForall_mathlib {ι : Type u_1} {α' : ιType u_2} [(i : ι) → Min (α' i)] :
                      Min ((i : ι) → α' i)
                      Equations
                      @[simp]
                      theorem Pi.inf_apply {ι : Type u_1} {α' : ιType u_2} [(i : ι) → Min (α' i)] (f g : (i : ι) → α' i) (i : ι) :
                      min f g i = f ig i
                      theorem Pi.inf_def {ι : Type u_1} {α' : ιType u_2} [(i : ι) → Min (α' i)] (f g : (i : ι) → α' i) :
                      fg = fun (i : ι) => f ig 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 b : π i) :
                      update f i (ab) = update f i aupdate f i b
                      theorem Function.update_inf {ι : Type u_1} {π : ιType u_2} [DecidableEq ι] [(i : ι) → SemilatticeInf (π i)] (f : (i : ι) → π i) (i : ι) (a b : π i) :
                      update f i (ab) = update f i aupdate f i b

                      Monotone functions and lattices #

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

                      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) :
                      Monotone (fg)

                      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 xf y f (xy)
                      theorem Monotone.map_inf_le {α : Type u} {β : Type v} [SemilatticeInf α] [SemilatticeInf β] {f : αβ} (h : Monotone f) (x y : α) :
                      f (xy) f xf y
                      theorem Monotone.of_map_inf_le_left {α : Type u} {β : Type v} [SemilatticeInf α] [Preorder β] {f : αβ} (h : ∀ (x y : α), f (xy) f x) :
                      theorem Monotone.of_map_inf_le {α : Type u} {β : Type v} [SemilatticeInf α] [SemilatticeInf β] {f : αβ} (h : ∀ (x y : α), f (xy) f xf y) :
                      theorem Monotone.of_map_inf {α : Type u} {β : Type v} [SemilatticeInf α] [SemilatticeInf β] {f : αβ} (h : ∀ (x y : α), f (xy) = f xf y) :
                      theorem Monotone.of_left_le_map_sup {α : Type u} {β : Type v} [SemilatticeSup α] [Preorder β] {f : αβ} (h : ∀ (x y : α), f x f (xy)) :
                      theorem Monotone.of_le_map_sup {α : Type u} {β : Type v} [SemilatticeSup α] [SemilatticeSup β] {f : αβ} (h : ∀ (x y : α), f xf y f (xy)) :
                      theorem Monotone.of_map_sup {α : Type u} {β : Type v} [SemilatticeSup α] [SemilatticeSup β] {f : αβ} (h : ∀ (x y : α), f (xy) = f xf y) :
                      theorem Monotone.map_sup {α : Type u} {β : Type v} [LinearOrder α] [SemilatticeSup β] {f : αβ} (hf : Monotone f) (x y : α) :
                      f (max x y) = f xf y
                      theorem Monotone.map_inf {α : Type u} {β : Type v} [LinearOrder α] [SemilatticeInf β] {f : αβ} (hf : Monotone f) (x y : α) :
                      f (min x y) = f xf y
                      theorem MonotoneOn.sup {α : Type u} {β : Type v} [Preorder α] [SemilatticeSup β] {f g : αβ} {s : Set α} (hf : MonotoneOn f s) (hg : MonotoneOn g s) :
                      MonotoneOn (fg) 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 (fg) 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 (xy) = f xf y) :
                      theorem MonotoneOn.of_map_sup {α : Type u} {β : Type v} {f : αβ} {s : Set α} [SemilatticeSup α] [SemilatticeSup β] (h : ∀ (x : α), x s∀ (y : α), y sf (xy) = f xf 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 (max x y) = f xf 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 (min x y) = f xf y
                      theorem Antitone.sup {α : Type u} {β : Type v} [Preorder α] [SemilatticeSup β] {f g : αβ} (hf : Antitone f) (hg : Antitone g) :
                      Antitone (fg)

                      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) :
                      Antitone (fg)

                      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 (xy) f xf y
                      theorem Antitone.le_map_inf {α : Type u} {β : Type v} [SemilatticeInf α] [SemilatticeSup β] {f : αβ} (h : Antitone f) (x y : α) :
                      f xf y f (xy)
                      theorem Antitone.map_sup {α : Type u} {β : Type v} [LinearOrder α] [SemilatticeInf β] {f : αβ} (hf : Antitone f) (x y : α) :
                      f (max x y) = f xf y
                      theorem Antitone.map_inf {α : Type u} {β : Type v} [LinearOrder α] [SemilatticeSup β] {f : αβ} (hf : Antitone f) (x y : α) :
                      f (min x y) = f xf y
                      theorem AntitoneOn.sup {α : Type u} {β : Type v} [Preorder α] [SemilatticeSup β] {f g : αβ} {s : Set α} (hf : AntitoneOn f s) (hg : AntitoneOn g s) :
                      AntitoneOn (fg) 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 (fg) 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 (xy) = f xf y) :
                      theorem AntitoneOn.of_map_sup {α : Type u} {β : Type v} {f : αβ} {s : Set α} [SemilatticeSup α] [SemilatticeInf β] (h : ∀ (x : α), x s∀ (y : α), y sf (xy) = f xf 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 (max x y) = f xf 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 (min x y) = f xf y

                      Products of (semi-)lattices #

                      instance Prod.instMax_mathlib (α : Type u) (β : Type v) [Max α] [Max β] :
                      Max (α × β)
                      Equations
                      instance Prod.instMin_mathlib (α : Type u) (β : Type v) [Min α] [Min β] :
                      Min (α × β)
                      Equations
                      @[simp]
                      theorem Prod.mk_sup_mk (α : Type u) (β : Type v) [Max α] [Max β] (a₁ a₂ : α) (b₁ b₂ : β) :
                      (a₁, b₁)(a₂, b₂) = (a₁a₂, b₁b₂)
                      @[simp]
                      theorem Prod.mk_inf_mk (α : Type u) (β : Type v) [Min α] [Min β] (a₁ a₂ : α) (b₁ b₂ : β) :
                      (a₁, b₁)(a₂, b₂) = (a₁a₂, b₁b₂)
                      @[simp]
                      theorem Prod.fst_sup (α : Type u) (β : Type v) [Max α] [Max β] (p q : α × β) :
                      (pq).fst = p.fstq.fst
                      @[simp]
                      theorem Prod.fst_inf (α : Type u) (β : Type v) [Min α] [Min β] (p q : α × β) :
                      (pq).fst = p.fstq.fst
                      @[simp]
                      theorem Prod.snd_sup (α : Type u) (β : Type v) [Max α] [Max β] (p q : α × β) :
                      (pq).snd = p.sndq.snd
                      @[simp]
                      theorem Prod.snd_inf (α : Type u) (β : Type v) [Min α] [Min β] (p q : α × β) :
                      (pq).snd = p.sndq.snd
                      @[simp]
                      theorem Prod.swap_sup (α : Type u) (β : Type v) [Max α] [Max β] (p q : α × β) :
                      (pq).swap = p.swapq.swap
                      @[simp]
                      theorem Prod.swap_inf (α : Type u) (β : Type v) [Min α] [Min β] (p q : α × β) :
                      (pq).swap = p.swapq.swap
                      theorem Prod.sup_def (α : Type u) (β : Type v) [Max α] [Max β] (p q : α × β) :
                      pq = (p.fstq.fst, p.sndq.snd)
                      theorem Prod.inf_def (α : Type u) (β : Type v) [Min α] [Min β] (p q : α × β) :
                      pq = (p.fstq.fst, p.sndq.snd)
                      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, inline]
                      abbrev Subtype.semilatticeSup {α : Type u} [SemilatticeSup α] {P : αProp} (Psup : ∀ ⦃x y : α⦄, P xP yP (xy)) :
                      SemilatticeSup { x : α // P x }

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

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[reducible, inline]
                        abbrev Subtype.semilatticeInf {α : Type u} [SemilatticeInf α] {P : αProp} (Pinf : ∀ ⦃x y : α⦄, P xP yP (xy)) :
                        SemilatticeInf { x : α // P x }

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

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[reducible, inline]
                          abbrev Subtype.lattice {α : Type u} [Lattice α] {P : αProp} (Psup : ∀ ⦃x y : α⦄, P xP yP (xy)) (Pinf : ∀ ⦃x y : α⦄, P xP yP (xy)) :
                          Lattice { x : α // P x }

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

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[simp]
                            theorem Subtype.coe_sup {α : Type u} [SemilatticeSup α] {P : αProp} (Psup : ∀ ⦃x y : α⦄, P xP yP (xy)) (x y : Subtype P) :
                            (xy) = xy
                            @[simp]
                            theorem Subtype.coe_inf {α : Type u} [SemilatticeInf α] {P : αProp} (Pinf : ∀ ⦃x y : α⦄, P xP yP (xy)) (x y : Subtype P) :
                            (xy) = xy
                            @[simp]
                            theorem Subtype.mk_sup_mk {α : Type u} [SemilatticeSup α] {P : αProp} (Psup : ∀ ⦃x y : α⦄, P xP yP (xy)) {x y : α} (hx : P x) (hy : P y) :
                            x, hxy, hy = xy,
                            @[simp]
                            theorem Subtype.mk_inf_mk {α : Type u} [SemilatticeInf α] {P : αProp} (Pinf : ∀ ⦃x y : α⦄, P xP yP (xy)) {x y : α} (hx : P x) (hy : P y) :
                            x, hxy, hy = xy,
                            @[reducible, inline]
                            abbrev Function.Injective.semilatticeSup {α : Type u} {β : Type v} [Max α] [SemilatticeSup β] (f : αβ) (hf_inj : Injective f) (map_sup : ∀ (a b : α), f (ab) = f af 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, inline]
                              abbrev Function.Injective.semilatticeInf {α : Type u} {β : Type v} [Min α] [SemilatticeInf β] (f : αβ) (hf_inj : Injective f) (map_inf : ∀ (a b : α), f (ab) = f af 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, inline]
                                abbrev Function.Injective.lattice {α : Type u} {β : Type v} [Max α] [Min α] [Lattice β] (f : αβ) (hf_inj : Injective f) (map_sup : ∀ (a b : α), f (ab) = f af b) (map_inf : ∀ (a b : α), f (ab) = f af 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, inline]
                                  abbrev Function.Injective.distribLattice {α : Type u} {β : Type v} [Max α] [Min α] [DistribLattice β] (f : αβ) (hf_inj : Injective f) (map_sup : ∀ (a b : α), f (ab) = f af b) (map_inf : ∀ (a b : α), f (ab) = f af 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