Mathlib.Order.LatticeIntervals

Set.Ico.semilatticeInf instance

[SemilatticeInf α] {a b : α} : SemilatticeInf (Ico a b)

Full source

instance semilatticeInf [SemilatticeInf α] {a b : α} : SemilatticeInf (Ico a b) :=
  Subtype.semilatticeInf fun _ _ hx hy => ⟨le_inf hx.1 hy.1, lt_of_le_of_lt inf_le_left hx.2⟩

Meet-Semilattice Structure on Left-Closed Right-Open Intervals

Informal description

For any two elements $a$ and $b$ in a meet-semilattice $\alpha$, the left-closed right-open interval $\text{Ico}(a, b)$ inherits a meet-semilattice structure from $\alpha$.

Set.Ico.orderBot abbrev

[PartialOrder α] {a b : α} (h : a < b) : OrderBot (Ico a b)

Full source

/-- `Ico a b` has a bottom element whenever `a < b`. -/
protected abbrev orderBot [PartialOrder α] {a b : α} (h : a < b) : OrderBot (Ico a b) :=
  (isLeast_Ico h).orderBot

Existence of a Bottom Element in the Interval $[a, b)$ for $a < b$

Informal description

For any two elements $a$ and $b$ in a partially ordered set $\alpha$ such that $a < b$, the left-closed right-open interval $[a, b)$ has a least element $\bot$ (which is $a$), making it an order with a bottom element.

Set.Iio.semilatticeInf instance

[SemilatticeInf α] {a : α} : SemilatticeInf (Iio a)

Full source

instance semilatticeInf [SemilatticeInf α] {a : α} : SemilatticeInf (Iio a) :=
  Subtype.semilatticeInf fun _ _ hx _ => lt_of_le_of_lt inf_le_left hx

Semilattice Structure on Left-Infinite Right-Open Intervals

Informal description

For any element $a$ in a semilattice $\alpha$ with infima, the left-infinite right-open interval $(-\infty, a)$ is also a semilattice with infima, where the infimum operation is inherited from $\alpha$.

Set.Ioc.semilatticeSup instance

[SemilatticeSup α] {a b : α} : SemilatticeSup (Ioc a b)

Full source

instance semilatticeSup [SemilatticeSup α] {a b : α} : SemilatticeSup (Ioc a b) :=
  Subtype.semilatticeSup fun _ _ hx hy => ⟨lt_of_lt_of_le hx.1 le_sup_left, sup_le hx.2 hy.2⟩

Semilattice Structure on Left-Open Right-Closed Intervals

Informal description

For any elements $a$ and $b$ in a semilattice $\alpha$ with a supremum operation, the left-open right-closed interval $\text{Ioc}(a, b)$ inherits a semilattice structure with the same supremum operation.

Set.Ioc.orderTop abbrev

[PartialOrder α] {a b : α} (h : a < b) : OrderTop (Ioc a b)

Full source

/-- `Ioc a b` has a top element whenever `a < b`. -/
protected abbrev orderTop [PartialOrder α] {a b : α} (h : a < b) : OrderTop (Ioc a b) :=
  (isGreatest_Ioc h).orderTop

Greatest Element Structure on Left-Open Right-Closed Interval $(a, b]$

Informal description

For any elements $a$ and $b$ in a partially ordered set $\alpha$ with $a < b$, the left-open right-closed interval $(a, b]$ has a greatest element (order top) structure, where $b$ serves as the top element $\top$.

Set.Ioi.semilatticeSup instance

[SemilatticeSup α] {a : α} : SemilatticeSup (Ioi a)

Full source

instance semilatticeSup [SemilatticeSup α] {a : α} : SemilatticeSup (Ioi a) :=
  Subtype.semilatticeSup fun _ _ hx _ => lt_of_lt_of_le hx le_sup_left

Semilattice with Supremum Structure on Left-Open Right-Infinite Interval

Informal description

For any element $a$ in a semilattice with supremum $\alpha$, the left-open right-infinite interval $(a, \infty)$ inherits a semilattice with supremum structure from $\alpha$.

Set.Iic.semilatticeInf instance

[SemilatticeInf α] : SemilatticeInf (Iic a)

Full source

instance semilatticeInf [SemilatticeInf α] : SemilatticeInf (Iic a) :=
  Subtype.semilatticeInf fun _ _ hx _ => le_trans inf_le_left hx

Semilattice with Infima Structure on $(-\infty, a]$

Informal description

For any semilattice with infima $\alpha$ and an element $a \in \alpha$, the left-infinite right-closed interval $(-\infty, a]$ inherits a semilattice with infima structure from $\alpha$.

