Mathlib.Order.Interval.Set.UnorderedInterval

Set.uIcc definition

(a b : α) : Set α

Full source

/-- `uIcc a b` is the set of elements lying between `a` and `b`, with `a` and `b` included.
Note that we define it more generally in a lattice as `Set.Icc (a ⊓ b) (a ⊔ b)`. In a product type,
`uIcc` corresponds to the bounding box of the two elements. -/
def uIcc (a b : α) : Set α := Icc (a ⊓ b) (a ⊔ b)

Unordered closed interval $[a, b]$ in a lattice

Informal description

For any two elements $ a $ and $ b $ in a lattice $ \alpha $, the set $ \text{uIcc}(a, b) $ is defined as the closed interval $[a \sqcap b, a \sqcup b]$, which consists of all elements $ x $ such that $ a \sqcap b \leq x \leq a \sqcup b $. This interval always contains all elements lying between $ a $ and $ b $, regardless of their order.

Interval.term[[_,_]] definition

: Lean.ParserDescr✝

Full source

/-- `[[a, b]]` denotes the set of elements lying between `a` and `b`, inclusive. -/
scoped[Interval] notation "[[" a ", " b "]]" => Set.uIcc a b

Closed interval notation for unordered endpoints

Informal description

The notation $[[a, b]]$ denotes the closed interval containing all elements between $a$ and $b$ (inclusive), regardless of the order of $a$ and $b$. In a lattice $\alpha$, this is equivalent to the interval $[a \sqcap b, a \sqcup b]$.

Set.uIcc_toDual theorem

(a b : α) : [[toDual a, toDual b]] = ofDual ⁻¹' [[a, b]]

Full source

@[simp]
lemma uIcc_toDual (a b : α) : [[toDual a, toDual b]] = ofDualofDual ⁻¹' [[a, b]] :=
  -- Note: needed to hint `(α := α)` after https://github.com/leanprover-community/mathlib4/pull/8386 (elaboration order?)
  Icc_toDual (α := α)

Duality of Unordered Intervals via Order Reversal

Informal description

For any elements $a$ and $b$ in a lattice $\alpha$, the unordered closed interval $[[a^\ast, b^\ast]]$ in the order dual of $\alpha$ is equal to the preimage under the order-reversing map $\operatorname{ofDual}$ of the unordered closed interval $[[a, b]]$ in $\alpha$, i.e., $$ [[\operatorname{toDual}(a), \operatorname{toDual}(b)]] = \operatorname{ofDual}^{-1}([[a, b]]). $$

Set.uIcc_ofDual theorem

(a b : αᵒᵈ) : [[ofDual a, ofDual b]] = toDual ⁻¹' [[a, b]]

Full source

@[simp]
theorem uIcc_ofDual (a b : αᵒᵈ) : [[ofDual a, ofDual b]] = toDualtoDual ⁻¹' [[a, b]] :=
  Icc_ofDual

Duality of Unordered Intervals via Order Reversal

Informal description

For any elements $a$ and $b$ in the order dual $\alpha^\text{op}$ of a lattice $\alpha$, the unordered closed interval $[[\text{ofDual}(a), \text{ofDual}(b)]]$ in $\alpha$ is equal to the preimage under $\text{toDual}$ of the unordered closed interval $[[a, b]]$ in $\alpha^\text{op}$. In other words: \[ [[\text{ofDual}(a), \text{ofDual}(b)]] = \text{toDual}^{-1}\big([[a, b]]\big) \]

Set.uIcc_of_le theorem

(h : a ≤ b) : [[a, b]] = Icc a b

Full source

@[simp]
lemma uIcc_of_le (h : a ≤ b) : [[a, b]] = Icc a b := by rw [uIcc, inf_eq_left.2 h, sup_eq_right.2 h]

Unordered Interval Equals Ordered Interval When $a \leq b$

Informal description

For any two elements $a$ and $b$ in a lattice $\alpha$ with $a \leq b$, the unordered closed interval $[[a, b]]$ is equal to the closed interval $[a, b]$.

Set.uIcc_of_ge theorem

(h : b ≤ a) : [[a, b]] = Icc b a

Full source

@[simp]
lemma uIcc_of_ge (h : b ≤ a) : [[a, b]] = Icc b a := by rw [uIcc, inf_eq_right.2 h, sup_eq_left.2 h]

Unordered Interval Equals Ordered Interval When $b \leq a$

Informal description

For any two elements $a$ and $b$ in a lattice $\alpha$ with $b \leq a$, the unordered closed interval $[[a, b]]$ is equal to the closed interval $[b, a]$.

Set.uIcc_comm theorem

(a b : α) : [[a, b]] = [[b, a]]

Full source

lemma uIcc_comm (a b : α) : [[a, b]] = [[b, a]] := by simp_rw [uIcc, inf_comm, sup_comm]

Commutativity of Unordered Closed Interval: $[[a, b]] = [[b, a]]$

Informal description

For any two elements $a$ and $b$ in a lattice $\alpha$, the unordered closed interval $[[a, b]]$ is equal to $[[b, a]]$.

Set.uIcc_of_lt theorem

(h : a < b) : [[a, b]] = Icc a b

Full source

lemma uIcc_of_lt (h : a < b) : [[a, b]] = Icc a b := uIcc_of_le h.le

Unordered Interval Equals Ordered Interval When $a < b$

Informal description

For any two elements $a$ and $b$ in a lattice $\alpha$ with $a < b$, the unordered closed interval $[[a, b]]$ is equal to the closed interval $[a, b]$.

Set.uIcc_of_gt theorem

(h : b < a) : [[a, b]] = Icc b a

Full source

lemma uIcc_of_gt (h : b < a) : [[a, b]] = Icc b a := uIcc_of_ge h.le

Unordered Interval Equals Ordered Interval When $b < a$

Informal description

For any two elements $a$ and $b$ in a lattice $\alpha$ with $b < a$, the unordered closed interval $[[a, b]]$ is equal to the closed interval $[b, a]$.

Set.uIcc_self theorem

: [[a, a]] = { a }

Full source

lemma uIcc_self : [[a, a]] = {a} := by simp [uIcc]

Singleton Property of Unordered Closed Interval: $[[a, a]] = \{a\}$

Informal description

For any element $a$ in a lattice $\alpha$, the unordered closed interval $[[a, a]]$ is equal to the singleton set $\{a\}$.

Set.nonempty_uIcc theorem

: [[a, b]].Nonempty

Full source

@[simp] lemma nonempty_uIcc : [[a, b]].Nonempty := nonempty_Icc.2 inf_le_sup

Nonemptiness of Unordered Closed Interval $[[a, b]]$

Informal description

For any elements $a$ and $b$ in a lattice $\alpha$, the unordered closed interval $[[a, b]] := [a \sqcap b, a \sqcup b]$ is nonempty.

Set.Icc_subset_uIcc theorem

: Icc a b ⊆ [[a, b]]

Full source

lemma Icc_subset_uIcc : IccIcc a b ⊆ [[a, b]] := Icc_subset_Icc inf_le_left le_sup_right

Inclusion of Ordered Interval in Unordered Interval: $[a, b] \subseteq [[a, b]]$

Informal description

For any elements $a$ and $b$ in a lattice $\alpha$, the closed interval $[a, b]$ is a subset of the unordered closed interval $[[a, b]] := [a \sqcap b, a \sqcup b]$.

Set.Icc_subset_uIcc' theorem

: Icc b a ⊆ [[a, b]]

Full source

lemma Icc_subset_uIcc' : IccIcc b a ⊆ [[a, b]] := Icc_subset_Icc inf_le_right le_sup_left

