LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Order.Lattice

`lt_sup_iff` theorem lt_sup_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, a < b ⊔ c ↔ a < b ∨ a < c This theorem states that for any given type `α` that has a linear ordering, and for any three elements `a`, `b`, and `c` of this type, `a` is less than the supremum (or maximum) of `b` and `c` if and only if `a` is less than `b` or `a` is less than `c`. The theorem is phrased in the form of an "if and only if" statement, expressing a bi-directional implication. More concisely: For any linear order type `α`, and elements `a`, `b`, `c` of `α`, `a` is less than the maximum of `b` and `c` if and only if `a` is less than both `b` and `c`.
`inf_le_inf_right` theorem inf_le_inf_right : ∀ {α : Type u} [inst : SemilatticeInf α] (a : α) {b c : α}, b ≤ c → b ⊓ a ≤ c ⊓ a This theorem states that for any type `α` that is a semilattice under the infimum operation (semilattice inf), given any three elements `a`, `b`, `c` of type `α`, if `b` is less than or equal to `c`, then the infimum of `b` and `a` is less than or equal to the infimum of `c` and `a`. This asserts a property of the infimum operation: where the position of a smaller element does not change the outcome when taking the infimum with a fixed other element. More concisely: For any semilattice `α` and elements `a, b, c` in `α` with `b ≤ c`, the infimum of `b` and `a` is less than or equal to the infimum of `c` and `a`.
`sup_sup_distrib_right` theorem sup_sup_distrib_right : ∀ {α : Type u} [inst : SemilatticeSup α] (a b c : α), a ⊔ b ⊔ c = a ⊔ c ⊔ (b ⊔ c) := by sorry This theorem states that for any type `α` that forms a semilattice with a supremum operation (denoted by `⊔`), and for any three elements `a`, `b`, and `c` of this type, the supremum of `a`, `b` and `c` distributed in the order `(a ⊔ b) ⊔ c` is equal to the supremum distributed in the order `a ⊔ (c ⊔ (b ⊔ c))`. In terms of set theory, this is akin to stating that the union of three sets distributed in two different ways gives the same result. More concisely: For any semilattice `α` with supremum operation `⊔`, the distributivity holds: `(a ⊔ b) ⊔ c = a ⊔ (c ⊔ b)` for all `a, b, c ∈ α`.
`Monotone.map_inf` theorem Monotone.map_inf : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : SemilatticeInf β] {f : α → β}, Monotone f → ∀ (x y : α), f (x ⊓ y) = f x ⊓ f y The theorem `Monotone.map_inf` asserts that for any types `α` and `β` equipped with a linear order and a semilattice structure respectively, and any function `f` from `α` to `β`, if `f` is monotone, then for any elements `x` and `y` in `α`, the infimum (or greatest lower bound) of `f(x)` and `f(y)` in `β` is equal to `f` of the infimum of `x` and `y` in `α`. In other words, a monotone function preserves the operation of taking infimums. More concisely: For any monotone function between linearly ordered semilattices, the image of the infimum of two elements is equal to the infimum of their images.
`AntitoneOn.min` theorem AntitoneOn.min : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : LinearOrder β] {f g : α → β} {s : Set α}, AntitoneOn f s → AntitoneOn g s → AntitoneOn (fun x => min (f x) (g x)) s The theorem `AntitoneOn.min` states that given two functions `f` and `g` from a type `α` to a type `β`, where `α` has a preorder structure and `β` has a linear order structure, and a set `s` of type `α`, if both `f` and `g` are antitone on `s` (meaning for any two elements `a` and `b` in `s`, if `a ≤ b` then `f b ≤ f a` and `g b ≤ g a`), then the function that maps each element `x` of `s` to the minimum of `f(x)` and `g(x)` is also antitone on `s`. In other words, taking the pointwise minimum of two antitone functions results in another antitone function. More concisely: If `f` and `g` are antitone functions from a preordered set `α` to an ordered set `β` with the property that `f(x) ≤ g(x)` for all `x` in a set `s`, then the function `x ↦ min (f x) (g x)` is also antitone on `s`.
`MonotoneOn.inf` theorem MonotoneOn.inf : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : SemilatticeInf β] {f g : α → β} {s : Set α}, MonotoneOn f s → MonotoneOn g s → MonotoneOn (f ⊓ g) s The theorem `MonotoneOn.inf` states that, for any set `s` of elements of some pre-ordered type `α`, if two functions `f` and `g` from `α` to a type `β` that forms a semilattice under an infimum operation are monotone on `s`, then their pointwise infimum (i.e., the function which at each point of `s` takes the infimum of the values of `f` and `g`) is also monotone on `s`. This means that for all `a, b ∈ s`, if `a ≤ b` then the infimum of `f(a)` and `g(a)` is less than or equal to the infimum of `f(b)` and `g(b)`. More concisely: If `f` and `g` are monotone functions from a pre-ordered set `s` to a semilattice with an infimum operation, then the pointwise infimum of `f` and `g` is also a monotone function on `s`.
`SemilatticeSup.le_sup_left` theorem SemilatticeSup.le_sup_left : ∀ {α : Type u} [self : SemilatticeSup α] (a b : α), a ≤ a ⊔ b This theorem states that, given any type `α` that has a supremum (`SemilatticeSup`), and any two elements `a` and `b` of this type, `a` is always less than or equal to the supremum of `a` and `b`. In other words, the supremum operation `⊔` produces a result that is an upper bound for its inputs, at least for its first input. This is a general property of semilattices and forms part of the definition of the supremum operation. More concisely: For any semilattice `α` and elements `a, b` in `α` with supremum `⊔`, we have `a ≤ ⊔(a, b)`.
`Monotone.of_map_inf` theorem Monotone.of_map_inf : ∀ {α : Type u} {β : Type v} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β] {f : α → β}, (∀ (x y : α), f (x ⊓ y) = f x ⊓ f y) → Monotone f The theorem `Monotone.of_map_inf` states that for any two types `α` and `β` with a semilattice structure (i.e., a structure with a binary operation that is associative, commutative, idempotent and has an order relation compatible with the operation), if a function `f` from `α` to `β` preserves the infimum operation (that is, applying `f` to the infimum of `x` and `y` is the same as taking the infimum of `f x` and `f y`), then `f` is a monotone function. In other words, if `a ≤ b` then `f a ≤ f b`. More concisely: If `f` is a function between semilattices that preserves the infimum operation, then `f` is monotone.
`inf_le_right` theorem inf_le_right : ∀ {α : Type u} [inst : SemilatticeInf α] {a b : α}, a ⊓ b ≤ b This theorem states that for any type `α` which forms a `SemilatticeInf` (i.e., a mathematical structure with a binary operation called `inf` that is associative, commutative, and idempotent), and for any two elements `a` and `b` of this type, the infimum (greatest lower bound) of `a` and `b` is less than or equal to `b`. This captures one of the fundamental properties of the infimum operation in a semilattice. More concisely: For any semilattice `α` and elements `a, b` in `α`, we have `a <= b` when `a` is the infimum of `a` and `b`.
`inf_le_left` theorem inf_le_left : ∀ {α : Type u} [inst : SemilatticeInf α] {a b : α}, a ⊓ b ≤ a This theorem states that for any type `α` which forms a semilattice with respect to an infimum operation `⊓`, the infimum of any two elements `a` and `b` of `α` is less than or equal to `a`. In terms of set theory, this means that the greatest lower bound of `a` and `b` is always less than or equal to `a`. More concisely: For any semilattice `α` with infimum operation `⊓`, for all `a, b ∈ α`, we have `a ⊓ b ≤ a`.
`sup_lt_iff` theorem sup_lt_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, b ⊔ c < a ↔ b < a ∧ c < a This theorem states that for any type `α` that has a linear order, and for any three elements `a`, `b`, and `c` of this type, the supremum (`b ⊔ c`, also known as the maximum or "max") of `b` and `c` is less than `a` if and only if both `b` and `c` are less than `a`. In mathematical terms, we have `max(b, c) < a` if and only if `b < a` and `c < a`. More concisely: For any type with a linear order, the maximum of two elements is strictly less than a third element if and only if both are strictly less than that element.
`MonotoneOn.sup` theorem MonotoneOn.sup : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : SemilatticeSup β] {f g : α → β} {s : Set α}, MonotoneOn f s → MonotoneOn g s → MonotoneOn (f ⊔ g) s The theorem `MonotoneOn.sup` states that for any set `s` of a certain type `α`, and for any two functions `f` and `g` from `α` to another type `β` (where `α` has a preorder structure and `β` has a semilattice sup structure), if both functions `f` and `g` are monotone on `s`, then the pointwise supremum function `(f ⊔ g)`, which is defined for each element in the set `s` as the maximum of the values of `f` and `g` at that element, is also monotone on `s`. This means that for any two elements `a` and `b` in the set `s`, if `a ≤ b`, then the maximum of `f(a)` and `g(a)` is less than or equal to the maximum of `f(b)` and `g(b)`. More concisely: If `f` and `g` are two monotone functions from a preordered set `α` to a semilattice `β`, then their pointwise supremum `f ⊔ g` is also a monotone function on `α`.
`Mathlib.Order.Lattice._auxLemma.11` theorem Mathlib.Order.Lattice._auxLemma.11 : ∀ {α : Type u} [inst : SemilatticeInf α] {a b : α}, (a ⊓ b ≤ a) = True This theorem, named `Mathlib.Order.Lattice._auxLemma.11`, asserts that for any type `α` with a structure of a semilattice under the infimum operation (`SemilatticeInf α`), for any two elements `a` and `b` of this type, the infimum of `a` and `b` is always less than or equal to `a`. This is a basic property of infimums (also known as "greatest lower bounds") in order theory and is always true, hence the result is `True`. In mathematical language, this can be written as $a \land b \leq a$. More concisely: For any semilattice `α` and elements `a, b` in `α`, the infimum of `a` and `b` is less than or equal to `a`. In mathematical notation: `∧-elim ∧⁡(SemilatticeInf α a b) a`.
`MonotoneOn.max` theorem MonotoneOn.max : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : LinearOrder β] {f g : α → β} {s : Set α}, MonotoneOn f s → MonotoneOn g s → MonotoneOn (fun x => max (f x) (g x)) s The theorem `MonotoneOn.max` states that for any given type `α` with a preorder relation, and any given type `β` with a linear order, if `f` and `g` are both monotone functions on a set `s` of `α`, then the function that takes an element `x` in `α` and returns the maximum of `f(x)` and `g(x)` is also a monotone function on `s`. In other words, if `f` and `g` are both monotone on `s`, then so is the pointwise maximum of `f` and `g`. More concisely: If `f` and `g` are monotone functions on a set `s` with respect to a preorder relation, then the function `x ↦ max (f x) (g x)` is also monotone on `s`.
`inf_le_of_right_le` theorem inf_le_of_right_le : ∀ {α : Type u} [inst : SemilatticeInf α] {a b c : α}, b ≤ c → a ⊓ b ≤ c This theorem states that for any type `α` that forms a semilattice with an infimum (or greatest lower bound), given three elements `a`, `b`, and `c` of this type, if `b` is less than or equal to `c`, then the infimum of `a` and `b` is also less than or equal to `c`. In mathematical terms, if `b ≤ c`, then `a ⊓ b ≤ c` where `⊓` represents the infimum operation. More concisely: For any semilattice `α` with an infimum, if `b` is less than or equal to `c` in `α`, then the infimum of `a` and `b` is less than or equal to `c`: `a ⊓ b ≤ c`.
`sup_le_sup_right` theorem sup_le_sup_right : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, a ≤ b → ∀ (c : α), a ⊔ c ≤ b ⊔ c := by sorry The theorem `sup_le_sup_right` states that for all types `α` that form a semilattice with a supremum (the least upper bound), given any three elements `a`, `b`, and `c` of type `α`, if `a` is less than or equal to `b`, then the supremum of `a` and `c` is less than or equal to the supremum of `b` and `c`. This essentially indicates that the supremum operation in a semilattice respects the order of the elements involved. More concisely: For all types `α` with a supremum and any elements `a`, `b`, `c` of type `α`, if `a ≤ b`, then `sup(a, c) ≤ sup(b, c)`.
`inf_inf_distrib_left` theorem inf_inf_distrib_left : ∀ {α : Type u} [inst : SemilatticeInf α] (a b c : α), a ⊓ (b ⊓ c) = a ⊓ b ⊓ (a ⊓ c) := by sorry This theorem states that for any type `α` that forms a semilattice under an infimum operation (`⊓`), the operation distributes over itself when it's applied from the left. In other words, for any three elements `a`, `b`, and `c` of `α`, the infimum of `a` and the infimum of `b` and `c` (`a ⊓ (b ⊓ c)`) equals the infimum of `a` and `b`, and the infimum of `a` and `c` (`a ⊓ b ⊓ (a ⊓ c)`). This is a property of the infimum operation in a semilattice. More concisely: In a semilattice, the infimum of any two elements is commutative and associative with respect to infimum. That is, for all elements `a, b, c`, `(a ⊓ b) = (b ⊓ a)` and `(a ⊓ b) ⊓ (a ⊓ c) = a ⊓ (b ⊓ c)`.
`sup_ind` theorem sup_ind : ∀ {α : Type u} [inst : LinearOrder α] (a b : α) {p : α → Prop}, p a → p b → p (a ⊔ b) This theorem states that for any type `α` that has a linear order and any two elements `a` and `b` of that type, if a property `p` holds true for both `a` and `b`, then it also holds true for the supremum of `a` and `b`. Here, the supremum (denoted by `a ⊔ b`) is the least upper bound of `a` and `b`, or in other words, the smallest element that is greater than or equal to both `a` and `b` in the linear order. More concisely: If `α` is a type with a linear order and `a`, `b` are elements of `α` such that `p` holds for `a` and `b`, then `p` holds for their supremum `a ⊔ b`.
`inf_le_inf` theorem inf_le_inf : ∀ {α : Type u} [inst : SemilatticeInf α] {a b c d : α}, a ≤ b → c ≤ d → a ⊓ c ≤ b ⊓ d This theorem, `inf_le_inf`, asserts that for any type `α` that forms a semilattice under an infimum operation (denoted by `⊓`), given four elements `a`, `b`, `c`, and `d` of this type, if `a` is less than or equal to `b` and `c` is less than or equal to `d`, then the infimum of `a` and `c` is less than or equal to the infimum of `b` and `d`. In other words, if two elements are each less than or equal to another pair of elements, then their infimum (greatest lower bound) will also be less than or equal to the infimum of the larger elements. More concisely: For any semilattice `α` with infimum operation `⊓`, if `a ≤ b` and `c ≤ d` in `α`, then `a \/$ c ≤ b \/$ d`. (Here, `\/` denotes the infimum operator.)
`left_lt_sup` theorem left_lt_sup : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, a < a ⊔ b ↔ ¬b ≤ a This theorem, `left_lt_sup`, states that for any type `α` that forms a semilattice with a supremum operation, and any two elements `a` and `b` of this type, `a` is less than the supremum of `a` and `b` if and only if `b` is not less than or equal to `a`. Here, the symbol "⊔" represents the supremum or least upper bound operation in the semilattice. More concisely: For any semilattice with supremum operation ⊔, element a, and element b, the condition a < ⊔(a, b) if and only if b ≥ a holds.
`Mathlib.Order.Lattice._auxLemma.5` theorem Mathlib.Order.Lattice._auxLemma.5 : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, (a ⊔ b = a) = (b ≤ a) This theorem, `Mathlib.Order.Lattice._auxLemma.5`, states that for any type `α` that is a semilattice with respect to an operation "sup" (denoted as `⊔`), and for any two elements `a` and `b` of this type, `a ⊔ b` being equal to `a` is equivalent to `b` being less than or equal to `a`. In other words, using the semilattice's sup operation, if the sup of `a` and `b` is equal to `a`, then `b` must be less than or equal to `a`. More concisely: For any semilattice `α` with operation `⊔`, if `a ⊔ b = a`, then `b ≤ a`.
`Antitone.max` theorem Antitone.max : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : LinearOrder β] {f g : α → β}, Antitone f → Antitone g → Antitone fun x => max (f x) (g x) The theorem `Antitone.max` states that given two types `α` and `β` where `α` has a preorder structure and `β` has a linear order structure, for any two functions `f` and `g` from `α` to `β` that are antitone, meaning that an increase in `α` causes a decrease in `β` (i.e., if `a ≤ b` then `f b ≤ f a`), the function that assigns to each `x` in `α` the maximum of `f(x)` and `g(x)` is also antitone. This illustrates the property that the pointwise maximum of two antitone functions is also an antitone function. More concisely: If `f` and `g` are antitone functions from a preordered type `α` to a linearly ordered type `β`, then the pointwise maximum of `f` and `g` is an antitone function from `α` to `β`.
`inf_of_le_right` theorem inf_of_le_right : ∀ {α : Type u} [inst : SemilatticeInf α] {a b : α}, b ≤ a → a ⊓ b = b This theorem, Alias of the reverse direction of `inf_eq_right`, states that for any type `α` equipped with a semilattice structure (denoted as `SemilatticeInf α`), for any two elements `a` and `b` of this type, if `b` is less than or equal to `a` (`b ≤ a`), then the infimum (greatest lower bound) of `a` and `b` is `b` (expressed as `a ⊓ b = b`). More concisely: For any semilattice `α`, if `b` is a lower bound of `a` and `b` is in `α`, then `a ⊓ b = b`.
`Mathlib.Order.Lattice._auxLemma.2` theorem Mathlib.Order.Lattice._auxLemma.2 : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, (b ≤ a ⊔ b) = True := by sorry This theorem, `Mathlib.Order.Lattice._auxLemma.2`, states that for any type `α` that forms a semilattice under the supremum operation, and any two elements `a` and `b` from this type `α`, `b` is always less than or equal to the supremum of `a` and `b`. In terms of mathematical notation, it asserts that $\forall a, b \in \alpha : b \leq a \vee b$ is always true in a semilattice. More concisely: In any semilattice, for all elements `a` and `b`, `b` is less than or equal to the supremum of `a` and `b`. In mathematical notation, $\forall a, b : a \sqcup b \geq b$, where $\sqcup$ denotes the supremum operation.
`inf_idem` theorem inf_idem : ∀ {α : Type u} [inst : SemilatticeInf α] (a : α), a ⊓ a = a This theorem, `inf_idem`, states that for any type `α` which is a semilattice with respect to the infimum operation (denoted by `⊓`), the infimum of any element `a` with itself is equal to `a`. In other words, in any such semilattice, taking the infimum of an element with itself doesn't change the element. More concisely: For any semilattice `α` with respect to the infimum operation, `⊓`, the infimum of any element `a` with itself equals `a`: `∀ α : Type, is_semilattice α → a ⊓ a = a`.
`inf_of_le_left` theorem inf_of_le_left : ∀ {α : Type u} [inst : SemilatticeInf α] {a b : α}, a ≤ b → a ⊓ b = a This theorem, `inf_of_le_left`, is an alias of the reverse direction of the theorem `inf_eq_left`. The theorem states that for any type `α` that has an instance of the `SemilatticeInf` structure, given any two elements `a` and `b` of type `α`, if `a` is less than or equal to `b` then the infimum (i.e. greatest lower bound) of `a` and `b` is `a`. More concisely: For any semilattice `α` and elements `a, b ∈ α` with `a ≤ b`, the infimum of `a` and `b` is `a`.
`sup_of_le_right` theorem sup_of_le_right : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, a ≤ b → a ⊔ b = b This theorem, `sup_of_le_right`, states that for any type `α` that has a semilattice structure, given any two elements `a` and `b` of this type, if `a` is less than or equal to `b`, then the supremum (or least upper bound) of `a` and `b` is `b`. It is an alias of the reverse direction of `sup_eq_right`. More concisely: If `α` is a semilattice type and `a ≤ b` in `α`, then `sup a b = b`.
`sup_eq_left` theorem sup_eq_left : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, a ⊔ b = a ↔ b ≤ a This theorem states that for any type `α` that is a semilattice with supremum (`SemilatticeSup`), and for any two elements `a` and `b` of type `α`, the supremum of `a` and `b` is equal to `a` if and only if `b` is less than or equal to `a`. In other words, in a semilattice structure, the least upper bound or "sup" (`⊔`) of `a` and `b` being `a` implies that `a` is greater or equal to `b`. More concisely: In a semilattice with supremum, the supremum of `a` and `b` equals `a` if and only if `b` is less than or equal to `a`.
`inf_sup_left` theorem inf_sup_left : ∀ {α : Type u} [inst : DistribLattice α] (a b c : α), a ⊓ (b ⊔ c) = a ⊓ b ⊔ a ⊓ c This theorem, `inf_sup_left`, states that for any distributive lattice of type `α`, the supremum (join operation) of two elements `b` and `c`, when infimum (meet operation) with another element `a`, distributes over the infimum operation. In other words, `a` meet (`b` join `c`) is equal to (`a` meet `b`) join (`a` meet `c`). This is a property of lattice theory in mathematics, symbolically represented as `a ⊓ (b ⊔ c) = a ⊓ b ⊔ a ⊓ c`. More concisely: In a distributive lattice, the meet of an element with the join of two other elements is equal to the meet of each element with the join of those two elements. (a ⊓ (b ⊔ c) = a ⊓ b ⊔ a ⊓ c)
`inf_eq_min` theorem inf_eq_min : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, a ⊓ b = min a b This theorem, `inf_eq_min`, states that for any type `α` which forms a linear order `inst`, the infimum (greatest lower bound) of any two elements `a` and `b` of type `α` is equal to the minimum of `a` and `b`. This essentially says that within a linear order, the concept of the infimum and the minimum of two elements coincide. More concisely: For any linear ordered type `α`, the infimum of `a` and `b` equals the minimum of `a` and `b`.
`inf_le_of_left_le` theorem inf_le_of_left_le : ∀ {α : Type u} [inst : SemilatticeInf α] {a b c : α}, a ≤ c → a ⊓ b ≤ c This theorem states that for any type `α` that has an instance of a semilattice with an infimum operation (denoted by `⊓`), given any three elements `a`, `b`, and `c` of type `α`, if `a` is less than or equal to `c`, then the infimum (`⊓`) of `a` and `b` is also less than or equal to `c`. This is a property of semilattices where the infimum of any two elements is less than or equal to any element greater than or equal to both of them. More concisely: If `α` is a semilattice with an infimum operation `⊓`, then for all `a`, `b`, and `c` in `α` with `a ≤ c`, it follows that `a ⊓ b ≤ c`.
`sup_assoc` theorem sup_assoc : ∀ {α : Type u} [inst : SemilatticeSup α] (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c) This theorem, named `sup_assoc`, states that for all types `α` that form a semilattice under a supremum (`⊔`) operation, the supremum of three elements `a`, `b`, and `c` is associative. In other words, the supremum of `a`, `b`, and `c` is the same whether you first take the supremum of `a` and `b` and then take the supremum with `c`, or first take the supremum of `b` and `c` and then take the supremum with `a`. In mathematical terms, it's stating that `a ⊔ b ⊔ c = a ⊔ (b ⊔ c)`. More concisely: For all types `α` with a semilattice structure under the `⊔` operation, the associativity of the supremum holds: `a ⊔ (b ⊔ c) = (a ⊔ b) ⊔ c`.
`Mathlib.Order.Lattice._auxLemma.12` theorem Mathlib.Order.Lattice._auxLemma.12 : ∀ {α : Type u} [inst : SemilatticeInf α] {a b : α}, (a ⊓ b ≤ b) = True This theorem, `Mathlib.Order.Lattice._auxLemma.12`, states that for any type `α` that is a semilattice under infimum (denoted `⊓`), and for any two elements `a` and `b` of that type, the infimum of `a` and `b` is always less than or equal to `b`. In mathematical terms, it means that for any semilattice $(α, ⊓)$, for any $a, b ∈ α$, we have $a ⊓ b ≤ b$. This is a basic property of lattices, reflecting that the infimum of two elements is a lower bound of those elements. More concisely: For any semilattice `α` and elements `a, b ∈ α`, the infimum `a ⊓ b` is less than or equal to `b`.
`le_inf_iff` theorem le_inf_iff : ∀ {α : Type u} [inst : SemilatticeInf α] {a b c : α}, a ≤ b ⊓ c ↔ a ≤ b ∧ a ≤ c This theorem, `le_inf_iff`, states that for any type `α` that forms a semilattice with an infimum operation, given any three elements `a`, `b`, and `c` of type `α`, `a` is less than or equal to the infimum of `b` and `c` if and only if `a` is less than or equal to `b` and `a` is less than or equal to `c`. More concisely: For any semilattice type `α` with infimum operation, `a ≤ inf(b, c)` if and only if `a ≤ b` and `a ≤ c`.
`inf_assoc` theorem inf_assoc : ∀ {α : Type u} [inst : SemilatticeInf α] (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c) This theorem, `inf_assoc`, states that for any type `α` that is a semilattice under the infimum operation (denoted as `⊓`), the operation is associative. In other words, for any three elements `a`, `b`, and `c` of this type, the infimum of `a` and the infimum of `b` and `c` equals the infimum of `a` and `b` and `c`. This is the same as saying, in the context of set theory, that intersection of three sets (i.e., `a`, `b`, `c`) is associative: `(a ∩ b) ∩ c = a ∩ (b ∩ c)`. More concisely: For any semilattice `α` with respect to infimum (⊓), the infimum is associative: `a ⊓ (b ⊓ c) = (a ⊓ b) ⊓ c`.
`sup_comm` theorem sup_comm : ∀ {α : Type u} [inst : SemilatticeSup α] (a b : α), a ⊔ b = b ⊔ a This theorem, named `sup_comm`, states that for any type `α` that forms a semilattice with a supremum operation (denoted by `⊔`), the supremum of any two elements `a` and `b` of this type is commutative. In other words, the supremum of `a` and `b` is the same as the supremum of `b` and `a`. This is a fundamental property of semilattices and is equivalent to stating that the order of the elements does not matter when finding their supremum. More concisely: For any semilattice `α` with supremum operation `⊔`, the supremum of `a` and `b` equals the supremum of `b` and `a`: `a ⊔ b = b ⊔ a`.
`Monotone.forall_le_of_antitone` theorem Monotone.forall_le_of_antitone : ∀ {α : Type u} [inst : SemilatticeSup α] {β : Type u_1} [inst_1 : Preorder β] {f g : α → β}, Monotone f → Antitone g → f ≤ g → ∀ (m n : α), f m ≤ g n The theorem states that if we have two functions, `f` and `g`, operating within preordered sets (sets with an order relation that is reflexive and transitive), then if `f` is a monotone function (meaning that an increase in the input never decreases the output, formally `a ≤ b` implies `f a ≤ f b`) and `g` is an antitone function (meaning that an increase in the input always decreases the output, formally `a ≤ b` implies `f b ≤ f a`), and overall `f` is less than or equal to `g`, then for any two elements `m` and `n` in the domain, the value of `f` at `m` is always less than or equal to the value of `g` at `n`. This theorem is a statement about the interplay between monotone and antitone functions in ordered sets. More concisely: If `f` is a monotone function and `g` is an antitone function in a preorder with `f ≤ g`, then for all `m` and `n`, `f m ≤ g n`.
`MonotoneOn.min` theorem MonotoneOn.min : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : LinearOrder β] {f g : α → β} {s : Set α}, MonotoneOn f s → MonotoneOn g s → MonotoneOn (fun x => min (f x) (g x)) s The theorem `MonotoneOn.min` states that for any two functions `f` and `g` from a type `α` to a type `β`, where `α` has a preorder and `β` has a linear order, if both functions are monotone on a set `s` of type `α`, then the function that maps each element `x` of `s` to the minimum of `f(x)` and `g(x)` is also monotone on `s`. In other words, the pointwise minimum of two monotone functions is a monotone function. More concisely: If `f` and `g` are monotone functions from a preordered type `α` to an ordered type `β`, then the pointwise minimum `x ↦ min (f x) (g x)` is also a monotone function from `α` to `β`.
`le_of_sup_eq` theorem le_of_sup_eq : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, a ⊔ b = b → a ≤ b This theorem, `le_of_sup_eq`, states that for any type `α` which has a 'semilattice with supremum' structure, given any two elements `a` and `b` of `α`, if the supremum (denoted as `a ⊔ b`) of `a` and `b` equals `b`, then `a` is less than or equal to `b`. This theorem is an alias for the forward direction of another theorem called `sup_eq_right`. More concisely: If `α` is a semilattice with supremum, and `a ⊔ b = b`, then `a ≤ b`.
`AntitoneOn.inf` theorem AntitoneOn.inf : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : SemilatticeInf β] {f g : α → β} {s : Set α}, AntitoneOn f s → AntitoneOn g s → AntitoneOn (f ⊓ g) s The theorem `AntitoneOn.inf` asserts that for every pair of functions `f` and `g` from a type `α` to a type `β`, and a set `s` of type `α`, if both `f` and `g` are antitone (i.e., they preserve the opposite of the order) on `s`, then their pointwise infimum (which is a new function that at each point takes the minimum of the results of `f` and `g`) is also antitone on `s`. In other words, if `f` and `g` are both decreasing on `s`, then the function that at each point takes the smaller of `f(x)` and `g(x)` is also decreasing on `s`. This statement assumes that `α` is preordered and `β` is a semilattice with respect to the infimum operation. More concisely: If `f` and `g` are antitone functions from a preordered type `α` to a semilattice `β`, then their pointwise infimum is also an antitone function on `α`.
`Lattice.le_inf` theorem Lattice.le_inf : ∀ {α : Type u} [self : Lattice α] (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c This theorem states that in a lattice structure, the infimum is the greatest lower bound. Specifically, for any given type `α` that has a lattice structure and for any three elements `a`, `b`, and `c` of this type, if `a` is less than or equal to `b` and `a` is less than or equal to `c`, then `a` is less than or equal to the infimum of `b` and `c`. The infimum here is represented by the operator `⊓`, and it is essentially the greatest value that is less than or equal to both `b` and `c`. More concisely: In a lattice, the infimum (least upper bound) is the greatest lower bound, that is, for all elements a, b, and c in the lattice, if a is less than or equal to both b and c, then a is less than or equal to the infimum of b and c (denoted as b ⊓ c).
`ite_le_sup` theorem ite_le_sup : ∀ {α : Type u} [inst : SemilatticeSup α] (s s' : α) (P : Prop) [inst_1 : Decidable P], (if P then s else s') ≤ s ⊔ s' This theorem, `ite_le_sup`, states that for any type `α` that forms a semilattice under a sup operation (denoted by `⊔`), for any propositions `s` and `s'` of type `α`, and for any proposition `P` that is decidable, the result of the `if-then-else` expression (i.e., `s` if `P` is true, `s'` otherwise) is less than or equal to the sup of `s` and `s'`. In other words, in a semilattice, the value of an `if-then-else` expression involving two elements of the semilattice is always less than or equal to the supremum (least upper bound) of those two elements. More concisely: For any semilattice `α` with sup operation `⊔`, and propositions `s`, `s' : α` and decidable `P : Prop`, if `s ≤ s' ∨ P` then `(ite P s s') ≤ s ⊔ s'`.
`Mathlib.Order.Lattice._auxLemma.6` theorem Mathlib.Order.Lattice._auxLemma.6 : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, (a ⊔ b = b) = (a ≤ b) This theorem, `Mathlib.Order.Lattice._auxLemma.6`, is a statement about semilattice structures in order theory. Specifically, it says that for any type `α` that has a semilattice structure (denoted by `SemilatticeSup α`), for any two elements `a` and `b` of `α`, the supremum (join or least upper bound) of `a` and `b` being equal to `b` is equivalent to `a` being less than or equal to `b`. In mathematical terms, this is saying that $a \vee b = b \iff a \leq b$ where $\vee$ represents the supremum operation. More concisely: For any semilattice `α`, `a ≤ b` if and only if `a ⨝ b = b`, where `⨝` denotes the supremum (join) operation.
`Monotone.min` theorem Monotone.min : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : LinearOrder β] {f g : α → β}, Monotone f → Monotone g → Monotone fun x => min (f x) (g x) The theorem `Monotone.min` states that given any two monotone functions `f` and `g` from a preordered set `α` to a linearly ordered set `β`, the pointwise minimum of `f` and `g`, defined as a function that takes any element `x` of `α` to the minimum of `f(x)` and `g(x)`, is also a monotone function. Here, a function is said to be monotone if for all pairs of elements `a` and `b` in its domain, `a ≤ b` implies `f(a) ≤ f(b)`. More concisely: If `f` and `g` are monotone functions from a preordered set `α` to a linearly ordered set `β`, then the pointwise minimum `x ↦ min (f x) (g x)` is also a monotone function.
`Lattice.inf_le_left` theorem Lattice.inf_le_left : ∀ {α : Type u} [self : Lattice α] (a b : α), a ⊓ b ≤ a This theorem states that for any lattice structure, the infimum (or greatest lower bound) of any two elements `a` and `b` is less than or equal to `a`. In other words, when you take the infimum of `a` and `b` in any given lattice structure, the result will always be a value that is less than or equal to `a`. More concisely: In any lattice, the infimum of elements `a` and `b` is a lower bound for `a`, i.e., `inf {a, b} ≤ a`.
`Lattice.inf_le_right` theorem Lattice.inf_le_right : ∀ {α : Type u} [self : Lattice α] (a b : α), a ⊓ b ≤ b This theorem, `Lattice.inf_le_right`, states that for any type `α` equipped with a lattice structure and for all elements `a` and `b` of `α`, the infimum (greatest lower bound) of `a` and `b`, denoted `a ⊓ b`, is less than or equal to `b`. In other words, `b` is an upper bound for the set `{a, b}` in the lattice `α`. More concisely: For all types `α` with lattice structure and all elements `a, b` in `α`, the infimum `a ⊓ b` satisfies `a ⊓ b ≤ b`.
`sup_le_iff` theorem sup_le_iff : ∀ {α : Type u} [inst : SemilatticeSup α] {a b c : α}, a ⊔ b ≤ c ↔ a ≤ c ∧ b ≤ c This theorem, `sup_le_iff`, states that for any three elements `a`, `b`, and `c` in a semilattice (with supremum operation), the supremum of `a` and `b` is less than or equal to `c` if and only if both `a` is less than or equal to `c` and `b` is less than or equal to `c`. In other words, the largest of `a` and `b` (which is what `a ⊔ b` represents) is less than or equal to `c` precisely when each of `a` and `b` individually is less than or equal to `c`. This theorem is a fundamental property in order theory and lattice theory. More concisely: In a semilattice, the supremum of two elements is less than or equal to a third element if and only if the first two elements are less than or equal to that element.
`inf_left_comm` theorem inf_left_comm : ∀ {α : Type u} [inst : SemilatticeInf α] (a b c : α), a ⊓ (b ⊓ c) = b ⊓ (a ⊓ c) This is a theorem about the infimum (greatest lower bound) operation in semilattices. For any semilattice of type α and for any three elements a, b, and c of this semilattice, the infimum of a and the infimum of b and c is the same as the infimum of b and the infimum of a and c. In mathematical terms, this can be written as $a \wedge (b \wedge c) = b \wedge (a \wedge c)$. This theorem thus expresses a property of left-commutativity for the infimum operation in any semilattice. More concisely: In any semilattice, the infimum of a and the infimum of b commute, that is, $a \wedge (b \wedge c) = b \wedge (a \wedge c)$.
`sup_sup_sup_comm` theorem sup_sup_sup_comm : ∀ {α : Type u} [inst : SemilatticeSup α] (a b c d : α), a ⊔ b ⊔ (c ⊔ d) = a ⊔ c ⊔ (b ⊔ d) This theorem, `sup_sup_sup_comm`, states that for any type `α` which forms a semilattice with a `sup` operation, and for any four elements `a`, `b`, `c`, and `d` of this type, the suprema (also known as the least upper bounds or joins) of these elements commute in a specific way. More specifically, the supremum of `a`, `b`, and the supremum of `c`, `d` is equal to the supremum of `a`, `c` and the supremum of `b`, `d`. In mathematical terms, we have $a \vee b \vee (c \vee d) = a \vee c \vee (b \vee d)$, where $\vee$ represents the `sup` operation. More concisely: For any semilattice with sup operation, the supremum of any four elements commutes, i.e., (a ∨ b) ∨ (c ∨ d) = a ∨ c ∨ (b ∨ d).
`Mathlib.Order.Lattice._auxLemma.10` theorem Mathlib.Order.Lattice._auxLemma.10 : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, (b < a ⊔ b) = ¬a ≤ b This theorem, `Mathlib.Order.Lattice._auxLemma.10`, states that for any type `α` that is a semilattice with respect to the operation "sup" (supremum), and for any two elements `a` and `b` of this type, `b` is less than the supremum of `a` and `b` if and only if `a` is not less than or equal to `b`. In other words, in a semilattice, the supremum of two elements always exceeds one of the elements unless that element is greater than or equal to the other. More concisely: In a semilattice, the supremum of two elements is strictly greater than one of them if and only if they are incomparable.
`Monotone.map_inf_le` theorem Monotone.map_inf_le : ∀ {α : Type u} {β : Type v} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β] {f : α → β}, Monotone f → ∀ (x y : α), f (x ⊓ y) ≤ f x ⊓ f y The theorem `Monotone.map_inf_le` states that for any types `α` and `β` that are semilattices with an infimum operation (denoted by `⊓`), if a function `f` from `α` to `β` is monotone, meaning it preserves the order (i.e., `a ≤ b` implies `f a ≤ f b`), then for any elements `x` and `y` from `α`, the value of function `f` at the infimum of `x` and `y` is less than or equal to the infimum of the values of function `f` at `x` and `y`. In mathematical terms, it expresses that $f(x \wedge y) \leq f(x) \wedge f(y)$ for a monotone function $f$ in a semilattice. More concisely: For any monotone function $f$ and semilattice elements $x, y$ with infimum, $f(x \wedge y) \leq f(x) \wedge f(y)$.
`AntitoneOn.max` theorem AntitoneOn.max : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : LinearOrder β] {f g : α → β} {s : Set α}, AntitoneOn f s → AntitoneOn g s → AntitoneOn (fun x => max (f x) (g x)) s The theorem `AntitoneOn.max` states that for any given set `s` of some type `α` and any two functions `f` and `g` from `α` to a type `β` (where `α` and `β` are preordered and `β` additionally has a linear order), if both `f` and `g` are antitone on `s`, then the function that to each element of `s` assigns the maximum of its images under `f` and `g` is also antitone on `s`. In other words, if for all `a, b` in `s`, `a ≤ b` implies `f(b) ≤ f(a)` and `g(b) ≤ g(a)`, then the same relation holds for the maximum function: `max(f(b), g(b)) ≤ max(f(a), g(a))`. More concisely: If `f` and `g` are antitone functions from a preordered set `α` to an ordered type `β`, then the function that maps each element of `α` to the maximum of its images under `f` and `g` is also antitone.
`sup_idem` theorem sup_idem : ∀ {α : Type u} [inst : SemilatticeSup α] (a : α), a ⊔ a = a This theorem, named `sup_idem`, states that for any type `α` that is a semilattice with a supremum, the supremum of any element `a` with itself is equal to `a`. In terms of set theory and lattice theory, it's saying that the least upper bound (or supremum) of a single element is the element itself. This principle is fundamental in order theory and is a key property of lattices and semilattices. More concisely: In any semilattice with supremum, the supremum of an element with itself is equal to that element.
`le_sup_left` theorem le_sup_left : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, a ≤ a ⊔ b This theorem states that for any type `α` that is a semilattice with an operation `sup` (or supremum), and for any two elements `a` and `b` of that type, `a` is less than or equal to the supremum of `a` and `b`. In other words, in any semilattice, an element is always less than or equal to the supremum of itself with any other element. In the language of order theory, this property is one of the defining characteristics of a join-semilattice. More concisely: For any semilattice type `α` and elements `a, b ∈ α`, we have `a ≤ sup a b`.
`sup_right_idem` theorem sup_right_idem : ∀ {α : Type u} [inst : SemilatticeSup α] (a b : α), a ⊔ b ⊔ b = a ⊔ b This theorem, named `sup_right_idem`, states that in any semilattice with a supremum operation (denoted as `⊔`), for all elements `a` and `b` of the semilattice, the supremum of `a` and `b` taken twice (`a ⊔ b ⊔ b`) is the same as the supremum of `a` and `b` (`a ⊔ b`). In simpler terms, this means in such a structure, taking the supremum of `a` and `b` and then taking the supremum of the result with `b` again doesn't change the result. More concisely: In a semilattice with supremum operation, the repeated application of the supremum operation to any two elements is idempotent. That is, for all `a` and `b` in the semilattice, `a ⊔ b ⊔ b = a ⊔ b`.
`inf_le_inf_left` theorem inf_le_inf_left : ∀ {α : Type u} [inst : SemilatticeInf α] (a : α) {b c : α}, b ≤ c → a ⊓ b ≤ a ⊓ c This theorem is stating that for any type `α` which forms a semilattice with the infimum operation, given three elements (say `a`, `b`, `c`) of type `α`, if `b` is less than or equal to `c`, then the infimum (greatest lower bound) of `a` and `b` is less than or equal to the infimum of `a` and `c`. Here, `SemilatticeInf α` implies that the type `α` has an associative, commutative, and idempotent infimum (binary operation). More concisely: For any semilattice `α` with infimum operation, if `b` is less than or equal to `c` in `α`, then the infimum of `a`, `b` is less than or equal to the infimum of `a` and `c`.
`le_sup_inf` theorem le_sup_inf : ∀ {α : Type u} [inst : DistribLattice α] {x y z : α}, (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z This theorem, `le_sup_inf`, states that for any type `α` which is a distributive lattice and any three elements `x`, `y`, `z` of this type, the supremum (join) of `x` and `y` intersected with the supremum of `x` and `z` is less than or equal to the supremum of `x` and the intersection of `y` and `z`. In terms of lattice theory, it relates the operations of join (supremum) and meet (infimum) in a specific way. This can be expressed in LaTeX as: $(x \vee y) \wedge (x \vee z) \leq x \vee (y \wedge z)$, where $\vee$ represents the supremum and $\wedge$ represents the infimum. More concisely: For any distributive lattice `α`, the join of two elements `x` and `y` intersected with the join of `x` and `z` is less than or equal to the join of `x` and the meet of `y` and `z`. In mathematical notation: $(x \vee y) \wedge (x \vee z) \leq x \vee (y \wedge z)$.
`sup_eq_sup_iff_right` theorem sup_eq_sup_iff_right : ∀ {α : Type u} [inst : SemilatticeSup α] {a b c : α}, a ⊔ c = b ⊔ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c The theorem `sup_eq_sup_iff_right` states that, for any type `α` that forms a semilattice with respect to the sup (or join) operation, and any three elements `a`, `b`, and `c` of this type, the supremum (or join) of `a` and `c` is equal to the supremum of `b` and `c` if and only if `a` is less than or equal to the supremum of `b` and `c` and `b` is less than or equal to the supremum of `a` and `c`. This theorem is a part of the order theory in mathematics and specifically deals with the lattice structure. More concisely: For any semilattice type `α` and elements `a`, `b`, and `c`, `a ⊔ c = b ⊔ c` if and only if `a ≤ b ≤ a ⊔ c`. (Here, `⊔` denotes the sup or join operation.)
`inf_right_comm` theorem inf_right_comm : ∀ {α : Type u} [inst : SemilatticeInf α] (a b c : α), a ⊓ b ⊓ c = a ⊓ c ⊓ b This theorem states that for any type `α` that is a semilattice with respect to the infimum operation, the order of infimum operations is commutative on the right side. In other words, for all elements `a`, `b`, and `c` of this type, the infimum of `a`, `b`, and `c` remains the same whether we first take the infimum of `b` and `c` and then with `a`, or first take the infimum of `c` and `b` and then with `a`. In mathematical notation, it states that $a \wedge (b \wedge c) = a \wedge (c \wedge b)$. More concisely: For any semilattice `α` with respect to infimum, the associativity of infimum holds: `a ∧ (b ∧ c) = a ∧ (c ∧ b)`.
`inf_comm` theorem inf_comm : ∀ {α : Type u} [inst : SemilatticeInf α] (a b : α), a ⊓ b = b ⊓ a This theorem, named `inf_comm`, states that for any type `α` having a semilattice with infimum structure, the infimum operation, denoted by `⊓`, is commutative. In other words, for any two elements `a` and `b` of type `α`, the infimum of `a` and `b` is equal to the infimum of `b` and `a`. This is a fundamental property of semilattices that the order of elements does not affect the result of the infimum operation. More concisely: For any semilattice `α` with infimum operation `⊓`, the infimum of `a` and `b` equals the infimum of `b` and `a` for all `a, b ∈ α`.
`inf_le_sup` theorem inf_le_sup : ∀ {α : Type u} [inst : Lattice α] {a b : α}, a ⊓ b ≤ a ⊔ b This theorem, `inf_le_sup`, states that for all types `α` that form a lattice (a mathematical structure with two binary operations called 'meet' and 'join'), the infimum (or 'meet', denoted by `⊓`) of any two elements `a` and `b` of the lattice is less than or equal to the supremum (or 'join', denoted by `⊔`) of those two elements. In mathematical terms, for any two elements `a` and `b` in a lattice `α`, it's always true that `a ⊓ b ≤ a ⊔ b`. More concisely: For all lattices α and elements a, b in α, the infimum (meet) of a and b is less than or equal to the supremum (join) of a and b: a ⊓ b ≤ a ⊔ b.
`Antitone.sup` theorem Antitone.sup : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : SemilatticeSup β] {f g : α → β}, Antitone f → Antitone g → Antitone (f ⊔ g) The theorem `Antitone.sup` states that for any two functions `f` and `g` from a type `α` to a type `β`, with `α` being a preorder and `β` being a semilattice with a supremum operation, if both the functions `f` and `g` are antitone (meaning for each `f` and `g`, if `a ≤ b` then `f b ≤ f a` and `g b ≤ g a` respectively), then the pointwise supremum of `f` and `g` (which is a new function that at each point takes the supremum of the values of `f` and `g`) is also an antitone function. More concisely: If `α` is a preorder type and `β` is a semilattice with supremum, and `f` and `g` are antitone functions from `α` to `β`, then the pointwise supremum of `f` and `g` is an antitone function.
`sup_inf_right` theorem sup_inf_right : ∀ {α : Type u} [inst : DistribLattice α] (a b c : α), a ⊓ b ⊔ c = (a ⊔ c) ⊓ (b ⊔ c) This theorem, `sup_inf_right`, states that for all types `α` equipped with a distributive lattice structure, for any elements `a`, `b`, and `c` of that type, the supremum (join, denoted by `⊔`) of the infimum (meet, denoted by `⊓`) of `a` and `b` with `c` is equal to the infimum of the supremum of `a` with `c` and the supremum of `b` with `c`. In mathematical terms, this is saying that `a ⊓ b ⊔ c = (a ⊔ c) ⊓ (b ⊔ c)` for all `a`, `b`, `c` in a distributive lattice. This property is one of the defining characteristics of distributive lattices. More concisely: In a distributive lattice, the supremum of the infimum of two elements with a third element is equal to the infimum of their supremums: `(a ⊓ b) ⊔ c = a ⊔ c ⊓ b ⊔ c` for all `a`, `b`, `c`.
`sup_right_comm` theorem sup_right_comm : ∀ {α : Type u} [inst : SemilatticeSup α] (a b c : α), a ⊔ b ⊔ c = a ⊔ c ⊔ b This theorem, `sup_right_comm`, states that for any semilattice (a partially ordered set with a supremum operation) of type `α`, the supremum operation (`⊔`) is right-commutative. In other words, for any three elements `a`, `b`, and `c` of type `α`, the supremum of `a`, `b` and `c` remains the same if the order of `b` and `c` is switched. The supremum of `a`, `b` and `c` is denoted by `a ⊔ b ⊔ c` and it is equal to `a ⊔ c ⊔ b`. More concisely: For any semilattice `α`, the supremum operation `⊔` is right-commutative, i.e., `a ⊔ b ⊔ c = a ⊔ c ⊔ b` for all `a, b, c` in `α`.
`Mathlib.Order.Lattice._auxLemma.1` theorem Mathlib.Order.Lattice._auxLemma.1 : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, (a ≤ a ⊔ b) = True := by sorry This theorem, from the Mathlib library in Lean, states that for any type `α` that is a semilattice with a supremum operation, and for any two elements `a` and `b` of this type, it is always true that `a` is less than or equal to the supremum of `a` and `b`. In mathematical terms, this theorem says that for all `a`, `b` in a given semilattice, we always have $a \leq a \vee b$, where $\vee$ denotes the supremum operation. More concisely: In any semilattice with supremum operation, for all elements `a` and `b`, we have `a ≤ a ∨ b` (or equivalently, `a ∧ (a ∨ b) = a`).
`inf_eq_left` theorem inf_eq_left : ∀ {α : Type u} [inst : SemilatticeInf α] {a b : α}, a ⊓ b = a ↔ a ≤ b This theorem, `inf_eq_left`, states that for any type `α` that forms a semilattice under an infimum operation, and for any two elements `a` and `b` of that type, the infimum of `a` and `b` is equal to `a` if and only if `a` is less than or equal to `b`. In simpler terms, in a structure where an "and"-like operation (infimum) is defined, `a` is at most `b` exactly when `a` combined with `b` using this operation results in `a`. More concisely: For any semilattice `α` and elements `a, b ∈ α`, `inf a b = a` if and only if `a ≤ b`.
`Monotone.max` theorem Monotone.max : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : LinearOrder β] {f g : α → β}, Monotone f → Monotone g → Monotone fun x => max (f x) (g x) The theorem `Monotone.max` states that for all types `α` and `β`, where `α` has a preorder and `β` has a linear order, if `f` and `g` are two monotone functions from `α` to `β`, then the function that gives the maximum of `f(x)` and `g(x)` for each `x` in `α` is also a monotone function. In other words, if `f` and `g` are monotone, then so is `max(f,g)`. More concisely: If `f` and `g` are monotone functions from a preordered type `α` to a linearly ordered type `β`, then the function `x ↔ max (f x) (g x)` is also monotone.
`inf_sup_right` theorem inf_sup_right : ∀ {α : Type u} [inst : DistribLattice α] (a b c : α), (a ⊔ b) ⊓ c = a ⊓ c ⊔ b ⊓ c This theorem, `inf_sup_right`, states that for all types `α` that form a distributive lattice, and for all elements `a`, `b`, and `c` of this type, the supremum (join, denoted by `⊔`) of `a` and `b`, followed by the infimum (meet, denoted by `⊓`) with `c`, equals the supremum of the infimum of `a` and `c` with the infimum of `b` and `c`. In mathematical terms, it expresses the distributive property of a lattice: `(a ∨ b) ∧ c = (a ∧ c) ∨ (b ∧ c)`, where `∨` represents the join operation and `∧` represents the meet operation. More concisely: For all types `α` that form a distributive lattice and all elements `a`, `b`, and `c` of this type, `(a ⊔ b) ⊓ c = a ⊓ c ⊔ b ⊓ c`.
`Monotone.le_map_sup` theorem Monotone.le_map_sup : ∀ {α : Type u} {β : Type v} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β] {f : α → β}, Monotone f → ∀ (x y : α), f x ⊔ f y ≤ f (x ⊔ y) The theorem `Monotone.le_map_sup` states that for any types `α` and `β` that are semilattices with a sup operation, and any function `f` from `α` to `β`, if `f` is a monotone function (i.e., if `a ≤ b` then `f a ≤ f b` for all `a` and `b`), then for all `x` and `y` of type `α`, the sup (least upper bound or join) of `f x` and `f y` is less than or equal to `f` of the sup of `x` and `y`. In LaTeX mathematics, this can be expressed as: if `f` is a monotone function, then for all `x, y` in `α`, we have `f(x) ⊔ f(y) ≤ f(x ⊔ y)`. More concisely: For any semilattice types `α` and `β` with a sup operation, and any monotone function `f` from `α` to `β`, `f(x ⊔ y) ≥ f(x) ⊔ f(y)` holds. (Note that the theorem states the opposite inequality in the given description, but mathematical conventions often prefer the stated form.)
`sup_eq_sup_iff_left` theorem sup_eq_sup_iff_left : ∀ {α : Type u} [inst : SemilatticeSup α] {a b c : α}, a ⊔ b = a ⊔ c ↔ b ≤ a ⊔ c ∧ c ≤ a ⊔ b This theorem states that for any type `α` that forms a semilattice with a supremum operation (denoted by `⊔`), and for any three elements `a`, `b`, and `c` of this type, the supremum of `a` and `b` being equal to the supremum of `a` and `c` is equivalent to `b` being less than or equal to the supremum of `a` and `c` and `c` being less than or equal to the supremum of `a` and `b`. In the context of ordered sets, the supremum operation `⊔` returns the least upper bound of the two elements. More concisely: For any semilattice `α` with supremum operation `⊔`, and for all `a`, `b`, and `c` in `α`, `a ⊔ b = a ⊔ c` if and only if `b ≤ a ⊔ c` and `c ≤ a ⊔ b`.
`inf_left_idem` theorem inf_left_idem : ∀ {α : Type u} [inst : SemilatticeInf α] (a b : α), a ⊓ (a ⊓ b) = a ⊓ b This theorem states that for any semilattice of infimum type `α` and for any two elements `a` and `b` of this type, the infimum of `a` and the infimum of `a` and `b` is equal to the infimum of `a` and `b`. In other words, it shows the idempotency of the infimum operation in the context of a semilattice, where infimum of `a` with itself and another element `b` doesn't change the result as compared to the infimum of `a` and `b`. More concisely: In a semilattice, the infimum of an element with itself is equal to the infimum of that element with any other element.
`Antitone.inf` theorem Antitone.inf : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : SemilatticeInf β] {f g : α → β}, Antitone f → Antitone g → Antitone (f ⊓ g) The theorem `Antitone.inf` states that for any two given functions `f` and `g` defined over a preordered set `α` and taking values in a semilattice `β`, if both `f` and `g` are antitone (i.e., they are decreasing functions; if `a ≤ b` then `f(b) ≤ f(a)` and `g(b) ≤ g(a)`), then the pointwise infimum function `(f ⊓ g)` is also antitone. Here, the pointwise infimum of `f` and `g` is a function that sends each element `a` of the domain to the infimum (or greatest lower bound) of the values `f(a)` and `g(a)`. More concisely: If `f` and `g` are antitone functions from a preordered set into a semilattice, then their pointwise infimum is also an antitone function.
`Function.update_inf` theorem Function.update_inf : ∀ {ι : Type u_1} {π : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → SemilatticeInf (π i)] (f : (i : ι) → π i) (i : ι) (a b : π i), Function.update f i (a ⊓ b) = Function.update f i a ⊓ Function.update f i b This theorem asserts that for any type `ι`, any type function `π : ι → Type`, given that equality is decidable for `ι` and each `π i` forms a semilattice with respect to an infimum operation, and for any function `f : (i : ι) → π i`, and any element `i : ι`, and any two elements `a, b : π i`, updating `f` at `i` with the infimum of `a` and `b` is the same as taking the infimum of `f` updated at `i` with `a` and `f` updated at `i` with `b`. In other words, the function update operation respects the infimum operation. More concisely: For any type `ι`, type function `π : ι → Type` with decidable equality and each `π i` a semilattice with respect to an infimum operation, the infimum of `f i` updated with `a` and `b` equals the infimum of `f` updated at `i` with `a` and `b`, for any function `f : ι → π i` and elements `a, b : π i`.
`inf_congr_right` theorem inf_congr_right : ∀ {α : Type u} [inst : SemilatticeInf α] {a b c : α}, b ⊓ c ≤ a → a ⊓ c ≤ b → a ⊓ c = b ⊓ c This theorem, `inf_congr_right`, states that for any type `α` that is a semilattice with an infimum (or greatest lower bound) operation, and for any three elements `a`, `b`, and `c` of this type, if `b` infimum `c` is less than or equal to `a` and `a` infimum `c` is less than or equal to `b`, then `a` infimum `c` is equal to `b` infimum `c`. In other words, in a semilattice, if the infimum of `b` and `c` doesn't exceed `a` and the infimum of `a` and `c` doesn't exceed `b`, then both infimums are equal. More concisely: In a semilattice, if `a` has infimum both with `b` and `c` and these infima are equal, then `a` infimum `b` = `a` infimum `c` = `b` infimum `c`.
`sup_eq_max` theorem sup_eq_max : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, a ⊔ b = max a b This theorem, `sup_eq_max`, states that for all types `α` that have a linear order, the supremum (denoted as `a ⊔ b`) of any two elements `a` and `b` of that type is equal to the maximum of `a` and `b`. This essentially means that in a linearly ordered set, the supremum - the least upper bound - of two elements is simply the larger of the two elements. More concisely: For all types `α` with a linear order and for all `a, b` in `α`, `a ⊔ b = max a b`.
`SemilatticeSup.le_sup_right` theorem SemilatticeSup.le_sup_right : ∀ {α : Type u} [self : SemilatticeSup α] (a b : α), b ≤ a ⊔ b The theorem `SemilatticeSup.le_sup_right` states that, for any semilattice structure `α` and any elements `a` and `b` of `α`, `b` is less than or equal to the supremum of `a` and `b`. In LaTeX mathematics, this is written as `b ≤ sup(a, b)`. This establishes that the supremum operation (notated as `⊔`) always results in a value that is an upper bound for its two inputs. More concisely: For any semilattice `α` and elements `a, b ∈ α`, we have `b ≤ sup(a, b)`.
`le_inf` theorem le_inf : ∀ {α : Type u} [inst : SemilatticeInf α] {a b c : α}, a ≤ b → a ≤ c → a ≤ b ⊓ c This theorem, `le_inf`, states that for any semilattice of infimum type `α` and for any elements `a`, `b`, `c` of type `α`, if `a` is less than or equal to both `b` and `c`, then `a` is also less than or equal to the infimum (greatest lower bound) of `b` and `c`. In terms of mathematical notation, given `a ≤ b` and `a ≤ c`, it follows that `a ≤ b ⊓ c`. More concisely: If `a` is an element of a semilattice of infimum type `α`, and `a ≤ b` and `a ≤ c`, then `a ≤ b ∧ c` implies `a ≤ b ⊓ c`.
`le_sup_of_le_right` theorem le_sup_of_le_right : ∀ {α : Type u} [inst : SemilatticeSup α] {a b c : α}, c ≤ b → c ≤ a ⊔ b This theorem, `le_sup_of_le_right`, states that for any semilattice (a partially ordered set with a supremum operation) of type α, and for any elements a, b, and c of that type, if c is less than or equal to b, then c is also less than or equal to the supremum of a and b. In other words, in a semilattice, if an element is less than or equal to another, then it is also less than or equal to the supremum of that element and any other element in the semilattice. More concisely: In a semilattice, if $c \leq b$, then $c \leq \sup(a, b)$.
`Mathlib.Order.Lattice._auxLemma.13` theorem Mathlib.Order.Lattice._auxLemma.13 : ∀ {α : Type u} [inst : SemilatticeInf α] {a b c : α}, (a ≤ b ⊓ c) = (a ≤ b ∧ a ≤ c) This theorem, titled `Mathlib.Order.Lattice._auxLemma.13`, states that for any type `α` which has a structure of a semilattice with respect to an infimum operation (denoted as `⊓`), for any three elements `a`, `b`, and `c` of this type, `a` is less than or equal to the infimum of `b` and `c` if and only if `a` is less than or equal to `b` and `a` is less than or equal to `c`. This encapsulates the fundamental property of the infimum in a semilattice, which is the greatest lower bound of a set. More concisely: For any semilattice `α` with infimum operation `⊓`, for all `a, b, c ∈ α`, `a ≤ b ∧ a ≤ c` if and only if `a ≤ b⊓c`.
`SemilatticeSup.sup_le` theorem SemilatticeSup.sup_le : ∀ {α : Type u} [self : SemilatticeSup α] (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c := by sorry This theorem states that, for any type `α` equipped with a semilattice structure, given three elements `a`, `b`, and `c` of `α`, if `a` and `b` are less than or equal to `c`, then the supremum (greatest lower bound) of `a` and `b` is also less than or equal to `c`. This property is fundamental to the definition of a semilattice and essentially says that the supremum of any two elements in the semilattice is the least upper bound for those two elements. More concisely: In a semilattice, if `a` and `b` are elements less than or equal to `c`, then the supremum of `a` and `b` is less than or equal to `c`.
`sup_of_le_left` theorem sup_of_le_left : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, b ≤ a → a ⊔ b = a This theorem, `sup_of_le_left`, is an alias of the reverse direction of the theorem `sup_eq_left` in Lean 4. It states that for any type `α` that is a semilattice with a supremum operation (`SemilatticeSup α`), and any two elements `a` and `b` of type `α`, if `b` is less than or equal to `a` (`b ≤ a`), then the supremum of `a` and `b` (`a ⊔ b`) is equals to `a`. In mathematical terms, if `b` is less than or equal to `a`, the "greatest" element between `a` and `b` is `a`. More concisely: If `α` is a semilattice with supremum, and `a` and `b` are elements of `α` with `b ≤ a`, then `a ⊔ b = a`.
`DistribLattice.le_sup_inf` theorem DistribLattice.le_sup_inf : ∀ {α : Type u_1} [self : DistribLattice α] (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z This theorem states that in a distributive lattice of any type `α`, the infimum (or greatest lower bound) distributes over the supremum (or least upper bound). Specifically, for any elements `x`, `y`, and `z` in this lattice, the infimum of the supremum of `x` and `y` and the supremum of `x` and `z`, is less than or equal to the supremum of `x` and the infimum of `y` and `z`. In terms of mathematical symbols, it says that $(x \vee y) \wedge (x \vee z) \leq x \vee (y \wedge z)$. More concisely: In a distributive lattice, the infimum of the supremum of any two elements is less than or equal to the supremum of the infimums of those elements. Mathematically expressed: inf(sup(x, y), sup(x, z)) ≤ sup(inf(x, y), inf(x, z)).
`SemilatticeInf.le_inf` theorem SemilatticeInf.le_inf : ∀ {α : Type u} [self : SemilatticeInf α] (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c := by sorry This theorem states that in a semilattice structure of type α, defined with an infimum operation (notated as "⊓"), if a certain element 'a' is less than or equal to two other elements 'b' and 'c' respectively, then 'a' is also less than or equal to the infimum of 'b' and 'c'. That is, the infimum of 'b' and 'c' serves as a greatest lower bound for 'a'. More concisely: In a semilattice with infimum operation, if a <= b and a <= c then a <= b \assenze c (intuitively, a is a lower bound for both b and c, so it is a lower bound for their infimum).
`SemilatticeInf.inf_le_right` theorem SemilatticeInf.inf_le_right : ∀ {α : Type u} [self : SemilatticeInf α] (a b : α), a ⊓ b ≤ b This theorem states that for any type `α` that has an infimum (or "greatest lower bound") operation defined on it (that is, it's a semilattice under the infimum operation), the infimum of any two elements `a` and `b` from `α` is always less than or equal to `b`. In other words, the infimum of `a` and `b` is a lower bound on `b`. In mathematical terms, this can be represented as `a ⊓ b ≤ b`. More concisely: For any semilattice `α` with infimum operation `⊓`, the infimum of any two elements `a` and `b` in `α`, `a ⊓ b`, is less than or equal to `b`, i.e., `a ⊓ b ≤ b`.
`Antitone.min` theorem Antitone.min : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : LinearOrder β] {f g : α → β}, Antitone f → Antitone g → Antitone fun x => min (f x) (g x) The theorem 'Antitone.min' states that for any two given functions 'f' and 'g' that map from a preordered type 'α' to a linearly ordered type 'β', if both 'f' and 'g' are antitone functions (i.e., if for any 'a' and 'b' in type 'α', 'a ≤ b' implies 'f(b) ≤ f(a)' and 'g(b) ≤ g(a)'), then the function which maps 'x' in 'α' to the minimum of 'f(x)' and 'g(x)' is also an antitone function. More concisely: If two antitone functions map between a preordered type and a linearly ordered type, then their pointwise minimum is also an antitone function.
`sup_le_sup_left` theorem sup_le_sup_left : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, a ≤ b → ∀ (c : α), c ⊔ a ≤ c ⊔ b := by sorry This theorem, `sup_le_sup_left`, states that for any type `α` that is a semilattice with an operation `sup` (supremum), and for any elements `a`, `b`, and `c` of this type, if `a` is less than or equal to `b`, then the supremum of `c` and `a` is less than or equal to the supremum of `c` and `b`. In simpler terms, if `a` is less than or equal to `b`, replacing `a` with `b` in the supremum with `c` will not decrease the overall value. This is a property of the supremum operation in semilattices. More concisely: For any semilattice `α` with supremum operation `sup`, and for all `a`, `b`, `c` in `α` with `a ≤ b`, we have `sup c a ≤ sup c b`.
`SemilatticeInf.inf_le_left` theorem SemilatticeInf.inf_le_left : ∀ {α : Type u} [self : SemilatticeInf α] (a b : α), a ⊓ b ≤ a This theorem states that for any semi-lattice (a partially ordered set that any two elements have a greatest lower bound) of type `α`, the infimum (greatest lower bound) of any two elements `a` and `b` is less than or equal to `a`. This means in the ordered set under consideration, if you take any two elements and find their greatest lower bound, that value will always be less than or equal to the first of those two elements. More concisely: For any semi-lattice α, the infimum of a and b is less than or equal to a for all a, b in α.
`right_lt_sup` theorem right_lt_sup : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, b < a ⊔ b ↔ ¬a ≤ b This theorem, referred to as `right_lt_sup`, states that for any type `α` that forms a semilattice with a supremum operation (denoted `⊔`), given any two elements `a` and `b` of this type, `b` is less than the supremum of `a` and `b` (`a ⊔ b`) if and only if `a` is not less than or equal to `b`. This theorem is a key part of the definition and properties of a semilattice, and it helps describe the relationship between the elements and the supremum operation. More concisely: For any semilattice `α` with supremum operation `⊔`, and any `a, b ∈ α`, `b < a ⊔ b` if and only if `a ≤ b`.
`sup_congr_right` theorem sup_congr_right : ∀ {α : Type u} [inst : SemilatticeSup α] {a b c : α}, a ≤ b ⊔ c → b ≤ a ⊔ c → a ⊔ c = b ⊔ c The theorem `sup_congr_right` states that for any type `α` that forms a semilattice under the "sup" operation, given three elements `a`, `b`, `c` from this type, if `a` is less than or equal to the supremum of `b` and `c`, and `b` is less than or equal to the supremum of `a` and `c`, then the supremum of `a` and `c` is equal to the supremum of `b` and `c`. In other words, if `a` and `b` both have the same supremum when joined with `c`, then these two supremums are equal. More concisely: If `α` is a semilattice with supremum, and `a`, `b`, `c` are in `α` such that `a ≤ sup(b, c)` and `b ≤ sup(a, c)`, then `sup(a, c) = sup(b, c)`.
`inf_eq_right` theorem inf_eq_right : ∀ {α : Type u} [inst : SemilatticeInf α] {a b : α}, a ⊓ b = b ↔ b ≤ a This theorem states that for any semilattice of type `α` and any elements `a` and `b` of type `α`, the infimum (greatest lower bound) of `a` and `b` equals to `b` if and only if `b` is less than or equal to `a`. In other words, `b` is the infimum of `α` and `b` precisely when `b` is less than or equal to `a`. More concisely: For any semilattice `α`, the infimum of `a` and `b` equals `b` if and only if `b` is less than or equal to `a`.
`le_sup_right` theorem le_sup_right : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, b ≤ a ⊔ b This is a theorem in the field of order theory relating to semilattices. It states that for any type `α` that is a semilattice with respect to an operation `⊔` (typically representing "sup" or "supremum"), and for any two elements `a` and `b` of type `α`, `b` is less than or equal to the supreme of `a` and `b`. This means that the supremum of `a` and `b` is at least as great as `b`, a fundamental property of the supremum operation in semilattices. More concisely: In a semilattice with respect to the operation `⊔`, for all elements `a` and `b`, `b ≤ a ⊔ b`.
`lt_inf_iff` theorem lt_inf_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, a < b ⊓ c ↔ a < b ∧ a < c This theorem states that for any type `α` that has a linear order, and any three elements `a`, `b`, `c` of type `α`, `a` is less than the infimum (greatest lower bound) of `b` and `c` if and only if `a` is less than both `b` and `c`. This is expressed with the mathematical symbols as $a < \inf\{b, c\} \iff a < b \land a < c$. More concisely: For any linear order type `α` and elements `a`, `b`, `c` of type `α`, `a` is below the infimum of `b` and `c` if and only if `a` is below both `b` and `c`. In mathematical notation: $a < \inf\{b, c\} \iff a < b \land a < c$.
`sup_le` theorem sup_le : ∀ {α : Type u} [inst : SemilatticeSup α] {a b c : α}, a ≤ c → b ≤ c → a ⊔ b ≤ c This theorem, `sup_le`, states that for any type `α` that forms a semilattice with the join operation `⊔`, and any three elements `a`, `b`, and `c` of this type, if `a` and `b` are both less than or equal to `c`, then the join (`⊔`) of `a` and `b` is also less than or equal to `c`. In other words, the least upper bound (`sup`, signified by `⊔`) of two elements in a semilattice that are both less than or equal to a third element, is itself less than or equal to that third element. More concisely: For any semilattice `α` with join operation `⊔`, and any elements `a`, `b`, and `c` in `α`, if `a ≤ c` and `b ≤ c`, then `a ⊔ b ≤ c`.
`AntitoneOn.sup` theorem AntitoneOn.sup : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : SemilatticeSup β] {f g : α → β} {s : Set α}, AntitoneOn f s → AntitoneOn g s → AntitoneOn (f ⊔ g) s The theorem `AntitoneOn.sup` states that for any two functions `f` and `g` from a preorder `α` to a semilattice `β`, if both functions are antitone (non-increasing) on a particular set `s` of `α`, then their pointwise supremum function (a function where the value at each point is the maximum of the values of `f` and `g` at that point) is also antitone on the same set `s`. In mathematical terms, if for all `a, b ∈ s` we have `a ≤ b` implies `f b ≤ f a` and `g b ≤ g a`, then `a ≤ b` also implies `(f ⊔ g) b ≤ (f ⊔ g) a`, where `f ⊔ g` is the pointwise supremum of `f` and `g`. More concisely: If two antitone functions from a preorder to a semilattice restrict to the same set satisfy `a ≤ b` implying `f(b) ≤ f(a)` and `g(b) ≤ g(a)`, then their pointwise supremum is also antitone on that set.
`inf_right_idem` theorem inf_right_idem : ∀ {α : Type u} [inst : SemilatticeInf α] (a b : α), a ⊓ b ⊓ b = a ⊓ b This theorem, named `inf_right_idem`, asserts that for all types `α` that is a semilattice under an infimum operation (`SemilatticeInf α`), the infimum of any `a` and `b` (`a` and `b` being elements of the type `α`) with `b` infimum `b` is the same as the infimum of `a` and `b`. In other words, it states that taking the infimum operation on `b` with itself doesn't change the result when taking the infimum with `a`. This can be written in mathematical terms as: for all `a` and `b` in a semilattice, `a ⊓ b ⊓ b = a ⊓ b`. More concisely: For all semilattices `α` and elements `a, b` in `α`, `a ⊓ b ⊓ b equals a ⊓ b`. In other words, the infimum of an element with itself is equal to the infimum of that element with another element.
`Mathlib.Order.Lattice._auxLemma.3` theorem Mathlib.Order.Lattice._auxLemma.3 : ∀ {α : Type u} [inst : SemilatticeSup α] {a b c : α}, (a ⊔ b ≤ c) = (a ≤ c ∧ b ≤ c) This theorem is a proposition in the field of order theory, specifically concerning semilattices. It states that for any type `α` that is a semilattice sup (a structure with an associative, commutative, and idempotent binary operation called sup), and any elements `a`, `b`, and `c` of that type, `a` joined with `b` being less than or equal to `c` is equivalent to `a` being less than or equal to `c` and `b` being less than or equal to `c`. In terms of lattice theory, the join (`a ⊔ b`) of `a` and `b` is less than or equal to `c` if and only if both `a` and `b` are individually less than or equal to `c`. More concisely: In a semilattice `α`, for all elements `a`, `b`, and `c`, `a ⊔ b ≤ c` if and only if `a ≤ c` and `b ≤ c`.
`sup_le_sup` theorem sup_le_sup : ∀ {α : Type u} [inst : SemilatticeSup α] {a b c d : α}, a ≤ b → c ≤ d → a ⊔ c ≤ b ⊔ d This theorem states that for any type `α` that has a semilattice super operation (denoted by `⊔`), given four elements `a`, `b`, `c`, and `d` of this type, if `a` is less than or equal to `b` and `c` is less than or equal to `d`, then the supremum (least upper bound) of `a` and `c` is less than or equal to the supremum of `b` and `d`. More concisely: For any semilattice `α` with operation `⊔`, if `a ≤ b` and `c ≤ d` in `α`, then `a ⊔ c ≤ b ⊔ d`.
`sup_left_comm` theorem sup_left_comm : ∀ {α : Type u} [inst : SemilatticeSup α] (a b c : α), a ⊔ (b ⊔ c) = b ⊔ (a ⊔ c) The theorem `sup_left_comm` states that for any type `α` that forms a semilattice with respect to the operation `⊔` (sup or supremum), the operation is left-commutative. In other words, for any three elements `a`, `b`, and `c` of type `α`, the supremum of `a` and the supremum of `b` and `c` is equal to the supremum of `b` and the supremum of `a` and `c`. This is a property of algebraic structures such as semilattices where the order of elements does not matter when combining them with an operation. More concisely: For any semilattice `α` with operation `⊔`, the supremum of `a ⊔ b` is equal to `b ⊔ a` for all `a, b ∈ α`.
`Pi.inf_apply` theorem Pi.inf_apply : ∀ {ι : Type u_1} {α' : ι → Type u_2} [inst : (i : ι) → Inf (α' i)] (f g : (i : ι) → α' i) (i : ι), (f ⊓ g) i = f i ⊓ g i This theorem states that for any type `ι`, any type `α'` that is a function of `ι`, and any two functions `f` and `g` that map from `ι` to `α'`, the infimum (greatest lower bound) of the function applied to `i` is equal to the infimum of the values of `f` and `g` applied to `i`. In mathematical terms, this can be denoted as (f ⊓ g)(i) = f(i) ⊓ g(i). This theorem essentially shows the distributive property of the infimum operation over function application. More concisely: For any types `ι`, `α'`, and functions `f` and `g` from `ι` to `α'`, the infimum of `(f ∘ id)` and `(g ∘ id)` is equal to `(inf (map f) = inf (map g)) ∘ id`, where `id` is the identity function on `ι` and `map` applies a function to each element of a list.
`sup_sup_distrib_left` theorem sup_sup_distrib_left : ∀ {α : Type u} [inst : SemilatticeSup α] (a b c : α), a ⊔ (b ⊔ c) = a ⊔ b ⊔ (a ⊔ c) := by sorry This theorem, `sup_sup_distrib_left`, is a distributive property of the supremum or "join" operation (denoted by `⊔`) in a semilattice. It states that for any type 'α', which has a semilattice structure with a supremum operation, and for any three elements 'a', 'b', and 'c' of this type, the supremum of 'a' and the supremum of 'b' and 'c' is equal to the supremum of 'a' and 'b' and the supremum of 'a' and 'c'. In other words, in such a semilattice, the supremum operation distributes over itself. More concisely: In a semilattice with supremum operation, the supremum of any two elements is commutative and associative with respect to the supremum of a third element. (Or, more succinctly: `⊔` is idempotent and associative over itself in a semilattice.)
`Monotone.map_sup` theorem Monotone.map_sup : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : SemilatticeSup β] {f : α → β}, Monotone f → ∀ (x y : α), f (x ⊔ y) = f x ⊔ f y The theorem `Monotone.map_sup` states that for any types `α` and `β`, given a linear order on `α`, a semilattice sup (supremum) structure on `β`, and a function `f` from `α` to `β`, if `f` is a monotone function, then for all elements `x` and `y` of `α`, the image under `f` of the supremum of `x` and `y` (`x ⊔ y`) is equal to the supremum of the images under `f` of `x` and `y` (`f x ⊔ f y`). This theorem is essentially saying that a monotone function preserves the operation of taking supremum. More concisely: If `f` is a monotone function from a type `α` equipped with a linear order and a supremum structure to a semilattice sup type `β`, then `f (x ⊔ y) = f x ⊔ f y` for all `x, y ∈ α`.
`Function.update_sup` theorem Function.update_sup : ∀ {ι : Type u_1} {π : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → SemilatticeSup (π i)] (f : (i : ι) → π i) (i : ι) (a b : π i), Function.update f i (a ⊔ b) = Function.update f i a ⊔ Function.update f i b This theorem states that for a function `f` mapping from type `ι` to a semilattice `π i` (for different `i`), the operation of updating the function at a certain point `i` with the supremum (`⊔`; greatest lower bound) of two values `a` and `b` is the same as the supremum of updating the function at the same point `i` first with `a` and then with `b`. This holds for all `i`, `a`, and `b` in the respective domains and for all functions `f` from `ι` to `π i`. Here, `DecidableEq ι` means that equality between elements of type `ι` is decidable, and `SemilatticeSup (π i)` means that `π i` forms a semilattice with the supremum operation. More concisely: For any function `f` from a decidably equipped type `ι` to a semilattice `π i`, updating `f` at `i` with the supremum of `a` and `b` is equal to updating it first with `a` and then with `b`, for all `i`, `a`, and `b` in their respective domains.
`sup_congr_left` theorem sup_congr_left : ∀ {α : Type u} [inst : SemilatticeSup α] {a b c : α}, b ≤ a ⊔ c → c ≤ a ⊔ b → a ⊔ b = a ⊔ c This theorem, `sup_congr_left`, states that for any type `α` that is a semilattice under the sup operation (denoted ⊔), given three elements `a`, `b`, and `c` of type `α`, if `b` is less than or equal to the sup of `a` and `c`, and `c` is less than or equal to the sup of `a` and `b`, then the sup of `a` and `b` is equal to the sup of `a` and `c`. In simpler terms, this theorem captures a specific property of partial ordering in the context of a semilattice: the sup operation, which gives the least upper bound of two elements, is commutative under certain conditions. More concisely: If `α` is a semilattice under sup and `a`, `b`, `c` are elements of `α` with `b ≤ a ⊔ c` and `c ≤ a ⊔ b`, then `a ⊔ b = a ⊔ c`.
`sup_eq_right` theorem sup_eq_right : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, a ⊔ b = b ↔ a ≤ b This theorem, `sup_eq_right`, states that for any type `α` that forms a semilattice with a supremum operation (denoted as `⊔`), and for any two elements `a` and `b` of this type, `a ⊔ b` being equal to `b` is equivalent to `a` being less than or equal to `b`. Essentially, it captures the intuition that in a semilattice, if the supremum of two elements is one of them, then the other element must not exceed it. More concisely: For any semilattice type `α` with supremum operation `⊔`, and any `a, b` in `α`, `a ⊔ b = b` if and only if `a ≤ b`.
`le_sup_of_le_left` theorem le_sup_of_le_left : ∀ {α : Type u} [inst : SemilatticeSup α] {a b c : α}, c ≤ a → c ≤ a ⊔ b This theorem states that for any type `α` that forms a semilattice with a sup operation (denoted by `⊔`), given three elements `a`, `b`, and `c` of type `α`, if `c` is less than or equal to `a`, then `c` is less than or equal to the sup of `a` and `b`. In mathematical terms, this is saying that if $c \leq a$ in the semilattice, then $c \leq a \vee b$, where $\vee$ denotes the sup operation. More concisely: For any semilattice `α` with sup operation `⊔`, if `c ≤ a` then `c ≤ a ⊔ b`.
`le_of_inf_le_sup_le` theorem le_of_inf_le_sup_le : ∀ {α : Type u} [inst : DistribLattice α] {x y z : α}, x ⊓ z ≤ y ⊓ z → x ⊔ z ≤ y ⊔ z → x ≤ y This theorem asserts that for any type `α` that is a distributive lattice, given any three elements `x`, `y`, and `z` from this type, if the infimum (greatest lower bound) of `x` and `z` is less than or equal to the infimum of `y` and `z`, and the supremum (least upper bound) of `x` and `z` is less than or equal to the supremum of `y` and `z`, then `x` is less than or equal to `y`. This can be viewed as a type of comparative property in the context of lattice theory. More concisely: If `α` is a distributive lattice and `x ≤ inf(y, z)`, `inf(x, z) ≤ inf(y, z)`, and `sup(x, z) ≤ sup(y, z)`, then `x ≤ y`.
`inf_inf_inf_comm` theorem inf_inf_inf_comm : ∀ {α : Type u} [inst : SemilatticeInf α] (a b c d : α), a ⊓ b ⊓ (c ⊓ d) = a ⊓ c ⊓ (b ⊓ d) This theorem, `inf_inf_inf_comm`, states that for all types `α` that form a semilattice under the infimum operation (notated as `⊓`), for any four elements `a`, `b`, `c`, and `d` of type `α`, the infimum of `a`, `b`, and the infimum of `c`, `d` is equal to the infimum of `a`, `c`, and the infimum of `b`, `d`. In other words, written in mathematical notation, regardless of the specific elements, the property $a \land b \land (c \land d) = a \land c \land (b \land d)$ holds for any semilattice. More concisely: For all semilattices α and elements a, b, c, d of type α, the infimum of a, b and the infimum of c, d equals the infimum of a, c and the infimum of b, d. In other words, a ⊓ b ⊓ (c ⊓ d) = a ⊓ c ⊓ b ⊓ d.
`Monotone.sup` theorem Monotone.sup : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : SemilatticeSup β] {f g : α → β}, Monotone f → Monotone g → Monotone (f ⊔ g) The theorem `Monotone.sup` states that for any two monotone functions `f` and `g`, from a preordered set `α` to a semilattice (with supremum operation) `β`, the pointwise supremum of these two functions, denoted as `f ⊔ g`, is also a monotone function. This means that if `a ≤ b` in the preordered set `α`, then `(f ⊔ g) a ≤ (f ⊔ g) b` in the semilattice `β`. More concisely: If `f` and `g` are monotone functions from a preordered set `α` to a semilattice `β` with supremum operation, then `f ⊔ g` is also a monotone function.
`eq_of_inf_eq_sup_eq` theorem eq_of_inf_eq_sup_eq : ∀ {α : Type u} [inst : DistribLattice α] {a b c : α}, b ⊓ a = c ⊓ a → b ⊔ a = c ⊔ a → b = c This theorem states that in a distributive lattice represented by the generic type `α`, given three elements `a`, `b`, and `c`, if the infimum (greatest lower bound) of `b` and `a` equals the infimum of `c` and `a` and the supremum (least upper bound) of `b` and `a` equals the supremum of `c` and `a`, then `b` must equal `c`. It essentially asserts that in such a lattice, the combination of infimum and supremum relationships uniquely determines an element's identity. More concisely: In a distributive lattice, if the infimum of `a` and `b` equals the infimum of `a` and `c` and the supremum of `a` and `b` equals the supremum of `a` and `c`, then `b` equals `c`.
`Mathlib.Order.Lattice._auxLemma.26` theorem Mathlib.Order.Lattice._auxLemma.26 : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, (a ≤ b ⊔ c) = (a ≤ b ∨ a ≤ c) This theorem from the Mathlib Order Lattice library states that, for any type `α` that has a linear order, the inequality `a ≤ b ⊔ c` holds true if and only if `a ≤ b` or `a ≤ c`. Here, `b ⊔ c` represents the least upper bound (or supremum) of `b` and `c`, that is, the smallest element that is greater than both `b` and `c`. Thus, this theorem is essentially a statement about the properties of supremum in a linearly ordered set. More concisely: In a linearly ordered set, for all elements a, b, and c, a is less than or equal to the least upper bound of b and c if and only if a is less than or equal to either b or c.
`semilatticeSup_mk'_partialOrder_eq_semilatticeInf_mk'_partialOrder` theorem semilatticeSup_mk'_partialOrder_eq_semilatticeInf_mk'_partialOrder : ∀ {α : Type u_1} [inst : Sup α] [inst_1 : Inf α] (sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a) (sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)) (sup_idem : ∀ (a : α), a ⊔ a = a) (inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a) (inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)) (inf_idem : ∀ (a : α), a ⊓ a = a), (∀ (a b : α), a ⊔ a ⊓ b = a) → (∀ (a b : α), a ⊓ (a ⊔ b) = a) → SemilatticeSup.toPartialOrder = SemilatticeInf.toPartialOrder The theorem `semilatticeSup_mk'_partialOrder_eq_semilatticeInf_mk'_partialOrder` states that for any type `α` equipped with a supremum (`sup`) and infimum (`inf`) operation, given that the operations satisfy the commutative and associative laws, and are idempotent - that is if `sup` and `inf` of an element with itself equals the element, if, additionally, the absorption laws are satisfied - that is `a ⊔ a ⊓ b = a` and `a ⊓ (a ⊔ b) = a` for all elements `a` and `b` of `α`, then the partial order derived from the semilattice structure by supremum equals to the partial order derived from the semilattice structure by infimum. More concisely: If a type `α` is equipped with a commutative, associative, idempotent supremum and infimum operation that satisfy the absorption laws, then the partial orders derived from the semilattice structure using supremum and infimum are equal.
`Pi.sup_apply` theorem Pi.sup_apply : ∀ {ι : Type u_1} {α' : ι → Type u_2} [inst : (i : ι) → Sup (α' i)] (f g : (i : ι) → α' i) (i : ι), (f ⊔ g) i = f i ⊔ g i This theorem states that for every type `ι`, for every function `α'` mapping each element of `ι` to a type, and given a supremum structure for each `α' i`, for any two functions `f` and `g` from `ι` to `α' i`, and for any `i` in `ι`, the supremum of `f` and `g` at `i` is equal to the supremum of `f i` and `g i`. Essentially, it tells us that the supremum of two functions at a certain point is equivalent to taking the supremum of the function values at that point. More concisely: For every type `ι`, given a supremum structure on each type `α' i`, the supremum of functions `f` and `g` from `ι` to `α' i` at any point `i` is equal to the supremum of `fi` and `gi`.
`le_sup_iff` theorem le_sup_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, a ≤ b ⊔ c ↔ a ≤ b ∨ a ≤ c This theorem, `le_sup_iff`, states that for all types `α` that have a linear order, and for all elements `a`, `b`, and `c` of this type, `a` is less than or equal to the supremum of `b` and `c` if and only if `a` is less than or equal to `b` or `a` is less than or equal to `c`. In other words, an element is less than or equal to the maximum of two other elements if and only if it is less than or equal to at least one of those two elements. More concisely: For all types with a linear order and elements `a`, `b`, `c`, `a ≤ sup from b c` if and only if `a ≤ b` or `a ≤ c`.
`le_of_inf_eq` theorem le_of_inf_eq : ∀ {α : Type u} [inst : SemilatticeInf α] {a b : α}, a ⊓ b = a → a ≤ b This theorem, `le_of_inf_eq`, states that for any type `α` that forms a semilattice under an infimum operation (`⊓`), given any two elements `a` and `b` of type `α`, if the infimum of `a` and `b` equals `a`, then `a` is less than or equal to `b`. In other words, in a semilattice, if the greatest lower bound of two elements is one of them, then the other element is greater than or equal to the first. More concisely: If `α` is a semilattice with infimum operation `⊓`, then `a ⊓ b = a` implies `a ≤ b`.
`Monotone.inf` theorem Monotone.inf : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : SemilatticeInf β] {f g : α → β}, Monotone f → Monotone g → Monotone (f ⊓ g) The theorem `Monotone.inf` states that for any two functions `f` and `g` that map elements from a preordered set `α` to a semilattice `β`, if both `f` and `g` are monotone (meaning that for all `a` and `b` in `α`, if `a ≤ b` then `f(a) ≤ f(b)` and `g(a) ≤ g(b)`), then the pointwise infimum of `f` and `g` (the function that maps any element `x` in `α` to the lesser of `f(x)` and `g(x)`) is also a monotone function. This means that for all `a` and `b` in `α`, if `a ≤ b` then the minimum of `f(a)` and `g(a)` is less than or equal to the minimum of `f(b)` and `g(b)`. More concisely: If `f` and `g` are monotone functions mapping a preordered set to a semilattice, then their pointwise infimum is also a monotone function.
`sup_inf_left` theorem sup_inf_left : ∀ {α : Type u} [inst : DistribLattice α] (a b c : α), a ⊔ b ⊓ c = (a ⊔ b) ⊓ (a ⊔ c) This theorem states that for any distributive lattice of type `α`, and for any three elements `a`, `b`, and `c` of this type, the supremum of `a` and the infimum of `b` and `c`, is equal to the infimum of the supremum of `a` and `b` and the supremum of `a` and `c`. In mathematical terms, it is equivalent to saying that `a ∨ (b ∧ c) = (a ∨ b) ∧ (a ∨ c)` for all `a`, `b`, and `c` in the distributive lattice. This is a basic property of distributive lattices. More concisely: In a distributive lattice, the supremum of any two elements is commutative and associative with respect to the infimum of any other element: `(a ∨ b) ∧ c = a ∨ (b ∧ c)` for all `a`, `b`, and `c`.

LeanAide GPT-4 documentation

Module: Mathlib.Order.Lattice

lt_sup_iff

theorem lt_sup_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, a < b ⊔ c ↔ a < b ∨ a < c

inf_le_inf_right

theorem inf_le_inf_right : ∀ {α : Type u} [inst : SemilatticeInf α] (a : α) {b c : α}, b ≤ c → b ⊓ a ≤ c ⊓ a

sup_sup_distrib_right

theorem sup_sup_distrib_right : ∀ {α : Type u} [inst : SemilatticeSup α] (a b c : α), a ⊔ b ⊔ c = a ⊔ c ⊔ (b ⊔ c) := by sorry

Monotone.map_inf

theorem Monotone.map_inf : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : SemilatticeInf β] {f : α → β}, Monotone f → ∀ (x y : α), f (x ⊓ y) = f x ⊓ f y