Set.Iic.coe_inf theorem

[SemilatticeInf α] {x y : Iic a} : (↑(x ⊓ y) : α) = (x : α) ⊓ (y : α)

Full source

@[simp, norm_cast]
protected lemma coe_inf [SemilatticeInf α] {x y : Iic a} :
    (↑(x ⊓ y) : α) = (x : α) ⊓ (y : α) :=
  rfl

Infimum in $(-\infty, a]$ Matches Infimum in $\alpha$

Informal description

For any semilattice with infima $\alpha$ and an element $a \in \alpha$, the infimum of two elements $x$ and $y$ in the interval $(-\infty, a]$, when viewed as elements of $\alpha$, equals the infimum of $x$ and $y$ in $\alpha$. That is, if $x, y \in (-\infty, a]$, then $(x \sqcap y) = x \sqcap y$ in $\alpha$.

Set.Iic.semilatticeSup instance

[SemilatticeSup α] : SemilatticeSup (Iic a)

Full source

instance semilatticeSup [SemilatticeSup α] : SemilatticeSup (Iic a) :=
  Subtype.semilatticeSup fun _ _ hx hy => sup_le hx hy

Semilattice with Supremum Structure on $(-\infty, a]$

Informal description

For any element $a$ in a semilattice with supremum $\alpha$, the left-infinite right-closed interval $(-\infty, a]$ inherits a semilattice with supremum structure, where the supremum operation is defined pointwise.

Set.Iic.coe_sup theorem

[SemilatticeSup α] {x y : Iic a} : (↑(x ⊔ y) : α) = (x : α) ⊔ (y : α)

Full source

@[simp, norm_cast]
protected lemma coe_sup [SemilatticeSup α] {x y : Iic a} :
    (↑(x ⊔ y) : α) = (x : α) ⊔ (y : α) :=
  rfl

Supremum in $(-\infty, a]$ Matches Supremum in $\alpha$

Informal description

For any semilattice with suprema $\alpha$ and an element $a \in \alpha$, the supremum of two elements $x$ and $y$ in the interval $(-\infty, a]$, when viewed as elements of $\alpha$, equals the supremum of $x$ and $y$ in $\alpha$. That is, if $x, y \in (-\infty, a]$, then $(x \sqcup y) = x \sqcup y$ in $\alpha$.

Set.Iic.instLatticeElem instance

[Lattice α] : Lattice (Iic a)

Full source

instance [Lattice α] : Lattice (Iic a) :=
  { Iic.semilatticeInf, Iic.semilatticeSup with }

Lattice Structure on $(-\infty, a]$

Informal description

For any lattice $\alpha$ and element $a \in \alpha$, the left-infinite right-closed interval $(-\infty, a]$ inherits a lattice structure from $\alpha$.

Set.Iic.orderTop instance

[Preorder α] : OrderTop (Iic a)

Full source

instance orderTop [Preorder α] :
    OrderTop (Iic a) where
  top := ⟨a, le_refl a⟩
  le_top x := x.prop

The Interval $(-\infty, a]$ has a Top Element $a$

Informal description

For any preorder $\alpha$ and element $a \in \alpha$, the left-infinite right-closed interval $(-\infty, a]$ has a greatest element $a$ with respect to the induced order.

Set.Iic.coe_top theorem

[Preorder α] : (⊤ : Iic a) = a

Full source

@[simp]
theorem coe_top [Preorder α] : (⊤ : Iic a) = a :=
  rfl

Top Element of $(-\infty, a]$ is $a$

Informal description

For any preorder $\alpha$ and element $a \in \alpha$, the top element of the interval $(-\infty, a]$ is equal to $a$ itself, i.e., $\top = a$ in $(-\infty, a]$.

Set.Iic.orderBot instance

[Preorder α] [OrderBot α] : OrderBot (Iic a)

Full source

instance orderBot [Preorder α] [OrderBot α] :
    OrderBot (Iic a) where
  bot := ⟨⊥, bot_le⟩
  bot_le := fun ⟨_, _⟩ => Subtype.mk_le_mk.2 bot_le

Bottom Element in Left-Infinite Right-Closed Interval

Informal description

For any preorder $\alpha$ with a bottom element $\bot$, the left-infinite right-closed interval $(-\infty, a]$ inherits an order with a bottom element from $\alpha$.

Set.Iic.coe_bot theorem

[Preorder α] [OrderBot α] : (⊥ : Iic a) = (⊥ : α)

Full source

@[simp]
theorem coe_bot [Preorder α] [OrderBot α] : (⊥ : Iic a) = (⊥ : α) :=
  rfl

Bottom Element Equality in $(-\infty, a]$ Interval