Inclusion of Ordered Interval in Unordered Interval: $[b, a] \subseteq [[a, b]]$

Informal description

For any elements $a$ and $b$ in a lattice $\alpha$, the closed interval $[b, a]$ is a subset of the unordered closed interval $[[a, b]] := [a \sqcap b, a \sqcup b]$.

Set.left_mem_uIcc theorem

: a ∈ [[a, b]]

Full source

@[simp] lemma left_mem_uIcc : a ∈ [[a, b]] := ⟨inf_le_left, le_sup_left⟩

Left Endpoint Belongs to Unordered Interval

Informal description

For any elements $a$ and $b$ in a lattice $\alpha$, the element $a$ belongs to the unordered closed interval $[[a, b]] := [a \sqcap b, a \sqcup b]$.

Set.right_mem_uIcc theorem

: b ∈ [[a, b]]

Full source

@[simp] lemma right_mem_uIcc : b ∈ [[a, b]] := ⟨inf_le_right, le_sup_right⟩

Right Endpoint Belongs to Unordered Interval

Informal description

For any elements $a$ and $b$ in a lattice $\alpha$, the element $b$ belongs to the unordered closed interval $[[a, b]] := [a \sqcap b, a \sqcup b]$.

Set.mem_uIcc_of_le theorem

(ha : a ≤ x) (hb : x ≤ b) : x ∈ [[a, b]]

Full source

lemma mem_uIcc_of_le (ha : a ≤ x) (hb : x ≤ b) : x ∈ [[a, b]] := Icc_subset_uIcc ⟨ha, hb⟩

Membership in Unordered Interval via Lower and Upper Bounds: $a \leq x \leq b \implies x \in [[a, b]]$

Informal description

For any elements $a$, $b$, and $x$ in a lattice $\alpha$, if $x$ satisfies $a \leq x \leq b$, then $x$ belongs to the unordered closed interval $[[a, b]] := [a \sqcap b, a \sqcup b]$.

Set.mem_uIcc_of_ge theorem

(hb : b ≤ x) (ha : x ≤ a) : x ∈ [[a, b]]

Full source

lemma mem_uIcc_of_ge (hb : b ≤ x) (ha : x ≤ a) : x ∈ [[a, b]] := Icc_subset_uIcc' ⟨hb, ha⟩

Membership in Unordered Interval via Upper and Lower Bounds

Informal description

For any elements $a$, $b$, and $x$ in a lattice $\alpha$, if $x$ satisfies $b \leq x \leq a$, then $x$ belongs to the unordered closed interval $[[a, b]] := [a \sqcap b, a \sqcup b]$.

Set.uIcc_subset_uIcc theorem

(h₁ : a₁ ∈ [[a₂, b₂]]) (h₂ : b₁ ∈ [[a₂, b₂]]) : [[a₁, b₁]] ⊆ [[a₂, b₂]]

Full source

lemma uIcc_subset_uIcc (h₁ : a₁ ∈ [[a₂, b₂]]) (h₂ : b₁ ∈ [[a₂, b₂]]) :
    [[a₁, b₁]][[a₁, b₁]] ⊆ [[a₂, b₂]] :=
  Icc_subset_Icc (le_inf h₁.1 h₂.1) (sup_le h₁.2 h₂.2)

Subset Property of Unordered Intervals in a Lattice

Informal description

For any elements $a₁, b₁, a₂, b₂$ in a lattice $\alpha$, if $a₁$ and $b₁$ both belong to the unordered interval $[[a₂, b₂]]$, then the unordered interval $[[a₁, b₁]]$ is a subset of $[[a₂, b₂]]$.

Set.uIcc_subset_Icc theorem

(ha : a₁ ∈ Icc a₂ b₂) (hb : b₁ ∈ Icc a₂ b₂) : [[a₁, b₁]] ⊆ Icc a₂ b₂

Full source

lemma uIcc_subset_Icc (ha : a₁ ∈ Icc a₂ b₂) (hb : b₁ ∈ Icc a₂ b₂) :
    [[a₁, b₁]][[a₁, b₁]] ⊆ Icc a₂ b₂ :=
  Icc_subset_Icc (le_inf ha.1 hb.1) (sup_le ha.2 hb.2)

Inclusion of Unordered Interval in Closed Interval

Informal description

For any elements $a₁, b₁, a₂, b₂$ in a lattice $\alpha$, if $a₁$ lies in the closed interval $[a₂, b₂]$ and $b₁$ lies in the closed interval $[a₂, b₂]$, then the unordered interval $[[a₁, b₁]]$ is a subset of $[a₂, b₂]$.

Set.uIcc_subset_uIcc_iff_mem theorem

: [[a₁, b₁]] ⊆ [[a₂, b₂]] ↔ a₁ ∈ [[a₂, b₂]] ∧ b₁ ∈ [[a₂, b₂]]

Full source

lemma uIcc_subset_uIcc_iff_mem :
    [[a₁, b₁]][[a₁, b₁]] ⊆ [[a₂, b₂]][[a₁, b₁]] ⊆ [[a₂, b₂]] ↔ a₁ ∈ [[a₂, b₂]] ∧ b₁ ∈ [[a₂, b₂]] :=
  Iff.intro (fun h => ⟨h left_mem_uIcc, h right_mem_uIcc⟩) fun h =>
    uIcc_subset_uIcc h.1 h.2

Subset Condition for Unordered Intervals via Membership

Informal description

For any elements $a_1, b_1, a_2, b_2$ in a lattice $\alpha$, the unordered interval $[[a_1, b_1]]$ is a subset of the unordered interval $[[a_2, b_2]]$ if and only if both $a_1$ and $b_1$ belong to $[[a_2, b_2]]$.

Set.uIcc_subset_uIcc_iff_le' theorem

: [[a₁, b₁]] ⊆ [[a₂, b₂]] ↔ a₂ ⊓ b₂ ≤ a₁ ⊓ b₁ ∧ a₁ ⊔ b₁ ≤ a₂ ⊔ b₂

Full source

lemma uIcc_subset_uIcc_iff_le' :
    [[a₁, b₁]][[a₁, b₁]] ⊆ [[a₂, b₂]][[a₁, b₁]] ⊆ [[a₂, b₂]] ↔ a₂ ⊓ b₂ ≤ a₁ ⊓ b₁ ∧ a₁ ⊔ b₁ ≤ a₂ ⊔ b₂ :=
  Icc_subset_Icc_iff inf_le_sup

Subset Condition for Unordered Intervals via Meets and Joins

Informal description

For any elements $a_1, b_1, a_2, b_2$ in a lattice $\alpha$, the unordered interval $[[a_1, b_1]]$ is a subset of the unordered interval $[[a_2, b_2]]$ if and only if the meet of $a_2$ and $b_2$ is less than or equal to the meet of $a_1$ and $b_1$, and the join of $a_1$ and $b_1$ is less than or equal to the join of $a_2$ and $b_2$. In symbols: $$ [[a_1, b_1]] \subseteq [[a_2, b_2]] \iff a_2 \sqcap b_2 \leq a_1 \sqcap b_1 \text{ and } a_1 \sqcup b_1 \leq a_2 \sqcup b_2 $$

Set.uIcc_subset_uIcc_right theorem

(h : x ∈ [[a, b]]) : [[x, b]] ⊆ [[a, b]]

Full source

lemma uIcc_subset_uIcc_right (h : x ∈ [[a, b]]) : [[x, b]][[x, b]] ⊆ [[a, b]] :=
  uIcc_subset_uIcc h right_mem_uIcc

Right Subinterval Property of Unordered Intervals

