Mathlib.Order.UpperLower.Basic

isUpperSet_empty theorem

: IsUpperSet (∅ : Set α)

Full source

theorem isUpperSet_empty : IsUpperSet (∅ : Set α) := fun _ _ _ => id

Empty Set is an Upper Set

Informal description

The empty set is an upper set in any partially ordered set.

isLowerSet_empty theorem

: IsLowerSet (∅ : Set α)

Full source

theorem isLowerSet_empty : IsLowerSet (∅ : Set α) := fun _ _ _ => id

Empty Set is Lower Set

Informal description

The empty set $\emptyset$ is a lower set in any partially ordered set $\alpha$.

isUpperSet_univ theorem

: IsUpperSet (univ : Set α)

Full source

theorem isUpperSet_univ : IsUpperSet (univ : Set α) := fun _ _ _ => id

Universal Set is an Upper Set

Informal description

The universal set `univ` (the set containing all elements of type `α`) is an upper set. That is, for any elements `x` and `y` in `α`, if `x ≤ y` and `x ∈ univ`, then `y ∈ univ`.

isLowerSet_univ theorem

: IsLowerSet (univ : Set α)

Full source

theorem isLowerSet_univ : IsLowerSet (univ : Set α) := fun _ _ _ => id

Universal Set is a Lower Set

Informal description

The universal set `univ` (the set containing all elements of type `α`) is a lower set. That is, for any elements `x` and `y` in `α`, if `x ≤ y` and `y ∈ univ`, then `x ∈ univ`.

IsUpperSet.compl theorem

(hs : IsUpperSet s) : IsLowerSet sᶜ

Full source

theorem IsUpperSet.compl (hs : IsUpperSet s) : IsLowerSet sᶜ := fun _a _b h hb ha => hb <| hs h ha

Complement of an Upper Set is a Lower Set

Informal description

If a set $s$ is an upper set, then its complement $s^c$ is a lower set.

IsLowerSet.compl theorem

(hs : IsLowerSet s) : IsUpperSet sᶜ

Full source

theorem IsLowerSet.compl (hs : IsLowerSet s) : IsUpperSet sᶜ := fun _a _b h hb ha => hb <| hs h ha

Complement of a Lower Set is an Upper Set

Informal description

If a set $s$ in a partially ordered set is a lower set (i.e., for any $x \in s$ and $y \leq x$, we have $y \in s$), then its complement $s^c$ is an upper set (i.e., for any $x \in s^c$ and $x \leq y$, we have $y \in s^c$).

isUpperSet_compl theorem

: IsUpperSet sᶜ ↔ IsLowerSet s

Full source

@[simp]
theorem isUpperSet_compl : IsUpperSetIsUpperSet sᶜ ↔ IsLowerSet s :=
  ⟨fun h => by
    convert h.compl
    rw [compl_compl], IsLowerSet.compl⟩

Characterization of Upper Set Complements via Lower Sets

Informal description

The complement $s^c$ of a set $s$ is an upper set if and only if $s$ is a lower set.

isLowerSet_compl theorem

: IsLowerSet sᶜ ↔ IsUpperSet s

Full source

@[simp]
theorem isLowerSet_compl : IsLowerSetIsLowerSet sᶜ ↔ IsUpperSet s :=
  ⟨fun h => by
    convert h.compl
    rw [compl_compl], IsUpperSet.compl⟩

Characterization of Lower Set Complements: $s^c$ is Lower $\leftrightarrow$ $s$ is Upper

Informal description

For any set $s$ in a partially ordered set, the complement $s^c$ is a lower set if and only if $s$ is an upper set. Here, a lower set is a set where for any $x \in s^c$ and $y \leq x$, we have $y \in s^c$, and an upper set is a set where for any $x \in s$ and $x \leq y$, we have $y \in s$.

IsUpperSet.union theorem

(hs : IsUpperSet s) (ht : IsUpperSet t) : IsUpperSet (s ∪ t)

Full source

theorem IsUpperSet.union (hs : IsUpperSet s) (ht : IsUpperSet t) : IsUpperSet (s ∪ t) :=
  fun _ _ h => Or.imp (hs h) (ht h)

Union of Upper Sets is Upper

Informal description

If $s$ and $t$ are upper sets in a partially ordered set, then their union $s \cup t$ is also an upper set.

IsLowerSet.union theorem

(hs : IsLowerSet s) (ht : IsLowerSet t) : IsLowerSet (s ∪ t)

Full source

theorem IsLowerSet.union (hs : IsLowerSet s) (ht : IsLowerSet t) : IsLowerSet (s ∪ t) :=
  fun _ _ h => Or.imp (hs h) (ht h)

Union of Lower Sets is Lower

Informal description

For any two sets $s$ and $t$ in a partially ordered set, if both $s$ and $t$ are lower sets, then their union $s \cup t$ is also a lower set. Here, a lower set is a set where for any element $x$ in the set and any element $y$ such that $y \leq x$, $y$ is also in the set.

IsUpperSet.inter theorem

(hs : IsUpperSet s) (ht : IsUpperSet t) : IsUpperSet (s ∩ t)

Full source

theorem IsUpperSet.inter (hs : IsUpperSet s) (ht : IsUpperSet t) : IsUpperSet (s ∩ t) :=
  fun _ _ h => And.imp (hs h) (ht h)

Intersection of Upper Sets is Upper

Informal description

For any two upper sets $s$ and $t$ in a partially ordered set, their intersection $s \cap t$ is also an upper set.

IsLowerSet.inter theorem

(hs : IsLowerSet s) (ht : IsLowerSet t) : IsLowerSet (s ∩ t)

Full source

theorem IsLowerSet.inter (hs : IsLowerSet s) (ht : IsLowerSet t) : IsLowerSet (s ∩ t) :=
  fun _ _ h => And.imp (hs h) (ht h)

Intersection of Lower Sets is Lower

Informal description

If $s$ and $t$ are lower sets in a partially ordered set, then their intersection $s \cap t$ is also a lower set.

isUpperSet_sUnion theorem

{S : Set (Set α)} (hf : ∀ s ∈ S, IsUpperSet s) : IsUpperSet (⋃₀ S)

Full source

