Mathlib.Order.Directed

Directed definition

(f : ι → α)

Full source

/-- A family of elements of α is directed (with respect to a relation `≼` on α)
  if there is a member of the family `≼`-above any pair in the family. -/
def Directed (f : ι → α) :=
  ∀ x y, ∃ z, f x ≼ f z ∧ f y ≼ f z

Directed family of elements

Informal description

An indexed family of elements $ f : \iota \to \alpha $ is called *directed* with respect to a relation $ \preccurlyeq $ on $ \alpha $ if for any two elements $ f(x) $ and $ f(y) $ in the family, there exists an element $ f(z) $ in the family such that both $ f(x) \preccurlyeq f(z) $ and $ f(y) \preccurlyeq f(z) $.

DirectedOn definition

(s : Set α)

Full source

/-- A subset of α is directed if there is an element of the set `≼`-above any
  pair of elements in the set. -/
def DirectedOn (s : Set α) :=
  ∀ x ∈ s, ∀ y ∈ s, ∃ z ∈ s, x ≼ z ∧ y ≼ z

Directed set with respect to a relation

Informal description

A subset $s$ of a type $\alpha$ is called *directed* with respect to a relation $\preccurlyeq$ if for any two elements $x, y \in s$, there exists an element $z \in s$ such that $x \preccurlyeq z$ and $y \preccurlyeq z$.

directedOn_iff_directed theorem

{s} : @DirectedOn α r s ↔ Directed r (Subtype.val : s → α)

Full source

theorem directedOn_iff_directed {s} : @DirectedOn α r s ↔ Directed r (Subtype.val : s → α) := by
  simp only [DirectedOn, Directed, Subtype.exists, exists_and_left, exists_prop, Subtype.forall]
  exact forall₂_congr fun x _ => by simp [And.comm, and_assoc]

Equivalence of Directed Set and Directed Family via Inclusion Map

Informal description

For any subset $s$ of a type $\alpha$ and a relation $r$ on $\alpha$, the set $s$ is directed with respect to $r$ if and only if the family of elements obtained by the inclusion map $\text{Subtype.val} : s \to \alpha$ is directed with respect to $r$.

directedOn_range theorem

{f : ι → α} : Directed r f ↔ DirectedOn r (Set.range f)

Full source

theorem directedOn_range {f : ι → α} : DirectedDirected r f ↔ DirectedOn r (Set.range f) := by
  simp_rw [Directed, DirectedOn, Set.forall_mem_range, Set.exists_range_iff]

Equivalence of Directed Families and Directed Ranges

Informal description

An indexed family of elements $f : \iota \to \alpha$ is directed with respect to a relation $\preccurlyeq$ if and only if the range of $f$ is a directed subset of $\alpha$ with respect to $\preccurlyeq$. That is, for any two elements $f(x)$ and $f(y)$ in the family, there exists an element $f(z)$ in the family such that both $f(x) \preccurlyeq f(z)$ and $f(y) \preccurlyeq f(z)$.

directedOn_image theorem