Informal description

For any elements $a, b, x$ in a lattice $\alpha$, if $x$ belongs to the unordered interval $[[a, b]]$, then the unordered interval $[[x, b]]$ is a subset of $[[a, b]]$.

Set.uIcc_subset_uIcc_left theorem

(h : x ∈ [[a, b]]) : [[a, x]] ⊆ [[a, b]]

Full source

lemma uIcc_subset_uIcc_left (h : x ∈ [[a, b]]) : [[a, x]][[a, x]] ⊆ [[a, b]] :=
  uIcc_subset_uIcc left_mem_uIcc h

Left Subinterval Property of Unordered Intervals

Informal description

For any elements $a, b, x$ in a lattice $\alpha$, if $x$ belongs to the unordered interval $[[a, b]]$, then the unordered interval $[[a, x]]$ is a subset of $[[a, b]]$.

Set.bdd_below_bdd_above_iff_subset_uIcc theorem

(s : Set α) : BddBelow s ∧ BddAbove s ↔ ∃ a b, s ⊆ [[a, b]]

Full source

lemma bdd_below_bdd_above_iff_subset_uIcc (s : Set α) :
    BddBelowBddBelow s ∧ BddAbove sBddBelow s ∧ BddAbove s ↔ ∃ a b, s ⊆ [[a, b]] :=
  bddBelow_bddAbove_iff_subset_Icc.trans
    ⟨fun ⟨a, b, h⟩ => ⟨a, b, fun _ hx => Icc_subset_uIcc (h hx)⟩, fun ⟨_, _, h⟩ => ⟨_, _, h⟩⟩

Characterization of Bounded Sets via Unordered Intervals

Informal description

For any subset $s$ of a lattice $\alpha$, $s$ is both bounded below and bounded above if and only if there exist elements $a, b \in \alpha$ such that $s$ is contained in the unordered closed interval $[[a, b]] := [a \sqcap b, a \sqcup b]$.

Set.uIcc_prod_uIcc theorem

(a₁ a₂ : α) (b₁ b₂ : β) : [[a₁, a₂]] ×ˢ [[b₁, b₂]] = [[(a₁, b₁), (a₂, b₂)]]

Full source

@[simp]
theorem uIcc_prod_uIcc (a₁ a₂ : α) (b₁ b₂ : β) :
    [[a₁, a₂]] ×ˢ [[b₁, b₂]] = [[(a₁, b₁), (a₂, b₂)]] :=
  Icc_prod_Icc _ _ _ _

Product of Unordered Intervals Equals Unordered Interval in Product Lattice

Informal description

For any elements $a_1, a_2$ in a lattice $\alpha$ and $b_1, b_2$ in a lattice $\beta$, the product of the unordered closed intervals $[[a_1, a_2]] \times [[b_1, b_2]]$ is equal to the unordered closed interval $[[(a_1, b_1), (a_2, b_2)]]$ in the product lattice $\alpha \times \beta$.

Set.uIcc_prod_eq theorem

(a b : α × β) : [[a, b]] = [[a.1, b.1]] ×ˢ [[a.2, b.2]]

Full source

theorem uIcc_prod_eq (a b : α × β) : [[a, b]] = [[a.1, b.1]] ×ˢ [[a.2, b.2]] := by simp

Decomposition of Unordered Interval in Product Lattice: $[[(a_1,a_2),(b_1,b_2)]] = [[a_1,b_1]] \times [[a_2,b_2]]$

Informal description

For any elements $a = (a_1, a_2)$ and $b = (b_1, b_2)$ in the product lattice $\alpha \times \beta$, the unordered closed interval $[[a, b]]$ is equal to the product of the unordered closed intervals $[[a_1, b_1]] \times [[a_2, b_2]]$.

Set.uIcc_injective_right theorem

(a : α) : Injective fun b => uIcc b a

Full source

lemma uIcc_injective_right (a : α) : Injective fun b => uIcc b a := fun b c h => by
  rw [Set.ext_iff] at h
  exact eq_of_mem_uIcc_of_mem_uIcc ((h _).1 left_mem_uIcc) ((h _).2 left_mem_uIcc)

Right-Injectivity of Unordered Interval Construction

Informal description

For any element $a$ in a lattice $\alpha$, the function $b \mapsto [[b, a]]$ is injective, where $[[b, a]]$ denotes the unordered closed interval $[b \sqcap a, b \sqcup a]$.

Set.uIcc_injective_left theorem

(a : α) : Injective (uIcc a)

Full source

lemma uIcc_injective_left (a : α) : Injective (uIcc a) := by
  simpa only [uIcc_comm] using uIcc_injective_right a

Left-Injectivity of Unordered Interval Construction

Informal description

For any element $a$ in a lattice $\alpha$, the function $b \mapsto [[a, b]]$ is injective, where $[[a, b]]$ denotes the unordered closed interval $[a \sqcap b, a \sqcup b]$.

MonotoneOn.mapsTo_uIcc theorem

(hf : MonotoneOn f (uIcc a b)) : MapsTo f (uIcc a b) (uIcc (f a) (f b))

Full source

lemma _root_.MonotoneOn.mapsTo_uIcc (hf : MonotoneOn f (uIcc a b)) :
    MapsTo f (uIcc a b) (uIcc (f a) (f b)) := by
  rw [uIcc, uIcc, ← hf.map_sup, ← hf.map_inf] <;>
    apply_rules [left_mem_uIcc, right_mem_uIcc, hf.mapsTo_Icc]

Monotone Function Maps Unordered Interval to Unordered Interval of Endpoints

Informal description

Let $f$ be a function defined on the unordered closed interval $[[a, b]] := [a \sqcap b, a \sqcup b]$ in a lattice $\alpha$. If $f$ is monotone on $[[a, b]]$, then $f$ maps every element $x \in [[a, b]]$ to an element $f(x) \in [[f(a), f(b)]]$.

AntitoneOn.mapsTo_uIcc theorem

(hf : AntitoneOn f (uIcc a b)) : MapsTo f (uIcc a b) (uIcc (f a) (f b))

Full source

lemma _root_.AntitoneOn.mapsTo_uIcc (hf : AntitoneOn f (uIcc a b)) :
    MapsTo f (uIcc a b) (uIcc (f a) (f b)) := by
  rw [uIcc, uIcc, ← hf.map_sup, ← hf.map_inf] <;>
    apply_rules [left_mem_uIcc, right_mem_uIcc, hf.mapsTo_Icc]

Antitone Function Maps Unordered Interval to Unordered Interval

Informal description

Let $ f $ be a function defined on the unordered closed interval $[[a, b]]$ in a lattice $\alpha$. If $ f $ is antitone (i.e., decreasing) on $[[a, b]]$, then $ f $ maps $[[a, b]]$ into the unordered closed interval $[[f(a), f(b)]]$.

Monotone.mapsTo_uIcc theorem

(hf : Monotone f) : MapsTo f (uIcc a b) (uIcc (f a) (f b))

Full source

lemma _root_.Monotone.mapsTo_uIcc (hf : Monotone f) : MapsTo f (uIcc a b) (uIcc (f a) (f b)) :=
  (hf.monotoneOn _).mapsTo_uIcc

Monotone Function Preserves Unordered Interval Inclusion

Informal description

Let $f$ be a monotone function on a lattice $\alpha$. Then $f$ maps the unordered closed interval $[[a, b]] := [a \sqcap b, a \sqcup b]$ into the unordered closed interval $[[f(a), f(b)]]$.

Antitone.mapsTo_uIcc theorem

(hf : Antitone f) : MapsTo f (uIcc a b) (uIcc (f a) (f b))