theorem isUpperSet_sUnion {S : Set (Set α)} (hf : ∀ s ∈ S, IsUpperSet s) : IsUpperSet (⋃₀ S) :=
  fun _ _ h => Exists.imp fun _ hs => ⟨hs.1, hf _ hs.1 h hs.2⟩

Union of Upper Sets is Upper

Informal description

For any family of sets $S$ in a type $\alpha$, if every set $s \in S$ is an upper set, then the union $\bigcup S$ is also an upper set.

isLowerSet_sUnion theorem

{S : Set (Set α)} (hf : ∀ s ∈ S, IsLowerSet s) : IsLowerSet (⋃₀ S)

Full source

theorem isLowerSet_sUnion {S : Set (Set α)} (hf : ∀ s ∈ S, IsLowerSet s) : IsLowerSet (⋃₀ S) :=
  fun _ _ h => Exists.imp fun _ hs => ⟨hs.1, hf _ hs.1 h hs.2⟩

Union of Lower Sets is Lower Set

Informal description

Let $S$ be a family of sets in a type $\alpha$ such that every set in $S$ is a lower set. Then the union of all sets in $S$ is also a lower set.

isUpperSet_iUnion theorem

{f : ι → Set α} (hf : ∀ i, IsUpperSet (f i)) : IsUpperSet (⋃ i, f i)

Full source

theorem isUpperSet_iUnion {f : ι → Set α} (hf : ∀ i, IsUpperSet (f i)) : IsUpperSet (⋃ i, f i) :=
  isUpperSet_sUnion <| forall_mem_range.2 hf

Union of Upper Sets is Upper

Informal description

For any family of sets $\{f_i\}_{i \in \iota}$ in a type $\alpha$, if each $f_i$ is an upper set, then the union $\bigcup_{i} f_i$ is also an upper set.

isLowerSet_iUnion theorem

{f : ι → Set α} (hf : ∀ i, IsLowerSet (f i)) : IsLowerSet (⋃ i, f i)

Full source

theorem isLowerSet_iUnion {f : ι → Set α} (hf : ∀ i, IsLowerSet (f i)) : IsLowerSet (⋃ i, f i) :=
  isLowerSet_sUnion <| forall_mem_range.2 hf

Union of Lower Sets is Lower Set

Informal description

Let $\{f_i\}_{i \in \iota}$ be a family of sets in a type $\alpha$ such that each $f_i$ is a lower set. Then the union $\bigcup_{i \in \iota} f_i$ is also a lower set.

isUpperSet_iUnion₂ theorem

{f : ∀ i, κ i → Set α} (hf : ∀ i j, IsUpperSet (f i j)) : IsUpperSet (⋃ (i) (j), f i j)

Full source

theorem isUpperSet_iUnion₂ {f : ∀ i, κ i → Set α} (hf : ∀ i j, IsUpperSet (f i j)) :
    IsUpperSet (⋃ (i) (j), f i j) :=
  isUpperSet_iUnion fun i => isUpperSet_iUnion <| hf i

Union of Doubly-Indexed Upper Sets is Upper

Informal description

For any doubly-indexed family of sets $\{f_{i,j}\}_{i \in \iota, j \in \kappa_i}$ in a type $\alpha$, if each $f_{i,j}$ is an upper set, then the union $\bigcup_{i,j} f_{i,j}$ is also an upper set.

isLowerSet_iUnion₂ theorem

{f : ∀ i, κ i → Set α} (hf : ∀ i j, IsLowerSet (f i j)) : IsLowerSet (⋃ (i) (j), f i j)

Full source

theorem isLowerSet_iUnion₂ {f : ∀ i, κ i → Set α} (hf : ∀ i j, IsLowerSet (f i j)) :
    IsLowerSet (⋃ (i) (j), f i j) :=
  isLowerSet_iUnion fun i => isLowerSet_iUnion <| hf i

Union of Doubly-Indexed Lower Sets is Lower

Informal description

Let $\{f_{i,j}\}_{i \in \iota, j \in \kappa_i}$ be a doubly-indexed family of sets in a type $\alpha$ such that each $f_{i,j}$ is a lower set. Then the union $\bigcup_{i,j} f_{i,j}$ is also a lower set.

isUpperSet_sInter theorem

{S : Set (Set α)} (hf : ∀ s ∈ S, IsUpperSet s) : IsUpperSet (⋂₀ S)

Full source

theorem isUpperSet_sInter {S : Set (Set α)} (hf : ∀ s ∈ S, IsUpperSet s) : IsUpperSet (⋂₀ S) :=
  fun _ _ h => forall₂_imp fun s hs => hf s hs h

Intersection of Upper Sets is Upper

Informal description

For any collection of sets $S$ in a type $\alpha$, if every set $s \in S$ is an upper set (i.e., for any $x \leq y$ in $\alpha$, if $x \in s$ then $y \in s$), then the intersection $\bigcap S$ is also an upper set.

isLowerSet_sInter theorem

{S : Set (Set α)} (hf : ∀ s ∈ S, IsLowerSet s) : IsLowerSet (⋂₀ S)

Full source

theorem isLowerSet_sInter {S : Set (Set α)} (hf : ∀ s ∈ S, IsLowerSet s) : IsLowerSet (⋂₀ S) :=
  fun _ _ h => forall₂_imp fun s hs => hf s hs h

Intersection of Lower Sets is Lower

Informal description

For any collection of sets $S$ in a type $\alpha$, if every set $s \in S$ is a lower set (i.e., for any $x \leq y$ in $\alpha$, if $y \in s$ then $x \in s$), then the intersection $\bigcap S$ is also a lower set.

isUpperSet_iInter theorem

{f : ι → Set α} (hf : ∀ i, IsUpperSet (f i)) : IsUpperSet (⋂ i, f i)

Full source

theorem isUpperSet_iInter {f : ι → Set α} (hf : ∀ i, IsUpperSet (f i)) : IsUpperSet (⋂ i, f i) :=
  isUpperSet_sInter <| forall_mem_range.2 hf

Intersection of a Family of Upper Sets is Upper

Informal description

For any family of sets $\{f_i\}_{i \in \iota}$ in a type $\alpha$, if each set $f_i$ is an upper set (i.e., for any $x \leq y$ in $\alpha$, if $x \in f_i$ then $y \in f_i$), then the intersection $\bigcap_{i \in \iota} f_i$ is also an upper set.

