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
            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
                  @[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) :
                          (SemilatticeSup.mk' sup_comm sup_assoc sup_idem).toPartialOrder = (SemilatticeInf.mk' inf_comm inf_assoc inf_idem).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} [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
                            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
                                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
                                      @[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
                                        Instances For
                                          @[instance 100]
                                          Equations
                                            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
                                                                        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
                                                                            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
                                                                                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
                                                                                            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
                                                                                                  instance ULift.instLattice {α : Type u} [Lattice α] :
                                                                                                  Equations