Informal description

For any preorder $\alpha$ with a bottom element $\bot$, the bottom element of the left-infinite right-closed interval $(-\infty, a]$ is equal to the bottom element of $\alpha$ when viewed as an element of $\alpha$.

Set.Iic.instBoundedOrderElemOfOrderBot instance

[Preorder α] [OrderBot α] : BoundedOrder (Iic a)

Full source

instance [Preorder α] [OrderBot α] : BoundedOrder (Iic a) :=
  { Iic.orderTop, Iic.orderBot with }

Bounded Order Structure on $(-\infty, a]$ with Bottom Element

Informal description

For any preorder $\alpha$ with a bottom element $\bot$, the left-infinite right-closed interval $(-\infty, a]$ inherits a bounded order structure from $\alpha$, with $\bot$ as the least element and $a$ as the greatest element.

Set.Iic.disjoint_iff theorem

[SemilatticeInf α] [OrderBot α] {x y : Iic a} : Disjoint x y ↔ Disjoint (x : α) (y : α)

Full source

protected lemma disjoint_iff [SemilatticeInf α] [OrderBot α] {x y : Iic a} :
    DisjointDisjoint x y ↔ Disjoint (x : α) (y : α) := by
  simp [_root_.disjoint_iff, Subtype.ext_iff]

Disjointness in Left-Infinite Right-Closed Interval

Informal description

Let $\alpha$ be a semilattice with infima and a bottom element $\bot$, and let $a \in \alpha$. For any two elements $x, y$ in the interval $(-\infty, a]$, $x$ and $y$ are disjoint in $(-\infty, a]$ if and only if they are disjoint in $\alpha$.

Set.Iic.codisjoint_iff theorem

[SemilatticeSup α] {x y : Iic a} : Codisjoint x y ↔ (x : α) ⊔ (y : α) = a

Full source

protected lemma codisjoint_iff [SemilatticeSup α] {x y : Iic a} :
    CodisjointCodisjoint x y ↔ (x : α) ⊔ (y : α) = a := by
  simpa only [_root_.codisjoint_iff] using Iic.eq_top_iff

Codisjointness Criterion in Left-Infinite Right-Closed Interval

Informal description

Let $\alpha$ be a semilattice with suprema, and let $a \in \alpha$. For any two elements $x, y$ in the interval $(-\infty, a]$, $x$ and $y$ are codisjoint in $(-\infty, a]$ if and only if their supremum in $\alpha$ equals $a$.

Set.Iic.isCompl_iff theorem

[Lattice α] [OrderBot α] {x y : Iic a} : IsCompl x y ↔ Disjoint (x : α) (y : α) ∧ (x : α) ⊔ (y : α) = a

Full source

protected lemma isCompl_iff [Lattice α] [OrderBot α] {x y : Iic a} :
    IsComplIsCompl x y ↔ Disjoint (x : α) (y : α) ∧ (x : α) ⊔ (y : α) = a := by
  rw [_root_.isCompl_iff, Iic.disjoint_iff, Iic.codisjoint_iff]

Complement Criterion in Left-Infinite Right-Closed Interval

Informal description

Let $\alpha$ be a lattice with a bottom element $\bot$, and let $a \in \alpha$. For any two elements $x, y$ in the interval $(-\infty, a]$, $x$ and $y$ are complements in $(-\infty, a]$ if and only if they are disjoint in $\alpha$ and their supremum in $\alpha$ equals $a$. In other words, $x$ and $y$ are complements in $(-\infty, a]$ if and only if $x \sqcap y = \bot$ and $x \sqcup y = a$ in $\alpha$.

Set.Iic.complementedLattice_iff theorem

 [Lattice α] [OrderBot α] : ComplementedLattice (Iic a) ↔ ∀ b, b ≤ a → ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a

Full source

protected lemma complementedLattice_iff [Lattice α] [OrderBot α] :
    ComplementedLatticeComplementedLattice (Iic a) ↔ ∀ b, b ≤ a → ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a := by
  refine ⟨fun h b hb ↦ ?_, fun h ↦ ⟨fun ⟨x, hx⟩ ↦ ?_⟩⟩
  · obtain ⟨⟨c, hc₁⟩, hc⟩ := exists_isCompl (⟨b, hb⟩ : Iic a)
    obtain ⟨hc₂, hc₃⟩ := Set.Iic.isCompl_iff.mp hc
    exact ⟨c, hc₁, disjoint_iff.mp hc₂, hc₃⟩
  · simp_rw [Set.Iic.isCompl_iff]
    obtain ⟨c, hc₁, hc₂, hc₃⟩ := h x hx
    exact ⟨⟨c, hc₁⟩, disjoint_iff.mpr hc₂, hc₃⟩