isLowerSet_iInter theorem

{f : ι → Set α} (hf : ∀ i, IsLowerSet (f i)) : IsLowerSet (⋂ i, f i)

Full source

theorem isLowerSet_iInter {f : ι → Set α} (hf : ∀ i, IsLowerSet (f i)) : IsLowerSet (⋂ i, f i) :=
  isLowerSet_sInter <| forall_mem_range.2 hf

Intersection of a Family of Lower Sets is Lower

Informal description

For any family of sets $\{f_i\}_{i \in \iota}$ in a type $\alpha$, if each $f_i$ is a lower set (i.e., for any $x \leq y$ in $\alpha$, if $y \in f_i$ then $x \in f_i$), then the intersection $\bigcap_{i} f_i$ is also a lower set.

isUpperSet_iInter₂ theorem

{f : ∀ i, κ i → Set α} (hf : ∀ i j, IsUpperSet (f i j)) : IsUpperSet (⋂ (i) (j), f i j)

Full source

theorem isUpperSet_iInter₂ {f : ∀ i, κ i → Set α} (hf : ∀ i j, IsUpperSet (f i j)) :
    IsUpperSet (⋂ (i) (j), f i j) :=
  isUpperSet_iInter fun i => isUpperSet_iInter <| hf i

Intersection of Doubly-Indexed Family of Upper Sets is Upper

Informal description

For any doubly-indexed family of sets $\{f_{i,j}\}_{i \in \iota, j \in \kappa_i}$ in a type $\alpha$, if each set $f_{i,j}$ is an upper set (i.e., for any $x \leq y$ in $\alpha$, if $x \in f_{i,j}$ then $y \in f_{i,j}$), then the intersection $\bigcap_{i \in \iota} \bigcap_{j \in \kappa_i} f_{i,j}$ is also an upper set.

isLowerSet_iInter₂ theorem

{f : ∀ i, κ i → Set α} (hf : ∀ i j, IsLowerSet (f i j)) : IsLowerSet (⋂ (i) (j), f i j)

Full source

theorem isLowerSet_iInter₂ {f : ∀ i, κ i → Set α} (hf : ∀ i j, IsLowerSet (f i j)) :
    IsLowerSet (⋂ (i) (j), f i j) :=
  isLowerSet_iInter fun i => isLowerSet_iInter <| hf i

Intersection of Doubly-Indexed Family of Lower Sets is Lower

Informal description

For any doubly-indexed family of sets $\{f_{i,j}\}_{i \in \iota, j \in \kappa_i}$ in a type $\alpha$, if each set $f_{i,j}$ is a lower set (i.e., for any $x \leq y$ in $\alpha$, if $y \in f_{i,j}$ then $x \in f_{i,j}$), then the intersection $\bigcap_{i \in \iota} \bigcap_{j \in \kappa_i} f_{i,j}$ is also a lower set.

isLowerSet_preimage_ofDual_iff theorem

