Mathlib.Order.Lattice

exactSubsetOfSSubset definition

: Mathlib.Tactic.GCongr.ForwardExt

Full source

/-- See if the term is `a ⊂ b` and the goal is `a ⊆ b`. -/
@[gcongr_forward] def exactSubsetOfSSubset : Mathlib.Tactic.GCongr.ForwardExt where
  eval h goal := do goal.assignIfDefEq (← Lean.Meta.mkAppM ``subset_of_ssubset #[h])

Tactic for proving subset from strict subset

Informal description

A tactic that proves `a ⊆ b` when given a hypothesis `a ⊂ b` (strict subset). This is implemented by applying the lemma that any strict subset relation implies the corresponding subset relation.

SemilatticeSup structure

(α : Type u) extends PartialOrder α

Full source

/-- A `SemilatticeSup` is a join-semilattice, that is, a partial order
  with a join (a.k.a. lub / least upper bound, sup / supremum) operation
  `⊔` which is the least element larger than both factors. -/
class SemilatticeSup (α : Type u) extends PartialOrder α where
  /-- The binary supremum, used to derive `Max α` -/
  sup : α → α → α
  /-- The supremum is an upper bound on the first argument -/
  protected le_sup_left : ∀ a b : α, a ≤ sup a b
  /-- The supremum is an upper bound on the second argument -/
  protected le_sup_right : ∀ a b : α, b ≤ sup a b
  /-- The supremum is the *least* upper bound -/
  protected sup_le : ∀ a b c : α, a ≤ c → b ≤ c → sup a b ≤ c

Join-semilattice

Informal description

A join-semilattice is a partially ordered set $(α, \leq)$ equipped with a binary operation $\sqcup$ (called the join or supremum) that satisfies the following properties for all elements $a, b, c \in α$: 1. Commutativity: $a \sqcup b = b \sqcup a$ 2. Associativity: $(a \sqcup b) \sqcup c = a \sqcup (b \sqcup c)$ 3. Idempotency: $a \sqcup a = a$ 4. Least upper bound property: $a \leq a \sqcup b$ and $b \leq a \sqcup b$, and for any $c$ such that $a \leq c$ and $b \leq c$, we have $a \sqcup b \leq c$.

SemilatticeSup.toMax instance

[SemilatticeSup α] : Max α

Full source

instance SemilatticeSup.toMax [SemilatticeSup α] : Max α where max a b := SemilatticeSup.sup a b

Maximum Operation in Join-Semilattices

Informal description

Every join-semilattice $\alpha$ has a canonical maximum operation, where for any two elements $a, b \in \alpha$, the maximum $\max(a, b)$ is defined as their supremum $a \sqcup b$.

SemilatticeSup.mk' definition

 {α : Type*} [Max α] (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) : SemilatticeSup α

Full source

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

The partial order is defined so that `a ≤ b` unfolds to `a ⊔ b = b`; cf. `sup_eq_right`.
-/
def SemilatticeSup.mk' {α : Type*} [Max α] (sup_comm : ∀ a b : α, a ⊔ b = b ⊔ a)
    (sup_assoc : ∀ a b c : α, a ⊔ ba ⊔ b ⊔ c = a ⊔ (b ⊔ c)) (sup_idem : ∀ a : α, a ⊔ a = a) :
    SemilatticeSup α where
  sup := (· ⊔ ·)
  le a b := a ⊔ b = b
  le_refl := sup_idem
  le_trans a b c hab hbc := by rw [← hbc, ← sup_assoc, hab]
  le_antisymm a b hab hba := by rwa [← hba, sup_comm]
  le_sup_left a b := by rw [← sup_assoc, sup_idem]
  le_sup_right a b := by rw [sup_comm, sup_assoc, sup_idem]
  sup_le a b c hac hbc := by rwa [sup_assoc, hbc]

Join-semilattice construction from commutative, associative, idempotent supremum

Informal description

Given a type $\alpha$ with a maximum operation $\sqcup$, if this operation satisfies the following properties for all $a, b, c \in \alpha$: 1. Commutativity: $a \sqcup b = b \sqcup a$ 2. Associativity: $(a \sqcup b) \sqcup c = a \sqcup (b \sqcup c)$ 3. Idempotency: $a \sqcup a = a$ then $\alpha$ can be endowed with the structure of a join-semilattice, where the partial order is defined by $a \leq b$ if and only if $a \sqcup b = b$.

le_sup_left theorem

: a ≤ a ⊔ b

Full source

@[simp]
theorem le_sup_left : a ≤ a ⊔ b :=
  SemilatticeSup.le_sup_left a b

Left Element is Less Than or Equal to Supremum

Informal description

For any elements $a$ and $b$ in a join-semilattice, the element $a$ is less than or equal to the supremum $a \sqcup b$.

le_sup_right theorem

: b ≤ a ⊔ b

Full source

@[simp]
theorem le_sup_right : b ≤ a ⊔ b :=
  SemilatticeSup.le_sup_right a b

Right Element is Less Than or Equal to Supremum

Informal description

For any elements $a$ and $b$ in a join-semilattice, the element $b$ is less than or equal to the supremum $a \sqcup b$.

le_sup_of_le_left theorem

(h : c ≤ a) : c ≤ a ⊔ b

Full source

theorem le_sup_of_le_left (h : c ≤ a) : c ≤ a ⊔ b :=
  le_trans h le_sup_left

Left Inequality Implies Supremum Inequality

Informal description

For any elements $a$, $b$, and $c$ in a join-semilattice, if $c \leq a$, then $c \leq a \sqcup b$.

le_sup_of_le_right theorem

(h : c ≤ b) : c ≤ a ⊔ b

Full source

theorem le_sup_of_le_right (h : c ≤ b) : c ≤ a ⊔ b :=
  le_trans h le_sup_right

Right Inequality Implies Supremum Inequality

Informal description

For any elements $a$, $b$, and $c$ in a join-semilattice, if $c \leq b$, then $c \leq a \sqcup b$.

lt_sup_of_lt_left theorem

(h : c < a) : c < a ⊔ b

Full source

theorem lt_sup_of_lt_left (h : c < a) : c < a ⊔ b :=
  h.trans_le le_sup_left

Strict Inequality Preserved Under Left Supremum

Informal description

For any elements $a$, $b$, and $c$ in a join-semilattice, if $c < a$, then $c < a \sqcup b$.

lt_sup_of_lt_right theorem

(h : c < b) : c < a ⊔ b

Full source

theorem lt_sup_of_lt_right (h : c < b) : c < a ⊔ b :=
  h.trans_le le_sup_right

Strict Inequality Preserved Under Right Supremum

Informal description

For any elements $a$, $b$, and $c$ in a join-semilattice, if $c < b$, then $c < a \sqcup b$.

sup_le theorem

: a ≤ c → b ≤ c → a ⊔ b ≤ c

Full source

theorem sup_le : a ≤ c → b ≤ c → a ⊔ b ≤ c :=
  SemilatticeSup.sup_le a b c

Supremum is Least Upper Bound in Join-Semilattices

Informal description

For any elements $a$, $b$, and $c$ in a join-semilattice, if $a \leq c$ and $b \leq c$, then the supremum $a \sqcup b$ is also less than or equal to $c$.

sup_le_iff theorem

: a ⊔ b ≤ c ↔ a ≤ c ∧ b ≤ c

Full source

@[simp]
theorem sup_le_iff : a ⊔ ba ⊔ b ≤ c ↔ a ≤ c ∧ b ≤ c :=
  ⟨fun h : a ⊔ b ≤ c => ⟨le_trans le_sup_left h, le_trans le_sup_right h⟩,
   fun ⟨h₁, h₂⟩ => sup_le h₁ h₂⟩

Supremum Bound Criterion: $a \sqcup b \leq c \leftrightarrow (a \leq c \land b \leq c)$

Informal description

For any elements $a$, $b$, and $c$ in a join-semilattice, the supremum $a \sqcup b$ is less than or equal to $c$ if and only if both $a \leq c$ and $b \leq c$.

sup_eq_left theorem

: a ⊔ b = a ↔ b ≤ a

Full source

@[simp]
theorem sup_eq_left : a ⊔ ba ⊔ b = a ↔ b ≤ a :=
  le_antisymm_iff.trans <| by simp [le_rfl]

Supremum Equals Left Operand iff Right Operand is Less Than or Equal

Informal description

For any elements $a$ and $b$ in a join-semilattice, the supremum $a \sqcup b$ equals $a$ if and only if $b \leq a$.

sup_eq_right theorem

: a ⊔ b = b ↔ a ≤ b

Full source

@[simp]
theorem sup_eq_right : a ⊔ ba ⊔ b = b ↔ a ≤ b :=
  le_antisymm_iff.trans <| by simp [le_rfl]

Supremum Equals Right Operand iff Left Operand is Less Than or Equal

Informal description

For any elements $a$ and $b$ in a join-semilattice, the supremum $a \sqcup b$ equals $b$ if and only if $a \leq b$.

left_eq_sup theorem

: a = a ⊔ b ↔ b ≤ a

Full source

@[simp]
theorem left_eq_sup : a = a ⊔ b ↔ b ≤ a :=
  eq_comm.trans sup_eq_left

Left Equals Supremum iff Right is Less Than or Equal

Informal description

For any elements $a$ and $b$ in a join-semilattice, the equality $a = a \sqcup b$ holds if and only if $b \leq a$.

right_eq_sup theorem

: b = a ⊔ b ↔ a ≤ b

Full source

@[simp]
theorem right_eq_sup : b = a ⊔ b ↔ a ≤ b :=
  eq_comm.trans sup_eq_right

Right Element Equals Supremum iff Left Element is Less Than or Equal

Informal description

For any elements $a$ and $b$ in a join-semilattice, the equality $b = a \sqcup b$ holds if and only if $a \leq b$.

left_lt_sup theorem

: a < a ⊔ b ↔ ¬b ≤ a

Full source

@[simp]
theorem left_lt_sup : a < a ⊔ b ↔ ¬b ≤ a :=
  le_sup_left.lt_iff_ne.trans <| not_congr left_eq_sup

Left Element Strictly Less Than Supremum iff Right Element Not Below

Informal description

For any elements $a$ and $b$ in a join-semilattice, the strict inequality $a < a \sqcup b$ holds if and only if $b$ is not less than or equal to $a$.

right_lt_sup theorem

: b < a ⊔ b ↔ ¬a ≤ b

Full source

@[simp]
theorem right_lt_sup : b < a ⊔ b ↔ ¬a ≤ b :=
  le_sup_right.lt_iff_ne.trans <| not_congr right_eq_sup

Strict Supremum Inequality on the Right: $b < a \sqcup b \leftrightarrow a \nleq b$

Informal description

For any elements $a$ and $b$ in a join-semilattice, the element $b$ is strictly less than the supremum $a \sqcup b$ if and only if $a$ is not less than or equal to $b$.

left_or_right_lt_sup theorem

(h : a ≠ b) : a < a ⊔ b ∨ b < a ⊔ b

Full source

theorem left_or_right_lt_sup (h : a ≠ b) : a < a ⊔ b ∨ b < a ⊔ b :=
  h.not_le_or_not_le.symm.imp left_lt_sup.2 right_lt_sup.2

Strict Supremum Inequality for Distinct Elements: $a \neq b \Rightarrow a < a \sqcup b \lor b < a \sqcup b$

Informal description

For any distinct elements $a$ and $b$ in a join-semilattice, either $a$ is strictly less than their supremum $a \sqcup b$, or $b$ is strictly less than $a \sqcup b$.

le_iff_exists_sup theorem

: a ≤ b ↔ ∃ c, b = a ⊔ c

Full source

theorem le_iff_exists_sup : a ≤ b ↔ ∃ c, b = a ⊔ c := by
  constructor
  · intro h
    exact ⟨b, (sup_eq_right.mpr h).symm⟩
  · rintro ⟨c, rfl : _ = _ ⊔ _⟩
    exact le_sup_left

Characterization of Order via Supremum Existence

Informal description

For any elements $a$ and $b$ in a join-semilattice, $a$ is less than or equal to $b$ if and only if there exists an element $c$ such that $b$ equals the supremum of $a$ and $c$ (i.e., $b = a \sqcup c$).

sup_le_sup theorem

(h₁ : a ≤ b) (h₂ : c ≤ d) : a ⊔ c ≤ b ⊔ d

Full source

@[gcongr]
theorem sup_le_sup (h₁ : a ≤ b) (h₂ : c ≤ d) : a ⊔ c ≤ b ⊔ d :=
  sup_le (le_sup_of_le_left h₁) (le_sup_of_le_right h₂)

Monotonicity of Supremum Operation: $a \leq b \land c \leq d \Rightarrow a \sqcup c \leq b \sqcup d$

Informal description

For any elements $a, b, c, d$ in a join-semilattice, if $a \leq b$ and $c \leq d$, then the supremum $a \sqcup c$ is less than or equal to the supremum $b \sqcup d$.

sup_le_sup_left theorem

(h₁ : a ≤ b) (c) : c ⊔ a ≤ c ⊔ b

Full source

@[gcongr]
theorem sup_le_sup_left (h₁ : a ≤ b) (c) : c ⊔ a ≤ c ⊔ b :=
  sup_le_sup le_rfl h₁

Left Monotonicity of Supremum Operation: $a \leq b \Rightarrow c \sqcup a \leq c \sqcup b$

Informal description

For any elements $a$, $b$, and $c$ in a join-semilattice, if $a \leq b$, then the supremum $c \sqcup a$ is less than or equal to the supremum $c \sqcup b$.

sup_le_sup_right theorem

(h₁ : a ≤ b) (c) : a ⊔ c ≤ b ⊔ c

Full source

@[gcongr]
theorem sup_le_sup_right (h₁ : a ≤ b) (c) : a ⊔ c ≤ b ⊔ c :=
  sup_le_sup h₁ le_rfl

Right Monotonicity of Join Operation: $a \leq b \Rightarrow a \sqcup c \leq b \sqcup c$

Informal description

For any elements $a, b, c$ in a join-semilattice, if $a \leq b$, then $a \sqcup c \leq b \sqcup c$.

sup_idem theorem

(a : α) : a ⊔ a = a

Full source

theorem sup_idem (a : α) : a ⊔ a = a := by simp

Idempotency of Join Operation in Semilattices

Informal description

For any element $a$ in a join-semilattice $\alpha$, the join (supremum) of $a$ with itself equals $a$, i.e., $a \sqcup a = a$.

instIdempotentOpMax_mathlib instance

: Std.IdempotentOp (α := α) (· ⊔ ·)

Full source

instance : Std.IdempotentOp (α := α) (· ⊔ ·) := ⟨sup_idem⟩

Idempotency of the Join Operation in Join-Semilattices

Informal description

The join operation $\sqcup$ in a join-semilattice $\alpha$ is idempotent, meaning that for any element $a \in \alpha$, we have $a \sqcup a = a$.

sup_comm theorem

(a b : α) : a ⊔ b = b ⊔ a

Full source

theorem sup_comm (a b : α) : a ⊔ b = b ⊔ a := by apply le_antisymm <;> simp

Commutativity of Join Operation in Semilattices

Informal description

For any elements $a$ and $b$ in a join-semilattice $\alpha$, the join operation $\sqcup$ is commutative, i.e., $a \sqcup b = b \sqcup a$.

instCommutativeMax_mathlib instance

: Std.Commutative (α := α) (· ⊔ ·)

Full source

instance : Std.Commutative (α := α) (· ⊔ ·) := ⟨sup_comm⟩

Commutativity of Join Operation in Semilattices

Informal description

The join operation $\sqcup$ in a join-semilattice $\alpha$ is commutative.

sup_assoc theorem

(a b c : α) : a ⊔ b ⊔ c = a ⊔ (b ⊔ c)

Full source

theorem sup_assoc (a b c : α) : a ⊔ ba ⊔ b ⊔ c = a ⊔ (b ⊔ c) :=
  eq_of_forall_ge_iff fun x => by simp only [sup_le_iff]; rw [and_assoc]

Associativity of Join Operation in Semilattices

Informal description

In a join-semilattice $\alpha$, the join operation $\sqcup$ is associative. That is, for any elements $a, b, c \in \alpha$, we have $(a \sqcup b) \sqcup c = a \sqcup (b \sqcup c)$.

instAssociativeMax_mathlib instance

: Std.Associative (α := α) (· ⊔ ·)

Full source

instance : Std.Associative (α := α) (· ⊔ ·) := ⟨sup_assoc⟩

Associativity of Join Operation in Semilattices

Informal description

The join operation $\sqcup$ in a join-semilattice $\alpha$ is associative.

sup_left_right_swap theorem

(a b c : α) : a ⊔ b ⊔ c = c ⊔ b ⊔ a

Full source

theorem sup_left_right_swap (a b c : α) : a ⊔ ba ⊔ b ⊔ c = c ⊔ bc ⊔ b ⊔ a := by
  rw [sup_comm, sup_comm a, sup_assoc]

Left-Right Swap Property of Join Operation in Semilattices

Informal description

In a join-semilattice $\alpha$, for any elements $a, b, c \in \alpha$, the join operation satisfies $(a \sqcup b) \sqcup c = (c \sqcup b) \sqcup a$.

sup_left_idem theorem

(a b : α) : a ⊔ (a ⊔ b) = a ⊔ b

Full source

theorem sup_left_idem (a b : α) : a ⊔ (a ⊔ b) = a ⊔ b := by simp

Left Idempotency of Join Operation in Semilattices

Informal description

In a join-semilattice $\alpha$, for any elements $a, b \in \alpha$, the join operation satisfies $a \sqcup (a \sqcup b) = a \sqcup b$.

sup_right_idem theorem

(a b : α) : a ⊔ b ⊔ b = a ⊔ b

Full source

theorem sup_right_idem (a b : α) : a ⊔ ba ⊔ b ⊔ b = a ⊔ b := by simp

Right Idempotency of Join Operation in Semilattices

Informal description

In a join-semilattice $\alpha$, for any elements $a, b \in \alpha$, the join operation satisfies $(a \sqcup b) \sqcup b = a \sqcup b$.

sup_left_comm theorem

(a b c : α) : a ⊔ (b ⊔ c) = b ⊔ (a ⊔ c)

Full source

theorem sup_left_comm (a b c : α) : a ⊔ (b ⊔ c) = b ⊔ (a ⊔ c) := by
  rw [← sup_assoc, ← sup_assoc, @sup_comm α _ a]

Left Commutativity of Join Operation in Semilattices: $a \sqcup (b \sqcup c) = b \sqcup (a \sqcup c)$

Informal description

In a join-semilattice $\alpha$, for any elements $a, b, c \in \alpha$, the join operation satisfies the left commutativity property: $$a \sqcup (b \sqcup c) = b \sqcup (a \sqcup c)$$

sup_right_comm theorem

(a b c : α) : a ⊔ b ⊔ c = a ⊔ c ⊔ b

Full source

theorem sup_right_comm (a b c : α) : a ⊔ ba ⊔ b ⊔ c = a ⊔ ca ⊔ c ⊔ b := by
  rw [sup_assoc, sup_assoc, sup_comm b]

Right Commutativity of Join Operation in Semilattices

Informal description

In a join-semilattice $\alpha$, for any elements $a, b, c \in \alpha$, the join operation satisfies $(a \sqcup b) \sqcup c = (a \sqcup c) \sqcup b$.

sup_sup_sup_comm theorem

(a b c d : α) : a ⊔ b ⊔ (c ⊔ d) = a ⊔ c ⊔ (b ⊔ d)

Full source

theorem sup_sup_sup_comm (a b c d : α) : a ⊔ ba ⊔ b ⊔ (c ⊔ d) = a ⊔ ca ⊔ c ⊔ (b ⊔ d) := by
  rw [sup_assoc, sup_left_comm b, ← sup_assoc]

Commutativity of Quadruple Join Operation: $a \sqcup b \sqcup (c \sqcup d) = a \sqcup c \sqcup (b \sqcup d)$

Informal description

In a join-semilattice $\alpha$, for any elements $a, b, c, d \in \alpha$, the join operation satisfies the following commutativity property: $$a \sqcup b \sqcup (c \sqcup d) = a \sqcup c \sqcup (b \sqcup d)$$

sup_sup_distrib_left theorem

(a b c : α) : a ⊔ (b ⊔ c) = a ⊔ b ⊔ (a ⊔ c)

Full source

theorem sup_sup_distrib_left (a b c : α) : a ⊔ (b ⊔ c) = a ⊔ ba ⊔ b ⊔ (a ⊔ c) := by
  rw [sup_sup_sup_comm, sup_idem]

Left Distributivity of Join Operation in Semilattices

Informal description

In a join-semilattice $\alpha$, for any elements $a, b, c \in \alpha$, the join operation satisfies the left distributivity property: $$a \sqcup (b \sqcup c) = (a \sqcup b) \sqcup (a \sqcup c)$$

sup_sup_distrib_right theorem

(a b c : α) : a ⊔ b ⊔ c = a ⊔ c ⊔ (b ⊔ c)

Full source

theorem sup_sup_distrib_right (a b c : α) : a ⊔ ba ⊔ b ⊔ c = a ⊔ ca ⊔ c ⊔ (b ⊔ c) := by
  rw [sup_sup_sup_comm, sup_idem]

Right-Distributivity of Join Operation in Semilattices

Informal description

In a join-semilattice $\alpha$, for any elements $a, b, c \in \alpha$, the join operation satisfies the following right-distributivity property: $$a \sqcup b \sqcup c = a \sqcup c \sqcup (b \sqcup c)$$

sup_congr_left theorem

(hb : b ≤ a ⊔ c) (hc : c ≤ a ⊔ b) : a ⊔ b = a ⊔ c

Full source

theorem sup_congr_left (hb : b ≤ a ⊔ c) (hc : c ≤ a ⊔ b) : a ⊔ b = a ⊔ c :=
  (sup_le le_sup_left hb).antisymm <| sup_le le_sup_left hc

Supremum Congruence under Left Absorption Conditions

Informal description

For any elements $a$, $b$, and $c$ in a join-semilattice, if $b \leq a \sqcup c$ and $c \leq a \sqcup b$, then the suprema $a \sqcup b$ and $a \sqcup c$ are equal, i.e., $a \sqcup b = a \sqcup c$.

sup_congr_right theorem

(ha : a ≤ b ⊔ c) (hb : b ≤ a ⊔ c) : a ⊔ c = b ⊔ c

Full source

theorem sup_congr_right (ha : a ≤ b ⊔ c) (hb : b ≤ a ⊔ c) : a ⊔ c = b ⊔ c :=
  (sup_le ha le_sup_right).antisymm <| sup_le hb le_sup_right

Supremum Congruence under Right Absorption Conditions

Informal description

For any elements $a$, $b$, and $c$ in a join-semilattice, if $a \leq b \sqcup c$ and $b \leq a \sqcup c$, then the suprema $a \sqcup c$ and $b \sqcup c$ are equal, i.e., $a \sqcup c = b \sqcup c$.

sup_eq_sup_iff_left theorem

: a ⊔ b = a ⊔ c ↔ b ≤ a ⊔ c ∧ c ≤ a ⊔ b

Full source

theorem sup_eq_sup_iff_left : a ⊔ ba ⊔ b = a ⊔ c ↔ b ≤ a ⊔ c ∧ c ≤ a ⊔ b :=
  ⟨fun h => ⟨h ▸ le_sup_right, h.symm ▸ le_sup_right⟩, fun h => sup_congr_left h.1 h.2⟩

Equality of Left Suprema in Join-Semilattices

Informal description

For any elements $a$, $b$, and $c$ in a join-semilattice, the supremum $a \sqcup b$ equals $a \sqcup c$ if and only if $b \leq a \sqcup c$ and $c \leq a \sqcup b$.

sup_eq_sup_iff_right theorem

: a ⊔ c = b ⊔ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c

Full source

theorem sup_eq_sup_iff_right : a ⊔ ca ⊔ c = b ⊔ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c :=
  ⟨fun h => ⟨h ▸ le_sup_left, h.symm ▸ le_sup_left⟩, fun h => sup_congr_right h.1 h.2⟩

Supremum Equality Criterion via Right Absorption Conditions

Informal description

For any elements $a$, $b$, and $c$ in a join-semilattice, the equality $a \sqcup c = b \sqcup c$ holds if and only if $a \leq b \sqcup c$ and $b \leq a \sqcup c$.

Ne.lt_sup_or_lt_sup theorem

(hab : a ≠ b) : a < a ⊔ b ∨ b < a ⊔ b

Full source

theorem Ne.lt_sup_or_lt_sup (hab : a ≠ b) : a < a ⊔ b ∨ b < a ⊔ b :=
  hab.symm.not_le_or_not_le.imp left_lt_sup.2 right_lt_sup.2

Strict Supremum Inequality for Distinct Elements in Join-Semilattices

Informal description

For any two distinct elements $a$ and $b$ in a join-semilattice, either $a$ is strictly less than their supremum $a \sqcup b$, or $b$ is strictly less than $a \sqcup b$.

Monotone.forall_le_of_antitone theorem

{β : Type*} [Preorder β] {f g : α → β} (hf : Monotone f) (hg : Antitone g) (h : f ≤ g) (m n : α) : f m ≤ g n

Full source

/-- If `f` is monotone, `g` is antitone, and `f ≤ g`, then for all `a`, `b` we have `f a ≤ g b`. -/
theorem Monotone.forall_le_of_antitone {β : Type*} [Preorder β] {f g : α → β} (hf : Monotone f)
    (hg : Antitone g) (h : f ≤ g) (m n : α) : f m ≤ g n :=
  calc
    f m ≤ f (m ⊔ n) := hf le_sup_left
    _ ≤ g (m ⊔ n) := h _
    _ ≤ g n := hg le_sup_right

Monotone and Antitone Functions with Pointwise Inequality

Informal description

Let $\alpha$ and $\beta$ be preordered sets, and let $f, g : \alpha \to \beta$ be functions. If $f$ is monotone, $g$ is antitone, and $f \leq g$ (pointwise), then for all $a, b \in \alpha$, we have $f(a) \leq g(b)$.

SemilatticeSup.ext_sup theorem

 {α} {A B : SemilatticeSup α}
  (H :
    ∀ x y : α,
      (haveI := A;
        x ≤ y) ↔
        x ≤ y)
  (x y : α) :
  (haveI := A;
    x ⊔ y) =
    x ⊔ y

Full source

theorem SemilatticeSup.ext_sup {α} {A B : SemilatticeSup α}
    (H : ∀ x y : α, (haveI := A; x ≤ y) ↔ x ≤ y)
    (x y : α) :
    (haveI := A; x ⊔ y) = x ⊔ y :=
  eq_of_forall_ge_iff fun c => by simp only [sup_le_iff]; rw [← H, @sup_le_iff α A, H, H]

Supremum Equality for Equivalent Join-Semilattice Structures

Informal description

Let $\alpha$ be a type, and let $A$ and $B$ be two join-semilattice structures on $\alpha$ such that for all $x, y \in \alpha$, the order relation $x \leq y$ under $A$ is equivalent to $x \leq y$ under $B$. Then for any $x, y \in \alpha$, the supremum $x \sqcup y$ computed in $A$ is equal to the supremum $x \sqcup y$ computed in $B$.

SemilatticeSup.ext theorem

 {α} {A B : SemilatticeSup α}
  (H :
    ∀ x y : α,
      (haveI := A;
        x ≤ y) ↔
        x ≤ y) :
  A = B

Full source

theorem SemilatticeSup.ext {α} {A B : SemilatticeSup α}
    (H : ∀ x y : α, (haveI := A; x ≤ y) ↔ x ≤ y) :
    A = B := by
  cases A
  cases B
  cases PartialOrder.ext H
  congr
  ext; apply SemilatticeSup.ext_sup H

Equality of Join-Semilattice Structures with Equivalent Order Relations

Informal description

Let $\alpha$ be a type, and let $A$ and $B$ be two join-semilattice structures on $\alpha$ such that for all $x, y \in \alpha$, the order relation $x \leq y$ under $A$ is equivalent to $x \leq y$ under $B$. Then the two join-semilattice structures $A$ and $B$ are equal.

ite_le_sup theorem

(s s' : α) (P : Prop) [Decidable P] : ite P s s' ≤ s ⊔ s'

Full source

theorem ite_le_sup (s s' : α) (P : Prop) [Decidable P] : ite P s s' ≤ s ⊔ s' :=
  if h : P then (if_pos h).trans_le le_sup_left else (if_neg h).trans_le le_sup_right

Conditional Element is Bounded by Supremum

Informal description

For any elements $s$ and $s'$ in a join-semilattice $\alpha$, and any decidable proposition $P$, the element $\text{ite}(P, s, s')$ (which equals $s$ if $P$ is true and $s'$ otherwise) is less than or equal to the supremum $s \sqcup s'$.

SemilatticeInf structure

(α : Type u) extends PartialOrder α

Full source

/-- A `SemilatticeInf` is a meet-semilattice, that is, a partial order
  with a meet (a.k.a. glb / greatest lower bound, inf / infimum) operation
  `⊓` which is the greatest element smaller than both factors. -/
class SemilatticeInf (α : Type u) extends PartialOrder α where
  /-- The binary infimum, used to derive `Min α` -/
  inf : α → α → α
  /-- The infimum is a lower bound on the first argument -/
  protected inf_le_left : ∀ a b : α, inf a b ≤ a
  /-- The infimum is a lower bound on the second argument -/
  protected inf_le_right : ∀ a b : α, inf a b ≤ b
  /-- The infimum is the *greatest* lower bound -/
  protected le_inf : ∀ a b c : α, a ≤ b → a ≤ c → a ≤ inf b c

Meet-semilattice

Informal description

A meet-semilattice is a partially ordered set equipped with a meet operation $\sqcap$ (greatest lower bound or infimum), such that for any two elements $a$ and $b$, $a \sqcap b$ is the greatest element less than or equal to both $a$ and $b$.

SemilatticeInf.toMin instance

[SemilatticeInf α] : Min α

Full source

instance SemilatticeInf.toMin [SemilatticeInf α] : Min α where min a b := SemilatticeInf.inf a b

Minimum Operation from Meet-Semilattice

Informal description

Every meet-semilattice $\alpha$ has a canonical minimum operation.

OrderDual.instSemilatticeSup instance

(α) [SemilatticeInf α] : SemilatticeSup αᵒᵈ

Full source

instance OrderDual.instSemilatticeSup (α) [SemilatticeInf α] : SemilatticeSup αᵒᵈ where
  sup := @SemilatticeInf.inf α _
  le_sup_left := @SemilatticeInf.inf_le_left α _
  le_sup_right := @SemilatticeInf.inf_le_right α _
  sup_le := fun _ _ _ hca hcb => @SemilatticeInf.le_inf α _ _ _ _ hca hcb

Order Dual of a Meet-Semilattice is a Join-Semilattice

Informal description

For any meet-semilattice $\alpha$, the order dual $\alpha^{\text{op}}$ is a join-semilattice.

OrderDual.instSemilatticeInf instance

(α) [SemilatticeSup α] : SemilatticeInf αᵒᵈ

Full source

instance OrderDual.instSemilatticeInf (α) [SemilatticeSup α] : SemilatticeInf αᵒᵈ where
  inf := @SemilatticeSup.sup α _
  inf_le_left := @le_sup_left α _
  inf_le_right := @le_sup_right α _
  le_inf := fun _ _ _ hca hcb => @sup_le α _ _ _ _ hca hcb

Order Dual of a Join-Semilattice is a Meet-Semilattice

Informal description

For any join-semilattice $\alpha$, the order dual $\alpha^{\text{op}}$ is a meet-semilattice.

SemilatticeSup.dual_dual theorem

(α : Type*) [H : SemilatticeSup α] : OrderDual.instSemilatticeSup αᵒᵈ = H

Full source

theorem SemilatticeSup.dual_dual (α : Type*) [H : SemilatticeSup α] :
    OrderDual.instSemilatticeSup αᵒᵈ = H :=
  SemilatticeSup.ext fun _ _ => Iff.rfl

Double Order Dual of a Join-Semilattice Equals Original Structure

Informal description

For any type $\alpha$ equipped with a join-semilattice structure $H$, the order dual of the order dual of $\alpha$ (i.e., $(\alpha^{\text{op}})^{\text{op}}$) is equal to the original join-semilattice structure $H$ on $\alpha$.

inf_le_left theorem

: a ⊓ b ≤ a

Full source

@[simp]
theorem inf_le_left : a ⊓ b ≤ a :=
  SemilatticeInf.inf_le_left a b

Infimum is Less Than or Equal to Left Argument

Informal description

For any elements $a$ and $b$ in a meet-semilattice, the infimum $a \sqcap b$ is less than or equal to $a$.

inf_le_right theorem

: a ⊓ b ≤ b

Full source

@[simp]
theorem inf_le_right : a ⊓ b ≤ b :=
  SemilatticeInf.inf_le_right a b

Infimum is Less Than or Equal to Right Argument

Informal description

For any elements $a$ and $b$ in a meet-semilattice, the infimum $a \sqcap b$ is less than or equal to $b$.

le_inf theorem

: a ≤ b → a ≤ c → a ≤ b ⊓ c

Full source

theorem le_inf : a ≤ b → a ≤ c → a ≤ b ⊓ c :=
  SemilatticeInf.le_inf a b c

Greatest Lower Bound Property in Meet-Semilattices

Informal description

For any elements $a$, $b$, and $c$ in a meet-semilattice, if $a \leq b$ and $a \leq c$, then $a \leq b \sqcap c$.

inf_le_of_left_le theorem

(h : a ≤ c) : a ⊓ b ≤ c

Full source

theorem inf_le_of_left_le (h : a ≤ c) : a ⊓ b ≤ c :=
  le_trans inf_le_left h

Infimum is Less Than or Equal to Right Argument When Left Argument Is

Informal description

For any elements $a$, $b$, and $c$ in a meet-semilattice, if $a \leq c$, then the infimum $a \sqcap b$ is less than or equal to $c$.

inf_le_of_right_le theorem

(h : b ≤ c) : a ⊓ b ≤ c

Full source

theorem inf_le_of_right_le (h : b ≤ c) : a ⊓ b ≤ c :=
  le_trans inf_le_right h

Infimum is Less Than or Equal to Right Argument When Right Argument Is

Informal description

For any elements $a$, $b$, and $c$ in a meet-semilattice, if $b \leq c$, then the infimum $a \sqcap b$ is less than or equal to $c$.

inf_lt_of_left_lt theorem

(h : a < c) : a ⊓ b < c

Full source

theorem inf_lt_of_left_lt (h : a < c) : a ⊓ b < c :=
  lt_of_le_of_lt inf_le_left h

Infimum is Strictly Less Than Right Argument When Left Argument Is

Informal description

For any elements $a$, $b$, and $c$ in a meet-semilattice, if $a < c$, then the infimum $a \sqcap b$ is strictly less than $c$.

inf_lt_of_right_lt theorem

(h : b < c) : a ⊓ b < c

Full source

theorem inf_lt_of_right_lt (h : b < c) : a ⊓ b < c :=
  lt_of_le_of_lt inf_le_right h

Infimum is Strictly Less Than Right Argument When Right Argument Is

Informal description

For any elements $a$, $b$, and $c$ in a meet-semilattice, if $b < c$, then the infimum $a \sqcap b$ is strictly less than $c$.

le_inf_iff theorem

: a ≤ b ⊓ c ↔ a ≤ b ∧ a ≤ c

Full source

@[simp]
theorem le_inf_iff : a ≤ b ⊓ c ↔ a ≤ b ∧ a ≤ c :=
  @sup_le_iff αᵒᵈ _ _ _ _

Characterization of Infimum Bound: $a \leq b \sqcap c \leftrightarrow (a \leq b \land a \leq c)$

Informal description

For any elements $a$, $b$, and $c$ in a meet-semilattice, the inequality $a \leq b \sqcap c$ holds if and only if both $a \leq b$ and $a \leq c$ hold.

inf_eq_left theorem

: a ⊓ b = a ↔ a ≤ b

Full source

@[simp]
theorem inf_eq_left : a ⊓ ba ⊓ b = a ↔ a ≤ b :=
  le_antisymm_iff.trans <| by simp [le_rfl]

Meet Equals Left Element if and only if Left is Less Than or Equal to Right

Informal description

For elements $a$ and $b$ in a meet-semilattice, the meet $a \sqcap b$ equals $a$ if and only if $a$ is less than or equal to $b$.

inf_eq_right theorem

: a ⊓ b = b ↔ b ≤ a

Full source

@[simp]
theorem inf_eq_right : a ⊓ ba ⊓ b = b ↔ b ≤ a :=
  le_antisymm_iff.trans <| by simp [le_rfl]

Meet Equals Right Element if and only if Right is Less Than or Equal to Left

Informal description

For any elements $a$ and $b$ in a meet-semilattice, the meet $a \sqcap b$ equals $b$ if and only if $b \leq a$.

left_eq_inf theorem

: a = a ⊓ b ↔ a ≤ b

Full source

@[simp]
theorem left_eq_inf : a = a ⊓ b ↔ a ≤ b :=
  eq_comm.trans inf_eq_left

Left Element Equals Meet if and only if Left is Less Than or Equal to Right

Informal description

For elements $a$ and $b$ in a meet-semilattice, $a$ equals the meet $a \sqcap b$ if and only if $a$ is less than or equal to $b$.

right_eq_inf theorem

: b = a ⊓ b ↔ b ≤ a

Full source

@[simp]
theorem right_eq_inf : b = a ⊓ b ↔ b ≤ a :=
  eq_comm.trans inf_eq_right

Right Element Equals Meet if and only if Right is Less Than or Equal to Left

Informal description

For any elements $a$ and $b$ in a meet-semilattice, the equality $b = a \sqcap b$ holds if and only if $b \leq a$.

inf_lt_left theorem

: a ⊓ b < a ↔ ¬a ≤ b

Full source

@[simp]
theorem inf_lt_left : a ⊓ ba ⊓ b < a ↔ ¬a ≤ b :=
  @left_lt_sup αᵒᵈ _ _ _

Meet Strictly Less Than Left Element if and only if Left Not Below Right

Informal description

For any elements $a$ and $b$ in a meet-semilattice, the strict inequality $a \sqcap b < a$ holds if and only if $a$ is not less than or equal to $b$.

inf_lt_right theorem

: a ⊓ b < b ↔ ¬b ≤ a

Full source

@[simp]
theorem inf_lt_right : a ⊓ ba ⊓ b < b ↔ ¬b ≤ a :=
  @right_lt_sup αᵒᵈ _ _ _

Strict Infimum Inequality on the Right: $a \sqcap b < b \leftrightarrow b \nleq a$

Informal description

For any elements $a$ and $b$ in a meet-semilattice, the infimum $a \sqcap b$ is strictly less than $b$ if and only if $b$ is not less than or equal to $a$.

inf_lt_left_or_right theorem

(h : a ≠ b) : a ⊓ b < a ∨ a ⊓ b < b

Full source

theorem inf_lt_left_or_right (h : a ≠ b) : a ⊓ ba ⊓ b < a ∨ a ⊓ b < b :=
  @left_or_right_lt_sup αᵒᵈ _ _ _ h

Strict Infimum Inequality for Distinct Elements: $a \neq b \Rightarrow a \sqcap b < a \lor a \sqcap b < b$

Informal description

For any distinct elements $a$ and $b$ in a meet-semilattice, either their infimum $a \sqcap b$ is strictly less than $a$, or $a \sqcap b$ is strictly less than $b$.

inf_le_inf theorem

(h₁ : a ≤ b) (h₂ : c ≤ d) : a ⊓ c ≤ b ⊓ d

Full source

@[gcongr]
theorem inf_le_inf (h₁ : a ≤ b) (h₂ : c ≤ d) : a ⊓ c ≤ b ⊓ d :=
  @sup_le_sup αᵒᵈ _ _ _ _ _ h₁ h₂

Monotonicity of Infimum Operation: $a \leq b \land c \leq d \Rightarrow a \sqcap c \leq b \sqcap d$

Informal description

For any elements $a, b, c, d$ in a meet-semilattice, if $a \leq b$ and $c \leq d$, then the infimum $a \sqcap c$ is less than or equal to the infimum $b \sqcap d$.

inf_le_inf_right theorem

(a : α) {b c : α} (h : b ≤ c) : b ⊓ a ≤ c ⊓ a

Full source

@[gcongr]
theorem inf_le_inf_right (a : α) {b c : α} (h : b ≤ c) : b ⊓ a ≤ c ⊓ a :=
  inf_le_inf h le_rfl

Right Monotonicity of Infimum Operation: $b \leq c \Rightarrow b \sqcap a \leq c \sqcap a$

Informal description

For any element $a$ in a meet-semilattice $\alpha$, and for any elements $b, c \in \alpha$ such that $b \leq c$, the infimum $b \sqcap a$ is less than or equal to the infimum $c \sqcap a$.

inf_le_inf_left theorem

(a : α) {b c : α} (h : b ≤ c) : a ⊓ b ≤ a ⊓ c

Full source

@[gcongr]
theorem inf_le_inf_left (a : α) {b c : α} (h : b ≤ c) : a ⊓ b ≤ a ⊓ c :=
  inf_le_inf le_rfl h

Left Monotonicity of Infimum Operation: $b \leq c \Rightarrow a \sqcap b \leq a \sqcap c$

Informal description

For any elements $a, b, c$ in a meet-semilattice $\alpha$, if $b \leq c$, then the infimum $a \sqcap b$ is less than or equal to the infimum $a \sqcap c$.

inf_idem theorem

(a : α) : a ⊓ a = a

Full source

theorem inf_idem (a : α) : a ⊓ a = a := by simp

Idempotence of Meet Operation: $a \sqcap a = a$

Informal description

For any element $a$ in a meet-semilattice $\alpha$, the meet (infimum) of $a$ with itself is equal to $a$, i.e., $a \sqcap a = a$.

instIdempotentOpMin_mathlib instance

: Std.IdempotentOp (α := α) (· ⊓ ·)

Full source

instance : Std.IdempotentOp (α := α) (· ⊓ ·) := ⟨inf_idem⟩

Idempotence of the Meet Operation in Meet-Semilattices

Informal description

The meet operation $\sqcap$ in a meet-semilattice $\alpha$ is idempotent, meaning that for any element $a \in \alpha$, the operation satisfies $a \sqcap a = a$.

inf_comm theorem

(a b : α) : a ⊓ b = b ⊓ a

Full source

theorem inf_comm (a b : α) : a ⊓ b = b ⊓ a := @sup_comm αᵒᵈ _ _ _

Commutativity of Meet Operation in Semilattices

Informal description

For any elements $a$ and $b$ in a meet-semilattice $\alpha$, the meet operation $\sqcap$ is commutative, i.e., $a \sqcap b = b \sqcap a$.

instCommutativeMin_mathlib instance

: Std.Commutative (α := α) (· ⊓ ·)

Full source

instance : Std.Commutative (α := α) (· ⊓ ·) := ⟨inf_comm⟩

Commutativity of Meet Operation in Semilattices

Informal description

The meet operation $\sqcap$ in a meet-semilattice $\alpha$ is commutative.

inf_assoc theorem

(a b c : α) : a ⊓ b ⊓ c = a ⊓ (b ⊓ c)

Full source

theorem inf_assoc (a b c : α) : a ⊓ ba ⊓ b ⊓ c = a ⊓ (b ⊓ c) := @sup_assoc αᵒᵈ _ _ _ _

Associativity of Meet Operation in Semilattices

Informal description

In a meet-semilattice $\alpha$, the meet operation $\sqcap$ is associative. That is, for any elements $a, b, c \in \alpha$, we have $(a \sqcap b) \sqcap c = a \sqcap (b \sqcap c)$.

instAssociativeMin_mathlib instance

: Std.Associative (α := α) (· ⊓ ·)

Full source

instance : Std.Associative (α := α) (· ⊓ ·) := ⟨inf_assoc⟩

Associativity of Meet Operation in Semilattices

Informal description

The meet operation $\sqcap$ in a meet-semilattice $\alpha$ is associative.

inf_left_right_swap theorem

(a b c : α) : a ⊓ b ⊓ c = c ⊓ b ⊓ a

Full source

theorem inf_left_right_swap (a b c : α) : a ⊓ ba ⊓ b ⊓ c = c ⊓ bc ⊓ b ⊓ a :=
  @sup_left_right_swap αᵒᵈ _ _ _ _

Left-Right Swap Property of Meet Operation in Semilattices

Informal description

In a meet-semilattice $\alpha$, for any elements $a, b, c \in \alpha$, the meet operation satisfies $(a \sqcap b) \sqcap c = (c \sqcap b) \sqcap a$.

inf_left_idem theorem

(a b : α) : a ⊓ (a ⊓ b) = a ⊓ b

Full source

theorem inf_left_idem (a b : α) : a ⊓ (a ⊓ b) = a ⊓ b := by simp

Left Idempotency of Meet Operation

Informal description

In a meet-semilattice $\alpha$, for any elements $a$ and $b$, the meet operation satisfies the left idempotency property: $a \sqcap (a \sqcap b) = a \sqcap b$.

inf_right_idem theorem

(a b : α) : a ⊓ b ⊓ b = a ⊓ b

Full source

theorem inf_right_idem (a b : α) : a ⊓ ba ⊓ b ⊓ b = a ⊓ b := by simp

Right Idempotency of Meet Operation

Informal description

In a meet-semilattice $\alpha$, for any elements $a$ and $b$, the meet operation satisfies the right idempotency property: $a \sqcap b \sqcap b = a \sqcap b$.

inf_left_comm theorem

(a b c : α) : a ⊓ (b ⊓ c) = b ⊓ (a ⊓ c)

Full source

theorem inf_left_comm (a b c : α) : a ⊓ (b ⊓ c) = b ⊓ (a ⊓ c) :=
  @sup_left_comm αᵒᵈ _ a b c

Left Commutativity of Meet Operation: $a \sqcap (b \sqcap c) = b \sqcap (a \sqcap c)$

Informal description

In a meet-semilattice $\alpha$, for any elements $a, b, c \in \alpha$, the meet operation satisfies the left commutativity property: $$a \sqcap (b \sqcap c) = b \sqcap (a \sqcap c)$$

inf_right_comm theorem

(a b c : α) : a ⊓ b ⊓ c = a ⊓ c ⊓ b

Full source

theorem inf_right_comm (a b c : α) : a ⊓ ba ⊓ b ⊓ c = a ⊓ ca ⊓ c ⊓ b :=
  @sup_right_comm αᵒᵈ _ a b c

Right Commutativity of Meet Operation: $a \sqcap b \sqcap c = a \sqcap c \sqcap b$

Informal description

In a meet-semilattice $\alpha$, for any elements $a, b, c \in \alpha$, the meet operation satisfies the right commutativity property: $$a \sqcap b \sqcap c = a \sqcap c \sqcap b$$

inf_inf_inf_comm theorem

(a b c d : α) : a ⊓ b ⊓ (c ⊓ d) = a ⊓ c ⊓ (b ⊓ d)

Full source

theorem inf_inf_inf_comm (a b c d : α) : a ⊓ ba ⊓ b ⊓ (c ⊓ d) = a ⊓ ca ⊓ c ⊓ (b ⊓ d) :=
  @sup_sup_sup_comm αᵒᵈ _ _ _ _ _

Commutativity of Quadruple Meet Operation: $a \sqcap b \sqcap (c \sqcap d) = a \sqcap c \sqcap (b \sqcap d)$

Informal description

In a meet-semilattice $\alpha$, for any elements $a, b, c, d \in \alpha$, the meet operation satisfies the following commutativity property: $$a \sqcap b \sqcap (c \sqcap d) = a \sqcap c \sqcap (b \sqcap d)$$

inf_inf_distrib_left theorem

(a b c : α) : a ⊓ (b ⊓ c) = a ⊓ b ⊓ (a ⊓ c)

Full source

theorem inf_inf_distrib_left (a b c : α) : a ⊓ (b ⊓ c) = a ⊓ ba ⊓ b ⊓ (a ⊓ c) :=
  @sup_sup_distrib_left αᵒᵈ _ _ _ _

Left Distributivity of Meet Operation: $a \sqcap (b \sqcap c) = (a \sqcap b) \sqcap (a \sqcap c)$

Informal description

In a meet-semilattice $\alpha$, for any elements $a, b, c \in \alpha$, the meet operation satisfies the left distributivity property: $$a \sqcap (b \sqcap c) = (a \sqcap b) \sqcap (a \sqcap c)$$

inf_inf_distrib_right theorem

(a b c : α) : a ⊓ b ⊓ c = a ⊓ c ⊓ (b ⊓ c)

Full source

theorem inf_inf_distrib_right (a b c : α) : a ⊓ ba ⊓ b ⊓ c = a ⊓ ca ⊓ c ⊓ (b ⊓ c) :=
  @sup_sup_distrib_right αᵒᵈ _ _ _ _

Right-Distributivity of Meet Operation in Meet-Semilattices: $a \sqcap b \sqcap c = a \sqcap c \sqcap (b \sqcap c)$

Informal description

In a meet-semilattice $\alpha$, for any elements $a, b, c \in \alpha$, the meet operation satisfies the following right-distributivity property: $$a \sqcap b \sqcap c = a \sqcap c \sqcap (b \sqcap c)$$

inf_congr_left theorem

(hb : a ⊓ c ≤ b) (hc : a ⊓ b ≤ c) : a ⊓ b = a ⊓ c

Full source

theorem inf_congr_left (hb : a ⊓ c ≤ b) (hc : a ⊓ b ≤ c) : a ⊓ b = a ⊓ c :=
  @sup_congr_left αᵒᵈ _ _ _ _ hb hc

Infimum Congruence under Left Absorption Conditions

Informal description

For any elements $a$, $b$, and $c$ in a meet-semilattice, if $a \sqcap c \leq b$ and $a \sqcap b \leq c$, then the infima $a \sqcap b$ and $a \sqcap c$ are equal, i.e., $a \sqcap b = a \sqcap c$.

inf_congr_right theorem

(h1 : b ⊓ c ≤ a) (h2 : a ⊓ c ≤ b) : a ⊓ c = b ⊓ c

Full source

theorem inf_congr_right (h1 : b ⊓ c ≤ a) (h2 : a ⊓ c ≤ b) : a ⊓ c = b ⊓ c :=
  @sup_congr_right αᵒᵈ _ _ _ _ h1 h2

Infimum Congruence under Right Absorption Conditions

Informal description

For any elements $a$, $b$, and $c$ in a meet-semilattice, if $b \sqcap c \leq a$ and $a \sqcap c \leq b$, then the infima $a \sqcap c$ and $b \sqcap c$ are equal, i.e., $a \sqcap c = b \sqcap c$.

inf_eq_inf_iff_left theorem

: a ⊓ b = a ⊓ c ↔ a ⊓ c ≤ b ∧ a ⊓ b ≤ c

Full source

theorem inf_eq_inf_iff_left : a ⊓ ba ⊓ b = a ⊓ c ↔ a ⊓ c ≤ b ∧ a ⊓ b ≤ c :=
  @sup_eq_sup_iff_left αᵒᵈ _ _ _ _

Infimum Equality under Left Absorption Conditions

Informal description

For any elements $a$, $b$, and $c$ in a meet-semilattice, the equality $a \sqcap b = a \sqcap c$ holds if and only if $a \sqcap c \leq b$ and $a \sqcap b \leq c$.

inf_eq_inf_iff_right theorem

: a ⊓ c = b ⊓ c ↔ b ⊓ c ≤ a ∧ a ⊓ c ≤ b

Full source

theorem inf_eq_inf_iff_right : a ⊓ ca ⊓ c = b ⊓ c ↔ b ⊓ c ≤ a ∧ a ⊓ c ≤ b :=
  @sup_eq_sup_iff_right αᵒᵈ _ _ _ _

Infimum Equality Criterion via Right Absorption Conditions

Informal description

For any elements $a$, $b$, and $c$ in a meet-semilattice, the equality $a \sqcap c = b \sqcap c$ holds if and only if $b \sqcap c \leq a$ and $a \sqcap c \leq b$.

Ne.inf_lt_or_inf_lt theorem

: a ≠ b → a ⊓ b < a ∨ a ⊓ b < b

Full source

theorem Ne.inf_lt_or_inf_lt : a ≠ b → a ⊓ ba ⊓ b < a ∨ a ⊓ b < b :=
  @Ne.lt_sup_or_lt_sup αᵒᵈ _ _ _

Strict Infimum Inequality for Distinct Elements in Meet-Semilattices

Informal description

For any two distinct elements $a$ and $b$ in a meet-semilattice, the infimum $a \sqcap b$ is strictly less than $a$ or strictly less than $b$.

SemilatticeInf.ext_inf theorem

 {α} {A B : SemilatticeInf α}
  (H :
    ∀ x y : α,
      (haveI := A;
        x ≤ y) ↔
        x ≤ y)
  (x y : α) :
  (haveI := A;
    x ⊓ y) =
    x ⊓ y

Full source

theorem SemilatticeInf.ext_inf {α} {A B : SemilatticeInf α}
    (H : ∀ x y : α, (haveI := A; x ≤ y) ↔ x ≤ y)
    (x y : α) :
    (haveI := A; x ⊓ y) = x ⊓ y :=
  eq_of_forall_le_iff fun c => by simp only [le_inf_iff]; rw [← H, @le_inf_iff α A, H, H]

Extensionality of Meet-Semilattice Structures with Respect to Order Relation

Informal description

Let $\alpha$ be a type, and let $A$ and $B$ be two meet-semilattice structures on $\alpha$. If for all $x, y \in \alpha$, the order relation $\leq$ in $A$ coincides with the order relation in $B$ (i.e., $x \leq y$ under $A$ if and only if $x \leq y$ under $B$), then for any $x, y \in \alpha$, the meet operation $x \sqcap y$ in $A$ is equal to the meet operation in $B$.

SemilatticeInf.ext theorem

 {α} {A B : SemilatticeInf α}
  (H :
    ∀ x y : α,
      (haveI := A;
        x ≤ y) ↔
        x ≤ y) :
  A = B

Full source

theorem SemilatticeInf.ext {α} {A B : SemilatticeInf α}
    (H : ∀ x y : α, (haveI := A; x ≤ y) ↔ x ≤ y) :
    A = B := by
  cases A
  cases B
  cases PartialOrder.ext H
  congr
  ext; apply SemilatticeInf.ext_inf H

Extensionality of Meet-Semilattice Structures via Order Relation

Informal description

Let $\alpha$ be a type equipped with two meet-semilattice structures $A$ and $B$. If for all elements $x, y \in \alpha$, the order relation $\leq$ under $A$ coincides with the order relation under $B$, then the two meet-semilattice structures $A$ and $B$ are equal.

SemilatticeInf.dual_dual theorem

(α : Type*) [H : SemilatticeInf α] : OrderDual.instSemilatticeInf αᵒᵈ = H

Full source

theorem SemilatticeInf.dual_dual (α : Type*) [H : SemilatticeInf α] :
    OrderDual.instSemilatticeInf αᵒᵈ = H :=
  SemilatticeInf.ext fun _ _ => Iff.rfl

Double Order Dual of a Meet-Semilattice is Itself

Informal description

For any meet-semilattice $\alpha$, the order dual of the order dual of $\alpha$ is equal to $\alpha$ itself as a meet-semilattice.

inf_le_ite theorem

(s s' : α) (P : Prop) [Decidable P] : s ⊓ s' ≤ ite P s s'

Full source

theorem inf_le_ite (s s' : α) (P : Prop) [Decidable P] : s ⊓ s' ≤ ite P s s' :=
  @ite_le_sup αᵒᵈ _ _ _ _ _

Infimum is Bounded by Conditional Element in Meet-Semilattice

Informal description

For any elements $s$ and $s'$ in a meet-semilattice $\alpha$, and any decidable proposition $P$, the infimum $s \sqcap s'$ is less than or equal to the element $\text{ite}(P, s, s')$ (which equals $s$ if $P$ is true and $s'$ otherwise).

SemilatticeInf.mk' definition

 {α : Type*} [Min α] (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) : SemilatticeInf α

Full source

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

The partial order is defined so that `a ≤ b` unfolds to `b ⊓ a = a`; cf. `inf_eq_right`.
-/
def SemilatticeInf.mk' {α : Type*} [Min α] (inf_comm : ∀ a b : α, a ⊓ b = b ⊓ a)
    (inf_assoc : ∀ a b c : α, a ⊓ ba ⊓ b ⊓ c = a ⊓ (b ⊓ c)) (inf_idem : ∀ a : α, a ⊓ a = a) :
    SemilatticeInf α := by
  haveI : SemilatticeSup αᵒᵈ := SemilatticeSup.mk' inf_comm inf_assoc inf_idem
  haveI i := OrderDual.instSemilatticeInf αᵒᵈ
  exact i

Meet-semilattice construction from commutative, associative, idempotent infimum

Informal description

Given a type $\alpha$ with a minimum operation $\sqcap$, if this operation satisfies the following properties for all $a, b, c \in \alpha$: 1. Commutativity: $a \sqcap b = b \sqcap a$ 2. Associativity: $(a \sqcap b) \sqcap c = a \sqcap (b \sqcap c)$ 3. Idempotency: $a \sqcap a = a$ then $\alpha$ can be endowed with the structure of a meet-semilattice, where the partial order is defined by $a \leq b$ if and only if $a \sqcap b = a$.

Lattice structure

(α : Type u) extends SemilatticeSup α, SemilatticeInf α

Full source

/-- A lattice is a join-semilattice which is also a meet-semilattice. -/
class Lattice (α : Type u) extends SemilatticeSup α, SemilatticeInf α

Lattice

Informal description

A lattice is a partially ordered set that is both a join-semilattice and a meet-semilattice, meaning it has both a supremum (join) operation $\sqcup$ and an infimum (meet) operation $\sqcap$ for any two elements.

OrderDual.instLattice instance

(α) [Lattice α] : Lattice αᵒᵈ

Full source

instance OrderDual.instLattice (α) [Lattice α] : Lattice αᵒᵈ where

Order Dual of a Lattice is a Lattice

Informal description

For any lattice $\alpha$, the order dual $\alpha^{\text{op}}$ is also a lattice.

semilatticeSup_mk'_partialOrder_eq_semilatticeInf_mk'_partialOrder theorem

 {α : Type*} [Max α] [Min α] (sup_comm : ∀ a b : α, a ⊔ b = b ⊔ a) (sup_assoc : ∀ a b c : α, a ⊔ b ⊔ c = a ⊔ (b ⊔ c))
  (sup_idem : ∀ a : α, a ⊔ a = a) (inf_comm : ∀ a b : α, a ⊓ b = b ⊓ a)
  (inf_assoc : ∀ a b c : α, a ⊓ b ⊓ c = a ⊓ (b ⊓ c)) (inf_idem : ∀ a : α, a ⊓ a = a)
  (sup_inf_self : ∀ a b : α, a ⊔ a ⊓ b = a) (inf_sup_self : ∀ a b : α, a ⊓ (a ⊔ b) = a) :
  @SemilatticeSup.toPartialOrder _ (SemilatticeSup.mk' sup_comm sup_assoc sup_idem) =
    @SemilatticeInf.toPartialOrder _ (SemilatticeInf.mk' inf_comm inf_assoc inf_idem)

Full source

/-- The partial orders from `SemilatticeSup_mk'` and `SemilatticeInf_mk'` agree
if `sup` and `inf` satisfy the lattice absorption laws `sup_inf_self` (`a ⊔ a ⊓ b = a`)
and `inf_sup_self` (`a ⊓ (a ⊔ b) = a`). -/
theorem semilatticeSup_mk'_partialOrder_eq_semilatticeInf_mk'_partialOrder
    {α : Type*} [Max α] [Min α]
    (sup_comm : ∀ a b : α, a ⊔ b = b ⊔ a) (sup_assoc : ∀ a b c : α, a ⊔ ba ⊔ 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 ⊓ ba ⊓ b ⊓ c = a ⊓ (b ⊓ c)) (inf_idem : ∀ a : α, a ⊓ a = a)
    (sup_inf_self : ∀ a b : α, a ⊔ a ⊓ b = a) (inf_sup_self : ∀ a b : α, a ⊓ (a ⊔ b) = a) :
    @SemilatticeSup.toPartialOrder _ (SemilatticeSup.mk' sup_comm sup_assoc sup_idem) =
      @SemilatticeInf.toPartialOrder _ (SemilatticeInf.mk' inf_comm inf_assoc inf_idem) :=
  PartialOrder.ext fun a b =>
    show a ⊔ ba ⊔ b = b ↔ b ⊓ a = a from
      ⟨fun h => by rw [← h, inf_comm, inf_sup_self], fun h => by rw [← h, sup_comm, sup_inf_self]⟩

Equivalence of Join- and Meet-Semilattice Partial Orders under Lattice Absorption Laws

Informal description

Let $\alpha$ be a type equipped with both maximum ($\sqcup$) and minimum ($\sqcap$) operations. Suppose these operations satisfy the following properties for all $a, b, c \in \alpha$: 1. **Supremum properties**: - Commutativity: $a \sqcup b = b \sqcup a$ - Associativity: $(a \sqcup b) \sqcup c = a \sqcup (b \sqcup c)$ - Idempotency: $a \sqcup a = a$ 2. **Infimum properties**: - Commutativity: $a \sqcap b = b \sqcap a$ - Associativity: $(a \sqcap b) \sqcap c = a \sqcap (b \sqcap c)$ - Idempotency: $a \sqcap a = a$ 3. **Lattice absorption laws**: - $a \sqcup (a \sqcap b) = a$ - $a \sqcap (a \sqcup b) = a$ Then the partial order induced by the join-semilattice construction (via `SemilatticeSup.mk'`) coincides with the partial order induced by the meet-semilattice construction (via `SemilatticeInf.mk'`).

Lattice.mk' definition

 {α : Type*} [Max α] [Min α] (sup_comm : ∀ a b : α, a ⊔ b = b ⊔ a) (sup_assoc : ∀ a b c : α, a ⊔ b ⊔ c = a ⊔ (b ⊔ c))
  (inf_comm : ∀ a b : α, a ⊓ b = b ⊓ a) (inf_assoc : ∀ a b c : α, a ⊓ b ⊓ c = a ⊓ (b ⊓ c))
  (sup_inf_self : ∀ a b : α, a ⊔ a ⊓ b = a) (inf_sup_self : ∀ a b : α, a ⊓ (a ⊔ b) = a) : Lattice α

Full source

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

The partial order is defined so that `a ≤ b` unfolds to `a ⊔ b = b`; cf. `sup_eq_right`.
-/
def Lattice.mk' {α : Type*} [Max α] [Min α] (sup_comm : ∀ a b : α, a ⊔ b = b ⊔ a)
    (sup_assoc : ∀ a b c : α, a ⊔ ba ⊔ b ⊔ c = a ⊔ (b ⊔ c)) (inf_comm : ∀ a b : α, a ⊓ b = b ⊓ a)
    (inf_assoc : ∀ a b c : α, a ⊓ ba ⊓ b ⊓ c = a ⊓ (b ⊓ c)) (sup_inf_self : ∀ a b : α, a ⊔ a ⊓ b = a)
    (inf_sup_self : ∀ a b : α, a ⊓ (a ⊔ b) = a) : Lattice α :=
  have sup_idem : ∀ b : α, b ⊔ b = b := fun b =>
    calc
      b ⊔ b = b ⊔ b ⊓ (b ⊔ b) := by rw [inf_sup_self]
      _ = b := by rw [sup_inf_self]

  have inf_idem : ∀ b : α, b ⊓ b = b := fun b =>
    calc
      b ⊓ b = b ⊓ (b ⊔ b ⊓ b) := by rw [sup_inf_self]
      _ = b := by rw [inf_sup_self]

  let semilatt_inf_inst := SemilatticeInf.mk' inf_comm inf_assoc inf_idem
  let semilatt_sup_inst := SemilatticeSup.mk' sup_comm sup_assoc sup_idem
  have partial_order_eq : @SemilatticeSup.toPartialOrder _ semilatt_sup_inst =
                          @SemilatticeInf.toPartialOrder _ semilatt_inf_inst :=
    semilatticeSup_mk'_partialOrder_eq_semilatticeInf_mk'_partialOrder _ _ _ _ _ _
      sup_inf_self inf_sup_self
  { semilatt_sup_inst, semilatt_inf_inst with
    inf_le_left := fun a b => by
      rw [partial_order_eq]
      apply inf_le_left,
    inf_le_right := fun a b => by
      rw [partial_order_eq]
      apply inf_le_right,
    le_inf := fun a b c => by
      rw [partial_order_eq]
      apply le_inf }

Lattice construction from commutative, associative, and absorbing operations

Informal description

Given a type $\alpha$ equipped with binary operations $\sqcup$ (supremum) and $\sqcap$ (infimum) that satisfy the following properties for all $a, b, c \in \alpha$: 1. **Commutativity**: - $a \sqcup b = b \sqcup a$ - $a \sqcap b = b \sqcap a$ 2. **Associativity**: - $(a \sqcup b) \sqcup c = a \sqcup (b \sqcup c)$ - $(a \sqcap b) \sqcap c = a \sqcap (b \sqcap c)$ 3. **Absorption laws**: - $a \sqcup (a \sqcap b) = a$ - $a \sqcap (a \sqcup b) = a$ then $\alpha$ can be endowed with the structure of a lattice, where the partial order is defined by $a \leq b$ if and only if $a \sqcup b = b$.

inf_le_sup theorem

: a ⊓ b ≤ a ⊔ b

Full source

theorem inf_le_sup : a ⊓ b ≤ a ⊔ b :=
  inf_le_left.trans le_sup_left

Infimum is Less Than or Equal to Supremum in a Lattice

Informal description

For any two elements $a$ and $b$ in a lattice, the infimum $a \sqcap b$ is less than or equal to the supremum $a \sqcup b$.

sup_le_inf theorem

: a ⊔ b ≤ a ⊓ b ↔ a = b

Full source

theorem sup_le_inf : a ⊔ ba ⊔ b ≤ a ⊓ b ↔ a = b := by simp [le_antisymm_iff, and_comm]

Supremum Less Than or Equal to Infimum iff Elements Are Equal

Informal description

For any two elements $a$ and $b$ in a lattice, the supremum $a \sqcup b$ is less than or equal to the infimum $a \sqcap b$ if and only if $a = b$.

inf_eq_sup theorem

: a ⊓ b = a ⊔ b ↔ a = b

Full source

@[simp] lemma inf_eq_sup : a ⊓ ba ⊓ b = a ⊔ b ↔ a = b := by rw [← inf_le_sup.ge_iff_eq, sup_le_inf]

Infimum Equals Supremum iff Elements Are Equal ($a \sqcap b = a \sqcup b \leftrightarrow a = b$)

Informal description

For any two elements $a$ and $b$ in a lattice, the infimum $a \sqcap b$ equals the supremum $a \sqcup b$ if and only if $a = b$.

sup_eq_inf theorem

: a ⊔ b = a ⊓ b ↔ a = b

Full source

@[simp] lemma sup_eq_inf : a ⊔ ba ⊔ b = a ⊓ b ↔ a = b := eq_comm.trans inf_eq_sup

Supremum Equals Infimum iff Elements Are Equal ($a \sqcup b = a \sqcap b \leftrightarrow a = b$)

Informal description

For any two elements $a$ and $b$ in a lattice, the supremum $a \sqcup b$ equals the infimum $a \sqcap b$ if and only if $a = b$.

inf_lt_sup theorem

: a ⊓ b < a ⊔ b ↔ a ≠ b

Full source

@[simp] lemma inf_lt_sup : a ⊓ ba ⊓ b < a ⊔ b ↔ a ≠ b := by rw [inf_le_sup.lt_iff_ne, Ne, inf_eq_sup]

Infimum Strictly Less Than Supremum iff Elements Are Distinct ($a \sqcap b < a \sqcup b \leftrightarrow a \neq b$)

Informal description

For any two elements $a$ and $b$ in a lattice, the infimum $a \sqcap b$ is strictly less than the supremum $a \sqcup b$ if and only if $a$ and $b$ are distinct, i.e., $a \sqcap b < a \sqcup b \leftrightarrow a \neq b$.

inf_eq_and_sup_eq_iff theorem

: a ⊓ b = c ∧ a ⊔ b = c ↔ a = c ∧ b = c

Full source

lemma inf_eq_and_sup_eq_iff : a ⊓ ba ⊓ b = c ∧ a ⊔ b = ca ⊓ b = c ∧ a ⊔ b = c ↔ a = c ∧ b = c := by
  refine ⟨fun h ↦ ?_, ?_⟩
  · obtain rfl := sup_eq_inf.1 (h.2.trans h.1.symm)
    simpa using h
  · rintro ⟨rfl, rfl⟩
    exact ⟨inf_idem _, sup_idem _⟩

Characterization of Equality via Meet and Join: $a \sqcap b = c \land a \sqcup b = c \leftrightarrow a = c \land b = c$

Informal description

For any elements $a$, $b$, and $c$ in a lattice, the meet (infimum) of $a$ and $b$ equals $c$ and the join (supremum) of $a$ and $b$ equals $c$ if and only if both $a$ and $b$ are equal to $c$, i.e., $a \sqcap b = c \land a \sqcup b = c \leftrightarrow a = c \land b = c$.

sup_inf_le theorem

: a ⊔ b ⊓ c ≤ (a ⊔ b) ⊓ (a ⊔ c)

Full source

theorem sup_inf_le : a ⊔ b ⊓ c ≤ (a ⊔ b) ⊓ (a ⊔ c) :=
  le_inf (sup_le_sup_left inf_le_left _) (sup_le_sup_left inf_le_right _)

Join-Meet Inequality in Lattices: $a \sqcup (b \sqcap c) \leq (a \sqcup b) \sqcap (a \sqcup c)$

Informal description

For any elements $a$, $b$, and $c$ in a lattice, the join of $a$ with the meet of $b$ and $c$ is less than or equal to the meet of the joins $a \sqcup b$ and $a \sqcup c$, i.e., $$ a \sqcup (b \sqcap c) \leq (a \sqcup b) \sqcap (a \sqcup c). $$

le_inf_sup theorem

: a ⊓ b ⊔ a ⊓ c ≤ a ⊓ (b ⊔ c)

Full source

theorem le_inf_sup : a ⊓ ba ⊓ b ⊔ a ⊓ c ≤ a ⊓ (b ⊔ c) :=
  sup_le (inf_le_inf_left _ le_sup_left) (inf_le_inf_left _ le_sup_right)

Join-Meet Inequality: $(a \sqcap b) \sqcup (a \sqcap c) \leq a \sqcap (b \sqcup c)$

Informal description

For any elements $a$, $b$, and $c$ in a lattice, the join of the meets $a \sqcap b$ and $a \sqcap c$ is less than or equal to the meet of $a$ with the join $b \sqcup c$, i.e., $$ (a \sqcap b) \sqcup (a \sqcap c) \leq a \sqcap (b \sqcup c). $$

inf_sup_self theorem

: a ⊓ (a ⊔ b) = a

Full source

theorem inf_sup_self : a ⊓ (a ⊔ b) = a := by simp

Absorption Law: Meet over Join

Informal description

For any elements $a$ and $b$ in a lattice, the meet of $a$ with the join of $a$ and $b$ equals $a$, i.e., $a \sqcap (a \sqcup b) = a$.

sup_inf_self theorem

: a ⊔ a ⊓ b = a

Full source

theorem sup_inf_self : a ⊔ a ⊓ b = a := by simp

Absorption Law: Join over Meet

Informal description

For any elements $a$ and $b$ in a lattice, the supremum of $a$ and the infimum of $a$ and $b$ equals $a$, i.e., $a \sqcup (a \sqcap b) = a$.

sup_eq_iff_inf_eq theorem

: a ⊔ b = b ↔ a ⊓ b = a

Full source

theorem sup_eq_iff_inf_eq : a ⊔ ba ⊔ b = b ↔ a ⊓ b = a := by rw [sup_eq_right, ← inf_eq_left]

Supremum Equals Right Operand iff Infimum Equals Left Operand

Informal description

For any elements $a$ and $b$ in a lattice, the supremum $a \sqcup b$ equals $b$ if and only if the infimum $a \sqcap b$ equals $a$.

Lattice.ext theorem

 {α} {A B : Lattice α}
  (H :
    ∀ x y : α,
      (haveI := A;
        x ≤ y) ↔
        x ≤ y) :
  A = B

Full source

theorem Lattice.ext {α} {A B : Lattice α} (H : ∀ x y : α, (haveI := A; x ≤ y) ↔ x ≤ y) :
    A = B := by
  cases A
  cases B
  cases SemilatticeSup.ext H
  cases SemilatticeInf.ext H
  congr

Extensionality of Lattice Structures via Order Relation

Informal description

Let $\alpha$ be a type equipped with two lattice structures $A$ and $B$. If for all elements $x, y \in \alpha$, the order relation $x \leq y$ under $A$ coincides with the order relation under $B$, then the two lattice structures $A$ and $B$ are equal.

DistribLattice structure

(α) extends Lattice α

Full source

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

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

A classic example of a distributive lattice
is the lattice of subsets of a set, and in fact this example is
generic in the sense that every distributive lattice is realizable
as a sublattice of a powerset lattice. -/
class DistribLattice (α) extends Lattice α where
  /-- The infimum distributes over the supremum -/
  protected le_sup_inf : ∀ x y z : α, (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z

Distributive Lattice

Informal description

A distributive lattice is a lattice where the binary operations of join (least upper bound, $\sqcup$) and meet (greatest lower bound, $\sqcap$) satisfy the distributivity property: $$(x \sqcup y) \sqcap (x \sqcup z) \leq x \sqcup (y \sqcap z)$$ for all elements $x, y, z$ in the lattice. This structure generalizes the lattice of subsets of a set, where join and meet correspond to union and intersection, respectively. Every distributive lattice can be realized as a sublattice of such a powerset lattice.

le_sup_inf theorem

: ∀ {x y z : α}, (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z

Full source

theorem le_sup_inf : ∀ {x y z : α}, (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z :=
  fun {x y z} => DistribLattice.le_sup_inf x y z

Distributive Inequality in Lattices: $(x \sqcup y) \sqcap (x \sqcup z) \leq x \sqcup (y \sqcap z)$

Informal description

In a distributive lattice $\alpha$, for any elements $x, y, z \in \alpha$, the following inequality holds: $$(x \sqcup y) \sqcap (x \sqcup z) \leq x \sqcup (y \sqcap z).$$

sup_inf_left theorem

(a b c : α) : a ⊔ b ⊓ c = (a ⊔ b) ⊓ (a ⊔ c)

Full source

theorem sup_inf_left (a b c : α) : a ⊔ b ⊓ c = (a ⊔ b) ⊓ (a ⊔ c) :=
  le_antisymm sup_inf_le le_sup_inf

Left Distributivity of Join over Meet in Lattices: $a \sqcup (b \sqcap c) = (a \sqcup b) \sqcap (a \sqcup c)$

Informal description

In a distributive lattice $\alpha$, for any elements $a, b, c \in \alpha$, the following equality holds: $$ a \sqcup (b \sqcap c) = (a \sqcup b) \sqcap (a \sqcup c). $$

sup_inf_right theorem

(a b c : α) : a ⊓ b ⊔ c = (a ⊔ c) ⊓ (b ⊔ c)

Full source

theorem sup_inf_right (a b c : α) : a ⊓ ba ⊓ b ⊔ c = (a ⊔ c) ⊓ (b ⊔ c) := by
  simp only [sup_inf_left, sup_comm _ c, eq_self_iff_true]

Right Distributivity of Join over Meet in Lattices: $(a \sqcap b) \sqcup c = (a \sqcup c) \sqcap (b \sqcup c)$

Informal description

In a distributive lattice $\alpha$, for any elements $a, b, c \in \alpha$, the following equality holds: $$ (a \sqcap b) \sqcup c = (a \sqcup c) \sqcap (b \sqcup c). $$

inf_sup_left theorem

(a b c : α) : a ⊓ (b ⊔ c) = a ⊓ b ⊔ a ⊓ c

Full source

theorem inf_sup_left (a b c : α) : a ⊓ (b ⊔ c) = a ⊓ ba ⊓ b ⊔ a ⊓ c :=
  calc
    a ⊓ (b ⊔ c) = a ⊓ (a ⊔ c)a ⊓ (a ⊔ c) ⊓ (b ⊔ c) := by rw [inf_sup_self]
    _ = a ⊓ (a ⊓ b ⊔ c) := by simp only [inf_assoc, sup_inf_right, eq_self_iff_true]
    _ = (a ⊔ a ⊓ b) ⊓ (a ⊓ b ⊔ c) := by rw [sup_inf_self]
    _ = (a ⊓ b ⊔ a) ⊓ (a ⊓ b ⊔ c) := by rw [sup_comm]
    _ = a ⊓ ba ⊓ b ⊔ a ⊓ c := by rw [sup_inf_left]

Left Distributivity of Meet over Join in Lattices: $a \sqcap (b \sqcup c) = (a \sqcap b) \sqcup (a \sqcap c)$

Informal description

In a distributive lattice $\alpha$, for any elements $a, b, c \in \alpha$, the meet operation distributes over the join operation on the left: $$ a \sqcap (b \sqcup c) = (a \sqcap b) \sqcup (a \sqcap c). $$

OrderDual.instDistribLattice instance

(α : Type*) [DistribLattice α] : DistribLattice αᵒᵈ

Full source

instance OrderDual.instDistribLattice (α : Type*) [DistribLattice α] : DistribLattice αᵒᵈ where
  le_sup_inf _ _ _ := (inf_sup_left _ _ _).le

Order Dual of a Distributive Lattice is a Distributive Lattice

Informal description

For any distributive lattice $\alpha$, the order dual $\alpha^{\text{op}}$ is also a distributive lattice.

inf_sup_right theorem

(a b c : α) : (a ⊔ b) ⊓ c = a ⊓ c ⊔ b ⊓ c

Full source

theorem inf_sup_right (a b c : α) : (a ⊔ b) ⊓ c = a ⊓ ca ⊓ c ⊔ b ⊓ c := by
  simp only [inf_sup_left, inf_comm _ c, eq_self_iff_true]

Right Distributivity of Meet over Join in Lattices: $(a \sqcup b) \sqcap c = (a \sqcap c) \sqcup (b \sqcap c)$

Informal description

In a distributive lattice $\alpha$, for any elements $a, b, c \in \alpha$, the meet operation distributes over the join operation on the right: $$ (a \sqcup b) \sqcap c = (a \sqcap c) \sqcup (b \sqcap c). $$

le_of_inf_le_sup_le theorem

(h₁ : x ⊓ z ≤ y ⊓ z) (h₂ : x ⊔ z ≤ y ⊔ z) : x ≤ y

Full source

theorem le_of_inf_le_sup_le (h₁ : x ⊓ z ≤ y ⊓ z) (h₂ : x ⊔ z ≤ y ⊔ z) : x ≤ y :=
  calc
    x ≤ y ⊓ zy ⊓ z ⊔ x := le_sup_right
    _ = (y ⊔ x) ⊓ (x ⊔ z) := by rw [sup_inf_right, sup_comm x]
    _ ≤ (y ⊔ x) ⊓ (y ⊔ z) := inf_le_inf_left _ h₂
    _ = y ⊔ x ⊓ z := by rw [← sup_inf_left]
    _ ≤ y ⊔ y ⊓ z := sup_le_sup_left h₁ _
    _ ≤ _ := sup_le (le_refl y) inf_le_left

Comparison via Infimum and Supremum: $x \sqcap z \leq y \sqcap z \land x \sqcup z \leq y \sqcup z \Rightarrow x \leq y$

Informal description

For any elements $x$, $y$, and $z$ in a lattice, if both $x \sqcap z \leq y \sqcap z$ and $x \sqcup z \leq y \sqcup z$ hold, then $x \leq y$.

DistribLattice.ofInfSupLe abbrev

[Lattice α] (inf_sup_le : ∀ a b c : α, a ⊓ (b ⊔ c) ≤ a ⊓ b ⊔ a ⊓ c) : DistribLattice α

Full source

/-- Prove distributivity of an existing lattice from the dual distributive law. -/
abbrev DistribLattice.ofInfSupLe
    [Lattice α] (inf_sup_le : ∀ a b c : α, a ⊓ (b ⊔ c) ≤ a ⊓ ba ⊓ b ⊔ a ⊓ c) : DistribLattice α where
  le_sup_inf := (@OrderDual.instDistribLattice αᵒᵈ {inferInstanceAs (Lattice αᵒᵈ) with
      le_sup_inf := inf_sup_le}).le_sup_inf

Distributive Lattice Construction via Inf-Sup Inequality

Informal description

Given a lattice $\alpha$ satisfying the inequality $$a \sqcap (b \sqcup c) \leq (a \sqcap b) \sqcup (a \sqcap c)$$ for all elements $a, b, c \in \alpha$, then $\alpha$ is a distributive lattice.

LinearOrder.toLattice instance

{α : Type u} [LinearOrder α] : Lattice α

Full source

instance (priority := 100) LinearOrder.toLattice {α : Type u} [LinearOrder α] : Lattice α where
  sup := max
  inf := min
  le_sup_left := le_max_left; le_sup_right := le_max_right; sup_le _ _ _ := max_le
  inf_le_left := min_le_left; inf_le_right := min_le_right; le_inf _ _ _ := le_min

Lattice Structure on Linear Orders

Informal description

Every linearly ordered set $\alpha$ is a lattice, where the supremum (join) operation $\sqcup$ is given by the maximum and the infimum (meet) operation $\sqcap$ is given by the minimum.

sup_eq_max theorem

: a ⊔ b = max a b

Full source

@[deprecated "is syntactical" (since := "2024-11-13"), nolint synTaut]
theorem sup_eq_max : a ⊔ b = max a b :=
  rfl

Supremum Equals Maximum in Join-Semilattices

Informal description

For any two elements $a$ and $b$ in a join-semilattice, the supremum $a \sqcup b$ equals the maximum of $a$ and $b$.

inf_eq_min theorem

: a ⊓ b = min a b

Full source

@[deprecated "is syntactical" (since := "2024-11-13"), nolint synTaut]
theorem inf_eq_min : a ⊓ b = min a b :=
  rfl

Infimum Equals Minimum in Meet-Semilattices

Informal description

For any two elements $a$ and $b$ in a meet-semilattice, the infimum $a \sqcap b$ is equal to the minimum of $a$ and $b$.

sup_ind theorem

(a b : α) {p : α → Prop} (ha : p a) (hb : p b) : p (a ⊔ b)

Full source

theorem sup_ind (a b : α) {p : α → Prop} (ha : p a) (hb : p b) : p (a ⊔ b) :=
  (IsTotal.total a b).elim (fun h : a ≤ b => by rwa [sup_eq_right.2 h]) fun h => by
  rwa [sup_eq_left.2 h]

Supremum Induction Principle in Join-Semilattices

Informal description

For any elements $a$ and $b$ in a join-semilattice $\alpha$, and for any predicate $p$ on $\alpha$, if $p(a)$ and $p(b)$ both hold, then $p(a \sqcup b)$ also holds.

le_sup_iff theorem

: a ≤ b ⊔ c ↔ a ≤ b ∨ a ≤ c

Full source

@[simp]
theorem le_sup_iff : a ≤ b ⊔ c ↔ a ≤ b ∨ a ≤ c := by
  exact ⟨fun h =>
    (le_total c b).imp
      (fun bc => by rwa [sup_eq_left.2 bc] at h)
      (fun bc => by rwa [sup_eq_right.2 bc] at h),
    fun h => h.elim le_sup_of_le_left le_sup_of_le_right⟩

Supremum Order Characterization: $a \leq b \sqcup c \leftrightarrow a \leq b \lor a \leq c$

Informal description

For any elements $a$, $b$, and $c$ in a join-semilattice, $a$ is less than or equal to the supremum $b \sqcup c$ if and only if $a \leq b$ or $a \leq c$.

lt_sup_iff theorem

: a < b ⊔ c ↔ a < b ∨ a < c

Full source

@[simp]
theorem lt_sup_iff : a < b ⊔ c ↔ a < b ∨ a < c := by
  exact ⟨fun h =>
    (le_total c b).imp
      (fun bc => by rwa [sup_eq_left.2 bc] at h)
      (fun bc => by rwa [sup_eq_right.2 bc] at h),
    fun h => h.elim lt_sup_of_lt_left lt_sup_of_lt_right⟩

Characterization of Strict Inequality Under Supremum

Informal description

For any elements $a$, $b$, and $c$ in a join-semilattice, the inequality $a < b \sqcup c$ holds if and only if either $a < b$ or $a < c$ holds.

sup_lt_iff theorem

: b ⊔ c < a ↔ b < a ∧ c < a

Full source

@[simp]
theorem sup_lt_iff : b ⊔ cb ⊔ c < a ↔ b < a ∧ c < a :=
  ⟨fun h => ⟨le_sup_left.trans_lt h, le_sup_right.trans_lt h⟩,
   fun h => sup_ind (p := (· < a)) b c h.1 h.2⟩

Supremum Strictly Less Than Element if and only if Both Elements Are Strictly Less Than

Informal description

For any elements $a$, $b$, and $c$ in a join-semilattice, the supremum $b \sqcup c$ is strictly less than $a$ if and only if both $b$ and $c$ are strictly less than $a$.

inf_ind theorem

(a b : α) {p : α → Prop} : p a → p b → p (a ⊓ b)

Full source

theorem inf_ind (a b : α) {p : α → Prop} : p a → p b → p (a ⊓ b) :=
  @sup_ind αᵒᵈ _ _ _ _

Infimum Induction Principle in Meet-Semilattices

Informal description

For any elements $a$ and $b$ in a meet-semilattice $\alpha$, and for any predicate $p$ on $\alpha$, if $p(a)$ and $p(b)$ both hold, then $p(a \sqcap b)$ also holds.

inf_le_iff theorem

: b ⊓ c ≤ a ↔ b ≤ a ∨ c ≤ a

Full source

@[simp]
theorem inf_le_iff : b ⊓ cb ⊓ c ≤ a ↔ b ≤ a ∨ c ≤ a :=
  @le_sup_iff αᵒᵈ _ _ _ _

Infimum Order Characterization: $b \sqcap c \leq a \leftrightarrow b \leq a \lor c \leq a$

Informal description

For any elements $a$, $b$, and $c$ in a meet-semilattice, the infimum $b \sqcap c$ is less than or equal to $a$ if and only if $b \leq a$ or $c \leq a$.

inf_lt_iff theorem

: b ⊓ c < a ↔ b < a ∨ c < a

Full source

@[simp]
theorem inf_lt_iff : b ⊓ cb ⊓ c < a ↔ b < a ∨ c < a :=
  @lt_sup_iff αᵒᵈ _ _ _ _

Characterization of Strict Inequality Under Infimum

Informal description

For any elements $a$, $b$, and $c$ in a meet-semilattice, the inequality $b \sqcap c < a$ holds if and only if either $b < a$ or $c < a$ holds.

lt_inf_iff theorem

: a < b ⊓ c ↔ a < b ∧ a < c

Full source

@[simp]
theorem lt_inf_iff : a < b ⊓ c ↔ a < b ∧ a < c :=
  @sup_lt_iff αᵒᵈ _ _ _ _

Element Strictly Less Than Infimum if and only if Strictly Less Than Both Elements

Informal description

For any elements $a$, $b$, and $c$ in a meet-semilattice, the element $a$ is strictly less than the infimum $b \sqcap c$ if and only if $a$ is strictly less than both $b$ and $c$.

max_max_max_comm theorem

: max (max a b) (max c d) = max (max a c) (max b d)

Full source

theorem max_max_max_comm : max (max a b) (max c d) = max (max a c) (max b d) :=
  sup_sup_sup_comm _ _ _ _

Commutativity of Nested Maximum Operations: $\max(\max(a, b), \max(c, d)) = \max(\max(a, c), \max(b, d))$

Informal description

For any elements $a, b, c, d$ in a linearly ordered set, the following equality holds: $$\max(\max(a, b), \max(c, d)) = \max(\max(a, c), \max(b, d))$$

min_min_min_comm theorem

: min (min a b) (min c d) = min (min a c) (min b d)

Full source

theorem min_min_min_comm : min (min a b) (min c d) = min (min a c) (min b d) :=
  inf_inf_inf_comm _ _ _ _

Commutativity of Nested Minimum Operations: $\min(\min(a, b), \min(c, d)) = \min(\min(a, c), \min(b, d))$

Informal description

For any elements $a, b, c, d$ in a linearly ordered set, the following equality holds: $$\min(\min(a, b), \min(c, d)) = \min(\min(a, c), \min(b, d))$$

sup_eq_maxDefault theorem

[SemilatticeSup α] [DecidableLE α] [IsTotal α (· ≤ ·)] : (· ⊔ ·) = (maxDefault : α → α → α)

Full source

theorem sup_eq_maxDefault [SemilatticeSup α] [DecidableLE α] [IsTotal α (· ≤ ·)] :
    (· ⊔ ·) = (maxDefault : α → α → α) := by
  ext x y
  unfold maxDefault
  split_ifs with h'
  exacts [sup_of_le_right h', sup_of_le_left <| (total_of (· ≤ ·) x y).resolve_left h']

Supremum Equals Default Maximum in Total Join-Semilattices

Informal description

In a join-semilattice $\alpha$ with a decidable total order $\leq$, the supremum operation $\sqcup$ coincides with the default maximum operation $\mathrm{maxDefault}$ on $\alpha$.

inf_eq_minDefault theorem

[SemilatticeInf α] [DecidableLE α] [IsTotal α (· ≤ ·)] : (· ⊓ ·) = (minDefault : α → α → α)

Full source

theorem inf_eq_minDefault [SemilatticeInf α] [DecidableLE α] [IsTotal α (· ≤ ·)] :
    (· ⊓ ·) = (minDefault : α → α → α) := by
  ext x y
  unfold minDefault
  split_ifs with h'
  exacts [inf_of_le_left h', inf_of_le_right <| (total_of (· ≤ ·) x y).resolve_left h']

Infimum Equals Default Minimum in Total Meet-Semilattices

Informal description

For any meet-semilattice $\alpha$ with a decidable order relation $\leq$ that is total, the infimum operation $\sqcap$ coincides with the default minimum operation $\mathrm{minDefault}$ on $\alpha$.

Lattice.toLinearOrder abbrev

(α : Type u) [Lattice α] [DecidableEq α] [DecidableLE α] [DecidableLT α] [IsTotal α (· ≤ ·)] : LinearOrder α

Full source

/-- A lattice with total order is a linear order.

See note [reducible non-instances]. -/
abbrev Lattice.toLinearOrder (α : Type u) [Lattice α] [DecidableEq α]
    [DecidableLE α] [DecidableLT α] [IsTotal α (· ≤ ·)] : LinearOrder α where
  toDecidableLE := ‹_›
  toDecidableEq := ‹_›
  toDecidableLT := ‹_›
  le_total := total_of (· ≤ ·)
  max_def := by exact congr_fun₂ sup_eq_maxDefault
  min_def := by exact congr_fun₂ inf_eq_minDefault

Linear Order Structure on a Total Lattice

Informal description

For any lattice $\alpha$ with a decidable equality relation, decidable order relations $\leq$ and $<$, and a total order $\leq$, there exists a canonical linear order structure on $\alpha$.

instDistribLatticeOfLinearOrder instance

{α : Type u} [LinearOrder α] : DistribLattice α

Full source

instance (priority := 100) {α : Type u} [LinearOrder α] : DistribLattice α where
  le_sup_inf _ b c :=
    match le_total b c with
    | Or.inl h => inf_le_of_left_le <| sup_le_sup_left (le_inf (le_refl b) h) _
    | Or.inr h => inf_le_of_right_le <| sup_le_sup_left (le_inf h (le_refl c)) _

Linear Orders are Distributive Lattices

Informal description

Every linearly ordered set $\alpha$ is a distributive lattice, where the join and meet operations are given by the maximum and minimum operations respectively.

instDistribLatticeNat instance

: DistribLattice ℕ

Full source

instance : DistribLattice ℕ := inferInstance

Distributive Lattice Structure on Natural Numbers

Informal description

The natural numbers $\mathbb{N}$ form a distributive lattice, where the join and meet operations are given by the maximum and minimum operations respectively.

instLatticeInt instance

: Lattice ℤ

Full source

instance : Lattice ℤ := inferInstance

The Lattice Structure on Integers

Informal description

The integers $\mathbb{Z}$ form a lattice, where the join and meet operations are given by the maximum and minimum operations respectively.

ofDual_inf theorem

[Max α] (a b : αᵒᵈ) : ofDual (a ⊓ b) = ofDual a ⊔ ofDual b

Full source

@[simp]
theorem ofDual_inf [Max α] (a b : αᵒᵈ) : ofDual (a ⊓ b) = ofDualofDual a ⊔ ofDual b :=
  rfl

Duality Transformation of Infimum Equals Supremum of Duals

Informal description

Let $\alpha$ be a type with a maximum operation (join-semilattice structure). For any elements $a, b$ in the order dual $\alpha^{\text{op}}$, the image under the duality map of their infimum $a \sqcap b$ equals the supremum of their images, i.e., $\text{ofDual}(a \sqcap b) = \text{ofDual}(a) \sqcup \text{ofDual}(b)$.

ofDual_sup theorem

[Min α] (a b : αᵒᵈ) : ofDual (a ⊔ b) = ofDual a ⊓ ofDual b

Full source

@[simp]
theorem ofDual_sup [Min α] (a b : αᵒᵈ) : ofDual (a ⊔ b) = ofDualofDual a ⊓ ofDual b :=
  rfl

Duality Transformation of Supremum Equals Infimum of Duals

Informal description

Let $\alpha$ be a type with a minimum operation (meet-semilattice structure). For any elements $a, b$ in the order dual $\alpha^{\text{op}}$, the image under the duality map of their supremum $a \sqcup b$ equals the infimum of their images, i.e., $\text{ofDual}(a \sqcup b) = \text{ofDual}(a) \sqcap \text{ofDual}(b)$.

toDual_inf theorem

[Min α] (a b : α) : toDual (a ⊓ b) = toDual a ⊔ toDual b

Full source

@[simp]
theorem toDual_inf [Min α] (a b : α) : toDual (a ⊓ b) = toDualtoDual a ⊔ toDual b :=
  rfl

Duality Transformation of Infimum Equals Supremum of Duals

Informal description

Let $\alpha$ be a type with a minimum operation (meet-semilattice structure). For any elements $a, b$ in $\alpha$, the image under the duality map of their infimum $a \sqcap b$ equals the supremum of their images under the duality map, i.e., $\text{toDual}(a \sqcap b) = \text{toDual}(a) \sqcup \text{toDual}(b)$.

toDual_sup theorem

[Max α] (a b : α) : toDual (a ⊔ b) = toDual a ⊓ toDual b

Full source

@[simp]
theorem toDual_sup [Max α] (a b : α) : toDual (a ⊔ b) = toDualtoDual a ⊓ toDual b :=
  rfl

Duality Transformation of Supremum Equals Infimum of Duals

Informal description

Let $\alpha$ be a type with a maximum operation (join-semilattice structure). For any elements $a, b$ in $\alpha$, the image under the duality map of their supremum $a \sqcup b$ equals the infimum of their images under the duality map, i.e., $\text{toDual}(a \sqcup b) = \text{toDual}(a) \sqcap \text{toDual}(b)$.

ofDual_min theorem

(a b : αᵒᵈ) : ofDual (min a b) = max (ofDual a) (ofDual b)

Full source

@[simp]
theorem ofDual_min (a b : αᵒᵈ) : ofDual (min a b) = max (ofDual a) (ofDual b) :=
  rfl

Duality Transformation of Minimum Equals Maximum of Duals

Informal description

For any elements $a, b$ in the order dual $\alpha^\mathrm{op}$ of a lattice $\alpha$, the image under the duality map of their minimum $\min(a, b)$ equals the maximum of their images under the duality map, i.e., $\text{ofDual}(\min(a, b)) = \max(\text{ofDual}(a), \text{ofDual}(b))$.

ofDual_max theorem

(a b : αᵒᵈ) : ofDual (max a b) = min (ofDual a) (ofDual b)

Full source

@[simp]
theorem ofDual_max (a b : αᵒᵈ) : ofDual (max a b) = min (ofDual a) (ofDual b) :=
  rfl

Duality Transformation of Maximum Equals Minimum of Duals

Informal description

For any elements $a, b$ in the order dual $\alpha^{\text{op}}$ of a lattice $\alpha$, the image under the duality map of their maximum $\max(a, b)$ equals the minimum of their images under the duality map, i.e., $\text{ofDual}(\max(a, b)) = \min(\text{ofDual}(a), \text{ofDual}(b))$.

toDual_min theorem

(a b : α) : toDual (min a b) = max (toDual a) (toDual b)

Full source

@[simp]
theorem toDual_min (a b : α) : toDual (min a b) = max (toDual a) (toDual b) :=
  rfl

Duality of Minimum and Maximum via Order Dual

Informal description

For any elements $a$ and $b$ in a type $\alpha$ with a meet-semilattice structure, the dual of the minimum of $a$ and $b$ equals the maximum of the duals of $a$ and $b$. That is, $\text{toDual}(\min(a, b)) = \max(\text{toDual}(a), \text{toDual}(b))$.

toDual_max theorem

(a b : α) : toDual (max a b) = min (toDual a) (toDual b)

Full source

@[simp]
theorem toDual_max (a b : α) : toDual (max a b) = min (toDual a) (toDual b) :=
  rfl

Dual of Maximum Equals Minimum of Duals

Informal description

For any elements $a$ and $b$ in a type $\alpha$, the dual of their maximum $\max(a, b)$ equals the minimum of their duals $\min(\text{toDual}(a), \text{toDual}(b))$.

Pi.instMaxForall_mathlib instance

[∀ i, Max (α' i)] : Max (∀ i, α' i)

Full source

instance [∀ i, Max (α' i)] : Max (∀ i, α' i) :=
  ⟨fun f g i => f i ⊔ g i⟩

Pointwise Maximum Operation on Product Types

Informal description

For any family of types $(α'_i)_{i \in \iota}$ where each $α'_i$ has a maximum operation, the product type $\prod_{i \in \iota} α'_i$ also has a maximum operation defined pointwise. That is, for any two functions $f, g \in \prod_{i \in \iota} α'_i$, their supremum $f \sqcup g$ is the function given by $(f \sqcup g)(i) = f(i) \sqcup g(i)$ for each $i \in \iota$.

Pi.sup_apply theorem

[∀ i, Max (α' i)] (f g : ∀ i, α' i) (i : ι) : (f ⊔ g) i = f i ⊔ g i

Full source

@[simp]
theorem sup_apply [∀ i, Max (α' i)] (f g : ∀ i, α' i) (i : ι) : (f ⊔ g) i = f i ⊔ g i :=
  rfl

Pointwise Evaluation of Supremum in Product Lattice

Informal description

For any family of types $(α'_i)_{i \in \iota}$ where each $α'_i$ has a maximum operation, and for any two functions $f, g \in \prod_{i \in \iota} α'_i$, the evaluation of their supremum $f \sqcup g$ at any index $i \in \iota$ equals the supremum of their evaluations at $i$, i.e., $(f \sqcup g)(i) = f(i) \sqcup g(i)$.

Pi.sup_def theorem

[∀ i, Max (α' i)] (f g : ∀ i, α' i) : f ⊔ g = fun i => f i ⊔ g i

Full source

theorem sup_def [∀ i, Max (α' i)] (f g : ∀ i, α' i) : f ⊔ g = fun i => f i ⊔ g i :=
  rfl

Pointwise Definition of Supremum for Product Types

Informal description

For any family of types $(α'_i)_{i \in \iota}$ where each $α'_i$ has a maximum operation, and for any two functions $f, g \in \prod_{i \in \iota} α'_i$, the supremum $f \sqcup g$ is equal to the function defined pointwise by $(f \sqcup g)(i) = f(i) \sqcup g(i)$ for each $i \in \iota$.

Pi.instMinForall_mathlib instance

[∀ i, Min (α' i)] : Min (∀ i, α' i)

Full source

instance [∀ i, Min (α' i)] : Min (∀ i, α' i) :=
  ⟨fun f g i => f i ⊓ g i⟩

Pointwise Minimum Operation on Product Types

Informal description

For any family of types $\alpha'$ indexed by $i$ where each $\alpha' i$ has a minimum operation, the product type $\forall i, \alpha' i$ also has a minimum operation defined pointwise.

Pi.inf_apply theorem

[∀ i, Min (α' i)] (f g : ∀ i, α' i) (i : ι) : (f ⊓ g) i = f i ⊓ g i

Full source

@[simp]
theorem inf_apply [∀ i, Min (α' i)] (f g : ∀ i, α' i) (i : ι) : (f ⊓ g) i = f i ⊓ g i :=
  rfl

Pointwise Infimum Evaluation in Product Types

Informal description

For any family of types $\alpha'$ indexed by $i$ where each $\alpha' i$ has a minimum operation, and for any two functions $f, g \colon \forall i, \alpha' i$, the infimum $f \sqcap g$ evaluated at any index $i$ equals the infimum of $f(i)$ and $g(i)$, i.e., $(f \sqcap g)(i) = f(i) \sqcap g(i)$.

Pi.inf_def theorem

[∀ i, Min (α' i)] (f g : ∀ i, α' i) : f ⊓ g = fun i => f i ⊓ g i

Full source

theorem inf_def [∀ i, Min (α' i)] (f g : ∀ i, α' i) : f ⊓ g = fun i => f i ⊓ g i :=
  rfl

Pointwise Infimum of Functions in Product Types

Informal description

For any family of types $\alpha'$ indexed by $i$ where each $\alpha' i$ has a minimum operation, the pointwise infimum of two functions $f, g \colon \forall i, \alpha' i$ is equal to the function defined by $\lambda i, f i \sqcap g i$.

Pi.instSemilatticeSup instance

[∀ i, SemilatticeSup (α' i)] : SemilatticeSup (∀ i, α' i)

Full source

instance instSemilatticeSup [∀ i, SemilatticeSup (α' i)] : SemilatticeSup (∀ i, α' i) where
  sup x y i := x i ⊔ y i
  le_sup_left _ _ _ := le_sup_left
  le_sup_right _ _ _ := le_sup_right
  sup_le _ _ _ ac bc i := sup_le (ac i) (bc i)

Pointwise Join-Semilattice Structure on Product Types

Informal description

For any family of types $\alpha'$ indexed by $i$ where each $\alpha' i$ is a join-semilattice, the product type $\forall i, \alpha' i$ is also a join-semilattice with the pointwise supremum operation defined by $(f \sqcup g)(i) = f(i) \sqcup g(i)$ for any $f, g \in \forall i, \alpha' i$.

Pi.instSemilatticeInf instance

[∀ i, SemilatticeInf (α' i)] : SemilatticeInf (∀ i, α' i)

Full source

instance instSemilatticeInf [∀ i, SemilatticeInf (α' i)] : SemilatticeInf (∀ i, α' i) where
  inf x y i := x i ⊓ y i
  inf_le_left _ _ _ := inf_le_left
  inf_le_right _ _ _ := inf_le_right
  le_inf _ _ _ ac bc i := le_inf (ac i) (bc i)

Pointwise Meet-Semilattice Structure on Product Types

Informal description

For any family of types $\alpha'$ indexed by $i$ where each $\alpha' i$ is a meet-semilattice, the product type $\forall i, \alpha' i$ is also a meet-semilattice with the pointwise infimum operation defined by $(f \sqcap g)(i) = f(i) \sqcap g(i)$ for any $f, g \in \forall i, \alpha' i$.

Pi.instLattice instance

[∀ i, Lattice (α' i)] : Lattice (∀ i, α' i)

Full source

instance instLattice [∀ i, Lattice (α' i)] : Lattice (∀ i, α' i) where

Pointwise Lattice Structure on Product Types

Informal description

For any family of types $\alpha'$ indexed by $i$ where each $\alpha' i$ is a lattice, the product type $\forall i, \alpha' i$ is also a lattice with the pointwise supremum and infimum operations defined by $(f \sqcup g)(i) = f(i) \sqcup g(i)$ and $(f \sqcap g)(i) = f(i) \sqcap g(i)$ for any $f, g \in \forall i, \alpha' i$.

Pi.instDistribLattice instance

[∀ i, DistribLattice (α' i)] : DistribLattice (∀ i, α' i)

Full source

instance instDistribLattice [∀ i, DistribLattice (α' i)] : DistribLattice (∀ i, α' i) where
  le_sup_inf _ _ _ _ := le_sup_inf

Pointwise Distributive Lattice Structure on Product Types

Informal description

For any family of types $\alpha'$ indexed by $i$ where each $\alpha' i$ is a distributive lattice, the product type $\forall i, \alpha' i$ is also a distributive lattice with the pointwise supremum and infimum operations defined by $(f \sqcup g)(i) = f(i) \sqcup g(i)$ and $(f \sqcap g)(i) = f(i) \sqcap g(i)$ for any $f, g \in \forall i, \alpha' i$.

Function.update_sup theorem

 [∀ i, SemilatticeSup (π i)] (f : ∀ i, π i) (i : ι) (a b : π i) : update f i (a ⊔ b) = update f i a ⊔ update f i b

Full source

theorem update_sup [∀ i, SemilatticeSup (π i)] (f : ∀ i, π i) (i : ι) (a b : π i) :
    update f i (a ⊔ b) = updateupdate f i a ⊔ update f i b :=
  funext fun j => by obtain rfl | hji := eq_or_ne j i <;> simp [update_of_ne, *]

Join Preservation under Function Update in Product Semilattices

Informal description

Let $\pi$ be a family of join-semilattices indexed by $i \in \iota$. For any function $f : \forall i, \pi i$, any index $i \in \iota$, and any elements $a, b \in \pi i$, the update of $f$ at $i$ with the join $a \sqcup b$ is equal to the join of the updates of $f$ at $i$ with $a$ and $b$ respectively. That is, \[ \text{update } f \, i \, (a \sqcup b) = \text{update } f \, i \, a \sqcup \text{update } f \, i \, b. \]

Function.update_inf theorem

 [∀ i, SemilatticeInf (π i)] (f : ∀ i, π i) (i : ι) (a b : π i) : update f i (a ⊓ b) = update f i a ⊓ update f i b

Full source

theorem update_inf [∀ i, SemilatticeInf (π i)] (f : ∀ i, π i) (i : ι) (a b : π i) :
    update f i (a ⊓ b) = updateupdate f i a ⊓ update f i b :=
  funext fun j => by obtain rfl | hji := eq_or_ne j i <;> simp [update_of_ne, *]

Meet Preservation under Function Update in Product Semilattices

Informal description

Let $\pi$ be a family of meet-semilattices indexed by $i \in \iota$. For any function $f : \forall i, \pi i$, any index $i \in \iota$, and any elements $a, b \in \pi i$, the update of $f$ at $i$ with the meet $a \sqcap b$ is equal to the meet of the updates of $f$ at $i$ with $a$ and $b$ respectively. That is, \[ \text{update } f \, i \, (a \sqcap b) = \text{update } f \, i \, a \sqcap \text{update } f \, i \, b. \]

Monotone.sup theorem

[Preorder α] [SemilatticeSup β] {f g : α → β} (hf : Monotone f) (hg : Monotone g) : Monotone (f ⊔ g)

Full source

/-- Pointwise supremum of two monotone functions is a monotone function. -/
protected theorem sup [Preorder α] [SemilatticeSup β] {f g : α → β} (hf : Monotone f)
    (hg : Monotone g) :
    Monotone (f ⊔ g) := fun _ _ h => sup_le_sup (hf h) (hg h)

Monotonicity of Pointwise Supremum of Monotone Functions

Informal description

Let $\alpha$ be a preorder and $\beta$ be a join-semilattice. Given two monotone functions $f, g : \alpha \to \beta$, their pointwise supremum $f \sqcup g$ (defined by $(f \sqcup g)(x) = f(x) \sqcup g(x)$ for all $x \in \alpha$) is also monotone.

Monotone.inf theorem

[Preorder α] [SemilatticeInf β] {f g : α → β} (hf : Monotone f) (hg : Monotone g) : Monotone (f ⊓ g)

Full source

/-- Pointwise infimum of two monotone functions is a monotone function. -/
protected theorem inf [Preorder α] [SemilatticeInf β] {f g : α → β} (hf : Monotone f)
    (hg : Monotone g) :
    Monotone (f ⊓ g) := fun _ _ h => inf_le_inf (hf h) (hg h)

Monotonicity of Pointwise Infimum of Monotone Functions

Informal description

Let $\alpha$ be a preorder and $\beta$ be a meet-semilattice. For any two monotone functions $f, g : \alpha \to \beta$, their pointwise infimum $f \sqcap g$ (defined by $(f \sqcap g)(x) = f(x) \sqcap g(x)$ for all $x \in \alpha$) is also monotone.

Monotone.max theorem

 [Preorder α] [LinearOrder β] {f g : α → β} (hf : Monotone f) (hg : Monotone g) : Monotone fun x => max (f x) (g x)

Full source

/-- Pointwise maximum of two monotone functions is a monotone function. -/
protected theorem max [Preorder α] [LinearOrder β] {f g : α → β} (hf : Monotone f)
    (hg : Monotone g) :
    Monotone fun x => max (f x) (g x) :=
  hf.sup hg

Monotonicity of Pointwise Maximum of Monotone Functions in Linear Orders

Informal description

Let $\alpha$ be a preorder and $\beta$ be a linearly ordered set. Given two monotone functions $f, g : \alpha \to \beta$, the pointwise maximum function $x \mapsto \max(f(x), g(x))$ is also monotone.

Monotone.min theorem

 [Preorder α] [LinearOrder β] {f g : α → β} (hf : Monotone f) (hg : Monotone g) : Monotone fun x => min (f x) (g x)

Full source

/-- Pointwise minimum of two monotone functions is a monotone function. -/
protected theorem min [Preorder α] [LinearOrder β] {f g : α → β} (hf : Monotone f)
    (hg : Monotone g) :
    Monotone fun x => min (f x) (g x) :=
  hf.inf hg

Monotonicity of Pointwise Minimum of Monotone Functions in Linear Orders

Informal description

Let $\alpha$ be a preorder and $\beta$ be a linearly ordered set. For any two monotone functions $f, g : \alpha \to \beta$, the pointwise minimum function $x \mapsto \min(f(x), g(x))$ is also monotone.

Monotone.le_map_sup theorem

[SemilatticeSup α] [SemilatticeSup β] {f : α → β} (h : Monotone f) (x y : α) : f x ⊔ f y ≤ f (x ⊔ y)

Full source

theorem le_map_sup [SemilatticeSup α] [SemilatticeSup β] {f : α → β} (h : Monotone f) (x y : α) :
    f x ⊔ f y ≤ f (x ⊔ y) :=
  sup_le (h le_sup_left) (h le_sup_right)

Monotonicity Preserves Supremum Inequality

Informal description

Let $\alpha$ and $\beta$ be join-semilattices, and let $f : \alpha \to \beta$ be a monotone function. Then for any elements $x, y \in \alpha$, the supremum of $f(x)$ and $f(y)$ is less than or equal to $f$ applied to the supremum of $x$ and $y$, i.e., $f(x) \sqcup f(y) \leq f(x \sqcup y)$.

Monotone.map_inf_le theorem

[SemilatticeInf α] [SemilatticeInf β] {f : α → β} (h : Monotone f) (x y : α) : f (x ⊓ y) ≤ f x ⊓ f y

Full source

theorem map_inf_le [SemilatticeInf α] [SemilatticeInf β] {f : α → β} (h : Monotone f) (x y : α) :
    f (x ⊓ y) ≤ f x ⊓ f y :=
  le_inf (h inf_le_left) (h inf_le_right)

Monotonicity Preserves Infimum Inequality

Informal description

Let $\alpha$ and $\beta$ be meet-semilattices, and let $f : \alpha \to \beta$ be a monotone function. Then for any elements $x, y \in \alpha$, we have $f(x \sqcap y) \leq f(x) \sqcap f(y)$.

Monotone.of_map_inf_le_left theorem

[SemilatticeInf α] [Preorder β] {f : α → β} (h : ∀ x y, f (x ⊓ y) ≤ f x) : Monotone f

Full source

theorem of_map_inf_le_left [SemilatticeInf α] [Preorder β] {f : α → β}
    (h : ∀ x y, f (x ⊓ y) ≤ f x) : Monotone f := by
  intro x y hxy
  rw [← inf_eq_right.2 hxy]
  apply h

Monotonicity Criterion via Infimum Inequality on the Left

Informal description

Let $\alpha$ be a meet-semilattice and $\beta$ a preorder. For a function $f : \alpha \to \beta$, if for all $x, y \in \alpha$ we have $f(x \sqcap y) \leq f(x)$, then $f$ is monotone.

Monotone.of_map_inf_le theorem

[SemilatticeInf α] [SemilatticeInf β] {f : α → β} (h : ∀ x y, f (x ⊓ y) ≤ f x ⊓ f y) : Monotone f

Full source

theorem of_map_inf_le [SemilatticeInf α] [SemilatticeInf β] {f : α → β}
    (h : ∀ x y, f (x ⊓ y) ≤ f x ⊓ f y) : Monotone f :=
  of_map_inf_le_left fun x y ↦ (h x y).trans inf_le_left

Monotonicity Criterion via Infimum Inequality

Informal description

Let $\alpha$ and $\beta$ be meet-semilattices. For a function $f : \alpha \to \beta$, if for all $x, y \in \alpha$ we have $f(x \sqcap y) \leq f(x) \sqcap f(y)$, then $f$ is monotone.

Monotone.of_map_inf theorem

[SemilatticeInf α] [SemilatticeInf β] {f : α → β} (h : ∀ x y, f (x ⊓ y) = f x ⊓ f y) : Monotone f

Full source

theorem of_map_inf [SemilatticeInf α] [SemilatticeInf β] {f : α → β}
    (h : ∀ x y, f (x ⊓ y) = f x ⊓ f y) : Monotone f :=
  of_map_inf_le fun x y ↦ (h x y).le

Monotonicity of Infimum-Preserving Functions

Informal description

Let $\alpha$ and $\beta$ be meet-semilattices. For a function $f \colon \alpha \to \beta$, if for all $x, y \in \alpha$ we have $f(x \sqcap y) = f(x) \sqcap f(y)$, then $f$ is monotone.

Monotone.of_left_le_map_sup theorem

[SemilatticeSup α] [Preorder β] {f : α → β} (h : ∀ x y, f x ≤ f (x ⊔ y)) : Monotone f

Full source

theorem of_left_le_map_sup [SemilatticeSup α] [Preorder β] {f : α → β}
    (h : ∀ x y, f x ≤ f (x ⊔ y)) : Monotone f :=
  monotone_dual_iff.1 <| of_map_inf_le_left h

Monotonicity Criterion via Supremum Inequality on the Left

Informal description

Let $\alpha$ be a join-semilattice and $\beta$ a preorder. For a function $f : \alpha \to \beta$, if for all $x, y \in \alpha$ we have $f(x) \leq f(x \sqcup y)$, then $f$ is monotone.

Monotone.of_le_map_sup theorem

[SemilatticeSup α] [SemilatticeSup β] {f : α → β} (h : ∀ x y, f x ⊔ f y ≤ f (x ⊔ y)) : Monotone f

Full source

theorem of_le_map_sup [SemilatticeSup α] [SemilatticeSup β] {f : α → β}
    (h : ∀ x y, f x ⊔ f y ≤ f (x ⊔ y)) : Monotone f :=
  monotone_dual_iff.mp <| of_map_inf_le h

Monotonicity Criterion via Supremum Inequality

Informal description

Let $\alpha$ and $\beta$ be join-semilattices. For a function $f : \alpha \to \beta$, if for all $x, y \in \alpha$ we have $f(x) \sqcup f(y) \leq f(x \sqcup y)$, then $f$ is monotone.

Monotone.of_map_sup theorem

[SemilatticeSup α] [SemilatticeSup β] {f : α → β} (h : ∀ x y, f (x ⊔ y) = f x ⊔ f y) : Monotone f

Full source

theorem of_map_sup [SemilatticeSup α] [SemilatticeSup β] {f : α → β}
    (h : ∀ x y, f (x ⊔ y) = f x ⊔ f y) : Monotone f :=
  (@of_map_inf (OrderDual α) (OrderDual β) _ _ _ h).dual

Supremum-Preserving Functions are Monotone

Informal description

Let $\alpha$ and $\beta$ be join-semilattices. For a function $f \colon \alpha \to \beta$, if for all $x, y \in \alpha$ we have $f(x \sqcup y) = f(x) \sqcup f(y)$, then $f$ is monotone.

Monotone.map_sup theorem

[SemilatticeSup β] {f : α → β} (hf : Monotone f) (x y : α) : f (x ⊔ y) = f x ⊔ f y

Full source

theorem map_sup [SemilatticeSup β] {f : α → β} (hf : Monotone f) (x y : α) :
    f (x ⊔ y) = f x ⊔ f y :=
  (IsTotal.total x y).elim (fun h : x ≤ y => by simp only [h, hf h, sup_of_le_right]) fun h => by
    simp only [h, hf h, sup_of_le_left]

Monotone Functions Preserve Suprema

Informal description

Let $\alpha$ and $\beta$ be join-semilattices, and let $f : \alpha \to \beta$ be a monotone function. Then for any elements $x, y \in \alpha$, the function $f$ preserves the supremum operation, i.e., $f(x \sqcup y) = f(x) \sqcup f(y)$.

Monotone.map_inf theorem

[SemilatticeInf β] {f : α → β} (hf : Monotone f) (x y : α) : f (x ⊓ y) = f x ⊓ f y

Full source

theorem map_inf [SemilatticeInf β] {f : α → β} (hf : Monotone f) (x y : α) :
    f (x ⊓ y) = f x ⊓ f y :=
  hf.dual.map_sup _ _

Monotone Functions Preserve Infima

Informal description

Let $\alpha$ be a type and $\beta$ be a meet-semilattice. For any monotone function $f : \alpha \to \beta$ and elements $x, y \in \alpha$, the function $f$ preserves the infimum operation, i.e., $f(x \sqcap y) = f(x) \sqcap f(y)$.

MonotoneOn.sup theorem

 [Preorder α] [SemilatticeSup β] {f g : α → β} {s : Set α} (hf : MonotoneOn f s) (hg : MonotoneOn g s) :
  MonotoneOn (f ⊔ g) s

Full source

/-- Pointwise supremum of two monotone functions is a monotone function. -/
protected theorem sup [Preorder α] [SemilatticeSup β] {f g : α → β} {s : Set α}
    (hf : MonotoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (f ⊔ g) s :=
  fun _ hx _ hy h => sup_le_sup (hf hx hy h) (hg hx hy h)

Monotonicity of Pointwise Supremum of Monotone Functions

Informal description

Let $\alpha$ be a preorder and $\beta$ a join-semilattice. Given two functions $f, g : \alpha \to \beta$ that are monotone on a subset $s \subseteq \alpha$, their pointwise supremum $f \sqcup g$ (defined by $(f \sqcup g)(x) = f(x) \sqcup g(x)$ for all $x \in \alpha$) is also monotone on $s$.

MonotoneOn.inf theorem

 [Preorder α] [SemilatticeInf β] {f g : α → β} {s : Set α} (hf : MonotoneOn f s) (hg : MonotoneOn g s) :
  MonotoneOn (f ⊓ g) s

Full source

/-- Pointwise infimum of two monotone functions is a monotone function. -/
protected theorem inf [Preorder α] [SemilatticeInf β] {f g : α → β} {s : Set α}
    (hf : MonotoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (f ⊓ g) s :=
  (hf.dual.sup hg.dual).dual

Monotonicity of Pointwise Infimum of Monotone Functions

Informal description

Let $\alpha$ be a preorder and $\beta$ a meet-semilattice. Given two functions $f, g \colon \alpha \to \beta$ that are monotone on a subset $s \subseteq \alpha$, their pointwise infimum $f \sqcap g$ (defined by $(f \sqcap g)(x) = f(x) \sqcap g(x)$ for all $x \in \alpha$) is also monotone on $s$.

MonotoneOn.max theorem

 [Preorder α] [LinearOrder β] {f g : α → β} {s : Set α} (hf : MonotoneOn f s) (hg : MonotoneOn g s) :
  MonotoneOn (fun x => max (f x) (g x)) s

Full source

/-- Pointwise maximum of two monotone functions is a monotone function. -/
protected theorem max [Preorder α] [LinearOrder β] {f g : α → β} {s : Set α} (hf : MonotoneOn f s)
    (hg : MonotoneOn g s) : MonotoneOn (fun x => max (f x) (g x)) s :=
  hf.sup hg

Monotonicity of Pointwise Maximum of Monotone Functions

Informal description

Let $\alpha$ be a preorder and $\beta$ a linear order. Given two functions $f, g : \alpha \to \beta$ that are monotone on a subset $s \subseteq \alpha$, the pointwise maximum function $x \mapsto \max(f(x), g(x))$ is also monotone on $s$.

MonotoneOn.min theorem

 [Preorder α] [LinearOrder β] {f g : α → β} {s : Set α} (hf : MonotoneOn f s) (hg : MonotoneOn g s) :
  MonotoneOn (fun x => min (f x) (g x)) s

Full source

/-- Pointwise minimum of two monotone functions is a monotone function. -/
protected theorem min [Preorder α] [LinearOrder β] {f g : α → β} {s : Set α} (hf : MonotoneOn f s)
    (hg : MonotoneOn g s) : MonotoneOn (fun x => min (f x) (g x)) s :=
  hf.inf hg

Monotonicity of Pointwise Minimum of Monotone Functions

Informal description

Let $\alpha$ be a preorder and $\beta$ a linear order. Given two functions $f, g \colon \alpha \to \beta$ that are monotone on a subset $s \subseteq \alpha$, the pointwise minimum function $x \mapsto \min(f(x), g(x))$ is also monotone on $s$.

MonotoneOn.of_map_inf theorem

[SemilatticeInf α] [SemilatticeInf β] (h : ∀ x ∈ s, ∀ y ∈ s, f (x ⊓ y) = f x ⊓ f y) : MonotoneOn f s

Full source

theorem of_map_inf [SemilatticeInf α] [SemilatticeInf β]
    (h : ∀ x ∈ s, ∀ y ∈ s, f (x ⊓ y) = f x ⊓ f y) : MonotoneOn f s := fun x hx y hy hxy =>
  inf_eq_left.1 <| by rw [← h _ hx _ hy, inf_eq_left.2 hxy]

Monotonicity from Meet-Preserving Property on Subset

Informal description

Let $\alpha$ and $\beta$ be meet-semilattices, and let $f : \alpha \to \beta$ be a function defined on a subset $s \subseteq \alpha$. If for all $x, y \in s$, the function $f$ satisfies $f(x \sqcap y) = f(x) \sqcap f(y)$, then $f$ is monotone on $s$.

MonotoneOn.of_map_sup theorem

[SemilatticeSup α] [SemilatticeSup β] (h : ∀ x ∈ s, ∀ y ∈ s, f (x ⊔ y) = f x ⊔ f y) : MonotoneOn f s

Full source

theorem of_map_sup [SemilatticeSup α] [SemilatticeSup β]
    (h : ∀ x ∈ s, ∀ y ∈ s, f (x ⊔ y) = f x ⊔ f y) : MonotoneOn f s :=
  (@of_map_inf αᵒᵈ βᵒᵈ _ _ _ _ h).dual

Monotonicity from Join-Preserving Property on Subset

Informal description

Let $\alpha$ and $\beta$ be join-semilattices, and let $f : \alpha \to \beta$ be a function defined on a subset $s \subseteq \alpha$. If for all $x, y \in s$, the function $f$ satisfies $f(x \sqcup y) = f(x) \sqcup f(y)$, then $f$ is monotone on $s$.

MonotoneOn.map_sup theorem

[SemilatticeSup β] (hf : MonotoneOn f s) (hx : x ∈ s) (hy : y ∈ s) : f (x ⊔ y) = f x ⊔ f y

Full source

theorem map_sup [SemilatticeSup β] (hf : MonotoneOn f s) (hx : x ∈ s) (hy : y ∈ s) :
    f (x ⊔ y) = f x ⊔ f y := by
  cases le_total x y <;> have := hf ?_ ?_ ‹_› <;>
    first
    | assumption
    | simp only [*, sup_of_le_left, sup_of_le_right]

Join-Preservation Property of Monotone Functions on Subsets

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ equipped with a join-semilattice structure. Given a function $f : \alpha \to \beta$ that is monotone on a subset $s \subseteq \alpha$, and elements $x, y \in s$, the function $f$ preserves the join operation, i.e., $f(x \sqcup y) = f(x) \sqcup f(y)$.

MonotoneOn.map_inf theorem

[SemilatticeInf β] (hf : MonotoneOn f s) (hx : x ∈ s) (hy : y ∈ s) : f (x ⊓ y) = f x ⊓ f y

Full source

theorem map_inf [SemilatticeInf β] (hf : MonotoneOn f s) (hx : x ∈ s) (hy : y ∈ s) :
    f (x ⊓ y) = f x ⊓ f y :=
  hf.dual.map_sup hx hy

Meet-Preservation Property of Monotone Functions on Subsets

Informal description

Let $\alpha$ be a type and $\beta$ be a meet-semilattice. Given a function $f : \alpha \to \beta$ that is monotone on a subset $s \subseteq \alpha$, and elements $x, y \in s$, the function $f$ preserves the meet operation, i.e., $f(x \sqcap y) = f(x) \sqcap f(y)$.

Antitone.sup theorem

[Preorder α] [SemilatticeSup β] {f g : α → β} (hf : Antitone f) (hg : Antitone g) : Antitone (f ⊔ g)

Full source

/-- Pointwise supremum of two monotone functions is a monotone function. -/
protected theorem sup [Preorder α] [SemilatticeSup β] {f g : α → β} (hf : Antitone f)
    (hg : Antitone g) :
    Antitone (f ⊔ g) := fun _ _ h => sup_le_sup (hf h) (hg h)

Pointwise Supremum of Antitone Functions is Antitone

Informal description

Let $\alpha$ be a preorder and $\beta$ be a join-semilattice. For any two antitone functions $f, g : \alpha \to \beta$, their pointwise supremum $f \sqcup g$ is also antitone. That is, for any $x, y \in \alpha$ with $x \leq y$, we have $(f \sqcup g)(y) \leq (f \sqcup g)(x)$.

Antitone.inf theorem

[Preorder α] [SemilatticeInf β] {f g : α → β} (hf : Antitone f) (hg : Antitone g) : Antitone (f ⊓ g)

Full source

/-- Pointwise infimum of two monotone functions is a monotone function. -/
protected theorem inf [Preorder α] [SemilatticeInf β] {f g : α → β} (hf : Antitone f)
    (hg : Antitone g) :
    Antitone (f ⊓ g) := fun _ _ h => inf_le_inf (hf h) (hg h)

Pointwise Infimum of Antitone Functions is Antitone

Informal description

Let $\alpha$ be a preorder and $\beta$ be a meet-semilattice. For any two antitone functions $f, g : \alpha \to \beta$, their pointwise infimum $f \sqcap g$ is also antitone. That is, for any $x, y \in \alpha$ with $x \leq y$, we have $(f \sqcap g)(y) \leq (f \sqcap g)(x)$.

Antitone.max theorem

 [Preorder α] [LinearOrder β] {f g : α → β} (hf : Antitone f) (hg : Antitone g) : Antitone fun x => max (f x) (g x)

Full source

/-- Pointwise maximum of two monotone functions is a monotone function. -/
protected theorem max [Preorder α] [LinearOrder β] {f g : α → β} (hf : Antitone f)
    (hg : Antitone g) :
    Antitone fun x => max (f x) (g x) :=
  hf.sup hg

Pointwise Maximum of Antitone Functions is Antitone

Informal description

Let $\alpha$ be a preorder and $\beta$ be a linearly ordered set. For any two antitone functions $f, g : \alpha \to \beta$, the pointwise maximum function $x \mapsto \max(f(x), g(x))$ is also antitone. That is, for any $x, y \in \alpha$ with $x \leq y$, we have $\max(f(y), g(y)) \leq \max(f(x), g(x))$.

Antitone.min theorem

 [Preorder α] [LinearOrder β] {f g : α → β} (hf : Antitone f) (hg : Antitone g) : Antitone fun x => min (f x) (g x)

Full source

/-- Pointwise minimum of two monotone functions is a monotone function. -/
protected theorem min [Preorder α] [LinearOrder β] {f g : α → β} (hf : Antitone f)
    (hg : Antitone g) :
    Antitone fun x => min (f x) (g x) :=
  hf.inf hg

Pointwise Minimum of Antitone Functions is Antitone

Informal description

Let $\alpha$ be a preorder and $\beta$ be a linearly ordered set. For any two antitone functions $f, g : \alpha \to \beta$, the pointwise minimum function $x \mapsto \min(f(x), g(x))$ is also antitone. That is, for any $x, y \in \alpha$ with $x \leq y$, we have $\min(f(y), g(y)) \leq \min(f(x), g(x))$.

Antitone.map_sup_le theorem

[SemilatticeSup α] [SemilatticeInf β] {f : α → β} (h : Antitone f) (x y : α) : f (x ⊔ y) ≤ f x ⊓ f y

Full source

theorem map_sup_le [SemilatticeSup α] [SemilatticeInf β] {f : α → β} (h : Antitone f) (x y : α) :
    f (x ⊔ y) ≤ f x ⊓ f y :=
  h.dual_right.le_map_sup x y

Antitone Function Inequality: $f(x \sqcup y) \leq f(x) \sqcap f(y)$

Informal description

Let $\alpha$ be a join-semilattice and $\beta$ be a meet-semilattice. For any antitone function $f : \alpha \to \beta$ and elements $x, y \in \alpha$, the image of the supremum $x \sqcup y$ under $f$ is less than or equal to the infimum of $f(x)$ and $f(y)$, i.e., $f(x \sqcup y) \leq f(x) \sqcap f(y)$.

Antitone.le_map_inf theorem

[SemilatticeInf α] [SemilatticeSup β] {f : α → β} (h : Antitone f) (x y : α) : f x ⊔ f y ≤ f (x ⊓ y)

Full source

theorem le_map_inf [SemilatticeInf α] [SemilatticeSup β] {f : α → β} (h : Antitone f) (x y : α) :
    f x ⊔ f y ≤ f (x ⊓ y) :=
  h.dual_right.map_inf_le x y

Antitone Function Inequality: $f(x) \sqcup f(y) \leq f(x \sqcap y)$

Informal description

Let $\alpha$ be a meet-semilattice and $\beta$ be a join-semilattice. For any antitone function $f : \alpha \to \beta$ and elements $x, y \in \alpha$, the supremum of $f(x)$ and $f(y)$ is less than or equal to $f$ evaluated at the infimum of $x$ and $y$, i.e., $f(x) \sqcup f(y) \leq f(x \sqcap y)$.

Antitone.map_sup theorem

[SemilatticeInf β] {f : α → β} (hf : Antitone f) (x y : α) : f (x ⊔ y) = f x ⊓ f y

Full source

theorem map_sup [SemilatticeInf β] {f : α → β} (hf : Antitone f) (x y : α) :
    f (x ⊔ y) = f x ⊓ f y :=
  hf.dual_right.map_sup x y

Antitone Function Maps Supremum to Infimum: $f(x \sqcup y) = f(x) \sqcap f(y)$

Informal description

Let $\alpha$ be a type with a join-semilattice structure and $\beta$ be a type with a meet-semilattice structure. For any antitone function $f : \alpha \to \beta$ and elements $x, y \in \alpha$, the function $f$ maps the supremum $x \sqcup y$ to the infimum of $f(x)$ and $f(y)$, i.e., $f(x \sqcup y) = f(x) \sqcap f(y)$.

Antitone.map_inf theorem

[SemilatticeSup β] {f : α → β} (hf : Antitone f) (x y : α) : f (x ⊓ y) = f x ⊔ f y

Full source

theorem map_inf [SemilatticeSup β] {f : α → β} (hf : Antitone f) (x y : α) :
    f (x ⊓ y) = f x ⊔ f y :=
  hf.dual_right.map_inf x y

Antitone Function Maps Infimum to Supremum: $f(x \sqcap y) = f(x) \sqcup f(y)$

Informal description

Let $\alpha$ be a type and $\beta$ be a join-semilattice. For any antitone function $f : \alpha \to \beta$ and elements $x, y \in \alpha$, the function $f$ maps the infimum of $x$ and $y$ to the supremum of $f(x)$ and $f(y)$, i.e., $f(x \sqcap y) = f(x) \sqcup f(y)$.

AntitoneOn.sup theorem

 [Preorder α] [SemilatticeSup β] {f g : α → β} {s : Set α} (hf : AntitoneOn f s) (hg : AntitoneOn g s) :
  AntitoneOn (f ⊔ g) s

Full source

/-- Pointwise supremum of two antitone functions is an antitone function. -/
protected theorem sup [Preorder α] [SemilatticeSup β] {f g : α → β} {s : Set α}
    (hf : AntitoneOn f s) (hg : AntitoneOn g s) : AntitoneOn (f ⊔ g) s :=
  fun _ hx _ hy h => sup_le_sup (hf hx hy h) (hg hx hy h)

Pointwise Supremum of Antitone Functions is Antitone

Informal description

Let $\alpha$ be a preorder and $\beta$ a join-semilattice. Given two functions $f, g : \alpha \to \beta$ that are antitone on a set $s \subseteq \alpha$, their pointwise supremum $f \sqcup g$ (defined by $(f \sqcup g)(x) = f(x) \sqcup g(x)$ for all $x \in \alpha$) is also antitone on $s$.

AntitoneOn.inf theorem

 [Preorder α] [SemilatticeInf β] {f g : α → β} {s : Set α} (hf : AntitoneOn f s) (hg : AntitoneOn g s) :
  AntitoneOn (f ⊓ g) s

Full source

/-- Pointwise infimum of two antitone functions is an antitone function. -/
protected theorem inf [Preorder α] [SemilatticeInf β] {f g : α → β} {s : Set α}
    (hf : AntitoneOn f s) (hg : AntitoneOn g s) : AntitoneOn (f ⊓ g) s :=
  (hf.dual.sup hg.dual).dual

Pointwise Infimum of Antitone Functions is Antitone

Informal description

Let $\alpha$ be a preorder and $\beta$ a meet-semilattice. Given two functions $f, g \colon \alpha \to \beta$ that are antitone on a subset $s \subseteq \alpha$, their pointwise infimum $f \sqcap g$ (defined by $(f \sqcap g)(x) = f(x) \sqcap g(x)$ for all $x \in \alpha$) is also antitone on $s$.

AntitoneOn.max theorem

 [Preorder α] [LinearOrder β] {f g : α → β} {s : Set α} (hf : AntitoneOn f s) (hg : AntitoneOn g s) :
  AntitoneOn (fun x => max (f x) (g x)) s

Full source

/-- Pointwise maximum of two antitone functions is an antitone function. -/
protected theorem max [Preorder α] [LinearOrder β] {f g : α → β} {s : Set α} (hf : AntitoneOn f s)
    (hg : AntitoneOn g s) : AntitoneOn (fun x => max (f x) (g x)) s :=
  hf.sup hg

Pointwise Maximum of Antitone Functions is Antitone on a Linear Order

Informal description

Let $\alpha$ be a preorder and $\beta$ a linear order. Given two functions $f, g : \alpha \to \beta$ that are antitone on a subset $s \subseteq \alpha$, the pointwise maximum function $x \mapsto \max(f(x), g(x))$ is also antitone on $s$.

AntitoneOn.min theorem

 [Preorder α] [LinearOrder β] {f g : α → β} {s : Set α} (hf : AntitoneOn f s) (hg : AntitoneOn g s) :
  AntitoneOn (fun x => min (f x) (g x)) s

Full source

/-- Pointwise minimum of two antitone functions is an antitone function. -/
protected theorem min [Preorder α] [LinearOrder β] {f g : α → β} {s : Set α} (hf : AntitoneOn f s)
    (hg : AntitoneOn g s) : AntitoneOn (fun x => min (f x) (g x)) s :=
  hf.inf hg

Pointwise Minimum of Antitone Functions is Antitone on a Linear Order

Informal description

Let $\alpha$ be a preorder and $\beta$ a linear order. Given two functions $f, g \colon \alpha \to \beta$ that are antitone on a subset $s \subseteq \alpha$, the pointwise minimum function $x \mapsto \min(f(x), g(x))$ is also antitone on $s$.

AntitoneOn.of_map_inf theorem

[SemilatticeInf α] [SemilatticeSup β] (h : ∀ x ∈ s, ∀ y ∈ s, f (x ⊓ y) = f x ⊔ f y) : AntitoneOn f s

Full source

theorem of_map_inf [SemilatticeInf α] [SemilatticeSup β]
    (h : ∀ x ∈ s, ∀ y ∈ s, f (x ⊓ y) = f x ⊔ f y) : AntitoneOn f s := fun x hx y hy hxy =>
  sup_eq_left.1 <| by rw [← h _ hx _ hy, inf_eq_left.2 hxy]

Antitone Property from Infimum-to-Supremum Mapping

Informal description

Let $α$ be a meet-semilattice and $β$ a join-semilattice. For a function $f : α \to β$ and a subset $s \subseteq α$, if for all $x, y \in s$ we have $f(x \sqcap y) = f(x) \sqcup f(y)$, then $f$ is antitone on $s$.

AntitoneOn.of_map_sup theorem

[SemilatticeSup α] [SemilatticeInf β] (h : ∀ x ∈ s, ∀ y ∈ s, f (x ⊔ y) = f x ⊓ f y) : AntitoneOn f s

Full source

theorem of_map_sup [SemilatticeSup α] [SemilatticeInf β]
    (h : ∀ x ∈ s, ∀ y ∈ s, f (x ⊔ y) = f x ⊓ f y) : AntitoneOn f s :=
  (@of_map_inf αᵒᵈ βᵒᵈ _ _ _ _ h).dual

Antitone Property from Supremum-to-Infimum Mapping

Informal description

Let $\alpha$ be a join-semilattice and $\beta$ a meet-semilattice. For a function $f : \alpha \to \beta$ and a subset $s \subseteq \alpha$, if for all $x, y \in s$ we have $f(x \sqcup y) = f(x) \sqcap f(y)$, then $f$ is antitone on $s$.

AntitoneOn.map_sup theorem

[SemilatticeInf β] (hf : AntitoneOn f s) (hx : x ∈ s) (hy : y ∈ s) : f (x ⊔ y) = f x ⊓ f y

Full source

theorem map_sup [SemilatticeInf β] (hf : AntitoneOn f s) (hx : x ∈ s) (hy : y ∈ s) :
    f (x ⊔ y) = f x ⊓ f y := by
  cases le_total x y <;> have := hf ?_ ?_ ‹_› <;>
    first
    | assumption
    | simp only [*, sup_of_le_left, sup_of_le_right, inf_of_le_left, inf_of_le_right]

Antitone Function Maps Supremum to Infimum in Meet-Semilattice

Informal description

Let $\beta$ be a meet-semilattice, $f : \alpha \to \beta$ be a function, and $s \subseteq \alpha$ be a subset. If $f$ is antitone on $s$ and $x, y \in s$, then $f(x \sqcup y) = f(x) \sqcap f(y)$.

AntitoneOn.map_inf theorem

[SemilatticeSup β] (hf : AntitoneOn f s) (hx : x ∈ s) (hy : y ∈ s) : f (x ⊓ y) = f x ⊔ f y

Full source

theorem map_inf [SemilatticeSup β] (hf : AntitoneOn f s) (hx : x ∈ s) (hy : y ∈ s) :
    f (x ⊓ y) = f x ⊔ f y :=
  hf.dual.map_sup hx hy

Antitone Function Maps Infimum to Supremum in Join-Semilattice

Informal description

Let $\alpha$ be a type with a meet operation $\sqcap$, $\beta$ be a join-semilattice, and $f : \alpha \to \beta$ be a function. For a subset $s \subseteq \alpha$, if $f$ is antitone on $s$ and $x, y \in s$, then $f(x \sqcap y) = f(x) \sqcup f(y)$.

Prod.instMax_mathlib instance

[Max α] [Max β] : Max (α × β)

Full source

instance [Max α] [Max β] : Max (α × β) :=
  ⟨fun p q => ⟨p.1 ⊔ q.1, p.2 ⊔ q.2⟩⟩

Componentwise Maximum Operation on Product Types

Informal description

For any types $\alpha$ and $\beta$ equipped with a maximum operation, the product type $\alpha \times \beta$ is also equipped with a maximum operation defined componentwise.

Prod.instMin_mathlib instance

[Min α] [Min β] : Min (α × β)

Full source

instance [Min α] [Min β] : Min (α × β) :=
  ⟨fun p q => ⟨p.1 ⊓ q.1, p.2 ⊓ q.2⟩⟩

Minimum Operation on Product Types

Informal description

For types $\alpha$ and $\beta$ each equipped with a minimum operation, the product type $\alpha \times \beta$ is also equipped with a minimum operation defined componentwise.

Prod.mk_sup_mk theorem

[Max α] [Max β] (a₁ a₂ : α) (b₁ b₂ : β) : (a₁, b₁) ⊔ (a₂, b₂) = (a₁ ⊔ a₂, b₁ ⊔ b₂)

Full source

@[simp]
theorem mk_sup_mk [Max α] [Max β] (a₁ a₂ : α) (b₁ b₂ : β) :
    (a₁, b₁)(a₁, b₁) ⊔ (a₂, b₂) = (a₁ ⊔ a₂, b₁ ⊔ b₂) :=
  rfl

Componentwise Supremum of Product Pairs

Informal description

For any types $\alpha$ and $\beta$ equipped with a maximum operation $\sqcup$, and for any elements $a_1, a_2 \in \alpha$ and $b_1, b_2 \in \beta$, the supremum of the pairs $(a_1, b_1)$ and $(a_2, b_2)$ in the product type $\alpha \times \beta$ is equal to the pair of suprema $(a_1 \sqcup a_2, b_1 \sqcup b_2)$.

Prod.mk_inf_mk theorem

[Min α] [Min β] (a₁ a₂ : α) (b₁ b₂ : β) : (a₁, b₁) ⊓ (a₂, b₂) = (a₁ ⊓ a₂, b₁ ⊓ b₂)

Full source

@[simp]
theorem mk_inf_mk [Min α] [Min β] (a₁ a₂ : α) (b₁ b₂ : β) :
    (a₁, b₁)(a₁, b₁) ⊓ (a₂, b₂) = (a₁ ⊓ a₂, b₁ ⊓ b₂) :=
  rfl

Componentwise Meet in Product Lattice: $(a₁, b₁) \sqcap (a₂, b₂) = (a₁ \sqcap a₂, b₁ \sqcap b₂)$

Informal description

For any elements $a₁, a₂$ in a type $\alpha$ with a meet operation $\sqcap$ and any elements $b₁, b₂$ in a type $\beta$ with a meet operation $\sqcap$, the meet of the pairs $(a₁, b₁)$ and $(a₂, b₂)$ in the product type $\alpha \times \beta$ is given by $(a₁ \sqcap a₂, b₁ \sqcap b₂)$.

Prod.fst_sup theorem

[Max α] [Max β] (p q : α × β) : (p ⊔ q).fst = p.fst ⊔ q.fst

Full source

@[simp]
theorem fst_sup [Max α] [Max β] (p q : α × β) : (p ⊔ q).fst = p.fst ⊔ q.fst :=
  rfl

First Component Preserves Supremum in Product Lattice

Informal description

For any types $\alpha$ and $\beta$ equipped with a maximum operation $\sqcup$, and for any pairs $p, q \in \alpha \times \beta$, the first component of the supremum $p \sqcup q$ equals the supremum of the first components of $p$ and $q$, i.e., $(p \sqcup q).1 = p.1 \sqcup q.1$.

Prod.fst_inf theorem

[Min α] [Min β] (p q : α × β) : (p ⊓ q).fst = p.fst ⊓ q.fst

Full source

@[simp]
theorem fst_inf [Min α] [Min β] (p q : α × β) : (p ⊓ q).fst = p.fst ⊓ q.fst :=
  rfl

First Component Preserves Infimum in Product Lattice

Informal description

For any types $\alpha$ and $\beta$ equipped with a minimum operation $\sqcap$, and for any pairs $p, q \in \alpha \times \beta$, the first component of the infimum $p \sqcap q$ equals the infimum of the first components of $p$ and $q$, i.e., $(p \sqcap q).1 = p.1 \sqcap q.1$.

Prod.snd_sup theorem

[Max α] [Max β] (p q : α × β) : (p ⊔ q).snd = p.snd ⊔ q.snd

Full source

@[simp]
theorem snd_sup [Max α] [Max β] (p q : α × β) : (p ⊔ q).snd = p.snd ⊔ q.snd :=
  rfl

Second Component Preserves Supremum in Product Lattice

Informal description

For any types $\alpha$ and $\beta$ equipped with a maximum operation $\sqcup$, and for any pairs $p, q \in \alpha \times \beta$, the second component of the supremum $p \sqcup q$ equals the supremum of the second components of $p$ and $q$, i.e., $(p \sqcup q).2 = p.2 \sqcup q.2$.

Prod.snd_inf theorem

[Min α] [Min β] (p q : α × β) : (p ⊓ q).snd = p.snd ⊓ q.snd

Full source

@[simp]
theorem snd_inf [Min α] [Min β] (p q : α × β) : (p ⊓ q).snd = p.snd ⊓ q.snd :=
  rfl

Second Component Preserves Infimum in Product Lattice

Informal description

For any types $\alpha$ and $\beta$ each equipped with a minimum operation $\sqcap$, and for any pairs $p, q \in \alpha \times \beta$, the second component of the infimum $p \sqcap q$ equals the infimum of the second components of $p$ and $q$, i.e., $(p \sqcap q).2 = p.2 \sqcap q.2$.

Prod.swap_sup theorem

[Max α] [Max β] (p q : α × β) : (p ⊔ q).swap = p.swap ⊔ q.swap

Full source

@[simp]
theorem swap_sup [Max α] [Max β] (p q : α × β) : (p ⊔ q).swap = p.swap ⊔ q.swap :=
  rfl

Swap Commutes with Supremum in Product Lattices

Informal description

For any types $\alpha$ and $\beta$ equipped with a maximum operation $\sqcup$, and for any pairs $p, q \in \alpha \times \beta$, swapping the components of the supremum $p \sqcup q$ is equal to the supremum of the swapped pairs. That is, $(p \sqcup q).\text{swap} = p.\text{swap} \sqcup q.\text{swap}$.

Prod.swap_inf theorem

[Min α] [Min β] (p q : α × β) : (p ⊓ q).swap = p.swap ⊓ q.swap

Full source

@[simp]
theorem swap_inf [Min α] [Min β] (p q : α × β) : (p ⊓ q).swap = p.swap ⊓ q.swap :=
  rfl

Swap Commutes with Infimum in Product Lattices

Informal description

For any types $\alpha$ and $\beta$ equipped with a minimum operation $\sqcap$, and for any pairs $p, q \in \alpha \times \beta$, swapping the components of the infimum $p \sqcap q$ is equal to the infimum of the swapped pairs. That is, $(p \sqcap q).\text{swap} = p.\text{swap} \sqcap q.\text{swap}$.

Prod.sup_def theorem

[Max α] [Max β] (p q : α × β) : p ⊔ q = (p.fst ⊔ q.fst, p.snd ⊔ q.snd)

Full source

theorem sup_def [Max α] [Max β] (p q : α × β) : p ⊔ q = (p.fst ⊔ q.fst, p.snd ⊔ q.snd) :=
  rfl

Componentwise Definition of Supremum in Product Lattices

Informal description

For any types $\alpha$ and $\beta$ equipped with a maximum operation $\sqcup$, and for any pairs $p, q \in \alpha \times \beta$, the supremum $p \sqcup q$ is equal to the pair formed by taking the supremum of their first components and the supremum of their second components. That is, $p \sqcup q = (p_1 \sqcup q_1, p_2 \sqcup q_2)$, where $p = (p_1, p_2)$ and $q = (q_1, q_2)$.

Prod.inf_def theorem

[Min α] [Min β] (p q : α × β) : p ⊓ q = (p.fst ⊓ q.fst, p.snd ⊓ q.snd)

Full source

theorem inf_def [Min α] [Min β] (p q : α × β) : p ⊓ q = (p.fst ⊓ q.fst, p.snd ⊓ q.snd) :=
  rfl

Componentwise Infimum in Product Lattices

Informal description

For any types $\alpha$ and $\beta$ equipped with a minimum operation $\sqcap$, and for any pairs $p = (p_1, p_2)$ and $q = (q_1, q_2)$ in $\alpha \times \beta$, the infimum of $p$ and $q$ is given componentwise by $p \sqcap q = (p_1 \sqcap q_1, p_2 \sqcap q_2)$.

Prod.instSemilatticeSup instance

[SemilatticeSup α] [SemilatticeSup β] : SemilatticeSup (α × β)

Full source

instance instSemilatticeSup [SemilatticeSup α] [SemilatticeSup β] : SemilatticeSup (α × β) where
  sup a b := ⟨a.1 ⊔ b.1, a.2 ⊔ b.2⟩
  sup_le _ _ _ h₁ h₂ := ⟨sup_le h₁.1 h₂.1, sup_le h₁.2 h₂.2⟩
  le_sup_left _ _ := ⟨le_sup_left, le_sup_left⟩
  le_sup_right _ _ := ⟨le_sup_right, le_sup_right⟩

Componentwise Join-Semilattice Structure on Products

Informal description

For any types $\alpha$ and $\beta$ that are join-semilattices, the product type $\alpha \times \beta$ is also a join-semilattice, where the join operation is defined componentwise. That is, for any $(a_1, b_1), (a_2, b_2) \in \alpha \times \beta$, their join is given by $(a_1 \sqcup a_2, b_1 \sqcup b_2)$.

Prod.instSemilatticeInf instance

[SemilatticeInf α] [SemilatticeInf β] : SemilatticeInf (α × β)

Full source

instance instSemilatticeInf [SemilatticeInf α] [SemilatticeInf β] : SemilatticeInf (α × β) where
  inf a b := ⟨a.1 ⊓ b.1, a.2 ⊓ b.2⟩
  le_inf _ _ _ h₁ h₂ := ⟨le_inf h₁.1 h₂.1, le_inf h₁.2 h₂.2⟩
  inf_le_left _ _ := ⟨inf_le_left, inf_le_left⟩
  inf_le_right _ _ := ⟨inf_le_right, inf_le_right⟩

Componentwise Meet-Semilattice Structure on Products

Informal description

For any meet-semilattices $\alpha$ and $\beta$, the product type $\alpha \times \beta$ is also a meet-semilattice, where the meet operation is defined componentwise. That is, for any $(a_1, b_1), (a_2, b_2) \in \alpha \times \beta$, their meet is given by $(a_1 \sqcap a_2, b_1 \sqcap b_2)$.

Prod.instLattice instance

[Lattice α] [Lattice β] : Lattice (α × β)

Full source

instance instLattice [Lattice α] [Lattice β] : Lattice (α × β) where

Componentwise Lattice Structure on Products

Informal description

For any lattices $\alpha$ and $\beta$, the product type $\alpha \times \beta$ is also a lattice, where the join and meet operations are defined componentwise. That is, for any $(a_1, b_1), (a_2, b_2) \in \alpha \times \beta$, their join is $(a_1 \sqcup a_2, b_1 \sqcup b_2)$ and their meet is $(a_1 \sqcap a_2, b_1 \sqcap b_2)$.

Prod.instDistribLattice instance

[DistribLattice α] [DistribLattice β] : DistribLattice (α × β)

Full source

instance instDistribLattice [DistribLattice α] [DistribLattice β] : DistribLattice (α × β) where
  le_sup_inf _ _ _ := ⟨le_sup_inf, le_sup_inf⟩

Componentwise Distributive Lattice Structure on Products

Informal description

For any distributive lattices $\alpha$ and $\beta$, the product type $\alpha \times \beta$ is also a distributive lattice, where the join and meet operations are defined componentwise. That is, for any $(a_1, b_1), (a_2, b_2) \in \alpha \times \beta$, their join is $(a_1 \sqcup a_2, b_1 \sqcup b_2)$ and their meet is $(a_1 \sqcap a_2, b_1 \sqcap b_2)$, and these operations satisfy the distributivity laws.

Subtype.semilatticeSup abbrev

 [SemilatticeSup α] {P : α → Prop} (Psup : ∀ ⦃x y⦄, P x → P y → P (x ⊔ y)) : SemilatticeSup { x : α // P x }

Full source

/-- A subtype forms a `⊔`-semilattice if `⊔` preserves the property.
See note [reducible non-instances]. -/
protected abbrev semilatticeSup [SemilatticeSup α] {P : α → Prop}
    (Psup : ∀ ⦃x y⦄, P x → P y → P (x ⊔ y)) :
    SemilatticeSup { x : α // P x } where
  sup x y := ⟨x.1 ⊔ y.1, Psup x.2 y.2⟩
  le_sup_left _ _ := le_sup_left
  le_sup_right _ _ := le_sup_right
  sup_le _ _ _ h1 h2 := sup_le h1 h2

Join-Semilattice Structure on Subtypes Closed Under Supremum

Informal description

Let $\alpha$ be a join-semilattice with a binary operation $\sqcup$ (supremum), and let $P : \alpha \to \text{Prop}$ be a predicate on $\alpha$. If for any $x, y \in \alpha$ satisfying $P(x)$ and $P(y)$, their supremum $x \sqcup y$ also satisfies $P$, then the subtype $\{x \in \alpha \mid P(x)\}$ forms a join-semilattice with the induced supremum operation.

Subtype.semilatticeInf abbrev

 [SemilatticeInf α] {P : α → Prop} (Pinf : ∀ ⦃x y⦄, P x → P y → P (x ⊓ y)) : SemilatticeInf { x : α // P x }

Full source

/-- A subtype forms a `⊓`-semilattice if `⊓` preserves the property.
See note [reducible non-instances]. -/
protected abbrev semilatticeInf [SemilatticeInf α] {P : α → Prop}
    (Pinf : ∀ ⦃x y⦄, P x → P y → P (x ⊓ y)) :
    SemilatticeInf { x : α // P x } where
  inf x y := ⟨x.1 ⊓ y.1, Pinf x.2 y.2⟩
  inf_le_left _ _ := inf_le_left
  inf_le_right _ _ := inf_le_right
  le_inf _ _ _ h1 h2 := le_inf h1 h2

Meet-Semilattice Structure on Subtypes Closed Under Infimum

Informal description

Let $\alpha$ be a meet-semilattice with a binary operation $\sqcap$ (infimum), and let $P : \alpha \to \text{Prop}$ be a predicate on $\alpha$. If for any $x, y \in \alpha$ satisfying $P(x)$ and $P(y)$, their infimum $x \sqcap y$ also satisfies $P$, then the subtype $\{x \in \alpha \mid P(x)\}$ forms a meet-semilattice with the induced infimum operation.

Subtype.lattice abbrev

 [Lattice α] {P : α → Prop} (Psup : ∀ ⦃x y⦄, P x → P y → P (x ⊔ y)) (Pinf : ∀ ⦃x y⦄, P x → P y → P (x ⊓ y)) :
  Lattice { x : α // P x }

Full source

/-- A subtype forms a lattice if `⊔` and `⊓` preserve the property.
See note [reducible non-instances]. -/
protected abbrev lattice [Lattice α] {P : α → Prop} (Psup : ∀ ⦃x y⦄, P x → P y → P (x ⊔ y))
    (Pinf : ∀ ⦃x y⦄, P x → P y → P (x ⊓ y)) : Lattice { x : α // P x } where
  __ := Subtype.semilatticeInf Pinf
  __ := Subtype.semilatticeSup Psup

Lattice Structure on Subtypes Closed Under Supremum and Infimum

Informal description

Let $\alpha$ be a lattice with supremum $\sqcup$ and infimum $\sqcap$ operations, and let $P : \alpha \to \text{Prop}$ be a predicate on $\alpha$. If for any $x, y \in \alpha$ satisfying $P(x)$ and $P(y)$, both their supremum $x \sqcup y$ and infimum $x \sqcap y$ also satisfy $P$, then the subtype $\{x \in \alpha \mid P(x)\}$ forms a lattice with the induced supremum and infimum operations.

Subtype.coe_sup theorem

 [SemilatticeSup α] {P : α → Prop} (Psup : ∀ ⦃x y⦄, P x → P y → P (x ⊔ y)) (x y : Subtype P) :
  (haveI := Subtype.semilatticeSup Psup;
      (x ⊔ y : Subtype P) :
      α) =
    (x ⊔ y : α)

Full source

@[simp, norm_cast]
theorem coe_sup [SemilatticeSup α] {P : α → Prop}
    (Psup : ∀ ⦃x y⦄, P x → P y → P (x ⊔ y)) (x y : Subtype P) :
    (haveI := Subtype.semilatticeSup Psup; (x ⊔ y : Subtype P) : α) = (x ⊔ y : α) :=
  rfl

Supremum in Subtype Matches Supremum in Parent Join-Semilattice

Informal description

Let $\alpha$ be a join-semilattice with a binary operation $\sqcup$ (supremum), and let $P : \alpha \to \text{Prop}$ be a predicate on $\alpha$ such that for any $x, y \in \alpha$ satisfying $P(x)$ and $P(y)$, their supremum $x \sqcup y$ also satisfies $P$. Then for any $x, y$ in the subtype $\{x \in \alpha \mid P(x)\}$, the supremum of $x$ and $y$ in the induced join-semilattice structure on the subtype coincides with their supremum in $\alpha$.

Subtype.coe_inf theorem

 [SemilatticeInf α] {P : α → Prop} (Pinf : ∀ ⦃x y⦄, P x → P y → P (x ⊓ y)) (x y : Subtype P) :
  (haveI := Subtype.semilatticeInf Pinf;
      (x ⊓ y : Subtype P) :
      α) =
    (x ⊓ y : α)

Full source

@[simp, norm_cast]
theorem coe_inf [SemilatticeInf α] {P : α → Prop}
    (Pinf : ∀ ⦃x y⦄, P x → P y → P (x ⊓ y)) (x y : Subtype P) :
    (haveI := Subtype.semilatticeInf Pinf; (x ⊓ y : Subtype P) : α) = (x ⊓ y : α) :=
  rfl

Infimum in Subtype Matches Infimum in Original Meet-Semilattice

Informal description

Let $\alpha$ be a meet-semilattice with an infimum operation $\sqcap$, and let $P : \alpha \to \text{Prop}$ be a predicate on $\alpha$ such that for any $x, y \in \alpha$ satisfying $P(x)$ and $P(y)$, their infimum $x \sqcap y$ also satisfies $P$. Then for any elements $x, y$ in the subtype $\{x \in \alpha \mid P(x)\}$, the infimum of $x$ and $y$ in the induced meet-semilattice structure on the subtype coincides with their infimum in $\alpha$.

Subtype.mk_sup_mk theorem

 [SemilatticeSup α] {P : α → Prop} (Psup : ∀ ⦃x y⦄, P x → P y → P (x ⊔ y)) {x y : α} (hx : P x) (hy : P y) :
  (haveI := Subtype.semilatticeSup Psup;
    (⟨x, hx⟩ ⊔ ⟨y, hy⟩ : Subtype P)) =
    ⟨x ⊔ y, Psup hx hy⟩

Full source

@[simp]
theorem mk_sup_mk [SemilatticeSup α] {P : α → Prop}
    (Psup : ∀ ⦃x y⦄, P x → P y → P (x ⊔ y)) {x y : α} (hx : P x) (hy : P y) :
    (haveI := Subtype.semilatticeSup Psup; (⟨x, hx⟩⟨x, hx⟩ ⊔ ⟨y, hy⟩ : Subtype P)) =
      ⟨x ⊔ y, Psup hx hy⟩ :=
  rfl

Supremum of Subtype Elements in Induced Join-Semilattice

Informal description

Let $\alpha$ be a join-semilattice with a binary operation $\sqcup$ (supremum), and let $P : \alpha \to \text{Prop}$ be a predicate on $\alpha$ such that for any $x, y \in \alpha$ satisfying $P(x)$ and $P(y)$, their supremum $x \sqcup y$ also satisfies $P$. Then for any $x, y \in \alpha$ with $P(x)$ and $P(y)$, the supremum of the subtype elements $\langle x, hx \rangle$ and $\langle y, hy \rangle$ in the induced join-semilattice structure on $\{x \in \alpha \mid P(x)\}$ is equal to $\langle x \sqcup y, Psup\ hx\ hy \rangle$.

Subtype.mk_inf_mk theorem

 [SemilatticeInf α] {P : α → Prop} (Pinf : ∀ ⦃x y⦄, P x → P y → P (x ⊓ y)) {x y : α} (hx : P x) (hy : P y) :
  (haveI := Subtype.semilatticeInf Pinf;
    (⟨x, hx⟩ ⊓ ⟨y, hy⟩ : Subtype P)) =
    ⟨x ⊓ y, Pinf hx hy⟩

Full source

@[simp]
theorem mk_inf_mk [SemilatticeInf α] {P : α → Prop}
    (Pinf : ∀ ⦃x y⦄, P x → P y → P (x ⊓ y)) {x y : α} (hx : P x) (hy : P y) :
    (haveI := Subtype.semilatticeInf Pinf; (⟨x, hx⟩⟨x, hx⟩ ⊓ ⟨y, hy⟩ : Subtype P)) =
      ⟨x ⊓ y, Pinf hx hy⟩ :=
  rfl

Infimum of Subtype Elements in Induced Meet-Semilattice

Informal description

Let $\alpha$ be a meet-semilattice with a binary operation $\sqcap$ (infimum), and let $P : \alpha \to \text{Prop}$ be a predicate on $\alpha$ such that for any $x, y \in \alpha$ satisfying $P(x)$ and $P(y)$, their infimum $x \sqcap y$ also satisfies $P$. Then for any $x, y \in \alpha$ with $P(x)$ and $P(y)$, the infimum of the subtype elements $\langle x, hx \rangle$ and $\langle y, hy \rangle$ in the induced meet-semilattice structure on $\{x \in \alpha \mid P(x)\}$ is equal to $\langle x \sqcap y, Pinf\ hx\ hy \rangle$.

Function.Injective.semilatticeSup abbrev

 [Max α] [SemilatticeSup β] (f : α → β) (hf_inj : Function.Injective f) (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) :
  SemilatticeSup α

Full source

/-- A type endowed with `⊔` is a `SemilatticeSup`, if it admits an injective map that
preserves `⊔` to a `SemilatticeSup`.
See note [reducible non-instances]. -/
protected abbrev Function.Injective.semilatticeSup [Max α] [SemilatticeSup β] (f : α → β)
    (hf_inj : Function.Injective f) (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) :
    SemilatticeSup α where
  __ := PartialOrder.lift f hf_inj
  sup a b := max a b
  le_sup_left a b := by
    change f a ≤ f (a ⊔ b)
    rw [map_sup]
    exact le_sup_left
  le_sup_right a b := by
    change f b ≤ f (a ⊔ b)
    rw [map_sup]
    exact le_sup_right
  sup_le a b c ha hb := by
    change f (a ⊔ b) ≤ f c
    rw [map_sup]
    exact sup_le ha hb

Injective Join-Preserving Function Induces Join-Semilattice Structure

Informal description

Let $\alpha$ and $\beta$ be types, where $\beta$ is a join-semilattice. Given an injective function $f : \alpha \to \beta$ that preserves the join operation (i.e., $f(a \sqcup b) = f(a) \sqcup f(b)$ for all $a, b \in \alpha$), then $\alpha$ can be endowed with a join-semilattice structure where the join operation is defined via $f$.

Function.Injective.semilatticeInf abbrev

 [Min α] [SemilatticeInf β] (f : α → β) (hf_inj : Function.Injective f) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b) :
  SemilatticeInf α

Full source

/-- A type endowed with `⊓` is a `SemilatticeInf`, if it admits an injective map that
preserves `⊓` to a `SemilatticeInf`.
See note [reducible non-instances]. -/
protected abbrev Function.Injective.semilatticeInf [Min α] [SemilatticeInf β] (f : α → β)
    (hf_inj : Function.Injective f) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b) :
    SemilatticeInf α where
  __ := PartialOrder.lift f hf_inj
  inf a b := min a b
  inf_le_left a b := by
    change f (a ⊓ b) ≤ f a
    rw [map_inf]
    exact inf_le_left
  inf_le_right a b := by
    change f (a ⊓ b) ≤ f b
    rw [map_inf]
    exact inf_le_right
  le_inf a b c ha hb := by
    change f a ≤ f (b ⊓ c)
    rw [map_inf]
    exact le_inf ha hb

Injective Meet-Preserving Function Induces Meet-Semilattice Structure

Informal description

Let $\alpha$ and $\beta$ be types, where $\beta$ is a meet-semilattice. Given an injective function $f : \alpha \to \beta$ that preserves the meet operation (i.e., $f(a \sqcap b) = f(a) \sqcap f(b)$ for all $a, b \in \alpha$), then $\alpha$ can be endowed with a meet-semilattice structure where the meet operation is defined via $f$.

Function.Injective.lattice abbrev

 [Max α] [Min α] [Lattice β] (f : α → β) (hf_inj : Function.Injective f) (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b)
  (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b) : Lattice α

Full source

/-- A type endowed with `⊔` and `⊓` is a `Lattice`, if it admits an injective map that
preserves `⊔` and `⊓` to a `Lattice`.
See note [reducible non-instances]. -/
protected abbrev Function.Injective.lattice [Max α] [Min α] [Lattice β] (f : α → β)
    (hf_inj : Function.Injective f)
    (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b) :
    Lattice α where
  __ := hf_inj.semilatticeSup f map_sup
  __ := hf_inj.semilatticeInf f map_inf

Injective Lattice-Preserving Function Induces Lattice Structure

Informal description

Let $\alpha$ and $\beta$ be types, where $\beta$ is a lattice. Given an injective function $f : \alpha \to \beta$ that preserves both the join and meet operations (i.e., $f(a \sqcup b) = f(a) \sqcup f(b)$ and $f(a \sqcap b) = f(a) \sqcap f(b)$ for all $a, b \in \alpha$), then $\alpha$ can be endowed with a lattice structure where the join and meet operations are defined via $f$.

Function.Injective.distribLattice abbrev

 [Max α] [Min α] [DistribLattice β] (f : α → β) (hf_inj : Function.Injective f) (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b)
  (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b) : DistribLattice α

Full source

/-- A type endowed with `⊔` and `⊓` is a `DistribLattice`, if it admits an injective map that
preserves `⊔` and `⊓` to a `DistribLattice`.
See note [reducible non-instances]. -/
protected abbrev Function.Injective.distribLattice [Max α] [Min α] [DistribLattice β] (f : α → β)
    (hf_inj : Function.Injective f) (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b)
    (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b) :
    DistribLattice α where
  __ := hf_inj.lattice f map_sup map_inf
  le_sup_inf a b c := by
    change f ((a ⊔ b) ⊓ (a ⊔ c)) ≤ f (a ⊔ b ⊓ c)
    rw [map_inf, map_sup, map_sup, map_sup, map_inf]
    exact le_sup_inf

Injective Distributive Lattice-Preserving Function Induces Distributive Lattice Structure

Informal description

Let $\alpha$ and $\beta$ be types, where $\beta$ is a distributive lattice. Given an injective function $f : \alpha \to \beta$ that preserves both the join and meet operations (i.e., $f(a \sqcup b) = f(a) \sqcup f(b)$ and $f(a \sqcap b) = f(a) \sqcap f(b)$ for all $a, b \in \alpha$), then $\alpha$ can be endowed with a distributive lattice structure where the join and meet operations are defined via $f$.

ULift.instSemilatticeSup instance

[SemilatticeSup α] : SemilatticeSup (ULift.{v} α)

Full source

instance [SemilatticeSup α] : SemilatticeSup (ULift.{v} α) :=
  ULift.down_injective.semilatticeSup _ down_sup

Join-Semilattice Structure on Lifted Types

Informal description

For any join-semilattice $\alpha$, the lifted type $\text{ULift}\, \alpha$ inherits a join-semilattice structure where the join operation is defined componentwise.

ULift.instSemilatticeInf instance

[SemilatticeInf α] : SemilatticeInf (ULift.{v} α)

Full source

instance [SemilatticeInf α] : SemilatticeInf (ULift.{v} α) :=
  ULift.down_injective.semilatticeInf _ down_inf

Meet-Semilattice Structure on Lifted Types

Informal description

For any meet-semilattice $\alpha$, the lifted type $\text{ULift}\, \alpha$ inherits a meet-semilattice structure where the meet operation is defined componentwise.

ULift.instLattice instance

[Lattice α] : Lattice (ULift.{v} α)

Full source

instance [Lattice α] : Lattice (ULift.{v} α) :=
  ULift.down_injective.lattice _ down_sup down_inf

Lattice Structure on Lifted Types

Informal description

For any lattice $\alpha$, the lifted type $\text{ULift}\, \alpha$ inherits a lattice structure where the join and meet operations are defined componentwise.

ULift.instDistribLattice instance

[DistribLattice α] : DistribLattice (ULift.{v} α)

Full source

instance [DistribLattice α] : DistribLattice (ULift.{v} α) :=
  ULift.down_injective.distribLattice _ down_sup down_inf

Distributive Lattice Structure on Lifted Types

Informal description

For any distributive lattice $\alpha$, the lifted type $\text{ULift}\, \alpha$ inherits a distributive lattice structure where the join and meet operations are defined componentwise.

ULift.instLinearOrder instance

[LinearOrder α] : LinearOrder (ULift.{v} α)

Full source

instance [LinearOrder α] : LinearOrder (ULift.{v} α) :=
  LinearOrder.liftWithOrd ULift.down ULift.down_injective down_sup down_inf
    fun _x _y => (down_compare _ _).symm

Linear Order on Lifted Types

Informal description

For any linearly ordered type $\alpha$, the lifted type $\text{ULift}\, \alpha$ is also linearly ordered, inheriting the order structure from $\alpha$.

Bool.instDistribLattice instance

: DistribLattice Bool

Full source

instance Bool.instDistribLattice : DistribLattice Bool :=
  inferInstance

Boolean Algebra as a Distributive Lattice

Informal description

The boolean type $\text{Bool}$ is a distributive lattice, where the join and meet operations are given by logical OR and AND respectively.

Mathlib.Order.Lattice

Main declarations

Notations

TODO

Tags