Complemented Lattice Criterion for $(-\infty, a]$ Interval

Informal description

Let $\alpha$ be a lattice with a bottom element $\bot$, and let $a \in \alpha$. The interval $(-\infty, a]$ is a complemented lattice if and only if for every element $b \leq a$ in $\alpha$, there exists an element $c \leq a$ such that $b \sqcap c = \bot$ and $b \sqcup c = a$.

Set.Ici.semilatticeInf instance

[SemilatticeInf α] {a : α} : SemilatticeInf (Ici a)

Full source

instance semilatticeInf [SemilatticeInf α] {a : α} : SemilatticeInf (Ici a) :=
  Subtype.semilatticeInf fun _ _ hx hy => le_inf hx hy

Semilattice Structure on $[a, \infty)$ with Finite Meets

Informal description

For any element $a$ in a semilattice $\alpha$ with finite meets, the left-closed right-infinite interval $[a, \infty)$ inherits a semilattice structure with finite meets.

Set.Ici.semilatticeSup instance

[SemilatticeSup α] {a : α} : SemilatticeSup (Ici a)

Full source

instance semilatticeSup [SemilatticeSup α] {a : α} : SemilatticeSup (Ici a) :=
  Subtype.semilatticeSup fun _ _ hx _ => le_trans hx le_sup_left

Semilattice with Supremum Structure on $[a, \infty)$

Informal description

For any element $a$ in a semilattice with supremum $\alpha$, the interval $[a, \infty)$ forms a semilattice with supremum, where the supremum operation is inherited from $\alpha$.

Set.Ici.lattice instance

[Lattice α] {a : α} : Lattice (Ici a)

Full source

instance lattice [Lattice α] {a : α} : Lattice (Ici a) :=
  { Ici.semilatticeInf, Ici.semilatticeSup with }

Lattice Structure on $[a, \infty)$

Informal description

For any element $a$ in a lattice $\alpha$, the left-closed right-infinite interval $[a, \infty)$ inherits a lattice structure from $\alpha$.

Set.Ici.distribLattice instance

[DistribLattice α] {a : α} : DistribLattice (Ici a)

Full source

instance distribLattice [DistribLattice α] {a : α} : DistribLattice (Ici a) :=
  { Ici.lattice with le_sup_inf := fun _ _ _ => le_sup_inf }

Distributive Lattice Structure on $[a, \infty)$

Informal description

For any element $a$ in a distributive lattice $\alpha$, the left-closed right-infinite interval $[a, \infty)$ inherits a distributive lattice structure from $\alpha$.

Set.Ici.orderBot instance

[Preorder α] {a : α} : OrderBot (Ici a)

Full source

instance orderBot [Preorder α] {a : α} :
    OrderBot (Ici a) where
  bot := ⟨a, le_refl a⟩
  bot_le x := x.prop

Bottom Element in the Interval $[a, \infty)$

Informal description

For any preorder $\alpha$ and any element $a \in \alpha$, the left-closed right-infinite interval $[a, \infty)$ has a bottom element $a$ with respect to the induced order.

Set.Ici.coe_bot theorem

[Preorder α] {a : α} : ↑(⊥ : Ici a) = a

Full source

@[simp]
theorem coe_bot [Preorder α] {a : α} : ↑(⊥ : Ici a) = a :=
  rfl

Bottom Element of $[a, \infty)$ is $a$

Informal description

For any preorder $\alpha$ and any element $a \in \alpha$, the bottom element $\bot$ of the interval $[a, \infty)$, when viewed as an element of $\alpha$, is equal to $a$.

Set.Ici.orderTop instance

[Preorder α] [OrderTop α] {a : α} : OrderTop (Ici a)

Full source

instance orderTop [Preorder α] [OrderTop α] {a : α} :
    OrderTop (Ici a) where
  top := ⟨⊤, le_top⟩
  le_top := fun ⟨_, _⟩ => Subtype.mk_le_mk.2 le_top

Top Element in Left-Closed Right-Infinite Interval

Informal description

For any preorder $\alpha$ with a top element $\top$ and any element $a \in \alpha$, the interval $[a, \infty)$ has a top element inherited from $\alpha$.

Set.Ici.coe_top theorem

[Preorder α] [OrderTop α] {a : α} : ↑(⊤ : Ici a) = (⊤ : α)

Full source

@[simp]
theorem coe_top [Preorder α] [OrderTop α] {a : α} : ↑(⊤ : Ici a) = (⊤ : α) :=
  rfl

Top Element of $[a, \infty)$ is $\top$