: IsLowerSet (ofDual ⁻¹' s) ↔ IsUpperSet s

Full source

@[simp]
theorem isLowerSet_preimage_ofDual_iff : IsLowerSetIsLowerSet (ofDual ⁻¹' s) ↔ IsUpperSet s :=
  Iff.rfl

Lower set preimage under order dual ↔ Upper set

Informal description

For any set $s$ in a preorder $\alpha$, the preimage of $s$ under the order dual map $\text{ofDual} : \alpha^\text{op} \to \alpha$ is a lower set if and only if $s$ is an upper set in $\alpha$.

isUpperSet_preimage_ofDual_iff theorem

: IsUpperSet (ofDual ⁻¹' s) ↔ IsLowerSet s

Full source

@[simp]
theorem isUpperSet_preimage_ofDual_iff : IsUpperSetIsUpperSet (ofDual ⁻¹' s) ↔ IsLowerSet s :=
  Iff.rfl

Upper set preimage under order dual ↔ Lower set

Informal description

For any set $s$ in a preorder $\alpha$, the preimage of $s$ under the order dual map $\text{ofDual} : \alpha^\text{op} \to \alpha$ is an upper set if and only if $s$ is a lower set in $\alpha$.

isLowerSet_preimage_toDual_iff theorem

{s : Set αᵒᵈ} : IsLowerSet (toDual ⁻¹' s) ↔ IsUpperSet s

Full source

@[simp]
theorem isLowerSet_preimage_toDual_iff {s : Set αᵒᵈ} : IsLowerSetIsLowerSet (toDual ⁻¹' s) ↔ IsUpperSet s :=
  Iff.rfl

Lower set preimage under order dual ↔ Upper set in dual order

Informal description

For any set $s$ in the order dual $\alpha^\text{op}$ of a preorder $\alpha$, the preimage of $s$ under the order dual map $\text{toDual} : \alpha \to \alpha^\text{op}$ is a lower set in $\alpha$ if and only if $s$ is an upper set in $\alpha^\text{op}$.

isUpperSet_preimage_toDual_iff theorem

{s : Set αᵒᵈ} : IsUpperSet (toDual ⁻¹' s) ↔ IsLowerSet s

Full source

@[simp]
theorem isUpperSet_preimage_toDual_iff {s : Set αᵒᵈ} : IsUpperSetIsUpperSet (toDual ⁻¹' s) ↔ IsLowerSet s :=
  Iff.rfl

Upper set preimage under order dual ↔ Lower set in dual order

Informal description

For any set $s$ in the order dual $\alpha^\text{op}$ of a preorder $\alpha$, the preimage of $s$ under the order dual map $\text{toDual} : \alpha \to \alpha^\text{op}$ is an upper set in $\alpha$ if and only if $s$ is a lower set in $\alpha^\text{op}$.

IsUpperSet.isLowerSet_preimage_coe theorem

(hs : IsUpperSet s) : IsLowerSet ((↑) ⁻¹' t : Set s) ↔ ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t

Full source

lemma IsUpperSet.isLowerSet_preimage_coe (hs : IsUpperSet s) :
    IsLowerSetIsLowerSet ((↑) ⁻¹' t : Set s) ↔ ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t := by aesop

Characterization of Lower Set Preimage in an Upper Set

Informal description

Let $s$ be an upper set in a partially ordered set $\alpha$, and let $t$ be a subset of $s$. Then the preimage of $t$ under the inclusion map $\iota : s \hookrightarrow \alpha$ is a lower set in $s$ if and only if for every $b \in s$ and $c \in t$, if $b \leq c$, then $b \in t$.

IsLowerSet.isUpperSet_preimage_coe theorem

(hs : IsLowerSet s) : IsUpperSet ((↑) ⁻¹' t : Set s) ↔ ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t

Full source

lemma IsLowerSet.isUpperSet_preimage_coe (hs : IsLowerSet s) :
    IsUpperSetIsUpperSet ((↑) ⁻¹' t : Set s) ↔ ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t := by aesop

Characterization of Upper Set Preimage in a Lower Set

Informal description

Let $s$ be a lower set in a partially ordered set $\alpha$, and let $t$ be a subset of $s$. Then the preimage of $t$ under the inclusion map $\iota : s \hookrightarrow \alpha$ is an upper set in $s$ if and only if for every $b \in s$ and $c \in t$, if $c \leq b$, then $b \in t$.

IsUpperSet.sdiff theorem

(hs : IsUpperSet s) (ht : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t) : IsUpperSet (s \ t)

Full source

lemma IsUpperSet.sdiff (hs : IsUpperSet s) (ht : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t) :
    IsUpperSet (s \ t) :=
  fun _b _c hbc hb ↦ ⟨hs hbc hb.1, fun hc ↦ hb.2 <| ht _ hb.1 _ hc hbc⟩

Difference of Upper Set with Respect to a Condition Preserves Upper Set Property

Informal description

Let $s$ be an upper set and $t$ be a subset such that for any $b \in s$ and $c \in t$, if $b \leq c$ then $b \in t$. Then the set difference $s \setminus t$ is also an upper set.

IsLowerSet.sdiff theorem

(hs : IsLowerSet s) (ht : ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t) : IsLowerSet (s \ t)

Full source

lemma IsLowerSet.sdiff (hs : IsLowerSet s) (ht : ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t) :
    IsLowerSet (s \ t) :=
  fun _b _c hcb hb ↦ ⟨hs hcb hb.1, fun hc ↦ hb.2 <| ht _ hb.1 _ hc hcb⟩

Set Difference of Lower Set Preserves Lower Set Property

Informal description

Let $s$ be a lower set and $t$ be a set such that for any $b \in s$ and $c \in t$, if $c \leq b$ then $b \in t$. Then the set difference $s \setminus t$ is also a lower set.

IsUpperSet.sdiff_of_isLowerSet theorem

(hs : IsUpperSet s) (ht : IsLowerSet t) : IsUpperSet (s \ t)

Full source

lemma IsUpperSet.sdiff_of_isLowerSet (hs : IsUpperSet s) (ht : IsLowerSet t) : IsUpperSet (s \ t) :=
  hs.sdiff <| by aesop

Difference of Upper Set and Lower Set is Upper Set

Informal description

Let $s$ be an upper set and $t$ be a lower set in a partially ordered set. Then the set difference $s \setminus t$ is also an upper set.

IsLowerSet.sdiff_of_isUpperSet theorem

(hs : IsLowerSet s) (ht : IsUpperSet t) : IsLowerSet (s \ t)

Full source

lemma IsLowerSet.sdiff_of_isUpperSet (hs : IsLowerSet s) (ht : IsUpperSet t) : IsLowerSet (s \ t) :=
  hs.sdiff <| by aesop

Set Difference of Lower Set with Upper Set Preserves Lower Set Property

Informal description

Let $s$ be a lower set and $t$ be an upper set. Then the set difference $s \setminus t$ is also a lower set.

IsUpperSet.erase theorem

(hs : IsUpperSet s) (has : ∀ b ∈ s, b ≤ a → b = a) : IsUpperSet (s \ { a })

Full source

lemma IsUpperSet.erase (hs : IsUpperSet s) (has : ∀ b ∈ s, b ≤ a → b = a) : IsUpperSet (s \ {a}) :=
  hs.sdiff <| by simpa using has

Removal of Maximal Element Preserves Upper Set Property

Informal description

Let $s$ be an upper set and $a$ be an element such that for any $b \in s$, if $b \leq a$ then $b = a$. Then the set difference $s \setminus \{a\}$ is also an upper set.

IsLowerSet.erase theorem

(hs : IsLowerSet s) (has : ∀ b ∈ s, a ≤ b → b = a) : IsLowerSet (s \ { a })

Full source

lemma IsLowerSet.erase (hs : IsLowerSet s) (has : ∀ b ∈ s, a ≤ b → b = a) : IsLowerSet (s \ {a}) :=
  hs.sdiff <| by simpa using has

Removal of Minimal Element Preserves Lower Set Property

Informal description

Let $s$ be a lower set and $a$ be an element such that for any $b \in s$, if $a \leq b$ then $b = a$. Then the set difference $s \setminus \{a\}$ is also a lower set.

isUpperSet_Ici theorem

: IsUpperSet (Ici a)

Full source

theorem isUpperSet_Ici : IsUpperSet (Ici a) := fun _ _ => ge_trans

The interval $[a, \infty)$ is an upper set

Informal description

For any element $a$ in a preorder $\alpha$, the left-closed right-infinite interval $[a, \infty)$ is an upper set. That is, if $x \in [a, \infty)$ and $x \leq y$, then $y \in [a, \infty)$.

isLowerSet_Iic theorem

: IsLowerSet (Iic a)

Full source

theorem isLowerSet_Iic : IsLowerSet (Iic a) := fun _ _ => le_trans

The interval $(-\infty, a]$ is a lower set

Informal description

For any element $a$ in a preorder, the left-infinite right-closed interval $(-\infty, a]$ is a lower set. That is, the set $\{x \mid x \leq a\}$ is downward closed: if $x \in (-\infty, a]$ and $y \leq x$, then $y \in (-\infty, a]$.

isUpperSet_Ioi theorem

: IsUpperSet (Ioi a)

Full source

theorem isUpperSet_Ioi : IsUpperSet (Ioi a) := fun _ _ => flip lt_of_lt_of_le

The interval $(a, \infty)$ is an upper set

Informal description

For any element $a$ in a preorder $\alpha$, the left-open right-infinite interval $(a, \infty)$ is an upper set. That is, if $x \in (a, \infty)$ and $x \leq y$, then $y \in (a, \infty)$.

isLowerSet_Iio theorem

: IsLowerSet (Iio a)

Full source

theorem isLowerSet_Iio : IsLowerSet (Iio a) := fun _ _ => lt_of_le_of_lt

The interval $(-\infty, a)$ is a lower set

Informal description

For any element $a$ in a preorder, the left-infinite right-open interval $(-\infty, a)$ is a lower set. That is, the set $\{x \mid x < a\}$ is downward closed: if $x \in (-\infty, a)$ and $y \leq x$, then $y \in (-\infty, a)$.

isUpperSet_iff_Ici_subset theorem

: IsUpperSet s ↔ ∀ ⦃a⦄, a ∈ s → Ici a ⊆ s

Full source

theorem isUpperSet_iff_Ici_subset : IsUpperSetIsUpperSet s ↔ ∀ ⦃a⦄, a ∈ s → Ici a ⊆ s := by
  simp [IsUpperSet, subset_def, @forall_swap (_ ∈ s)]

Characterization of Upper Sets via Interval Inclusion

Informal description

A subset $s$ of a preorder is an upper set if and only if for every element $a \in s$, the left-closed right-infinite interval $[a, \infty)$ is contained in $s$.

isLowerSet_iff_Iic_subset theorem

: IsLowerSet s ↔ ∀ ⦃a⦄, a ∈ s → Iic a ⊆ s

Full source

theorem isLowerSet_iff_Iic_subset : IsLowerSetIsLowerSet s ↔ ∀ ⦃a⦄, a ∈ s → Iic a ⊆ s := by
  simp [IsLowerSet, subset_def, @forall_swap (_ ∈ s)]

Characterization of Lower Sets via Interval Inclusion

Informal description

A subset $s$ of a preorder is a lower set if and only if for every element $a \in s$, the left-infinite right-closed interval $(-\infty, a]$ is entirely contained in $s$.

IsUpperSet.Ioi_subset theorem

(h : IsUpperSet s) ⦃a⦄ (ha : a ∈ s) : Ioi a ⊆ s

Full source

theorem IsUpperSet.Ioi_subset (h : IsUpperSet s) ⦃a⦄ (ha : a ∈ s) : IoiIoi a ⊆ s :=
  Ioi_subset_Ici_self.trans <| h.Ici_subset ha

Upper Sets Contain Open Upper Intervals

Informal description

For any subset $s$ of a preorder that is an upper set, and for any element $a \in s$, the left-open right-infinite interval $(a, \infty)$ is contained in $s$.

IsLowerSet.Iio_subset theorem

(h : IsLowerSet s) ⦃a⦄ (ha : a ∈ s) : Iio a ⊆ s

Full source

theorem IsLowerSet.Iio_subset (h : IsLowerSet s) ⦃a⦄ (ha : a ∈ s) : IioIio a ⊆ s :=
  h.toDual.Ioi_subset ha

Lower Sets Contain Open Lower Intervals

Informal description

For any subset $s$ of a preorder that is a lower set, and for any element $a \in s$, the left-infinite right-open interval $(-\infty, a)$ is contained in $s$.

IsUpperSet.ordConnected theorem

(h : IsUpperSet s) : s.OrdConnected

Full source

theorem IsUpperSet.ordConnected (h : IsUpperSet s) : s.OrdConnected :=
  ⟨fun _ ha _ _ => Icc_subset_Ici_self.trans <| h.Ici_subset ha⟩

Upper Sets are Order Connected

Informal description

For any subset $s$ of a preorder $\alpha$ that is an upper set, $s$ is order connected. That is, for any two elements $x, y \in s$, the closed interval $[x, y]$ is entirely contained in $s$.

IsLowerSet.ordConnected theorem

(h : IsLowerSet s) : s.OrdConnected

Full source

theorem IsLowerSet.ordConnected (h : IsLowerSet s) : s.OrdConnected :=
  ⟨fun _ _ _ hb => Icc_subset_Iic_self.trans <| h.Iic_subset hb⟩

Lower Sets are Order Connected

Informal description

For any subset $s$ of a preorder $\alpha$ that is a lower set, $s$ is order connected. That is, for any two elements $x, y \in s$, the closed interval $[x, y]$ is entirely contained in $s$.

IsUpperSet.preimage theorem

(hs : IsUpperSet s) {f : β → α} (hf : Monotone f) : IsUpperSet (f ⁻¹' s : Set β)

Full source

theorem IsUpperSet.preimage (hs : IsUpperSet s) {f : β → α} (hf : Monotone f) :
    IsUpperSet (f ⁻¹' s : Set β) := fun _ _ h => hs <| hf h

Preimage of an Upper Set under a Monotone Function is Upper

Informal description

Let $s$ be an upper set in a partially ordered set $\alpha$, and let $f : \beta \to \alpha$ be a monotone function. Then the preimage $f^{-1}(s)$ is an upper set in $\beta$.

IsLowerSet.preimage theorem

(hs : IsLowerSet s) {f : β → α} (hf : Monotone f) : IsLowerSet (f ⁻¹' s : Set β)

Full source

theorem IsLowerSet.preimage (hs : IsLowerSet s) {f : β → α} (hf : Monotone f) :
    IsLowerSet (f ⁻¹' s : Set β) := fun _ _ h => hs <| hf h

Preimage of a Lower Set under a Monotone Function is Lower

Informal description

Let $s$ be a lower set in a partially ordered set $\alpha$ and $f : \beta \to \alpha$ be a monotone function. Then the preimage $f^{-1}(s)$ is a lower set in $\beta$.

IsUpperSet.image theorem

(hs : IsUpperSet s) (f : α ≃o β) : IsUpperSet (f '' s : Set β)

Full source

theorem IsUpperSet.image (hs : IsUpperSet s) (f : α ≃o β) : IsUpperSet (f '' s : Set β) := by
  change IsUpperSet ((f : α ≃ β) '' s)
  rw [Set.image_equiv_eq_preimage_symm]
  exact hs.preimage f.symm.monotone

Image of an Upper Set under an Order Isomorphism is Upper

Informal description

Let $s$ be an upper set in a partially ordered set $\alpha$, and let $f : \alpha \to \beta$ be an order isomorphism. Then the image $f(s)$ is an upper set in $\beta$.

IsLowerSet.image theorem

(hs : IsLowerSet s) (f : α ≃o β) : IsLowerSet (f '' s : Set β)

Full source

theorem IsLowerSet.image (hs : IsLowerSet s) (f : α ≃o β) : IsLowerSet (f '' s : Set β) := by
  change IsLowerSet ((f : α ≃ β) '' s)
  rw [Set.image_equiv_eq_preimage_symm]
  exact hs.preimage f.symm.monotone

Image of a Lower Set under an Order Isomorphism is Lower

Informal description

Let $s$ be a lower set in a partially ordered set $\alpha$ and $f : \alpha \simeq \beta$ be an order isomorphism. Then the image $f(s)$ is a lower set in $\beta$.

OrderEmbedding.image_Ici theorem

(e : α ↪o β) (he : IsUpperSet (range e)) (a : α) : e '' Ici a = Ici (e a)

Full source

theorem OrderEmbedding.image_Ici (e : α ↪o β) (he : IsUpperSet (range e)) (a : α) :
    e '' Ici a = Ici (e a) := by
  rw [← e.preimage_Ici, image_preimage_eq_inter_range,
    inter_eq_left.2 <| he.Ici_subset (mem_range_self _)]

Image of Closed Right-Infinite Interval under Order Embedding with Upper Set Range

Informal description

For an order embedding $e : \alpha \hookrightarrow \beta$ such that the range of $e$ is an upper set, and for any element $a \in \alpha$, the image under $e$ of the closed right-infinite interval $[a, \infty)$ in $\alpha$ is equal to the closed right-infinite interval $[e(a), \infty)$ in $\beta$, i.e., $$ e\big([a, \infty)\big) = [e(a), \infty). $$

OrderEmbedding.image_Iic theorem

(e : α ↪o β) (he : IsLowerSet (range e)) (a : α) : e '' Iic a = Iic (e a)

Full source

theorem OrderEmbedding.image_Iic (e : α ↪o β) (he : IsLowerSet (range e)) (a : α) :
    e '' Iic a = Iic (e a) :=
  e.dual.image_Ici he a

Image of Left-Infinite Right-Closed Interval under Order Embedding with Lower Set Range

Informal description

For an order embedding $e : \alpha \hookrightarrow \beta$ such that the range of $e$ is a lower set, and for any element $a \in \alpha$, the image under $e$ of the left-infinite right-closed interval $(-\infty, a]$ in $\alpha$ is equal to the left-infinite right-closed interval $(-\infty, e(a)]$ in $\beta$, i.e., $$ e\big((-\infty, a]\big) = (-\infty, e(a)]. $$

OrderEmbedding.image_Ioi theorem

(e : α ↪o β) (he : IsUpperSet (range e)) (a : α) : e '' Ioi a = Ioi (e a)

Full source

theorem OrderEmbedding.image_Ioi (e : α ↪o β) (he : IsUpperSet (range e)) (a : α) :
    e '' Ioi a = Ioi (e a) := by
  rw [← e.preimage_Ioi, image_preimage_eq_inter_range,
    inter_eq_left.2 <| he.Ioi_subset (mem_range_self _)]

Image of Open Right-Infinite Interval under Order Embedding with Upper Set Range

Informal description

For an order embedding $e : \alpha \hookrightarrow \beta$ such that the range of $e$ is an upper set, and for any element $a \in \alpha$, the image under $e$ of the open right-infinite interval $(a, \infty)$ in $\alpha$ is equal to the open right-infinite interval $(e(a), \infty)$ in $\beta$, i.e., $$ e\big((a, \infty)\big) = (e(a), \infty). $$

OrderEmbedding.image_Iio theorem

(e : α ↪o β) (he : IsLowerSet (range e)) (a : α) : e '' Iio a = Iio (e a)

Full source

theorem OrderEmbedding.image_Iio (e : α ↪o β) (he : IsLowerSet (range e)) (a : α) :
    e '' Iio a = Iio (e a) :=
  e.dual.image_Ioi he a

Image of Left-Infinite Interval under Order Embedding with Lower Set Range

Informal description

For an order embedding $e : \alpha \hookrightarrow \beta$ such that the range of $e$ is a lower set, and for any element $a \in \alpha$, the image under $e$ of the open left-infinite interval $(-\infty, a)$ in $\alpha$ is equal to the open left-infinite interval $(-\infty, e(a))$ in $\beta$, i.e., $$ e\big((-\infty, a)\big) = (-\infty, e(a)). $$

Set.monotone_mem theorem

: Monotone (· ∈ s) ↔ IsUpperSet s

Full source

@[simp]
theorem Set.monotone_mem : MonotoneMonotone (· ∈ s) ↔ IsUpperSet s :=
  Iff.rfl

Monotonicity of Membership Characterizes Upper Sets

Informal description

A set $s$ is an upper set if and only if the membership function $\lambda a, a \in s$ is monotone. That is, for any elements $a \leq b$, if $a \in s$ then $b \in s$.

Set.antitone_mem theorem

: Antitone (· ∈ s) ↔ IsLowerSet s

Full source

@[simp]
theorem Set.antitone_mem : AntitoneAntitone (· ∈ s) ↔ IsLowerSet s :=
  forall_swap

Characterization of Lower Sets via Antitone Membership Function

Informal description

A set $s$ is a lower set if and only if the membership function $(· ∈ s)$ is antitone (i.e., order-reversing). In other words, for any elements $x ≤ y$, if $y ∈ s$ then $x ∈ s$.

isUpperSet_setOf theorem

: IsUpperSet {a | p a} ↔ Monotone p

Full source

@[simp]
theorem isUpperSet_setOf : IsUpperSetIsUpperSet { a | p a } ↔ Monotone p :=
  Iff.rfl

Characterization of Upper Sets via Monotone Predicates

Informal description

A set $\{a \mid p(a)\}$ is an upper set if and only if the predicate $p$ is monotone. Here, an *upper set* is a set where for any element $a$ in the set and any element $b$ such that $a \leq b$, the element $b$ is also in the set.

isLowerSet_setOf theorem

: IsLowerSet {a | p a} ↔ Antitone p

Full source

@[simp]
theorem isLowerSet_setOf : IsLowerSetIsLowerSet { a | p a } ↔ Antitone p :=
  forall_swap

Characterization of Lower Sets via Antitone Predicates

Informal description

A set defined by a predicate $p$ (i.e., $\{a \mid p(a)\}$) is a lower set if and only if the predicate $p$ is antitone (i.e., order-reversing).

IsUpperSet.upperBounds_subset theorem

(hs : IsUpperSet s) : s.Nonempty → upperBounds s ⊆ s

Full source

lemma IsUpperSet.upperBounds_subset (hs : IsUpperSet s) : s.Nonempty → upperBoundsupperBounds s ⊆ s :=
  fun ⟨_a, ha⟩ _b hb ↦ hs (hb ha) ha

Upper Bounds of Nonempty Upper Sets are Contained Within

Informal description

For any nonempty set $s$ that is an upper set (i.e., if $x \in s$ and $x \leq y$, then $y \in s$), the set of upper bounds of $s$ is a subset of $s$.

IsLowerSet.lowerBounds_subset theorem

(hs : IsLowerSet s) : s.Nonempty → lowerBounds s ⊆ s

Full source

lemma IsLowerSet.lowerBounds_subset (hs : IsLowerSet s) : s.Nonempty → lowerBoundslowerBounds s ⊆ s :=
  fun ⟨_a, ha⟩ _b hb ↦ hs (hb ha) ha

Lower Bounds of Nonempty Lower Set are Contained in the Set

Informal description

For any lower set $s$ in a partially ordered set, if $s$ is nonempty, then the set of all lower bounds of $s$ is contained in $s$.

IsLowerSet.top_mem theorem

(hs : IsLowerSet s) : ⊤ ∈ s ↔ s = univ

Full source

theorem IsLowerSet.top_mem (hs : IsLowerSet s) : ⊤⊤ ∈ s⊤ ∈ s ↔ s = univ :=
  ⟨fun h => eq_univ_of_forall fun _ => hs le_top h, fun h => h.symm ▸ mem_univ _⟩

Characterization of Lower Sets Containing the Top Element

Informal description

For any lower set $s$ in a partially ordered set with a greatest element $\top$, the element $\top$ belongs to $s$ if and only if $s$ is the entire universe (i.e., $s$ contains all elements of the type).

IsUpperSet.top_mem theorem

(hs : IsUpperSet s) : ⊤ ∈ s ↔ s.Nonempty

Full source

theorem IsUpperSet.top_mem (hs : IsUpperSet s) : ⊤⊤ ∈ s⊤ ∈ s ↔ s.Nonempty :=
  ⟨fun h => ⟨_, h⟩, fun ⟨_a, ha⟩ => hs le_top ha⟩

Top Element Membership in Upper Sets Characterizes Nonemptiness

Informal description

For any upper set $s$ in a partially ordered set with a greatest element $\top$, the element $\top$ belongs to $s$ if and only if $s$ is nonempty.

IsUpperSet.not_top_mem theorem

(hs : IsUpperSet s) : ⊤ ∉ s ↔ s = ∅

Full source

theorem IsUpperSet.not_top_mem (hs : IsUpperSet s) : ⊤⊤ ∉ s⊤ ∉ s ↔ s = ∅ :=
  hs.top_mem.not.trans not_nonempty_iff_eq_empty

Characterization of Empty Upper Sets via Top Element Non-Membership

Informal description

For any upper set $s$ in a partially ordered set with a greatest element $\top$, the element $\top$ does not belong to $s$ if and only if $s$ is the empty set.

IsUpperSet.bot_mem theorem

(hs : IsUpperSet s) : ⊥ ∈ s ↔ s = univ

Full source

theorem IsUpperSet.bot_mem (hs : IsUpperSet s) : ⊥⊥ ∈ s⊥ ∈ s ↔ s = univ :=
  ⟨fun h => eq_univ_of_forall fun _ => hs bot_le h, fun h => h.symm ▸ mem_univ _⟩

Bottom Element Membership in Upper Sets Characterizes Universality

Informal description

For any upper set $s$ in an order with a bottom element $\bot$, the bottom element is in $s$ if and only if $s$ is the universal set (i.e., $s$ contains all elements of the order).

IsLowerSet.bot_mem theorem

(hs : IsLowerSet s) : ⊥ ∈ s ↔ s.Nonempty

Full source

theorem IsLowerSet.bot_mem (hs : IsLowerSet s) : ⊥⊥ ∈ s⊥ ∈ s ↔ s.Nonempty :=
  ⟨fun h => ⟨_, h⟩, fun ⟨_a, ha⟩ => hs bot_le ha⟩

Bottom Element Membership in Lower Sets Characterizes Nonemptiness

Informal description

For any lower set $s$ in an order with a bottom element $\bot$, the bottom element is in $s$ if and only if $s$ is nonempty.

IsLowerSet.not_bot_mem theorem

(hs : IsLowerSet s) : ⊥ ∉ s ↔ s = ∅

Full source

theorem IsLowerSet.not_bot_mem (hs : IsLowerSet s) : ⊥⊥ ∉ s⊥ ∉ s ↔ s = ∅ :=
  hs.bot_mem.not.trans not_nonempty_iff_eq_empty

Empty Lower Sets Exclude Bottom Element

Informal description

For any lower set $s$ in an order with a bottom element $\bot$, the bottom element is not in $s$ if and only if $s$ is empty.

IsUpperSet.not_bddAbove theorem

(hs : IsUpperSet s) : s.Nonempty → ¬BddAbove s

Full source

theorem IsUpperSet.not_bddAbove (hs : IsUpperSet s) : s.Nonempty → ¬BddAbove s := by
  rintro ⟨a, ha⟩ ⟨b, hb⟩
  obtain ⟨c, hc⟩ := exists_gt b
  exact hc.not_le (hb <| hs ((hb ha).trans hc.le) ha)

Nonempty upper sets are unbounded above

Informal description

For any nonempty upper set $s$ in a partially ordered set, $s$ is not bounded above.

not_bddAbove_Ici theorem

: ¬BddAbove (Ici a)

Full source

theorem not_bddAbove_Ici : ¬BddAbove (Ici a) :=
  (isUpperSet_Ici _).not_bddAbove nonempty_Ici

Unboundedness of the Interval $[a, \infty)$

Informal description

For any element $a$ in a preorder $\alpha$, the left-closed right-infinite interval $[a, \infty)$ is not bounded above.

not_bddAbove_Ioi theorem

: ¬BddAbove (Ioi a)

Full source

theorem not_bddAbove_Ioi : ¬BddAbove (Ioi a) :=
  (isUpperSet_Ioi _).not_bddAbove nonempty_Ioi

Unboundedness of the Interval $(a, \infty)$

Informal description

For any element $a$ in a preorder $\alpha$, the left-open right-infinite interval $(a, \infty)$ is not bounded above.

IsLowerSet.not_bddBelow theorem

(hs : IsLowerSet s) : s.Nonempty → ¬BddBelow s

Full source

theorem IsLowerSet.not_bddBelow (hs : IsLowerSet s) : s.Nonempty → ¬BddBelow s := by
  rintro ⟨a, ha⟩ ⟨b, hb⟩
  obtain ⟨c, hc⟩ := exists_lt b
  exact hc.not_le (hb <| hs (hc.le.trans <| hb ha) ha)

Nonempty lower sets are unbounded below

Informal description

For any nonempty lower set $s$ in a partially ordered set, $s$ is not bounded below.

not_bddBelow_Iic theorem

: ¬BddBelow (Iic a)

Full source

theorem not_bddBelow_Iic : ¬BddBelow (Iic a) :=
  (isLowerSet_Iic _).not_bddBelow nonempty_Iic

Unboundedness Below of the Interval $(-\infty, a]$

Informal description

For any element $a$ in a preorder, the left-infinite right-closed interval $(-\infty, a]$ is not bounded below.

not_bddBelow_Iio theorem

: ¬BddBelow (Iio a)

Full source

theorem not_bddBelow_Iio : ¬BddBelow (Iio a) :=
  (isLowerSet_Iio _).not_bddBelow nonempty_Iio

Unboundedness Below of the Interval $(-\infty, a)$

Informal description

For any element $a$ in a preorder, the left-infinite right-open interval $(-\infty, a)$ is not bounded below. That is, the set $\{x \mid x < a\}$ does not have a lower bound.

isUpperSet_iff_forall_lt theorem

: IsUpperSet s ↔ ∀ ⦃a b : α⦄, a < b → a ∈ s → b ∈ s

Full source

theorem isUpperSet_iff_forall_lt : IsUpperSetIsUpperSet s ↔ ∀ ⦃a b : α⦄, a < b → a ∈ s → b ∈ s :=
  forall_congr' fun a => by simp [le_iff_eq_or_lt, or_imp, forall_and]

Characterization of Upper Sets by Strict Order Preservation

Informal description

A subset $s$ of a partially ordered set $\alpha$ is an upper set if and only if for all elements $a, b \in \alpha$ with $a < b$, whenever $a \in s$ then $b \in s$.

isLowerSet_iff_forall_lt theorem

: IsLowerSet s ↔ ∀ ⦃a b : α⦄, b < a → a ∈ s → b ∈ s

Full source

theorem isLowerSet_iff_forall_lt : IsLowerSetIsLowerSet s ↔ ∀ ⦃a b : α⦄, b < a → a ∈ s → b ∈ s :=
  forall_congr' fun a => by simp [le_iff_eq_or_lt, or_imp, forall_and]

Characterization of Lower Sets via Order Relation

Informal description

A subset $s$ of a partially ordered set is a lower set if and only if for all elements $a, b$ with $b < a$, whenever $a$ belongs to $s$, then $b$ also belongs to $s$.

isUpperSet_iff_Ioi_subset theorem

: IsUpperSet s ↔ ∀ ⦃a⦄, a ∈ s → Ioi a ⊆ s

Full source

theorem isUpperSet_iff_Ioi_subset : IsUpperSetIsUpperSet s ↔ ∀ ⦃a⦄, a ∈ s → Ioi a ⊆ s := by
  simp [isUpperSet_iff_forall_lt, subset_def, @forall_swap (_ ∈ s)]

Characterization of Upper Sets via Interval Containment

Informal description

A subset $s$ of a preorder $\alpha$ is an upper set if and only if for every element $a \in s$, the left-open right-infinite interval $(a, \infty)$ is contained in $s$.

isLowerSet_iff_Iio_subset theorem

: IsLowerSet s ↔ ∀ ⦃a⦄, a ∈ s → Iio a ⊆ s

Full source

theorem isLowerSet_iff_Iio_subset : IsLowerSetIsLowerSet s ↔ ∀ ⦃a⦄, a ∈ s → Iio a ⊆ s := by
  simp [isLowerSet_iff_forall_lt, subset_def, @forall_swap (_ ∈ s)]

Characterization of Lower Sets via Interval Containment

Informal description

A subset $s$ of a preorder $\alpha$ is a lower set if and only if for every element $a \in s$, the left-infinite right-open interval $(-\infty, a)$ is entirely contained in $s$.

IsUpperSet.total theorem

(hs : IsUpperSet s) (ht : IsUpperSet t) : s ⊆ t ∨ t ⊆ s

Full source

theorem IsUpperSet.total (hs : IsUpperSet s) (ht : IsUpperSet t) : s ⊆ ts ⊆ t ∨ t ⊆ s := by
  by_contra! h
  simp_rw [Set.not_subset] at h
  obtain ⟨⟨a, has, hat⟩, b, hbt, hbs⟩ := h
  obtain hab | hba := le_total a b
  · exact hbs (hs hab has)
  · exact hat (ht hba hbt)

Total Ordering of Upper Sets in a Linear Order

Informal description

For any two upper sets $s$ and $t$ in a linear order, either $s$ is a subset of $t$ or $t$ is a subset of $s$.

IsLowerSet.total theorem

(hs : IsLowerSet s) (ht : IsLowerSet t) : s ⊆ t ∨ t ⊆ s

Full source

theorem IsLowerSet.total (hs : IsLowerSet s) (ht : IsLowerSet t) : s ⊆ ts ⊆ t ∨ t ⊆ s :=
  hs.toDual.total ht.toDual

Total Ordering of Lower Sets in a Linear Order

Informal description

For any two lower sets $s$ and $t$ in a linear order, either $s$ is a subset of $t$ or $t$ is a subset of $s$.

TODO