AntitoneOn.min

theorem AntitoneOn.min : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : LinearOrder β] {f g : α → β} {s : Set α}, AntitoneOn f s → AntitoneOn g s → AntitoneOn (fun x => min (f x) (g x)) s

MonotoneOn.inf

theorem MonotoneOn.inf : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : SemilatticeInf β] {f g : α → β} {s : Set α}, MonotoneOn f s → MonotoneOn g s → MonotoneOn (f ⊓ g) s

SemilatticeSup.le_sup_left

theorem SemilatticeSup.le_sup_left : ∀ {α : Type u} [self : SemilatticeSup α] (a b : α), a ≤ a ⊔ b

Monotone.of_map_inf

theorem Monotone.of_map_inf : ∀ {α : Type u} {β : Type v} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β] {f : α → β}, (∀ (x y : α), f (x ⊓ y) = f x ⊓ f y) → Monotone f

inf_le_right

theorem inf_le_right : ∀ {α : Type u} [inst : SemilatticeInf α] {a b : α}, a ⊓ b ≤ b

inf_le_left

theorem inf_le_left : ∀ {α : Type u} [inst : SemilatticeInf α] {a b : α}, a ⊓ b ≤ a

sup_lt_iff

theorem sup_lt_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, b ⊔ c < a ↔ b < a ∧ c < a