Full source

lemma _root_.Antitone.mapsTo_uIcc (hf : Antitone f) : MapsTo f (uIcc a b) (uIcc (f a) (f b)) :=
  (hf.antitoneOn _).mapsTo_uIcc

Antitone Function Preserves Unordered Interval Inclusion

Informal description

Let $f$ be an antitone function on a lattice $\alpha$. Then $f$ maps the unordered closed interval $[[a, b]]$ into the unordered closed interval $[[f(a), f(b)]]$.

MonotoneOn.image_uIcc_subset theorem

(hf : MonotoneOn f (uIcc a b)) : f '' uIcc a b ⊆ uIcc (f a) (f b)

Full source

lemma _root_.MonotoneOn.image_uIcc_subset (hf : MonotoneOn f (uIcc a b)) :
    f '' uIcc a bf '' uIcc a b ⊆ uIcc (f a) (f b) := hf.mapsTo_uIcc.image_subset

Monotone Function Maps Unordered Interval to Unordered Interval of Endpoints

Informal description

Let $f$ be a function defined on the unordered closed interval $[[a, b]] := [a \sqcap b, a \sqcup b]$ in a lattice $\alpha$. If $f$ is monotone on $[[a, b]]$, then the image of $[[a, b]]$ under $f$ is contained in the unordered closed interval $[[f(a), f(b)]]$.

AntitoneOn.image_uIcc_subset theorem

(hf : AntitoneOn f (uIcc a b)) : f '' uIcc a b ⊆ uIcc (f a) (f b)

Full source

lemma _root_.AntitoneOn.image_uIcc_subset (hf : AntitoneOn f (uIcc a b)) :
    f '' uIcc a bf '' uIcc a b ⊆ uIcc (f a) (f b) := hf.mapsTo_uIcc.image_subset

Antitone Function Maps Unordered Interval to Unordered Interval of Endpoints

Informal description

Let $f$ be a function defined on the unordered closed interval $[[a, b]] := [a \sqcap b, a \sqcup b]$ in a lattice $\alpha$. If $f$ is antitone on $[[a, b]]$, then the image of $[[a, b]]$ under $f$ is contained in the unordered closed interval $[[f(a), f(b)]]$.

Monotone.image_uIcc_subset theorem

(hf : Monotone f) : f '' uIcc a b ⊆ uIcc (f a) (f b)

Full source

lemma _root_.Monotone.image_uIcc_subset (hf : Monotone f) : f '' uIcc a bf '' uIcc a b ⊆ uIcc (f a) (f b) :=
  (hf.monotoneOn _).image_uIcc_subset

Monotone Function Maps Unordered Interval to Unordered Interval of Images

Informal description

Let $f$ be a monotone function on a lattice $\alpha$. Then the image of the unordered closed interval $[[a, b]] := [a \sqcap b, a \sqcup b]$ under $f$ is contained in the unordered closed interval $[[f(a), f(b)]]$.

Antitone.image_uIcc_subset theorem

(hf : Antitone f) : f '' uIcc a b ⊆ uIcc (f a) (f b)

Full source

lemma _root_.Antitone.image_uIcc_subset (hf : Antitone f) : f '' uIcc a bf '' uIcc a b ⊆ uIcc (f a) (f b) :=
  (hf.antitoneOn _).image_uIcc_subset

Image of Unordered Interval under Antitone Function is Contained in Unordered Interval of Endpoints

Informal description

Let $f$ be an antitone function on a lattice $\alpha$. Then the image of the unordered closed interval $[[a, b]] := [a \sqcap b, a \sqcup b]$ under $f$ is contained in the unordered closed interval $[[f(a), f(b)]]$.

Set.Icc_min_max theorem

: Icc (min a b) (max a b) = [[a, b]]

Full source

theorem Icc_min_max : Icc (min a b) (max a b) = [[a, b]] :=
  rfl

Equality of Ordered and Unordered Intervals: $[\min(a, b), \max(a, b)] = [[a, b]]$

Informal description

For any two elements $a$ and $b$ in a lattice $\alpha$, the closed interval $[\min(a, b), \max(a, b)]$ is equal to the unordered interval $[[a, b]]$.

Set.uIcc_of_not_le theorem

(h : ¬a ≤ b) : [[a, b]] = Icc b a

Full source

lemma uIcc_of_not_le (h : ¬a ≤ b) : [[a, b]] = Icc b a := uIcc_of_gt <| lt_of_not_ge h

Unordered Interval Equals Ordered Interval When $a \not\leq b$

Informal description

For any two elements $a$ and $b$ in a lattice $\alpha$, if $a \not\leq b$, then the unordered closed interval $[[a, b]]$ is equal to the closed interval $[b, a]$.

Set.uIcc_of_not_ge theorem

(h : ¬b ≤ a) : [[a, b]] = Icc a b

Full source

lemma uIcc_of_not_ge (h : ¬b ≤ a) : [[a, b]] = Icc a b := uIcc_of_lt <| lt_of_not_ge h

Unordered Interval Equals Ordered Interval When $b \not\leq a$

Informal description

For any two elements $a$ and $b$ in a lattice $\alpha$, if $b \not\leq a$, then the unordered closed interval $[[a, b]]$ is equal to the closed interval $[a, b]$.

Set.uIcc_eq_union theorem

: [[a, b]] = Icc a b ∪ Icc b a

Full source