{s : Set β} {f : β → α} : DirectedOn r (f '' s) ↔ DirectedOn (f ⁻¹'o r) s

Full source

theorem directedOn_image {s : Set β} {f : β → α} :
    DirectedOnDirectedOn r (f '' s) ↔ DirectedOn (f ⁻¹'o r) s := by
  simp only [DirectedOn, Set.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂, Order.Preimage]

Directedness of Image Set under Relation Pullback

Informal description

For any set $s \subseteq \beta$ and function $f : \beta \to \alpha$, the image $f(s)$ is directed with respect to a relation $r$ on $\alpha$ if and only if $s$ is directed with respect to the pullback relation $f^{-1}o\,r$ on $\beta$, where $x \mathrel{(f^{-1}o\,r)} y$ means $f(x) \mathrel{r} f(y)$.

DirectedOn.mono' theorem

 {s : Set α} (hs : DirectedOn r s) (h : ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → r a b → r' a b) : DirectedOn r' s

Full source

theorem DirectedOn.mono' {s : Set α} (hs : DirectedOn r s)
    (h : ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → r a b → r' a b) : DirectedOn r' s := fun _ hx _ hy =>
  let ⟨z, hz, hxz, hyz⟩ := hs _ hx _ hy
  ⟨z, hz, h hx hz hxz, h hy hz hyz⟩

Directedness is Preserved Under Weaker Relations

Informal description

Let $s$ be a subset of a type $\alpha$ that is directed with respect to a relation $\preccurlyeq$ (i.e., for any $x, y \in s$, there exists $z \in s$ such that $x \preccurlyeq z$ and $y \preccurlyeq z$). If for all $a, b \in s$, the relation $\preccurlyeq$ implies another relation $\preccurlyeq'$ (i.e., $a \preccurlyeq b \Rightarrow a \preccurlyeq' b$), then $s$ is also directed with respect to $\preccurlyeq'$.

DirectedOn.mono theorem

{s : Set α} (h : DirectedOn r s) (H : ∀ ⦃a b⦄, r a b → r' a b) : DirectedOn r' s

Full source

theorem DirectedOn.mono {s : Set α} (h : DirectedOn r s) (H : ∀ ⦃a b⦄, r a b → r' a b) :
    DirectedOn r' s :=
  h.mono' fun _ _ _ _ h ↦ H h

Directedness is Preserved Under Weaker Relations (Global Version)

Informal description

Let $s$ be a subset of a type $\alpha$ that is directed with respect to a relation $\preccurlyeq$ (i.e., for any $x, y \in s$, there exists $z \in s$ such that $x \preccurlyeq z$ and $y \preccurlyeq z$). If for all $a, b \in \alpha$, the relation $\preccurlyeq$ implies another relation $\preccurlyeq'$ (i.e., $a \preccurlyeq b \Rightarrow a \preccurlyeq' b$), then $s$ is also directed with respect to $\preccurlyeq'$.

directed_comp theorem

{ι} {f : ι → β} {g : β → α} : Directed r (g ∘ f) ↔ Directed (g ⁻¹'o r) f

Full source

theorem directed_comp {ι} {f : ι → β} {g : β → α} : DirectedDirected r (g ∘ f) ↔ Directed (g ⁻¹'o r) f :=
  Iff.rfl

Composition of Directed Families via Pullback Relation

Informal description

For any relation $r$ on $\alpha$, a family of elements $f : \iota \to \beta$, and a function $g : \beta \to \alpha$, the composition $g \circ f$ is $r$-directed if and only if $f$ is directed with respect to the pullback relation $g^{-1}o\,r$ (defined by $x \mathrel{(g^{-1}o\,r)} y \leftrightarrow g(x) \mathrel{r} g(y)$).

Directed.mono theorem

{s : α → α → Prop} {ι} {f : ι → α} (H : ∀ a b, r a b → s a b) (h : Directed r f) : Directed s f

Full source

theorem Directed.mono {s : α → α → Prop} {ι} {f : ι → α} (H : ∀ a b, r a b → s a b)
    (h : Directed r f) : Directed s f := fun a b =>
  let ⟨c, h₁, h₂⟩ := h a b
  ⟨c, H _ _ h₁, H _ _ h₂⟩

Preservation of Directedness under Weaker Relation

Informal description

Let $r$ and $s$ be relations on a type $\alpha$, and let $f : \iota \to \alpha$ be an indexed family. If $r$ implies $s$ (i.e., $r(a,b) \to s(a,b)$ for all $a,b \in \alpha$) and $f$ is $r$-directed, then $f$ is also $s$-directed.

Directed.mono_comp theorem

 (r : α → α → Prop) {ι} {rb : β → β → Prop} {g : α → β} {f : ι → α} (hg : ∀ ⦃x y⦄, r x y → rb (g x) (g y))
  (hf : Directed r f) : Directed rb (g ∘ f)

Full source

theorem Directed.mono_comp (r : α → α → Prop) {ι} {rb : β → β → Prop} {g : α → β} {f : ι → α}
    (hg : ∀ ⦃x y⦄, r x y → rb (g x) (g y)) (hf : Directed r f) : Directed rb (g ∘ f) :=
  directed_comp.2 <| hf.mono hg

Preservation of Directedness under Relation-Preserving Function Composition

Informal description

Let $r$ be a relation on $\alpha$ and $rb$ a relation on $\beta$. Given a function $g : \alpha \to \beta$ that preserves the relations (i.e., $r(x,y) \to rb(g(x), g(y))$ for all $x,y \in \alpha$) and an $r$-directed family $f : \iota \to \alpha$, then the composition $g \circ f$ is $rb$-directed.

DirectedOn.mono_comp theorem

 {r : α → α → Prop} {rb : β → β → Prop} {g : α → β} {s : Set α} (hg : ∀ ⦃x y⦄, r x y → rb (g x) (g y))
  (hf : DirectedOn r s) : DirectedOn rb (g '' s)

Full source

theorem DirectedOn.mono_comp {r : α → α → Prop} {rb : β → β → Prop} {g : α → β} {s : Set α}
    (hg : ∀ ⦃x y⦄, r x y → rb (g x) (g y)) (hf : DirectedOn r s) : DirectedOn rb (g '' s) :=
  directedOn_image.mpr (hf.mono hg)

Preservation of Directedness Under Relation-Preserving Image

Informal description

Let $r$ be a relation on a type $\alpha$ and $rb$ a relation on a type $\beta$. Given a function $g : \alpha \to \beta$ that preserves the relations (i.e., $r(x,y) \to rb(g(x), g(y))$ for all $x,y \in \alpha$) and a subset $s \subseteq \alpha$ that is $r$-directed, then the image $g(s)$ is $rb$-directed.

directedOn_of_sup_mem theorem

[SemilatticeSup α] {S : Set α} (H : ∀ ⦃i j⦄, i ∈ S → j ∈ S → i ⊔ j ∈ S) : DirectedOn (· ≤ ·) S

Full source

/-- A set stable by supremum is `≤`-directed. -/
theorem directedOn_of_sup_mem [SemilatticeSup α] {S : Set α}
    (H : ∀ ⦃i j⦄, i ∈ S → j ∈ S → i ⊔ ji ⊔ j ∈ S) : DirectedOn (· ≤ ·) S := fun a ha b hb =>
  ⟨a ⊔ b, H ha hb, le_sup_left, le_sup_right⟩

Supremum-Closed Sets are Directed

Informal description

Let $\alpha$ be a join-semilattice and $S$ a subset of $\alpha$. If for any two elements $i, j \in S$ their supremum $i \sqcup j$ also belongs to $S$, then $S$ is directed with respect to the order relation $\leq$.

Directed.extend_bot theorem

 [Preorder α] [OrderBot α] {e : ι → β} {f : ι → α} (hf : Directed (· ≤ ·) f) (he : Function.Injective e) :
  Directed (· ≤ ·) (Function.extend e f ⊥)

Full source

theorem Directed.extend_bot [Preorder α] [OrderBot α] {e : ι → β} {f : ι → α}
    (hf : Directed (· ≤ ·) f) (he : Function.Injective e) :
    Directed (· ≤ ·) (Function.extend e f ⊥) := by
  intro a b
  rcases (em (∃ i, e i = a)).symm with (ha | ⟨i, rfl⟩)
  · use b
    simp [Function.extend_apply' _ _ _ ha]
  rcases (em (∃ i, e i = b)).symm with (hb | ⟨j, rfl⟩)
  · use e i
    simp [Function.extend_apply' _ _ _ hb]
  rcases hf i j with ⟨k, hi, hj⟩
  use e k
  simp only [he.extend_apply, *, true_and]

Directedness of Extended Function with Bottom Default

Informal description

Let $\alpha$ be a preorder with a bottom element $\bot$, and let $\beta$ be another type. Given an injective function $e : \iota \to \beta$ and a directed family $f : \iota \to \alpha$ with respect to the order $\leq$, the extended function $\text{extend}\,e\,f\,\bot : \beta \to \alpha$ is also directed with respect to $\leq$. Here, $\text{extend}\,e\,f\,\bot$ is defined to be $f$ on the range of $e$ and $\bot$ elsewhere.

directedOn_of_inf_mem theorem

[SemilatticeInf α] {S : Set α} (H : ∀ ⦃i j⦄, i ∈ S → j ∈ S → i ⊓ j ∈ S) : DirectedOn (· ≥ ·) S

Full source

/-- A set stable by infimum is `≥`-directed. -/
theorem directedOn_of_inf_mem [SemilatticeInf α] {S : Set α}
    (H : ∀ ⦃i j⦄, i ∈ S → j ∈ S → i ⊓ ji ⊓ j ∈ S) : DirectedOn (· ≥ ·) S :=
  directedOn_of_sup_mem (α := αᵒᵈ) H

Infimum-Closed Sets are Directed with Respect to Reverse Order

Informal description

Let $\alpha$ be a meet-semilattice and $S$ a subset of $\alpha$. If for any two elements $i, j \in S$ their infimum $i \sqcap j$ also belongs to $S$, then $S$ is directed with respect to the reverse order relation $\geq$.

IsTotal.directed theorem

[IsTotal α r] (f : ι → α) : Directed r f

Full source

theorem IsTotal.directed [IsTotal α r] (f : ι → α) : Directed r f := fun i j =>
  Or.casesOn (total_of r (f i) (f j)) (fun h => ⟨j, h, refl _⟩) fun h => ⟨i, refl _, h⟩

Total Relation Implies Directed Family

Informal description

For any type $\alpha$ with a total relation $r$ and any indexed family $f : \iota \to \alpha$, the family $f$ is $r$-directed. That is, for any two elements $f(i)$ and $f(j)$ in the family, there exists an element $f(k)$ such that both $r(f(i), f(k))$ and $r(f(j), f(k))$ hold.

IsDirected structure

(α : Type*) (r : α → α → Prop)

Full source

/-- `IsDirected α r` states that for any elements `a`, `b` there exists an element `c` such that
`r a c` and `r b c`. -/
class IsDirected (α : Type*) (r : α → α → Prop) : Prop where
  /-- For every pair of elements `a` and `b` there is a `c` such that `r a c` and `r b c` -/
  directed (a b : α) : ∃ c, r a c ∧ r b c

Directedness with respect to a relation

Informal description

The structure `IsDirected α r` states that for any two elements $a, b$ in a type $\alpha$ with a relation $r$, there exists an element $c$ such that both $r(a, c)$ and $r(b, c)$ hold. In other words, every pair of elements in $\alpha$ has a common upper bound with respect to the relation $r$.

directed_of theorem

(r : α → α → Prop) [IsDirected α r] (a b : α) : ∃ c, r a c ∧ r b c

Full source

theorem directed_of (r : α → α → Prop) [IsDirected α r] (a b : α) : ∃ c, r a c ∧ r b c :=
  IsDirected.directed _ _

Existence of Common Upper Bound in Directed Relations

Informal description

For any type $\alpha$ with a directed relation $r$ (i.e., `IsDirected α r`), and for any two elements $a, b \in \alpha$, there exists an element $c \in \alpha$ such that $r(a, c)$ and $r(b, c)$ both hold.

directed_of₃ theorem

(r : α → α → Prop) [IsDirected α r] [IsTrans α r] (a b c : α) : ∃ d, r a d ∧ r b d ∧ r c d

Full source

theorem directed_of₃ (r : α → α → Prop) [IsDirected α r] [IsTrans α r] (a b c : α) :
    ∃ d, r a d ∧ r b d ∧ r c d :=
  have ⟨e, hae, hbe⟩ := directed_of r a b
  have ⟨f, hef, hcf⟩ := directed_of r e c
  ⟨f, Trans.trans hae hef, Trans.trans hbe hef, hcf⟩

Existence of Common Upper Bound for Three Elements in Directed Relations

Informal description

For any type $\alpha$ with a directed relation $r$ (i.e., `IsDirected α r`) that is also transitive, and for any three elements $a, b, c \in \alpha$, there exists an element $d \in \alpha$ such that $r(a, d)$, $r(b, d)$, and $r(c, d)$ all hold.

directed_id theorem

[IsDirected α r] : Directed r id

Full source

theorem directed_id [IsDirected α r] : Directed r id := directed_of r

Identity Function is Directed under a Directed Relation

Informal description

For any type $\alpha$ with a directed relation $r$ (i.e., `IsDirected α r`), the identity function $\mathrm{id} : \alpha \to \alpha$ is $r$-directed. That is, for any two elements $a, b \in \alpha$, there exists an element $c \in \alpha$ such that $a \preccurlyeq c$ and $b \preccurlyeq c$ under the relation $r$.

directed_id_iff theorem

: Directed r id ↔ IsDirected α r

Full source

theorem directed_id_iff : DirectedDirected r id ↔ IsDirected α r :=
  ⟨fun h => ⟨h⟩, @directed_id _ _⟩

Identity Function Directed iff Type is Directed

Informal description

For any relation $r$ on a type $\alpha$, the identity function $\mathrm{id} : \alpha \to \alpha$ is $r$-directed if and only if $\alpha$ is $r$-directed (i.e., every pair of elements in $\alpha$ has a common upper bound with respect to $r$).

directedOn_univ theorem

[IsDirected α r] : DirectedOn r Set.univ

Full source

theorem directedOn_univ [IsDirected α r] : DirectedOn r Set.univ := fun a _ b _ =>
  let ⟨c, hc⟩ := directed_of r a b
  ⟨c, trivial, hc⟩

Universal Set is Directed under a Directed Relation

Informal description

For any type $\alpha$ with a directed relation $r$ (i.e., `IsDirected α r`), the universal set $\text{univ} = \alpha$ is directed with respect to $r$. This means that for any two elements $a, b \in \alpha$, there exists an element $c \in \alpha$ such that $r(a, c)$ and $r(b, c)$ both hold.

directedOn_univ_iff theorem

: DirectedOn r Set.univ ↔ IsDirected α r

Full source

theorem directedOn_univ_iff : DirectedOnDirectedOn r Set.univ ↔ IsDirected α r :=
  ⟨fun h =>
    ⟨fun a b =>
      let ⟨c, _, hc⟩ := h a trivial b trivial
      ⟨c, hc⟩⟩,
    @directedOn_univ _ _⟩

Universal Set Directed iff Type is Directed

Informal description

For any relation $r$ on a type $\alpha$, the universal set $\text{univ} = \alpha$ is directed with respect to $r$ if and only if $\alpha$ is $r$-directed (i.e., every pair of elements in $\alpha$ has a common upper bound with respect to $r$).

IsTotal.to_isDirected instance

[IsTotal α r] : IsDirected α r

Full source

instance (priority := 100) IsTotal.to_isDirected [IsTotal α r] : IsDirected α r :=
  directed_id_iff.1 <| IsTotal.directed _

Total Relations are Directed

Informal description

For any type $\alpha$ with a total relation $r$, $\alpha$ is $r$-directed. That is, every pair of elements in $\alpha$ has a common upper bound with respect to $r$.

isDirected_mono theorem

[IsDirected α r] (h : ∀ ⦃a b⦄, r a b → s a b) : IsDirected α s

Full source

theorem isDirected_mono [IsDirected α r] (h : ∀ ⦃a b⦄, r a b → s a b) : IsDirected α s :=
  ⟨fun a b =>
    let ⟨c, ha, hb⟩ := IsDirected.directed a b
    ⟨c, h ha, h hb⟩⟩

Monotonicity of Directedness: If $r \subseteq s$ and $\alpha$ is $r$-directed, then $\alpha$ is $s$-directed.

Informal description

Let $\alpha$ be a type with a relation $r$ such that $\alpha$ is $r$-directed. If $s$ is another relation on $\alpha$ such that $r(a, b)$ implies $s(a, b)$ for all $a, b \in \alpha$, then $\alpha$ is also $s$-directed.

exists_ge_ge theorem

[LE α] [IsDirected α (· ≤ ·)] (a b : α) : ∃ c, a ≤ c ∧ b ≤ c

Full source

theorem exists_ge_ge [LE α] [IsDirected α (· ≤ ·)] (a b : α) : ∃ c, a ≤ c ∧ b ≤ c :=
  directed_of (· ≤ ·) a b

Existence of Common Upper Bound in Directed Preorders

Informal description

For any type $\alpha$ with a preorder $\leq$ such that $\alpha$ is directed (i.e., every pair of elements has a common upper bound), and for any two elements $a, b \in \alpha$, there exists an element $c \in \alpha$ such that $a \leq c$ and $b \leq c$.

exists_le_le theorem

[LE α] [IsDirected α (· ≥ ·)] (a b : α) : ∃ c, c ≤ a ∧ c ≤ b

Full source

theorem exists_le_le [LE α] [IsDirected α (· ≥ ·)] (a b : α) : ∃ c, c ≤ a ∧ c ≤ b :=
  directed_of (· ≥ ·) a b

Existence of Common Lower Bound in Directed Preorders

Informal description

For any type $\alpha$ with a preorder $\leq$ such that $\alpha$ is directed with respect to the relation $\geq$ (i.e., every pair of elements has a common lower bound), and for any two elements $a, b \in \alpha$, there exists an element $c \in \alpha$ such that $c \leq a$ and $c \leq b$.

OrderDual.isDirected_ge instance

[LE α] [IsDirected α (· ≤ ·)] : IsDirected αᵒᵈ (· ≥ ·)

Full source

instance OrderDual.isDirected_ge [LE α] [IsDirected α (· ≤ ·)] : IsDirected αᵒᵈ (· ≥ ·) := by
  assumption

Directedness of the Dual Order

Informal description

For any type $\alpha$ with a preorder $\leq$ that is directed (i.e., every pair of elements has a common upper bound), the dual order $\geq$ on $\alpha$ is also directed (i.e., every pair of elements has a common lower bound).

OrderDual.isDirected_le instance

[LE α] [IsDirected α (· ≥ ·)] : IsDirected αᵒᵈ (· ≤ ·)

Full source

instance OrderDual.isDirected_le [LE α] [IsDirected α (· ≥ ·)] : IsDirected αᵒᵈ (· ≤ ·) := by
  assumption

Directedness of Order Dual with Respect to $\leq$

Informal description

For any type $\alpha$ with a preorder $\leq$, if $\alpha$ is directed with respect to the relation $\geq$ (i.e., every pair of elements has a common lower bound), then the order dual $\alpha^{\text{op}}$ is directed with respect to the relation $\leq$.

directed_of_isDirected_le theorem

 [LE α] [IsDirected α (· ≤ ·)] {f : α → β} {r : β → β → Prop} (H : ∀ ⦃i j⦄, i ≤ j → r (f i) (f j)) : Directed r f

Full source

/-- A monotone function on an upwards-directed type is directed. -/
theorem directed_of_isDirected_le [LE α] [IsDirected α (· ≤ ·)] {f : α → β} {r : β → β → Prop}
    (H : ∀ ⦃i j⦄, i ≤ j → r (f i) (f j)) : Directed r f :=
  directed_id.mono_comp _ H

Monotone Functions on Directed Preorders are Directed

Informal description

Let $\alpha$ be a type with a preorder $\leq$ such that $\alpha$ is directed (i.e., any two elements have a common upper bound). Given a function $f : \alpha \to \beta$ and a relation $r$ on $\beta$, if $f$ is monotone with respect to $\leq$ and $r$ (i.e., $i \leq j$ implies $r(f(i), f(j))$ for all $i,j \in \alpha$), then the family $f$ is $r$-directed.

Monotone.directed_le theorem

[Preorder α] [IsDirected α (· ≤ ·)] [Preorder β] {f : α → β} : Monotone f → Directed (· ≤ ·) f

Full source

theorem Monotone.directed_le [Preorder α] [IsDirected α (· ≤ ·)] [Preorder β] {f : α → β} :
    Monotone f → Directed (· ≤ ·) f :=
  directed_of_isDirected_le

Monotone Functions Preserve Directedness with Respect to $\leq$

Informal description

Let $\alpha$ and $\beta$ be preorders, with $\alpha$ being directed with respect to $\leq$. For any monotone function $f : \alpha \to \beta$, the family $f$ is directed with respect to $\leq$ in $\beta$.

Antitone.directed_ge theorem

[Preorder α] [IsDirected α (· ≤ ·)] [Preorder β] {f : α → β} (hf : Antitone f) : Directed (· ≥ ·) f

Full source

theorem Antitone.directed_ge [Preorder α] [IsDirected α (· ≤ ·)] [Preorder β] {f : α → β}
    (hf : Antitone f) : Directed (· ≥ ·) f :=
  directed_of_isDirected_le hf

Antitone Functions on Directed Preorders are Directed with Respect to $\geq$

Informal description

Let $\alpha$ and $\beta$ be preorders, with $\alpha$ being directed with respect to $\leq$. For any antitone function $f : \alpha \to \beta$ (i.e., $x \leq y$ implies $f(y) \leq f(x)$ for all $x, y \in \alpha$), the family $f$ is directed with respect to $\geq$ in $\beta$. That is, for any two elements $f(x), f(y)$ in the image of $f$, there exists an element $f(z)$ such that $f(z) \geq f(x)$ and $f(z) \geq f(y)$.

directed_of_isDirected_ge theorem

 [LE α] [IsDirected α (· ≥ ·)] {r : β → β → Prop} {f : α → β} (hf : ∀ a₁ a₂, a₁ ≤ a₂ → r (f a₂) (f a₁)) : Directed r f

Full source

/-- An antitone function on a downwards-directed type is directed. -/
theorem directed_of_isDirected_ge [LE α] [IsDirected α (· ≥ ·)] {r : β → β → Prop} {f : α → β}
    (hf : ∀ a₁ a₂, a₁ ≤ a₂ → r (f a₂) (f a₁)) : Directed r f :=
  directed_of_isDirected_le (α := αᵒᵈ) fun _ _ ↦ hf _ _

Antitone Functions on Downwards-Directed Preorders are Directed

Informal description

Let $\alpha$ be a type with a preorder $\leq$ such that $\alpha$ is directed with respect to $\geq$ (i.e., any two elements have a common lower bound). Given a function $f : \alpha \to \beta$ and a relation $r$ on $\beta$, if $f$ is antitone with respect to $\leq$ and $r$ (i.e., $a_1 \leq a_2$ implies $r(f(a_2), f(a_1))$ for all $a_1, a_2 \in \alpha$), then the family $f$ is $r$-directed.

Monotone.directed_ge theorem

[Preorder α] [IsDirected α (· ≥ ·)] [Preorder β] {f : α → β} (hf : Monotone f) : Directed (· ≥ ·) f

Full source

theorem Monotone.directed_ge [Preorder α] [IsDirected α (· ≥ ·)] [Preorder β] {f : α → β}
    (hf : Monotone f) : Directed (· ≥ ·) f :=
  directed_of_isDirected_ge hf

Monotone Functions on Downwards-Directed Preorders are Directed with Respect to $\geq$

Informal description

Let $\alpha$ and $\beta$ be preorders, with $\alpha$ being directed with respect to $\geq$ (i.e., any two elements have a common lower bound). For any monotone function $f : \alpha \to \beta$ (i.e., $x \leq y$ implies $f(x) \leq f(y)$ for all $x, y \in \alpha$), the family $f$ is directed with respect to $\geq$ in $\beta$. That is, for any two elements $f(x), f(y)$ in the image of $f$, there exists an element $f(z)$ such that $f(z) \geq f(x)$ and $f(z) \geq f(y)$.

Antitone.directed_le theorem

[Preorder α] [IsDirected α (· ≥ ·)] [Preorder β] {f : α → β} (hf : Antitone f) : Directed (· ≤ ·) f

Full source

theorem Antitone.directed_le [Preorder α] [IsDirected α (· ≥ ·)] [Preorder β] {f : α → β}
    (hf : Antitone f) : Directed (· ≤ ·) f :=
  directed_of_isDirected_ge hf

Antitone Functions on Downwards-Directed Preorders are Directed with Respect to $\leq$

Informal description

Let $\alpha$ and $\beta$ be preorders, with $\alpha$ being directed with respect to $\geq$ (i.e., any two elements have a common lower bound). If $f : \alpha \to \beta$ is an antitone function (i.e., $a_1 \leq a_2$ implies $f(a_2) \leq f(a_1)$ for all $a_1, a_2 \in \alpha$), then the family $f$ is directed with respect to $\leq$ in $\beta$.

DirectedOn.insert theorem

 (h : Reflexive r) (a : α) {s : Set α} (hd : DirectedOn r s) (ha : ∀ b ∈ s, ∃ c ∈ s, a ≼ c ∧ b ≼ c) :
  DirectedOn r (insert a s)

Full source

protected theorem DirectedOn.insert (h : Reflexive r) (a : α) {s : Set α} (hd : DirectedOn r s)
    (ha : ∀ b ∈ s, ∃ c ∈ s, a ≼ c ∧ b ≼ c) : DirectedOn r (insert a s) := by
  rintro x (rfl | hx) y (rfl | hy)
  · exact ⟨y, Set.mem_insert _ _, h _, h _⟩
  · obtain ⟨w, hws, hwr⟩ := ha y hy
    exact ⟨w, Set.mem_insert_of_mem _ hws, hwr⟩
  · obtain ⟨w, hws, hwr⟩ := ha x hx
    exact ⟨w, Set.mem_insert_of_mem _ hws, hwr.symm⟩
  · obtain ⟨w, hws, hwr⟩ := hd x hx y hy
    exact ⟨w, Set.mem_insert_of_mem _ hws, hwr⟩

Directedness is Preserved by Insertion of a Common Upper Bound

Informal description

Let $\preccurlyeq$ be a reflexive relation on a type $\alpha$, and let $s$ be a subset of $\alpha$ that is directed with respect to $\preccurlyeq$. Given an element $a \in \alpha$ such that for every $b \in s$ there exists $c \in s$ with $a \preccurlyeq c$ and $b \preccurlyeq c$, then the set $\{a\} \cup s$ is also directed with respect to $\preccurlyeq$.

directedOn_singleton theorem

(h : Reflexive r) (a : α) : DirectedOn r ({ a } : Set α)

Full source

theorem directedOn_singleton (h : Reflexive r) (a : α) : DirectedOn r ({a} : Set α) :=
  fun x hx _ hy => ⟨x, hx, h _, hx.symm ▸ hy.symm ▸ h _⟩

Singleton sets are directed under reflexive relations

Informal description

For any reflexive relation $\preccurlyeq$ on a type $\alpha$ and any element $a \in \alpha$, the singleton set $\{a\}$ is directed with respect to $\preccurlyeq$.

directedOn_pair theorem

(h : Reflexive r) {a b : α} (hab : a ≼ b) : DirectedOn r ({ a, b } : Set α)

Full source

theorem directedOn_pair (h : Reflexive r) {a b : α} (hab : a ≼ b) : DirectedOn r ({a, b} : Set α) :=
  (directedOn_singleton h _).insert h _ fun c hc => ⟨c, hc, hc.symm ▸ hab, h _⟩

Pair of Elements with Upper Bound Forms Directed Set

Informal description

For any reflexive relation $\preccurlyeq$ on a type $\alpha$ and any two elements $a, b \in \alpha$ such that $a \preccurlyeq b$, the set $\{a, b\}$ is directed with respect to $\preccurlyeq$.

directedOn_pair' theorem

(h : Reflexive r) {a b : α} (hab : a ≼ b) : DirectedOn r ({ b, a } : Set α)

Full source

theorem directedOn_pair' (h : Reflexive r) {a b : α} (hab : a ≼ b) :
    DirectedOn r ({b, a} : Set α) := by
  rw [Set.pair_comm]
  apply directedOn_pair h hab

Directedness of Reversed Pair Under Reflexive Relation

Informal description

For any reflexive relation $\preccurlyeq$ on a type $\alpha$ and any two elements $a, b \in \alpha$ such that $a \preccurlyeq b$, the set $\{b, a\}$ is directed with respect to $\preccurlyeq$.

IsMin.isBot theorem

[IsDirected α (· ≥ ·)] (h : IsMin a) : IsBot a

Full source

protected theorem IsMin.isBot [IsDirected α (· ≥ ·)] (h : IsMin a) : IsBot a := fun b =>
  let ⟨_, hca, hcb⟩ := exists_le_le a b
  (h hca).trans hcb

Minimal Element in Downward-Directed Preorder is Bottom Element

Informal description

Let $\alpha$ be a type with a preorder $\leq$ such that $\alpha$ is directed with respect to the relation $\geq$ (i.e., every pair of elements has a common lower bound). If an element $a \in \alpha$ is minimal (i.e., for any $b \in \alpha$, $b \leq a$ implies $a \leq b$), then $a$ is a bottom element (i.e., $a \leq b$ for all $b \in \alpha$).

IsMax.isTop theorem

[IsDirected α (· ≤ ·)] (h : IsMax a) : IsTop a

Full source

protected theorem IsMax.isTop [IsDirected α (· ≤ ·)] (h : IsMax a) : IsTop a :=
  h.toDual.isBot

Maximal Element in Directed Preorder is Top Element

Informal description

Let $\alpha$ be a type with a preorder $\leq$ such that $\alpha$ is directed (i.e., every pair of elements has a common upper bound). If an element $a \in \alpha$ is maximal (i.e., for any $b \in \alpha$, $a \leq b$ implies $b \leq a$), then $a$ is a top element (i.e., $b \leq a$ for all $b \in \alpha$).

DirectedOn.is_bot_of_is_min theorem

 {s : Set α} (hd : DirectedOn (· ≥ ·) s) {m} (hm : m ∈ s) (hmin : ∀ a ∈ s, a ≤ m → m ≤ a) : ∀ a ∈ s, m ≤ a

Full source

lemma DirectedOn.is_bot_of_is_min {s : Set α} (hd : DirectedOn (· ≥ ·) s)
    {m} (hm : m ∈ s) (hmin : ∀ a ∈ s, a ≤ m → m ≤ a) : ∀ a ∈ s, m ≤ a := fun a as =>
  let ⟨x, xs, xm, xa⟩ := hd m hm a as
  (hmin x xs xm).trans xa

Minimal Element in Downward-Directed Set is Bottom Element

Informal description

Let $s$ be a subset of a type $\alpha$ that is directed with respect to the relation $\geq$ (i.e., for any $x, y \in s$, there exists $z \in s$ such that $z \leq x$ and $z \leq y$). If $m \in s$ is a minimal element (i.e., for any $a \in s$, $a \leq m$ implies $m \leq a$), then $m$ is a bottom element of $s$ (i.e., $m \leq a$ for all $a \in s$).

DirectedOn.is_top_of_is_max theorem

 {s : Set α} (hd : DirectedOn (· ≤ ·) s) {m} (hm : m ∈ s) (hmax : ∀ a ∈ s, m ≤ a → a ≤ m) : ∀ a ∈ s, a ≤ m

Full source

lemma DirectedOn.is_top_of_is_max {s : Set α} (hd : DirectedOn (· ≤ ·) s)
    {m} (hm : m ∈ s) (hmax : ∀ a ∈ s, m ≤ a → a ≤ m) : ∀ a ∈ s, a ≤ m :=
  @DirectedOn.is_bot_of_is_min αᵒᵈ _ s hd m hm hmax

Maximal Element in Upward-Directed Set is Top Element

Informal description

Let $s$ be a subset of a type $\alpha$ that is directed with respect to the relation $\leq$ (i.e., for any $x, y \in s$, there exists $z \in s$ such that $x \leq z$ and $y \leq z$). If $m \in s$ is a maximal element (i.e., for any $a \in s$, $m \leq a$ implies $a \leq m$), then $m$ is a top element of $s$ (i.e., $a \leq m$ for all $a \in s$).

isTop_or_exists_gt theorem

[IsDirected α (· ≤ ·)] (a : α) : IsTop a ∨ ∃ b, a < b

Full source

theorem isTop_or_exists_gt [IsDirected α (· ≤ ·)] (a : α) : IsTopIsTop a ∨ ∃ b, a < b :=
  (em (IsMax a)).imp IsMax.isTop not_isMax_iff.mp

Top Element or Strictly Greater Element in Directed Preorder

Informal description

Let $\alpha$ be a type with a preorder $\leq$ such that $\alpha$ is directed with respect to $\leq$ (i.e., every pair of elements has a common upper bound). Then for any element $a \in \alpha$, either $a$ is a top element (i.e., $b \leq a$ for all $b \in \alpha$) or there exists an element $b \in \alpha$ such that $a < b$.

isBot_or_exists_lt theorem

[IsDirected α (· ≥ ·)] (a : α) : IsBot a ∨ ∃ b, b < a

Full source

theorem isBot_or_exists_lt [IsDirected α (· ≥ ·)] (a : α) : IsBotIsBot a ∨ ∃ b, b < a :=
  @isTop_or_exists_gt αᵒᵈ _ _ a

Bottom Element or Strictly Lesser Element in Downward-Directed Preorder

Informal description

Let $\alpha$ be a type with a preorder $\leq$ such that $\alpha$ is directed with respect to $\geq$ (i.e., every pair of elements has a common lower bound). Then for any element $a \in \alpha$, either $a$ is a bottom element (i.e., $a \leq b$ for all $b \in \alpha$) or there exists an element $b \in \alpha$ such that $b < a$.

isBot_iff_isMin theorem

[IsDirected α (· ≥ ·)] : IsBot a ↔ IsMin a

Full source

theorem isBot_iff_isMin [IsDirected α (· ≥ ·)] : IsBotIsBot a ↔ IsMin a :=
  ⟨IsBot.isMin, IsMin.isBot⟩

Characterization of Bottom Elements as Minimal Elements in Downward-Directed Preorders

Informal description

Let $\alpha$ be a type with a preorder $\leq$ such that $\alpha$ is directed with respect to the relation $\geq$ (i.e., every pair of elements has a common lower bound). Then for any element $a \in \alpha$, $a$ is a bottom element (i.e., $a \leq b$ for all $b \in \alpha$) if and only if $a$ is minimal (i.e., for any $b \in \alpha$, $b \leq a$ implies $a \leq b$).

isTop_iff_isMax theorem

[IsDirected α (· ≤ ·)] : IsTop a ↔ IsMax a

Full source

theorem isTop_iff_isMax [IsDirected α (· ≤ ·)] : IsTopIsTop a ↔ IsMax a :=
  ⟨IsTop.isMax, IsMax.isTop⟩

Characterization of Top Elements as Maximal Elements in Directed Preorders

Informal description

Let $\alpha$ be a type with a preorder $\leq$ such that $\alpha$ is directed with respect to $\leq$ (i.e., every pair of elements has a common upper bound). Then for any element $a \in \alpha$, $a$ is a top element (i.e., $b \leq a$ for all $b \in \alpha$) if and only if $a$ is maximal (i.e., for any $b \in \alpha$, $a \leq b$ implies $b \leq a$).

exists_lt_of_directed_ge theorem

[IsDirected β (· ≥ ·)] : ∃ a b : β, a < b

Full source

theorem exists_lt_of_directed_ge [IsDirected β (· ≥ ·)] :
    ∃ a b : β, a < b := by
  rcases exists_pair_ne β with ⟨a, b, hne⟩
  rcases isBot_or_exists_lt a with (ha | ⟨c, hc⟩)
  exacts [⟨a, b, (ha b).lt_of_ne hne⟩, ⟨_, _, hc⟩]

Existence of Strictly Ordered Pair in Downward-Directed Preorder

Informal description

For any type $\beta$ with a preorder $\leq$ such that $\beta$ is directed with respect to $\geq$ (i.e., every pair of elements has a common lower bound), there exist two elements $a, b \in \beta$ with $a < b$.

exists_lt_of_directed_le theorem

[IsDirected β (· ≤ ·)] : ∃ a b : β, a < b

Full source

theorem exists_lt_of_directed_le [IsDirected β (· ≤ ·)] :
    ∃ a b : β, a < b :=
  let ⟨a, b, h⟩ := exists_lt_of_directed_ge βᵒᵈ
  ⟨b, a, h⟩

Existence of Strictly Ordered Pair in Directed Preorder

Informal description

For any type $\beta$ with a preorder $\leq$ such that $\beta$ is directed with respect to $\leq$ (i.e., every pair of elements has a common upper bound), there exist two elements $a, b \in \beta$ with $a < b$.

IsMin.not_isMax theorem

[IsDirected β (· ≥ ·)] {b : β} (hb : IsMin b) : ¬IsMax b

Full source

protected theorem IsMin.not_isMax [IsDirected β (· ≥ ·)] {b : β} (hb : IsMin b) : ¬ IsMax b := by
  intro hb'
  obtain ⟨a, c, hac⟩ := exists_lt_of_directed_ge β
  have := hb.isBot a
  obtain rfl := (hb' <| this).antisymm this
  exact hb'.not_lt hac

Minimal Elements Cannot Be Maximal in Downward-Directed Preorders

Informal description

Let $\beta$ be a type with a preorder $\leq$ such that $\beta$ is directed with respect to $\geq$ (i.e., every pair of elements has a common lower bound). If an element $b \in \beta$ is minimal, then $b$ cannot be maximal.

IsMin.not_isMax' theorem

[IsDirected β (· ≤ ·)] {b : β} (hb : IsMin b) : ¬IsMax b

Full source

protected theorem IsMin.not_isMax' [IsDirected β (· ≤ ·)] {b : β} (hb : IsMin b) : ¬ IsMax b :=
  fun hb' ↦ hb'.toDual.not_isMax hb.toDual

Minimal Elements Cannot Be Maximal in Directed Preorders

Informal description

Let $\beta$ be a type with a preorder $\leq$ such that $\beta$ is directed with respect to $\leq$ (i.e., every pair of elements has a common upper bound). If an element $b \in \beta$ is minimal, then $b$ cannot be maximal.

IsMax.not_isMin theorem

[IsDirected β (· ≤ ·)] {b : β} (hb : IsMax b) : ¬IsMin b

Full source

protected theorem IsMax.not_isMin [IsDirected β (· ≤ ·)] {b : β} (hb : IsMax b) : ¬ IsMin b :=
  fun hb' ↦ hb.toDual.not_isMax hb'.toDual

Maximal Elements Cannot Be Minimal in Directed Preorders

Informal description

Let $\beta$ be a type with a preorder $\leq$ such that $\beta$ is directed (i.e., every pair of elements has a common upper bound). If an element $b \in \beta$ is maximal, then $b$ cannot be minimal.

IsMax.not_isMin' theorem

[IsDirected β (· ≥ ·)] {b : β} (hb : IsMax b) : ¬IsMin b

Full source

protected theorem IsMax.not_isMin' [IsDirected β (· ≥ ·)] {b : β} (hb : IsMax b) : ¬ IsMin b :=
  fun hb' ↦ hb'.toDual.not_isMin hb.toDual

Maximal Elements Cannot Be Minimal in Downward-Directed Preorders

Informal description

Let $\beta$ be a type with a preorder $\leq$ such that $\beta$ is directed with respect to the relation $\geq$ (i.e., every pair of elements has a common lower bound). If an element $b \in \beta$ is maximal, then $b$ cannot be minimal.

constant_of_monotone_antitone theorem

[IsDirected α (· ≤ ·)] (hf : Monotone f) (hf' : Antitone f) (a b : α) : f a = f b

Full source

/-- If `f` is monotone and antitone on a directed order, then `f` is constant. -/
lemma constant_of_monotone_antitone [IsDirected α (· ≤ ·)] (hf : Monotone f) (hf' : Antitone f)
    (a b : α) : f a = f b := by
  obtain ⟨c, hac, hbc⟩ := exists_ge_ge a b
  exact le_antisymm ((hf hac).trans <| hf' hbc) ((hf hbc).trans <| hf' hac)

Function is Constant if Both Monotone and Antitone on a Directed Order

Informal description

Let $\alpha$ be a type with a directed preorder $\leq$ (i.e., any two elements have a common upper bound). If a function $f : \alpha \to \beta$ is both monotone (order-preserving) and antitone (order-reversing), then $f$ is constant. That is, for any $a, b \in \alpha$, we have $f(a) = f(b)$.

constant_of_monotoneOn_antitoneOn theorem

 (hf : MonotoneOn f s) (hf' : AntitoneOn f s) (hs : DirectedOn (· ≤ ·) s) : ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → f a = f b

Full source

/-- If `f` is monotone and antitone on a directed set `s`, then `f` is constant on `s`. -/
lemma constant_of_monotoneOn_antitoneOn (hf : MonotoneOn f s) (hf' : AntitoneOn f s)
    (hs : DirectedOn (· ≤ ·) s) : ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → f a = f b := by
  rintro a ha b hb
  obtain ⟨c, hc, hac, hbc⟩ := hs _ ha _ hb
  exact le_antisymm ((hf ha hc hac).trans <| hf' hb hc hbc) ((hf hb hc hbc).trans <| hf' ha hc hac)

Function Constant on Directed Set when Monotone and Antitone

Informal description

Let $s$ be a subset of a type $\alpha$ that is directed with respect to the relation $\leq$ (i.e., for any two elements $x, y \in s$, there exists $z \in s$ such that $x \leq z$ and $y \leq z$). If a function $f$ is both monotone and antitone on $s$, then $f$ is constant on $s$. That is, for any $a, b \in s$, we have $f(a) = f(b)$.

SemilatticeSup.to_isDirected_le instance

[SemilatticeSup α] : IsDirected α (· ≤ ·)

Full source

instance (priority := 100) SemilatticeSup.to_isDirected_le [SemilatticeSup α] :
    IsDirected α (· ≤ ·) :=
  ⟨fun a b => ⟨a ⊔ b, le_sup_left, le_sup_right⟩⟩

Join-Semilattices are Directed under $\leq$

Informal description

Every join-semilattice $\alpha$ is directed with respect to the relation $\leq$. That is, for any two elements $a, b \in \alpha$, there exists an element $c \in \alpha$ such that $a \leq c$ and $b \leq c$.

SemilatticeInf.to_isDirected_ge instance

[SemilatticeInf α] : IsDirected α (· ≥ ·)

Full source

instance (priority := 100) SemilatticeInf.to_isDirected_ge [SemilatticeInf α] :
    IsDirected α (· ≥ ·) :=
  ⟨fun a b => ⟨a ⊓ b, inf_le_left, inf_le_right⟩⟩

Meet-Semilattices are Directed under $\geq$

Informal description

Every meet-semilattice $\alpha$ is directed with respect to the relation $\geq$. That is, for any two elements $a, b \in \alpha$, there exists an element $c \in \alpha$ such that $a \geq c$ and $b \geq c$.

OrderTop.to_isDirected_le instance

[LE α] [OrderTop α] : IsDirected α (· ≤ ·)

Full source

instance (priority := 100) OrderTop.to_isDirected_le [LE α] [OrderTop α] : IsDirected α (· ≤ ·) :=
  ⟨fun _ _ => ⟨⊤, le_top _, le_top _⟩⟩

Directedness of Partial Orders with Top Element

Informal description

For any type $\alpha$ with a partial order and a greatest element $\top$, the relation $\leq$ is directed. That is, for any two elements $a, b \in \alpha$, there exists an element $c \in \alpha$ such that $a \leq c$ and $b \leq c$.

OrderBot.to_isDirected_ge instance

[LE α] [OrderBot α] : IsDirected α (· ≥ ·)

Full source

instance (priority := 100) OrderBot.to_isDirected_ge [LE α] [OrderBot α] : IsDirected α (· ≥ ·) :=
  ⟨fun _ _ => ⟨⊥, bot_le _, bot_le _⟩⟩

Directedness of Partial Orders with Bottom Element under $\geq$

Informal description

For any type $\alpha$ with a partial order and a least element $\bot$, the relation $\geq$ is directed. That is, for any two elements $a, b \in \alpha$, there exists an element $c \in \alpha$ such that $a \geq c$ and $b \geq c$.

DirectedOn.proj theorem

 {d : Set (Π i, α i)} (hd : DirectedOn (fun x y => ∀ i, r i (x i) (y i)) d) (i : ι) :
  DirectedOn (r i) ((fun a => a i) '' d)

Full source

lemma proj {d : Set (Π i, α i)} (hd : DirectedOn (fun x y => ∀ i, r i (x i) (y i)) d) (i : ι) :
    DirectedOn (r i) ((fun a => a i) '' d) :=
  DirectedOn.mono_comp (fun _ _ h => h) (mono hd fun ⦃_ _⦄ h ↦ h i)

Projection Preserves Directedness in Product Spaces

Informal description

Let $\{α_i\}_{i \in \iota}$ be a family of types, each equipped with a relation $r_i$. Given a subset $d \subseteq \prod_{i \in \iota} α_i$ that is directed with respect to the product relation (i.e., for any $x, y \in d$, there exists $z \in d$ such that $r_i(x_i, y_i) \to r_i(x_i, z_i)$ and $r_i(y_i, z_i)$ for all $i \in \iota$), then for any fixed index $i \in \iota$, the projection of $d$ onto the $i$-th coordinate is directed with respect to $r_i$.

DirectedOn.pi theorem

 {d : (i : ι) → Set (α i)} (hd : ∀ (i : ι), DirectedOn (r i) (d i)) :
  DirectedOn (fun x y => ∀ i, r i (x i) (y i)) (Set.pi Set.univ d)

Full source

lemma pi {d : (i : ι) → Set (α i)} (hd : ∀ (i : ι), DirectedOn (r i) (d i)) :
    DirectedOn (fun x y => ∀ i, r i (x i) (y i)) (Set.pi Set.univ d) := by
  intro a ha b hb
  choose f hfd haf hbf using fun i => hd i (a i) (ha i trivial) (b i) (hb i trivial)
  exact ⟨f, fun i _ => hfd i, haf, hbf⟩

Directedness of Product Sets

Informal description

Let $\{d_i\}_{i \in \iota}$ be a family of sets in types $\{\alpha_i\}_{i \in \iota}$, each directed with respect to a relation $r_i$ on $\alpha_i$. Then the product set $\prod_{i \in \iota} d_i$ is directed with respect to the relation defined by $(x, y) \mapsto \forall i, r_i(x_i, y_i)$.

DirectedOn.fst theorem

 {d : Set (α × β)} (hd : DirectedOn (fun p q ↦ p.1 ≼₁ q.1 ∧ p.2 ≼₂ q.2) d) : DirectedOn (· ≼₁ ·) (Prod.fst '' d)

Full source

lemma fst {d : Set (α × β)} (hd : DirectedOn (fun p q ↦ p.1 ≼₁ q.1 ∧ p.2 ≼₂ q.2) d) :
    DirectedOn (· ≼₁ ·) (Prod.fstProd.fst '' d) :=
  DirectedOn.mono_comp (fun ⦃_ _⦄ h ↦ h) (mono hd fun ⦃_ _⦄ h ↦ h.1)

Directedness of First Projection under Product Relation

Informal description

Let $d$ be a subset of the product type $\alpha \times \beta$ that is directed with respect to the product relation $(p, q) \mapsto (p.1 \preccurlyeq_1 q.1 \land p.2 \preccurlyeq_2 q.2)$. Then the projection of $d$ onto the first component, $\text{fst}(d)$, is directed with respect to the relation $\preccurlyeq_1$ on $\alpha$.

DirectedOn.snd theorem

 {d : Set (α × β)} (hd : DirectedOn (fun p q ↦ p.1 ≼₁ q.1 ∧ p.2 ≼₂ q.2) d) : DirectedOn (· ≼₂ ·) (Prod.snd '' d)

Full source

lemma snd {d : Set (α × β)} (hd : DirectedOn (fun p q ↦ p.1 ≼₁ q.1 ∧ p.2 ≼₂ q.2) d) :
    DirectedOn (· ≼₂ ·) (Prod.sndProd.snd '' d) :=
  DirectedOn.mono_comp (fun ⦃_ _⦄ h ↦ h) (mono hd fun ⦃_ _⦄ h ↦ h.2)

Directedness of Second Projection under Product Relation

Informal description

Let $d$ be a subset of the product type $\alpha \times \beta$ that is directed with respect to the product relation $(p, q) \mapsto (p_1 \preccurlyeq_1 q_1 \land p_2 \preccurlyeq_2 q_2)$. Then the projection of $d$ onto the second component, $\mathrm{snd}(d)$, is directed with respect to the relation $\preccurlyeq_2$ on $\beta$.

DirectedOn.prod theorem

 {d₁ : Set α} {d₂ : Set β} (h₁ : DirectedOn (· ≼₁ ·) d₁) (h₂ : DirectedOn (· ≼₂ ·) d₂) :
  DirectedOn (fun p q ↦ p.1 ≼₁ q.1 ∧ p.2 ≼₂ q.2) (d₁ ×ˢ d₂)

Full source

lemma prod {d₁ : Set α} {d₂ : Set β} (h₁ : DirectedOn (· ≼₁ ·) d₁) (h₂ : DirectedOn (· ≼₂ ·) d₂) :
    DirectedOn (fun p q ↦ p.1 ≼₁ q.1 ∧ p.2 ≼₂ q.2) (d₁ ×ˢ d₂) := fun _ hpd _ hqd => by
  obtain ⟨r₁, hdr₁, hpr₁, hqr₁⟩ := h₁ _ hpd.1 _ hqd.1
  obtain ⟨r₂, hdr₂, hpr₂, hqr₂⟩ := h₂ _ hpd.2 _ hqd.2
  exact ⟨⟨r₁, r₂⟩, ⟨hdr₁, hdr₂⟩, ⟨hpr₁, hpr₂⟩, ⟨hqr₁, hqr₂⟩⟩

Product of Directed Sets is Directed

Informal description

Let $d_1$ be a subset of a type $\alpha$ and $d_2$ a subset of a type $\beta$, both directed with respect to relations $\preccurlyeq_1$ and $\preccurlyeq_2$ respectively. Then the product set $d_1 \times d_2$ is directed with respect to the product relation defined by $(x_1, y_1) \preccurlyeq (x_2, y_2)$ if and only if $x_1 \preccurlyeq_1 x_2$ and $y_1 \preccurlyeq_2 y_2$.

Mathlib.Order.Directed

Main declarations

TODO

References