MonotoneOn.sup

theorem MonotoneOn.sup : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : SemilatticeSup β] {f g : α → β} {s : Set α}, MonotoneOn f s → MonotoneOn g s → MonotoneOn (f ⊔ g) s

Mathlib.Order.Lattice._auxLemma.11

theorem Mathlib.Order.Lattice._auxLemma.11 : ∀ {α : Type u} [inst : SemilatticeInf α] {a b : α}, (a ⊓ b ≤ a) = True

MonotoneOn.max

theorem MonotoneOn.max : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : LinearOrder β] {f g : α → β} {s : Set α}, MonotoneOn f s → MonotoneOn g s → MonotoneOn (fun x => max (f x) (g x)) s

inf_le_of_right_le

theorem inf_le_of_right_le : ∀ {α : Type u} [inst : SemilatticeInf α] {a b c : α}, b ≤ c → a ⊓ b ≤ c

sup_le_sup_right

theorem sup_le_sup_right : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, a ≤ b → ∀ (c : α), a ⊔ c ≤ b ⊔ c := by sorry

inf_inf_distrib_left

theorem inf_inf_distrib_left : ∀ {α : Type u} [inst : SemilatticeInf α] (a b c : α), a ⊓ (b ⊓ c) = a ⊓ b ⊓ (a ⊓ c) := by sorry