lemma uIcc_eq_union : [[a, b]] = IccIcc a b ∪ Icc b a := by rw [Icc_union_Icc', max_comm] <;> rfl

Unordered Interval as Union of Ordered Intervals: $[[a, b]] = [a, b] \cup [b, a]$

Informal description

For any two elements $a$ and $b$ in a lattice $\alpha$, the unordered closed interval $[[a, b]]$ is equal to the union of the closed intervals $[a, b]$ and $[b, a]$, i.e., $$ [[a, b]] = [a, b] \cup [b, a]. $$

Set.mem_uIcc theorem

: a ∈ [[b, c]] ↔ b ≤ a ∧ a ≤ c ∨ c ≤ a ∧ a ≤ b

Full source

lemma mem_uIcc : a ∈ [[b, c]]a ∈ [[b, c]] ↔ b ≤ a ∧ a ≤ c ∨ c ≤ a ∧ a ≤ b := by simp [uIcc_eq_union]

Membership Criterion for Unordered Interval: $a \in [[b, c]] \leftrightarrow (b \leq a \leq c) \lor (c \leq a \leq b)$

Informal description

For any elements $a$, $b$, and $c$ in a lattice $\alpha$, the element $a$ belongs to the unordered closed interval $[[b, c]]$ if and only if either $b \leq a \leq c$ or $c \leq a \leq b$ holds.

Set.not_mem_uIcc_of_lt theorem

(ha : c < a) (hb : c < b) : c ∉ [[a, b]]

Full source

lemma not_mem_uIcc_of_lt (ha : c < a) (hb : c < b) : c ∉ [[a, b]] :=
  not_mem_Icc_of_lt <| lt_min_iff.mpr ⟨ha, hb⟩

Non-membership in Unordered Interval Due to Strict Lower Bound

Informal description

For any elements $a$, $b$, and $c$ in a lattice $\alpha$, if $c$ is strictly less than both $a$ and $b$, then $c$ does not belong to the unordered closed interval $[[a, b]]$.

Set.not_mem_uIcc_of_gt theorem

(ha : a < c) (hb : b < c) : c ∉ [[a, b]]

Full source

lemma not_mem_uIcc_of_gt (ha : a < c) (hb : b < c) : c ∉ [[a, b]] :=
  not_mem_Icc_of_gt <| max_lt_iff.mpr ⟨ha, hb⟩

Non-membership in Unordered Interval Due to Strict Upper Bound

Informal description

For any elements $a$, $b$, and $c$ in a lattice $\alpha$, if both $a < c$ and $b < c$ hold, then $c$ does not belong to the unordered closed interval $[[a, b]]$.

Set.uIcc_subset_uIcc_iff_le theorem

: [[a₁, b₁]] ⊆ [[a₂, b₂]] ↔ min a₂ b₂ ≤ min a₁ b₁ ∧ max a₁ b₁ ≤ max a₂ b₂

Full source

lemma uIcc_subset_uIcc_iff_le :
    [[a₁, b₁]][[a₁, b₁]] ⊆ [[a₂, b₂]][[a₁, b₁]] ⊆ [[a₂, b₂]] ↔ min a₂ b₂ ≤ min a₁ b₁ ∧ max a₁ b₁ ≤ max a₂ b₂ :=
  uIcc_subset_uIcc_iff_le'

Subset condition for unordered intervals via minima and maxima

Informal description

For any elements $a_1, b_1, a_2, b_2$ in a linearly ordered set, the unordered interval $[[a_1, b_1]]$ is a subset of the unordered interval $[[a_2, b_2]]$ if and only if the minimum of $a_2$ and $b_2$ is less than or equal to the minimum of $a_1$ and $b_1$, and the maximum of $a_1$ and $b_1$ is less than or equal to the maximum of $a_2$ and $b_2$. In symbols: $$ [[a_1, b_1]] \subseteq [[a_2, b_2]] \iff \min(a_2, b_2) \leq \min(a_1, b_1) \text{ and } \max(a_1, b_1) \leq \max(a_2, b_2) $$

Set.uIcc_subset_uIcc_union_uIcc theorem

: [[a, c]] ⊆ [[a, b]] ∪ [[b, c]]

Full source

/-- A sort of triangle inequality. -/
lemma uIcc_subset_uIcc_union_uIcc : [[a, c]][[a, c]] ⊆ [[a, b]] ∪ [[b, c]] := fun x => by
  simp only [mem_uIcc, mem_union]
  rcases le_total x b with h2 | h2 <;> tauto

Triangle-like Inclusion for Unordered Intervals: $[[a, c]] \subseteq [[a, b]] \cup [[b, c]]$

Informal description

For any elements $a$, $b$, and $c$ in a lattice $\alpha$, the unordered closed interval $[[a, c]]$ is contained in the union of the unordered closed intervals $[[a, b]]$ and $[[b, c]]$. In other words, every element lying between $a$ and $c$ also lies between $a$ and $b$ or between $b$ and $c$.

Set.monotone_or_antitone_iff_uIcc theorem

: Monotone f ∨ Antitone f ↔ ∀ a b c, c ∈ [[a, b]] → f c ∈ [[f a, f b]]

Full source

lemma monotone_or_antitone_iff_uIcc :
    MonotoneMonotone f ∨ Antitone fMonotone f ∨ Antitone f ↔ ∀ a b c, c ∈ [[a, b]] → f c ∈ [[f a, f b]] := by
  constructor
  · rintro (hf | hf) a b c <;> simp_rw [← Icc_min_max, ← hf.map_min, ← hf.map_max]
    exacts [fun hc => ⟨hf hc.1, hf hc.2⟩, fun hc => ⟨hf hc.2, hf hc.1⟩]
  contrapose!
  rw [not_monotone_not_antitone_iff_exists_le_le]
  rintro ⟨a, b, c, hab, hbc, ⟨hfab, hfcb⟩ | ⟨hfba, hfbc⟩⟩
  · exact ⟨a, c, b, Icc_subset_uIcc ⟨hab, hbc⟩, fun h => h.2.not_lt <| max_lt hfab hfcb⟩
  · exact ⟨a, c, b, Icc_subset_uIcc ⟨hab, hbc⟩, fun h => h.1.not_lt <| lt_min hfba hfbc⟩

Characterization of Monotonicity/Antitonicity via Unordered Intervals

Informal description

A function $f$ on a lattice $\alpha$ is either monotone or antitone if and only if for all elements $a, b, c \in \alpha$, whenever $c$ lies in the unordered interval $[[a, b]] := [a \sqcap b, a \sqcup b]$, then $f(c)$ lies in the unordered interval $[[f(a), f(b)]]$.

Set.monotoneOn_or_antitoneOn_iff_uIcc theorem

: MonotoneOn f s ∨ AntitoneOn f s ↔ ∀ᵉ (a ∈ s) (b ∈ s) (c ∈ s), c ∈ [[a, b]] → f c ∈ [[f a, f b]]

Full source

lemma monotoneOn_or_antitoneOn_iff_uIcc :
    MonotoneOnMonotoneOn f s ∨ AntitoneOn f sMonotoneOn f s ∨ AntitoneOn f s ↔
      ∀ᵉ (a ∈ s) (b ∈ s) (c ∈ s), c ∈ [[a, b]] → f c ∈ [[f a, f b]] := by
  simp [monotoneOn_iff_monotone, antitoneOn_iff_antitone, monotone_or_antitone_iff_uIcc,
    mem_uIcc]

Characterization of Monotonicity or Antitonicity via Unordered Intervals

Informal description

A function $f$ defined on a set $s$ in a lattice $\alpha$ is either monotone or antitone on $s$ if and only if for all $a, b, c \in s$, whenever $c$ lies in the unordered interval $[[a, b]]$, then $f(c)$ lies in the unordered interval $[[f(a), f(b)]]$.

Set.uIoc definition

: α → α → Set α

Full source

/-- The open-closed uIcc with unordered bounds. -/
def uIoc : α → α → Set α := fun a b => Ioc (min a b) (max a b)

Open-closed interval with unordered bounds

Informal description

For any two elements $a$ and $b$ in a lattice $\alpha$, the interval $\text{uIoc}(a, b)$ is defined as the set of all elements $x$ such that $\min(a, b) < x \leq \max(a, b)$. This is an open-closed interval that automatically adjusts to the order of $a$ and $b$.

Interval.termΙ definition

: Lean.ParserDescr✝

Full source

/-- `Ι a b` denotes the open-closed interval with unordered bounds. Here, `Ι` is a capital iota,
distinguished from a capital `i`. -/
scoped[Interval] notation "Ι" => Set.uIoc

Open-closed interval with unordered bounds (`Ι a b`)

Informal description

The notation `Ι a b` denotes the open-closed interval with unordered bounds, where `Ι` is a capital iota (distinct from a capital `i`). This interval consists of all elements between `a` and `b`, regardless of their order, and includes the lower bound but excludes the upper bound.

Set.uIoc_of_le theorem

(h : a ≤ b) : Ι a b = Ioc a b

Full source

@[simp] lemma uIoc_of_le (h : a ≤ b) : Ι a b = Ioc a b := by simp [uIoc, h]

Unordered Open-Closed Interval Equals Ioc When $a \leq b$

Informal description

For any two elements $a$ and $b$ in a lattice $\alpha$, if $a \leq b$, then the unordered open-closed interval $\text{uIoc}(a, b)$ is equal to the left-open right-closed interval $\text{Ioc}(a, b)$.

Set.uIoc_of_ge theorem

(h : b ≤ a) : Ι a b = Ioc b a

Full source

@[simp] lemma uIoc_of_ge (h : b ≤ a) : Ι a b = Ioc b a := by simp [uIoc, h]

Unordered Open-Closed Interval Equals Ioc When $b \leq a$

Informal description

For any two elements $a$ and $b$ in a lattice $\alpha$, if $b \leq a$, then the unordered open-closed interval $\text{uIoc}(a, b)$ is equal to the left-open right-closed interval $\text{Ioc}(b, a)$.

Set.uIoc_eq_union theorem

: Ι a b = Ioc a b ∪ Ioc b a

Full source

lemma uIoc_eq_union : Ι a b = IocIoc a b ∪ Ioc b a := by
  cases le_total a b <;> simp [uIoc, *]

Decomposition of Unordered Open-Closed Interval into Ordered Intervals

Informal description

For any two elements $a$ and $b$ in a lattice $\alpha$, the unordered open-closed interval $\text{uIoc}(a, b)$ is equal to the union of the left-open right-closed intervals $\text{Ioc}(a, b)$ and $\text{Ioc}(b, a)$. That is, $\text{uIoc}(a, b) = \text{Ioc}(a, b) \cup \text{Ioc}(b, a)$.

Set.mem_uIoc theorem

: a ∈ Ι b c ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b

Full source

lemma mem_uIoc : a ∈ Ι b ca ∈ Ι b c ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b := by
  rw [uIoc_eq_union, mem_union, mem_Ioc, mem_Ioc]

Membership Criterion for Unordered Open-Closed Interval: $a \in \text{uIoc}(b, c) \leftrightarrow (b < a \leq c) \lor (c < a \leq b)$

Informal description

For any elements $a$, $b$, and $c$ in a lattice $\alpha$, the element $a$ belongs to the unordered open-closed interval $\text{uIoc}(b, c)$ if and only if either $b < a \leq c$ or $c < a \leq b$.

Set.not_mem_uIoc theorem

: a ∉ Ι b c ↔ a ≤ b ∧ a ≤ c ∨ c < a ∧ b < a

Full source

lemma not_mem_uIoc : a ∉ Ι b ca ∉ Ι b c ↔ a ≤ b ∧ a ≤ c ∨ c < a ∧ b < a := by
  simp only [uIoc_eq_union, mem_union, mem_Ioc, not_lt, ← not_le]
  tauto

Non-membership Criterion for Unordered Open-Closed Interval

Informal description

For any elements $a$, $b$, and $c$ in a lattice $\alpha$, the element $a$ does not belong to the open-closed interval $\text{uIoc}(b, c)$ if and only if either $a$ is less than or equal to both $b$ and $c$, or $a$ is greater than both $b$ and $c$. That is, $a \notin \text{uIoc}(b, c) \leftrightarrow (a \leq b \land a \leq c) \lor (c < a \land b < a)$.

Set.left_mem_uIoc theorem

: a ∈ Ι a b ↔ b < a

Full source

@[simp] lemma left_mem_uIoc : a ∈ Ι a ba ∈ Ι a b ↔ b < a := by simp [mem_uIoc]

Left Endpoint Membership in Open-Closed Interval: $a \in \text{uIoc}(a, b) \leftrightarrow b < a$

Informal description

For any two elements $a$ and $b$ in a lattice $\alpha$, the element $a$ belongs to the open-closed interval $\text{uIoc}(a, b)$ if and only if $b < a$.

Set.right_mem_uIoc theorem

: b ∈ Ι a b ↔ a < b

Full source

@[simp] lemma right_mem_uIoc : b ∈ Ι a bb ∈ Ι a b ↔ a < b := by simp [mem_uIoc]

Right Endpoint Membership in Open-Closed Interval: $b \in \text{uIoc}(a, b) \leftrightarrow a < b$

Informal description

For any two elements $a$ and $b$ in a lattice $\alpha$, the element $b$ belongs to the open-closed interval $\text{uIoc}(a, b)$ if and only if $a < b$.

Set.forall_uIoc_iff theorem

{P : α → Prop} : (∀ x ∈ Ι a b, P x) ↔ (∀ x ∈ Ioc a b, P x) ∧ ∀ x ∈ Ioc b a, P x

Full source

lemma forall_uIoc_iff {P : α → Prop} :
    (∀ x ∈ Ι a b, P x) ↔ (∀ x ∈ Ioc a b, P x) ∧ ∀ x ∈ Ioc b a, P x := by
  simp only [uIoc_eq_union, mem_union, or_imp, forall_and]

Universal Quantification over Unordered Open-Closed Interval Decomposes into Ordered Intervals

Informal description

For any predicate $P$ on elements of a lattice $\alpha$, the statement that $P(x)$ holds for all $x$ in the unordered open-closed interval $\text{uIoc}(a, b)$ is equivalent to the conjunction of $P(x)$ holding for all $x$ in the ordered open-closed interval $\text{Ioc}(a, b)$ and $P(x)$ holding for all $x$ in the ordered open-closed interval $\text{Ioc}(b, a)$. In symbols: \[ (\forall x \in \text{uIoc}(a, b),\, P(x)) \leftrightarrow (\forall x \in \text{Ioc}(a, b),\, P(x)) \land (\forall x \in \text{Ioc}(b, a),\, P(x)). \]

Set.uIoc_subset_uIoc_of_uIcc_subset_uIcc theorem

{a b c d : α} (h : [[a, b]] ⊆ [[c, d]]) : Ι a b ⊆ Ι c d

Full source

lemma uIoc_subset_uIoc_of_uIcc_subset_uIcc {a b c d : α}
    (h : [[a, b]][[a, b]] ⊆ [[c, d]]) : ΙΙ a b ⊆ Ι c d :=
  Ioc_subset_Ioc (uIcc_subset_uIcc_iff_le.1 h).1 (uIcc_subset_uIcc_iff_le.1 h).2

Inclusion of Unordered Open-Closed Intervals via Unordered Closed Intervals

Informal description

For any elements $a, b, c, d$ in a lattice $\alpha$, if the unordered closed interval $[[a, b]]$ is contained in the unordered closed interval $[[c, d]]$, then the unordered open-closed interval $\text{uIoc}(a, b)$ is contained in the unordered open-closed interval $\text{uIoc}(c, d)$. In symbols: \[ [[a, b]] \subseteq [[c, d]] \implies \text{uIoc}(a, b) \subseteq \text{uIoc}(c, d). \]

Set.uIoc_comm theorem

(a b : α) : Ι a b = Ι b a

Full source

lemma uIoc_comm (a b : α) : Ι a b = Ι b a := by simp only [uIoc, min_comm a b, max_comm a b]

Commutativity of Unordered Open-Closed Interval: $\text{uIoc}(a, b) = \text{uIoc}(b, a)$

Informal description

For any two elements $a$ and $b$ in a lattice $\alpha$, the unordered open-closed interval $\text{uIoc}(a, b)$ is equal to $\text{uIoc}(b, a)$. In other words, the interval is symmetric with respect to its arguments.

Set.Ioc_subset_uIoc theorem

: Ioc a b ⊆ Ι a b

Full source

lemma Ioc_subset_uIoc : IocIoc a b ⊆ Ι a b := Ioc_subset_Ioc (min_le_left _ _) (le_max_right _ _)

Inclusion of $(a, b]$ in $\text{uIoc}(a, b)$

Informal description

For any two elements $a$ and $b$ in a lattice $\alpha$, the left-open right-closed interval $(a, b]$ is contained in the unordered open-closed interval $\text{uIoc}(a, b)$, defined as the set of all $x$ such that $\min(a, b) < x \leq \max(a, b)$.

Set.Ioc_subset_uIoc' theorem

: Ioc a b ⊆ Ι b a

Full source

lemma Ioc_subset_uIoc' : IocIoc a b ⊆ Ι b a := Ioc_subset_Ioc (min_le_right _ _) (le_max_left _ _)

Inclusion of $(a, b]$ in $\text{uIoc}(b, a)$

Informal description

For any two elements $a$ and $b$ in a lattice $\alpha$, the left-open right-closed interval $(a, b]$ is contained in the unordered open-closed interval $\text{uIoc}(b, a)$.

Set.uIoc_subset_uIcc theorem

: Ι a b ⊆ uIcc a b

Full source

lemma uIoc_subset_uIcc : ΙΙ a b ⊆ uIcc a b := Ioc_subset_Icc_self

Inclusion of Unordered Open-Closed Interval in Unordered Closed Interval: $\text{uIoc}(a, b) \subseteq \text{uIcc}(a, b)$

Informal description

For any elements $a$ and $b$ in a lattice $\alpha$, the unordered open-closed interval $\text{uIoc}(a, b)$ is contained in the unordered closed interval $\text{uIcc}(a, b)$. That is, for all $x \in \alpha$ such that $\min(a, b) < x \leq \max(a, b)$, we have $\min(a, b) \leq x \leq \max(a, b)$.

Set.uIoc_injective_right theorem

(a : α) : Injective fun b => Ι b a

Full source

lemma uIoc_injective_right (a : α) : Injective fun b => Ι b a := by
  rintro b c h
  rw [Set.ext_iff] at h
  obtain ha | ha := le_or_lt b a
  · have hb := (h b).not
    simp only [ha, left_mem_uIoc, not_lt, true_iff, not_mem_uIoc, ← not_le,
      and_true, not_true, false_and, not_false_iff, or_false] at hb
    refine hb.eq_of_not_lt fun hc => ?_
    simpa [ha, and_iff_right hc, ← @not_le _ _ _ a, iff_not_self, -not_le] using h c
  · refine
      eq_of_mem_uIoc_of_mem_uIoc ((h _).1 <| left_mem_uIoc.2 ha)
        ((h _).2 <| left_mem_uIoc.2 <| ha.trans_le ?_)
    simpa [ha, ha.not_le, mem_uIoc] using h b

Injectivity of the Unordered Open-Closed Interval in the Right Argument

Informal description

For any element $a$ in a lattice $\alpha$, the function $b \mapsto \text{uIoc}(b, a)$ is injective. That is, for any $b_1, b_2 \in \alpha$, if $\text{uIoc}(b_1, a) = \text{uIoc}(b_2, a)$, then $b_1 = b_2$.

Set.uIoc_union_uIoc theorem

(h : b ∈ [[a, c]]) : Ι a b ∪ Ι b c = Ι a c

Full source

lemma uIoc_union_uIoc (h : b ∈ [[a, c]]) : ΙΙ a b ∪ Ι b c = Ι a c := by
  wlog hac : a ≤ c generalizing a c
  · rw [uIoc_comm, union_comm, uIoc_comm, this _ (le_of_not_le hac), uIoc_comm]
    rwa [uIcc_comm]
  rw [uIcc_of_le hac] at h
  rw [uIoc_of_le h.1, uIoc_of_le h.2, uIoc_of_le hac, Ioc_union_Ioc_eq_Ioc h.1 h.2]

Union of Adjacent Unordered Open-Closed Intervals: $\text{uIoc}(a, b) \cup \text{uIoc}(b, c) = \text{uIoc}(a, c)$ when $b \in [[a, c]]$

Informal description

For any elements $a$, $b$, and $c$ in a lattice $\alpha$ such that $b$ belongs to the unordered closed interval $[[a, c]]$, the union of the unordered open-closed intervals $\text{uIoc}(a, b)$ and $\text{uIoc}(b, c)$ equals $\text{uIoc}(a, c)$. In other words: \[ \text{uIoc}(a, b) \cup \text{uIoc}(b, c) = \text{uIoc}(a, c) \] when $b$ lies between $a$ and $c$.

Set.uIoo definition

(a b : α) : Set α

Full source

/-- `uIoo a b` is the set of elements lying between `a` and `b`, with `a` and `b` not included.
Note that we define it more generally in a lattice as `Set.Ioo (a ⊓ b) (a ⊔ b)`. In a product type,
`uIoo` corresponds to the bounding box of the two elements. -/
def uIoo (a b : α) : Set α := Ioo (a ⊓ b) (a ⊔ b)

Open unordered interval between $a$ and $b$

Informal description

For any two elements $a$ and $b$ in a lattice $\alpha$, the interval $\text{uIoo}(a, b)$ is defined as the open interval between the infimum and supremum of $a$ and $b$, i.e., $\text{Ioo}(a \sqcap b, a \sqcup b)$. This represents the set of all elements strictly between $a$ and $b$ in the lattice order, regardless of their relative ordering.

Set.uIoo_toDual theorem

(a b : α) : uIoo (toDual a) (toDual b) = ofDual ⁻¹' uIoo a b

Full source

@[simp]
lemma uIoo_toDual (a b : α) : uIoo (toDual a) (toDual b) = ofDualofDual ⁻¹' uIoo a b :=
  Ioo_toDual (α := α)

Duality of Unordered Open Intervals: $\text{uIoo}(a^\text{op}, b^\text{op}) = \text{ofDual}^{-1}(\text{uIoo}(a, b))$

Informal description

For any elements $a$ and $b$ in a lattice $\alpha$, the unordered open interval $\text{uIoo}(\text{toDual}(a), \text{toDual}(b))$ in the order dual $\alpha^\text{op}$ is equal to the preimage under $\text{ofDual}$ of the unordered open interval $\text{uIoo}(a, b)$ in $\alpha$. In other words: \[ \text{uIoo}(a^\text{op}, b^\text{op}) = \text{ofDual}^{-1}\big(\text{uIoo}(a, b)\big) \] where $a^\text{op} = \text{toDual}(a)$ and $b^\text{op} = \text{toDual}(b)$ denote the elements in the dual order.

Set.uIoo_ofDual theorem

(a b : αᵒᵈ) : uIoo (ofDual a) (ofDual b) = toDual ⁻¹' uIoo a b

Full source

@[simp]
theorem uIoo_ofDual (a b : αᵒᵈ) : uIoo (ofDual a) (ofDual b) = toDualtoDual ⁻¹' uIoo a b :=
  Ioo_ofDual

Dual Unordered Open Interval Correspondence: $\text{uIoo}$ in Dual Order Equals Preimage of $\text{uIoo}$

Informal description

For any elements $a$ and $b$ in the order dual $\alpha^\text{op}$ of a lattice $\alpha$, the unordered open interval $\text{uIoo}(\text{ofDual}(a), \text{ofDual}(b))$ is equal to the preimage under $\text{toDual}$ of the unordered open interval $\text{uIoo}(a, b)$. In other words: \[ \text{uIoo}(a^\text{op}, b^\text{op}) = \text{toDual}^{-1}\big(\text{uIoo}(a, b)\big) \] where $a^\text{op}$ and $b^\text{op}$ denote the elements in the dual order.

Set.uIoo_of_le theorem

(h : a ≤ b) : uIoo a b = Ioo a b

Full source

@[simp] lemma uIoo_of_le (h : a ≤ b) : uIoo a b = Ioo a b := by
  rw [uIoo, inf_eq_left.2 h, sup_eq_right.2 h]

Unordered Open Interval Equals Ordered Open Interval When $a \leq b$

Informal description

For any two elements $a$ and $b$ in a lattice $\alpha$ with $a \leq b$, the unordered open interval $\text{uIoo}(a, b)$ equals the open interval $(a, b)$.

Set.uIoo_of_ge theorem

(h : b ≤ a) : uIoo a b = Ioo b a

Full source

@[simp] lemma uIoo_of_ge (h : b ≤ a) : uIoo a b = Ioo b a := by
  rw [uIoo, inf_eq_right.2 h, sup_eq_left.2 h]

Unordered Open Interval Equals Ordered Open Interval When $b \leq a$

Informal description

For any two elements $a$ and $b$ in a lattice $\alpha$ with $b \leq a$, the unordered open interval $\text{uIoo}(a, b)$ equals the open interval $(b, a)$.

Set.uIoo_comm theorem

(a b : α) : uIoo a b = uIoo b a

Full source

lemma uIoo_comm (a b : α) : uIoo a b = uIoo b a := by simp_rw [uIoo, inf_comm, sup_comm]

Commutativity of Unordered Open Interval: $\text{uIoo}(a, b) = \text{uIoo}(b, a)$

Informal description

For any two elements $a$ and $b$ in a lattice $\alpha$, the unordered open interval $\text{uIoo}(a, b)$ is equal to $\text{uIoo}(b, a)$. In other words, the open interval between the infimum and supremum of $a$ and $b$ is symmetric in $a$ and $b$.

Set.uIoo_of_lt theorem

(h : a < b) : uIoo a b = Ioo a b

Full source

lemma uIoo_of_lt (h : a < b) : uIoo a b = Ioo a b := uIoo_of_le h.le

Unordered Open Interval Equals Ordered Open Interval When $a < b$

Informal description

For any two elements $a$ and $b$ in a lattice $\alpha$ with $a < b$, the unordered open interval $\text{uIoo}(a, b)$ equals the ordered open interval $(a, b)$.

Set.uIoo_of_gt theorem

(h : b < a) : uIoo a b = Ioo b a

Full source

lemma uIoo_of_gt (h : b < a) : uIoo a b = Ioo b a := uIoo_of_ge h.le

Unordered Open Interval Equals Ordered Open Interval When $b < a$

Informal description

For any two elements $a$ and $b$ in a lattice $\alpha$ with $b < a$, the unordered open interval $\text{uIoo}(a, b)$ equals the open interval $(b, a)$.

Set.uIoo_self theorem

: uIoo a a = ∅

Full source

lemma uIoo_self : uIoo a a = ∅ := by simp [uIoo]

Empty Unordered Open Interval at a Point

Informal description

For any element $a$ in a lattice $\alpha$, the unordered open interval $\text{uIoo}(a, a)$ is empty, i.e., $\text{uIoo}(a, a) = \emptyset$.

Set.Ioo_subset_uIoo theorem

: Ioo a b ⊆ uIoo a b

Full source

lemma Ioo_subset_uIoo : IooIoo a b ⊆ uIoo a b := Ioo_subset_Ioo inf_le_left le_sup_right

Inclusion of Open Interval in Unordered Open Interval

Informal description

For any elements $a$ and $b$ in a lattice $\alpha$, the open interval $(a, b)$ is a subset of the unordered open interval $\text{uIoo}(a, b)$, which is defined as the open interval between the infimum and supremum of $a$ and $b$, i.e., $(\inf(a, b), \sup(a, b))$.

Set.Ioo_subset_uIoo' theorem

: Ioo b a ⊆ uIoo a b

Full source

/-- Same as `Ioo_subset_uIoo` but with `Ioo a b` replaced by `Ioo b a`. -/
lemma Ioo_subset_uIoo' : IooIoo b a ⊆ uIoo a b := Ioo_subset_Ioo inf_le_right le_sup_left

Inclusion of Reversed Open Interval in Unordered Open Interval

Informal description

For any elements $a$ and $b$ in a lattice $\alpha$, the open interval $(b, a)$ is a subset of the unordered open interval $\text{uIoo}(a, b)$, which is defined as the open interval between the infimum and supremum of $a$ and $b$, i.e., $(\inf(a, b), \sup(a, b))$.

Set.mem_uIoo_of_lt theorem

(ha : a < x) (hb : x < b) : x ∈ uIoo a b

Full source

lemma mem_uIoo_of_lt (ha : a < x) (hb : x < b) : x ∈ uIoo a b := Ioo_subset_uIoo ⟨ha, hb⟩

Membership in Unordered Open Interval for Less-Than Case

Informal description

For any elements $a$, $b$, and $x$ in a lattice $\alpha$, if $a < x$ and $x < b$, then $x$ belongs to the unordered open interval $\text{uIoo}(a, b) = (\inf(a, b), \sup(a, b))$.

Set.mem_uIoo_of_gt theorem

(hb : b < x) (ha : x < a) : x ∈ uIoo a b

Full source

lemma mem_uIoo_of_gt (hb : b < x) (ha : x < a) : x ∈ uIoo a b := Ioo_subset_uIoo' ⟨hb, ha⟩

Membership in Unordered Open Interval for Greater-Than Case

Informal description

For any elements $a$, $b$, and $x$ in a lattice $\alpha$, if $b < x$ and $x < a$, then $x$ belongs to the unordered open interval $\text{uIoo}(a, b) = (\inf(a, b), \sup(a, b))$.

Set.Ioo_min_max theorem

: Ioo (min a b) (max a b) = uIoo a b

Full source

theorem Ioo_min_max : Ioo (min a b) (max a b) = uIoo a b := rfl

Open Interval as Unordered Interval: $(min(a,b), max(a,b)) = \text{uIoo}(a, b)$

Informal description

For any two elements $a$ and $b$ in a linearly ordered set, the open interval between the minimum and maximum of $a$ and $b$ is equal to the unordered open interval between $a$ and $b$, i.e., $$(min(a,b), max(a,b)) = \text{uIoo}(a, b).$$

Set.uIoo_of_not_le theorem

(h : ¬a ≤ b) : uIoo a b = Ioo b a

Full source

lemma uIoo_of_not_le (h : ¬a ≤ b) : uIoo a b = Ioo b a := uIoo_of_gt <| lt_of_not_ge h

Unordered Open Interval Equals Ordered Open Interval When $a \nleq b$

Informal description

For any two elements $a$ and $b$ in a lattice $\alpha$, if $a$ is not less than or equal to $b$, then the unordered open interval $\text{uIoo}(a, b)$ equals the open interval $(b, a)$.

Set.uIoo_of_not_ge theorem

(h : ¬b ≤ a) : uIoo a b = Ioo a b

Full source

lemma uIoo_of_not_ge (h : ¬b ≤ a) : uIoo a b = Ioo a b := uIoo_of_lt <| lt_of_not_ge h

Unordered Open Interval Equals Ordered Open Interval When $b \ngeq a$

Informal description

For any two elements $a$ and $b$ in a lattice $\alpha$, if $b$ is not greater than or equal to $a$, then the unordered open interval $\text{uIoo}(a, b)$ equals the open interval $(a, b)$.

Set.uIoo_subset_uIcc theorem

{α : Type*} [LinearOrder α] (a : α) (b : α) : uIoo a b ⊆ uIcc a b

Full source

theorem uIoo_subset_uIcc {α : Type*} [LinearOrder α] (a : α) (b : α) : uIoouIoo a b ⊆ uIcc a b := by
  simp [uIoo, uIcc, Ioo_subset_Icc_self]

Inclusion of Open Unordered Interval in Closed Unordered Interval

Informal description

For any two elements $a$ and $b$ in a linearly ordered type $\alpha$, the open unordered interval $\text{uIoo}(a, b)$ is a subset of the closed unordered interval $\text{uIcc}(a, b)$. In other words, every element strictly between $a$ and $b$ (in either order) is also between $a$ and $b$ (inclusive).

Notation