Informal description

For any preorder $\alpha$ with a top element $\top$ and any element $a \in \alpha$, the top element of the interval $[a, \infty)$, when viewed as an element of $\alpha$, is equal to the top element $\top$ of $\alpha$.

Set.Ici.boundedOrder instance

[Preorder α] [OrderTop α] {a : α} : BoundedOrder (Ici a)

Full source

instance boundedOrder [Preorder α] [OrderTop α] {a : α} : BoundedOrder (Ici a) :=
  { Ici.orderTop, Ici.orderBot with }

Bounded Order Structure on $[a, \infty)$

Informal description

For any preorder $\alpha$ with a top element $\top$ and any element $a \in \alpha$, the left-closed right-infinite interval $[a, \infty)$ forms a bounded order, inheriting both the top element from $\alpha$ and having $a$ as its bottom element.

Set.Icc.semilatticeInf instance

[SemilatticeInf α] : SemilatticeInf (Icc a b)

Full source

instance semilatticeInf [SemilatticeInf α] : SemilatticeInf (Icc a b) :=
  Subtype.semilatticeInf fun _ _ hx hy => ⟨le_inf hx.1 hy.1, le_trans inf_le_left hx.2⟩

Semilattice Structure on Closed Intervals via Infima

Informal description

For any elements $a$ and $b$ in a semilattice with infima $\alpha$, the closed interval $[a, b]$ forms a semilattice with infima, where the infimum operation is inherited from $\alpha$.

Set.Icc.semilatticeSup instance

[SemilatticeSup α] : SemilatticeSup (Icc a b)

Full source

instance semilatticeSup [SemilatticeSup α] : SemilatticeSup (Icc a b) :=
  Subtype.semilatticeSup fun _ _ hx hy => ⟨le_trans hx.1 le_sup_left, sup_le hx.2 hy.2⟩

Semilattice with Supremum Structure on Closed Intervals

Informal description

For any elements $a$ and $b$ in a semilattice $\alpha$ with a supremum operation, the closed interval $[a, b]$ forms a semilattice with supremum, where the supremum operation is inherited from $\alpha$.

Set.Icc.lattice instance

[Lattice α] : Lattice (Icc a b)

Full source

instance lattice [Lattice α] : Lattice (Icc a b) :=
  { Icc.semilatticeInf, Icc.semilatticeSup with }

Lattice Structure on Closed Intervals

Informal description

For any elements $a$ and $b$ in a lattice $\alpha$, the closed interval $[a, b]$ forms a lattice, where the infimum and supremum operations are inherited from $\alpha$.

Set.Icc.instOrderBotElem instance

: OrderBot (Icc a b)

Full source

/-- `Icc a b` has a bottom element whenever `a ≤ b`. -/
instance : OrderBot (Icc a b) :=
  (isLeast_Icc Fact.out).orderBot

Bottom Element in Closed Intervals

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ with $a \leq b$, the closed interval $[a, b]$ has a bottom element $a$.

Set.Icc.coe_bot theorem

: ↑(⊥ : Icc a b) = a

Full source

@[simp, norm_cast]
theorem coe_bot : ↑(⊥ : Icc a b) = a := rfl

Bottom Element of Closed Interval is Left Endpoint

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ with $a \leq b$, the bottom element of the closed interval $[a, b]$ is $a$ when viewed as an element of $\alpha$.

Set.Icc.instOrderTopElem instance

: OrderTop (Icc a b)

Full source

/-- `Icc a b` has a top element whenever `a ≤ b`. -/
instance : OrderTop (Icc a b) :=
  (isGreatest_Icc Fact.out).orderTop

Top Element in Closed Intervals

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ with $a \leq b$, the closed interval $[a, b]$ has a top element $b$.

Set.Icc.coe_top theorem

: ↑(⊤ : Icc a b) = b

Full source

@[simp, norm_cast]
theorem coe_top : ↑(⊤ : Icc a b) = b := rfl

Top Element of Closed Interval is Right Endpoint

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ with $a \leq b$, the top element of the closed interval $[a, b]$ is $b$ when viewed as an element of $\alpha$. In other words, the coercion of the top element $\top$ in the interval $[a, b]$ equals $b$.

Set.Icc.instBoundedOrderElem instance

: BoundedOrder (Icc a b)

Full source

/-- `Icc a b` is a `BoundedOrder` whenever `a ≤ b`. -/
instance : BoundedOrder (Icc a b) where

Bounded Order Structure on Closed Intervals

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ with $a \leq b$, the closed interval $[a, b]$ is a bounded order, meaning it has both a greatest element $b$ and a least element $a$.

Main definitions