sup_ind

theorem sup_ind : ∀ {α : Type u} [inst : LinearOrder α] (a b : α) {p : α → Prop}, p a → p b → p (a ⊔ b)

inf_le_inf

theorem inf_le_inf : ∀ {α : Type u} [inst : SemilatticeInf α] {a b c d : α}, a ≤ b → c ≤ d → a ⊓ c ≤ b ⊓ d

left_lt_sup

theorem left_lt_sup : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, a < a ⊔ b ↔ ¬b ≤ a

Mathlib.Order.Lattice._auxLemma.5

theorem Mathlib.Order.Lattice._auxLemma.5 : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, (a ⊔ b = a) = (b ≤ a)

Antitone.max

theorem Antitone.max : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : LinearOrder β] {f g : α → β}, Antitone f → Antitone g → Antitone fun x => max (f x) (g x)

inf_of_le_right

theorem inf_of_le_right : ∀ {α : Type u} [inst : SemilatticeInf α] {a b : α}, b ≤ a → a ⊓ b = b

Mathlib.Order.Lattice._auxLemma.2

theorem Mathlib.Order.Lattice._auxLemma.2 : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, (b ≤ a ⊔ b) = True := by sorry

inf_idem

theorem inf_idem : ∀ {α : Type u} [inst : SemilatticeInf α] (a : α), a ⊓ a = a

inf_of_le_left

theorem inf_of_le_left : ∀ {α : Type u} [inst : SemilatticeInf α] {a b : α}, a ≤ b → a ⊓ b = a

sup_of_le_right

theorem sup_of_le_right : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, a ≤ b → a ⊔ b = b

sup_eq_left

theorem sup_eq_left : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, a ⊔ b = a ↔ b ≤ a

inf_sup_left

theorem inf_sup_left : ∀ {α : Type u} [inst : DistribLattice α] (a b c : α), a ⊓ (b ⊔ c) = a ⊓ b ⊔ a ⊓ c

inf_eq_min

theorem inf_eq_min : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, a ⊓ b = min a b

inf_le_of_left_le

theorem inf_le_of_left_le : ∀ {α : Type u} [inst : SemilatticeInf α] {a b c : α}, a ≤ c → a ⊓ b ≤ c

sup_assoc

theorem sup_assoc : ∀ {α : Type u} [inst : SemilatticeSup α] (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)

Mathlib.Order.Lattice._auxLemma.12

theorem Mathlib.Order.Lattice._auxLemma.12 : ∀ {α : Type u} [inst : SemilatticeInf α] {a b : α}, (a ⊓ b ≤ b) = True

le_inf_iff

theorem le_inf_iff : ∀ {α : Type u} [inst : SemilatticeInf α] {a b c : α}, a ≤ b ⊓ c ↔ a ≤ b ∧ a ≤ c

inf_assoc

theorem inf_assoc : ∀ {α : Type u} [inst : SemilatticeInf α] (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)

sup_comm

theorem sup_comm : ∀ {α : Type u} [inst : SemilatticeSup α] (a b : α), a ⊔ b = b ⊔ a

Monotone.forall_le_of_antitone

theorem Monotone.forall_le_of_antitone : ∀ {α : Type u} [inst : SemilatticeSup α] {β : Type u_1} [inst_1 : Preorder β] {f g : α → β}, Monotone f → Antitone g → f ≤ g → ∀ (m n : α), f m ≤ g n

MonotoneOn.min

theorem MonotoneOn.min : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : LinearOrder β] {f g : α → β} {s : Set α}, MonotoneOn f s → MonotoneOn g s → MonotoneOn (fun x => min (f x) (g x)) s

le_of_sup_eq

theorem le_of_sup_eq : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, a ⊔ b = b → a ≤ b

`lt_sup_iff`

`inf_le_inf_right`

`sup_sup_distrib_right`

`Monotone.map_inf`

`AntitoneOn.min`

`MonotoneOn.inf`

`SemilatticeSup.le_sup_left`

`Monotone.of_map_inf`

`inf_le_right`

`inf_le_left`

`sup_lt_iff`

`MonotoneOn.sup`

`Mathlib.Order.Lattice._auxLemma.11`

`MonotoneOn.max`

`inf_le_of_right_le`

`sup_le_sup_right`

`inf_inf_distrib_left`

`sup_ind`

`inf_le_inf`

`left_lt_sup`

`Mathlib.Order.Lattice._auxLemma.5`

`Antitone.max`

`inf_of_le_right`

`Mathlib.Order.Lattice._auxLemma.2`

`inf_idem`

`inf_of_le_left`

`sup_of_le_right`

`sup_eq_left`

`inf_sup_left`

`inf_eq_min`

`inf_le_of_left_le`

`sup_assoc`

`Mathlib.Order.Lattice._auxLemma.12`

`le_inf_iff`

`inf_assoc`

`sup_comm`

`Monotone.forall_le_of_antitone`

`MonotoneOn.min`

`le_of_sup_eq`

`AntitoneOn.inf`

`Lattice.le_inf`

`ite_le_sup`

`Mathlib.Order.Lattice._auxLemma.6`

`Monotone.min`

`Lattice.inf_le_left`

`Lattice.inf_le_right`

`sup_le_iff`

`inf_left_comm`

`sup_sup_sup_comm`

`Mathlib.Order.Lattice._auxLemma.10`

`Monotone.map_inf_le`

`AntitoneOn.max`

`sup_idem`

`le_sup_left`

`sup_right_idem`

`inf_le_inf_left`

`le_sup_inf`

`sup_eq_sup_iff_right`

`inf_right_comm`

`inf_comm`

`inf_le_sup`

`Antitone.sup`

`sup_inf_right`

`sup_right_comm`

`Mathlib.Order.Lattice._auxLemma.1`

`inf_eq_left`

`Monotone.max`

`inf_sup_right`

`Monotone.le_map_sup`

`sup_eq_sup_iff_left`

`inf_left_idem`

`Antitone.inf`

`Function.update_inf`

`inf_congr_right`