Mathlib.Order.Interval.Finset.Basic

Finset.nonempty_Icc theorem

: (Icc a b).Nonempty ↔ a ≤ b

Full source

@[simp]
theorem nonempty_Icc : (Icc a b).Nonempty ↔ a ≤ b := by
  rw [← coe_nonempty, coe_Icc, Set.nonempty_Icc]

Nonemptiness of Closed Interval Finset Equivalent to $a \leq b$

Informal description

For any elements $a$ and $b$ in a locally finite order, the closed interval finset $\text{Icc}(a, b)$ is nonempty if and only if $a \leq b$.

Finset.nonempty_Ico theorem

: (Ico a b).Nonempty ↔ a < b

Full source

@[simp]
theorem nonempty_Ico : (Ico a b).Nonempty ↔ a < b := by
  rw [← coe_nonempty, coe_Ico, Set.nonempty_Ico]

Nonemptiness of Closed-Open Interval Finset Equivalent to Strict Inequality

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$, the closed-open interval finset $\text{Ico}(a, b)$ is nonempty if and only if $a < b$.

Finset.nonempty_Ioc theorem

: (Ioc a b).Nonempty ↔ a < b

Full source

@[simp]
theorem nonempty_Ioc : (Ioc a b).Nonempty ↔ a < b := by
  rw [← coe_nonempty, coe_Ioc, Set.nonempty_Ioc]

Nonemptiness of Open-Closed Interval Finset Equivalent to Strict Inequality

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$, the open-closed interval finset $\text{Ioc}(a, b)$ is nonempty if and only if $a < b$.

Finset.nonempty_Ioo theorem

[DenselyOrdered α] : (Ioo a b).Nonempty ↔ a < b

Full source

@[simp]
theorem nonempty_Ioo [DenselyOrdered α] : (Ioo a b).Nonempty ↔ a < b := by
  rw [← coe_nonempty, coe_Ioo, Set.nonempty_Ioo]

Nonempty Open Interval Finset Condition in Densely Ordered Sets

Informal description

In a densely ordered set $\alpha$, the open interval $(a, b)$ represented as a finset is nonempty if and only if $a < b$.

Finset.Icc_eq_empty_iff theorem

: Icc a b = ∅ ↔ ¬a ≤ b

Full source

@[simp]
theorem Icc_eq_empty_iff : IccIcc a b = ∅ ↔ ¬a ≤ b := by
  rw [← coe_eq_empty, coe_Icc, Set.Icc_eq_empty_iff]

Empty Closed Interval Criterion: $[a, b] = \emptyset \leftrightarrow a \nleq b$

Informal description

For any elements $a$ and $b$ in a preorder, the closed interval $[a, b]$ is empty if and only if $a$ is not less than or equal to $b$, i.e., $[a, b] = \emptyset \leftrightarrow a \nleq b$.

Finset.Ico_eq_empty_iff theorem

: Ico a b = ∅ ↔ ¬a < b

Full source

@[simp]
theorem Ico_eq_empty_iff : IcoIco a b = ∅ ↔ ¬a < b := by
  rw [← coe_eq_empty, coe_Ico, Set.Ico_eq_empty_iff]

Empty Closed-Open Interval Criterion: $\text{Ico}(a, b) = \emptyset \leftrightarrow a \geq b$

Informal description

For any elements $a$ and $b$ in a preorder, the closed-open interval finset $\text{Ico}(a, b)$ is empty if and only if $a \nless b$.

Finset.Ioc_eq_empty_iff theorem

: Ioc a b = ∅ ↔ ¬a < b

Full source

@[simp]
theorem Ioc_eq_empty_iff : IocIoc a b = ∅ ↔ ¬a < b := by
  rw [← coe_eq_empty, coe_Ioc, Set.Ioc_eq_empty_iff]

Empty Open-Closed Interval Criterion: $\text{Ioc}(a, b) = \emptyset \leftrightarrow a \geq b$

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$, the open-closed interval finset $\text{Ioc}(a, b)$ is empty if and only if $a \geq b$.

Finset.Ioo_eq_empty_iff theorem

[DenselyOrdered α] : Ioo a b = ∅ ↔ ¬a < b

Full source

@[simp]
theorem Ioo_eq_empty_iff [DenselyOrdered α] : IooIoo a b = ∅ ↔ ¬a < b := by
  rw [← coe_eq_empty, coe_Ioo, Set.Ioo_eq_empty_iff]

Empty Open Interval Finset Criterion in Densely Ordered Sets

Informal description

In a densely ordered set $\alpha$, the open interval finset $\text{Ioo}(a, b)$ is empty if and only if $a$ is not less than $b$, i.e., $\text{Ioo}(a, b) = \emptyset \leftrightarrow \neg (a < b)$.

Finset.Ioo_eq_empty theorem

(h : ¬a < b) : Ioo a b = ∅

Full source

@[simp]
theorem Ioo_eq_empty (h : ¬a < b) : Ioo a b = ∅ :=
  eq_empty_iff_forall_not_mem.2 fun _ hx => h ((mem_Ioo.1 hx).1.trans (mem_Ioo.1 hx).2)

Empty Open Interval Finset Condition: $\text{Ioo}(a, b) = \emptyset$ when $a \nless b$

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$, if $a$ is not less than $b$, then the open interval finset $\text{Ioo}(a, b)$ is empty.

Finset.Icc_eq_empty_of_lt theorem

(h : b < a) : Icc a b = ∅

Full source

@[simp]
theorem Icc_eq_empty_of_lt (h : b < a) : Icc a b = ∅ :=
  Icc_eq_empty h.not_le

Empty Closed Interval Finset Condition: $\text{Icc}(a, b) = \emptyset$ when $b < a$

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$, if $b < a$, then the closed interval finset $\text{Icc}(a, b)$ is empty.

Finset.Ico_eq_empty_of_le theorem

(h : b ≤ a) : Ico a b = ∅

Full source

@[simp]
theorem Ico_eq_empty_of_le (h : b ≤ a) : Ico a b = ∅ :=
  Ico_eq_empty h.not_lt

Empty Closed-Open Interval Finset Condition: $\text{Ico}(a, b) = \emptyset$ when $b \leq a$

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$, if $b \leq a$, then the closed-open interval finset $\text{Ico}(a, b)$ is empty.

Finset.Ioc_eq_empty_of_le theorem

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

Full source

@[simp]
theorem Ioc_eq_empty_of_le (h : b ≤ a) : Ioc a b = ∅ :=
  Ioc_eq_empty h.not_lt

Empty Open-Closed Interval Finset Condition: $\text{Ioc}(a, b) = \emptyset$ when $b \leq a$

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$, if $b \leq a$, then the open-closed interval finset $\text{Ioc}(a, b)$ is empty.

Finset.Ioo_eq_empty_of_le theorem

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

Full source

@[simp]
theorem Ioo_eq_empty_of_le (h : b ≤ a) : Ioo a b = ∅ :=
  Ioo_eq_empty h.not_lt

Empty Open Interval Finset Condition: $\text{Ioo}(a, b) = \emptyset$ when $b \leq a$

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$, if $b \leq a$, then the open interval finset $\text{Ioo}(a, b)$ is empty.

Finset.left_mem_Icc theorem

: a ∈ Icc a b ↔ a ≤ b

Full source

theorem left_mem_Icc : a ∈ Icc a ba ∈ Icc a b ↔ a ≤ b := by simp only [mem_Icc, true_and, le_rfl]

Left Endpoint Membership in Closed Interval

Informal description

For elements $a$ and $b$ in a locally finite order $\alpha$, the element $a$ belongs to the closed interval $[a, b]$ if and only if $a \leq b$.

Finset.left_mem_Ico theorem

: a ∈ Ico a b ↔ a < b

Full source

theorem left_mem_Ico : a ∈ Ico a ba ∈ Ico a b ↔ a < b := by simp only [mem_Ico, true_and, le_refl]

Left Endpoint Membership in Half-Open Interval: $a \in [a, b) \leftrightarrow a < b$

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$, the left endpoint $a$ belongs to the half-open interval $[a, b)$ if and only if $a < b$.

Finset.right_mem_Icc theorem

: b ∈ Icc a b ↔ a ≤ b

Full source

theorem right_mem_Icc : b ∈ Icc a bb ∈ Icc a b ↔ a ≤ b := by simp only [mem_Icc, and_true, le_rfl]

Right Endpoint Membership in Closed Interval

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$, the right endpoint $b$ belongs to the closed interval $[a, b]$ if and only if $a \leq b$.

Finset.right_mem_Ioc theorem

: b ∈ Ioc a b ↔ a < b

Full source

theorem right_mem_Ioc : b ∈ Ioc a bb ∈ Ioc a b ↔ a < b := by simp only [mem_Ioc, and_true, le_rfl]

Membership of Right Endpoint in Open-Closed Interval

Informal description

For elements $a$ and $b$ in a locally finite order $\alpha$, the element $b$ belongs to the open-closed interval $\text{Ioc}(a, b)$ if and only if $a < b$.

Finset.left_not_mem_Ioc theorem

: a ∉ Ioc a b

Full source

theorem left_not_mem_Ioc : a ∉ Ioc a b := fun h => lt_irrefl _ (mem_Ioc.1 h).1

Left Endpoint Not in Open-Closed Interval Finset: $a \notin \text{Ioc}(a, b)$

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$, the left endpoint $a$ does not belong to the open-closed interval finset $\text{Ioc}(a, b)$.

Finset.left_not_mem_Ioo theorem

: a ∉ Ioo a b

Full source

theorem left_not_mem_Ioo : a ∉ Ioo a b := fun h => lt_irrefl _ (mem_Ioo.1 h).1

Left Endpoint Not in Open Interval Finset: $a \notin \text{Ioo}(a, b)$

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$, the left endpoint $a$ does not belong to the open interval finset $\text{Ioo}(a, b)$.

Finset.right_not_mem_Ico theorem

: b ∉ Ico a b

Full source

theorem right_not_mem_Ico : b ∉ Ico a b := fun h => lt_irrefl _ (mem_Ico.1 h).2

Right Endpoint Not in Closed-Open Interval Finset: $b \notin \text{Ico}(a, b)$

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$, the element $b$ does not belong to the closed-open interval finset $\text{Ico}(a, b)$.

Finset.right_not_mem_Ioo theorem

: b ∉ Ioo a b

Full source

theorem right_not_mem_Ioo : b ∉ Ioo a b := fun h => lt_irrefl _ (mem_Ioo.1 h).2

Right Endpoint Not in Open Interval Finset: $b \notin \text{Ioo}(a, b)$

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$, the element $b$ does not belong to the open interval finset $\text{Ioo}(a, b)$.

Finset.Icc_subset_Icc theorem

(ha : a₂ ≤ a₁) (hb : b₁ ≤ b₂) : Icc a₁ b₁ ⊆ Icc a₂ b₂

Full source

@[gcongr]
theorem Icc_subset_Icc (ha : a₂ ≤ a₁) (hb : b₁ ≤ b₂) : IccIcc a₁ b₁ ⊆ Icc a₂ b₂ := by
  simpa [← coe_subset] using Set.Icc_subset_Icc ha hb

Inclusion of Closed Interval Finsets under Monotonicity Conditions: $\text{Icc}(a₁, b₁) \subseteq \text{Icc}(a₂, b₂)$ when $a₂ \leq a₁$ and $b₁ \leq b₂$

Informal description

For any elements $a₁, a₂, b₁, b₂$ in a locally finite order $\alpha$, if $a₂ \leq a₁$ and $b₁ \leq b₂$, then the closed interval finset $\text{Icc}(a₁, b₁)$ is a subset of the closed interval finset $\text{Icc}(a₂, b₂)$.

Finset.Ico_subset_Ico theorem

(ha : a₂ ≤ a₁) (hb : b₁ ≤ b₂) : Ico a₁ b₁ ⊆ Ico a₂ b₂

Full source

@[gcongr]
theorem Ico_subset_Ico (ha : a₂ ≤ a₁) (hb : b₁ ≤ b₂) : IcoIco a₁ b₁ ⊆ Ico a₂ b₂ := by
  simpa [← coe_subset] using Set.Ico_subset_Ico ha hb

Inclusion of Closed-Open Finset Intervals under Weakening Bounds

Informal description

For any elements $a₁, a₂, b₁, b₂$ in a locally finite order $\alpha$, if $a₂ \leq a₁$ and $b₁ \leq b₂$, then the closed-open interval finset $\text{Ico}(a₁, b₁)$ is a subset of the closed-open interval finset $\text{Ico}(a₂, b₂)$. In other words, $[a₁, b₁) \subseteq [a₂, b₂)$ under the given inequalities.

Finset.Ioc_subset_Ioc theorem

(ha : a₂ ≤ a₁) (hb : b₁ ≤ b₂) : Ioc a₁ b₁ ⊆ Ioc a₂ b₂

Full source

@[gcongr]
theorem Ioc_subset_Ioc (ha : a₂ ≤ a₁) (hb : b₁ ≤ b₂) : IocIoc a₁ b₁ ⊆ Ioc a₂ b₂ := by
  simpa [← coe_subset] using Set.Ioc_subset_Ioc ha hb

Inclusion of Open-Closed Interval Finsets under Endpoint Conditions

Informal description

For any elements $a₁, a₂, b₁, b₂$ in a locally finite order $\alpha$, if $a₂ \leq a₁$ and $b₁ \leq b₂$, then the open-closed interval finset $\text{Ioc}(a₁, b₁)$ is a subset of the interval finset $\text{Ioc}(a₂, b₂)$.

Finset.Ioo_subset_Ioo theorem

(ha : a₂ ≤ a₁) (hb : b₁ ≤ b₂) : Ioo a₁ b₁ ⊆ Ioo a₂ b₂

Full source

@[gcongr]
theorem Ioo_subset_Ioo (ha : a₂ ≤ a₁) (hb : b₁ ≤ b₂) : IooIoo a₁ b₁ ⊆ Ioo a₂ b₂ := by
  simpa [← coe_subset] using Set.Ioo_subset_Ioo ha hb

Monotonicity of Open Interval Finset Inclusion with Respect to Endpoints

Informal description

For any elements $a₁, a₂, b₁, b₂$ in a locally finite order $\alpha$, if $a₂ \leq a₁$ and $b₁ \leq b₂$, then the open interval finset $\text{Ioo}(a₁, b₁)$ is a subset of the open interval finset $\text{Ioo}(a₂, b₂)$.

Finset.Icc_subset_Icc_left theorem

(h : a₁ ≤ a₂) : Icc a₂ b ⊆ Icc a₁ b

Full source

@[gcongr]
theorem Icc_subset_Icc_left (h : a₁ ≤ a₂) : IccIcc a₂ b ⊆ Icc a₁ b :=
  Icc_subset_Icc h le_rfl

Left Endpoint Monotonicity of Closed Interval Finset Inclusion

Informal description

For any elements $a₁, a₂, b$ in a locally finite order $\alpha$, if $a₁ \leq a₂$, then the closed interval finset $\text{Icc}(a₂, b)$ is a subset of the closed interval finset $\text{Icc}(a₁, b)$.

Finset.Ico_subset_Ico_left theorem

(h : a₁ ≤ a₂) : Ico a₂ b ⊆ Ico a₁ b

Full source

@[gcongr]
theorem Ico_subset_Ico_left (h : a₁ ≤ a₂) : IcoIco a₂ b ⊆ Ico a₁ b :=
  Ico_subset_Ico h le_rfl

Left Endpoint Monotonicity of Closed-Open Interval Finset Inclusion

Informal description

For any elements $a₁, a₂, b$ in a locally finite order $\alpha$, if $a₁ \leq a₂$, then the closed-open interval finset $\text{Ico}(a₂, b)$ is a subset of the closed-open interval finset $\text{Ico}(a₁, b)$. In other words, $[a₂, b) \subseteq [a₁, b)$ when $a₁ \leq a₂$.

Finset.Ioc_subset_Ioc_left theorem

(h : a₁ ≤ a₂) : Ioc a₂ b ⊆ Ioc a₁ b

Full source

@[gcongr]
theorem Ioc_subset_Ioc_left (h : a₁ ≤ a₂) : IocIoc a₂ b ⊆ Ioc a₁ b :=
  Ioc_subset_Ioc h le_rfl

Left Endpoint Monotonicity of Open-Closed Interval Finset Inclusion

Informal description

For any elements $a₁, a₂, b$ in a locally finite order $\alpha$, if $a₁ \leq a₂$, then the open-closed interval finset $\text{Ioc}(a₂, b)$ is a subset of the interval finset $\text{Ioc}(a₁, b)$.

Finset.Ioo_subset_Ioo_left theorem

(h : a₁ ≤ a₂) : Ioo a₂ b ⊆ Ioo a₁ b

Full source

@[gcongr]
theorem Ioo_subset_Ioo_left (h : a₁ ≤ a₂) : IooIoo a₂ b ⊆ Ioo a₁ b :=
  Ioo_subset_Ioo h le_rfl

Left Endpoint Monotonicity of Open Interval Finset Inclusion

Informal description

For any elements $a₁, a₂, b$ in a locally finite order $\alpha$, if $a₁ \leq a₂$, then the open interval finset $\text{Ioo}(a₂, b)$ is a subset of the open interval finset $\text{Ioo}(a₁, b)$.

Finset.Icc_subset_Icc_right theorem

(h : b₁ ≤ b₂) : Icc a b₁ ⊆ Icc a b₂

Full source

@[gcongr]
theorem Icc_subset_Icc_right (h : b₁ ≤ b₂) : IccIcc a b₁ ⊆ Icc a b₂ :=
  Icc_subset_Icc le_rfl h

Right Monotonicity of Closed Interval Finsets: $\text{Icc}(a, b_1) \subseteq \text{Icc}(a, b_2)$ when $b_1 \leq b_2$

Informal description

For any elements $a, b_1, b_2$ in a locally finite order $\alpha$, if $b_1 \leq b_2$, then the closed interval finset $\text{Icc}(a, b_1)$ is a subset of the closed interval finset $\text{Icc}(a, b_2)$.

Finset.Ico_subset_Ico_right theorem

(h : b₁ ≤ b₂) : Ico a b₁ ⊆ Ico a b₂

Full source

@[gcongr]
theorem Ico_subset_Ico_right (h : b₁ ≤ b₂) : IcoIco a b₁ ⊆ Ico a b₂ :=
  Ico_subset_Ico le_rfl h

Right Weakening Preserves Closed-Open Interval Inclusion

Informal description

For any elements $a, b_1, b_2$ in a locally finite order $\alpha$, if $b_1 \leq b_2$, then the closed-open interval finset $\text{Ico}(a, b_1)$ is a subset of the closed-open interval finset $\text{Ico}(a, b_2)$. In other words, $[a, b_1) \subseteq [a, b_2)$ under the given inequality.

Finset.Ioc_subset_Ioc_right theorem

(h : b₁ ≤ b₂) : Ioc a b₁ ⊆ Ioc a b₂

Full source

@[gcongr]
theorem Ioc_subset_Ioc_right (h : b₁ ≤ b₂) : IocIoc a b₁ ⊆ Ioc a b₂ :=
  Ioc_subset_Ioc le_rfl h

Right Endpoint Monotonicity of Open-Closed Intervals

Informal description

For any elements $a, b_1, b_2$ in a locally finite order $\alpha$, if $b_1 \leq b_2$, then the open-closed interval $(a, b_1]$ is contained in the interval $(a, b_2]$.

Finset.Ioo_subset_Ioo_right theorem

(h : b₁ ≤ b₂) : Ioo a b₁ ⊆ Ioo a b₂

Full source

@[gcongr]
theorem Ioo_subset_Ioo_right (h : b₁ ≤ b₂) : IooIoo a b₁ ⊆ Ioo a b₂ :=
  Ioo_subset_Ioo le_rfl h

Right Endpoint Monotonicity of Open Interval Finset Inclusion

Informal description

For any elements $a, b_1, b_2$ in a locally finite order $\alpha$, if $b_1 \leq b_2$, then the open interval finset $\text{Ioo}(a, b_1)$ is a subset of the open interval finset $\text{Ioo}(a, b_2)$.

Finset.Ico_subset_Ioo_left theorem

(h : a₁ < a₂) : Ico a₂ b ⊆ Ioo a₁ b

Full source

theorem Ico_subset_Ioo_left (h : a₁ < a₂) : IcoIco a₂ b ⊆ Ioo a₁ b := by
  rw [← coe_subset, coe_Ico, coe_Ioo]
  exact Set.Ico_subset_Ioo_left h

Inclusion of Closed-Open Interval in Open Interval Under Left Endpoint Shift

Informal description

For any elements $a_1, a_2, b$ in a locally finite order $\alpha$, if $a_1 < a_2$, then the closed-open interval $[a_2, b)$ is contained in the open interval $(a_1, b)$.

Finset.Ioc_subset_Ioo_right theorem

(h : b₁ < b₂) : Ioc a b₁ ⊆ Ioo a b₂

Full source

theorem Ioc_subset_Ioo_right (h : b₁ < b₂) : IocIoc a b₁ ⊆ Ioo a b₂ := by
  rw [← coe_subset, coe_Ioc, coe_Ioo]
  exact Set.Ioc_subset_Ioo_right h

Inclusion of $(a, b₁]$ in $(a, b₂)$ for $b₁ < b₂$ in locally finite orders

Informal description

For any elements $a$, $b₁$, and $b₂$ in a locally finite order $\alpha$, if $b₁ < b₂$, then the finset $\text{Ioc}(a, b₁)$ is a subset of the finset $\text{Ioo}(a, b₂)$. In other words, the open-closed interval $(a, b₁]$ is contained within the open interval $(a, b₂)$ when $b₁ < b₂$.

Finset.Icc_subset_Ico_right theorem

(h : b₁ < b₂) : Icc a b₁ ⊆ Ico a b₂

Full source

theorem Icc_subset_Ico_right (h : b₁ < b₂) : IccIcc a b₁ ⊆ Ico a b₂ := by
  rw [← coe_subset, coe_Icc, coe_Ico]
  exact Set.Icc_subset_Ico_right h

Inclusion of Closed Interval in Closed-Open Interval Under Right Endpoint Expansion

Informal description

For any elements $a, b_1, b_2$ in a locally finite order $\alpha$, if $b_1 < b_2$, then the closed interval $[a, b_1]$ is contained in the closed-open interval $[a, b_2)$.

Finset.Ioo_subset_Ico_self theorem

: Ioo a b ⊆ Ico a b

Full source

theorem Ioo_subset_Ico_self : IooIoo a b ⊆ Ico a b := by
  rw [← coe_subset, coe_Ioo, coe_Ico]
  exact Set.Ioo_subset_Ico_self

Inclusion of Open Interval in Closed-Open Interval: $\text{Ioo}(a, b) \subseteq \text{Ico}(a, b)$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the open interval $(a, b)$ is a subset of the left-closed right-open interval $[a, b)$. In other words, $\text{Ioo}(a, b) \subseteq \text{Ico}(a, b)$.

Finset.Ioo_subset_Ioc_self theorem

: Ioo a b ⊆ Ioc a b

Full source

theorem Ioo_subset_Ioc_self : IooIoo a b ⊆ Ioc a b := by
  rw [← coe_subset, coe_Ioo, coe_Ioc]
  exact Set.Ioo_subset_Ioc_self

Inclusion of Open Interval in Open-Closed Interval: $\text{Ioo}(a, b) \subseteq \text{Ioc}(a, b)$

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$, the open interval finset $\text{Ioo}(a, b)$ is a subset of the open-closed interval finset $\text{Ioc}(a, b)$. In other words, every element $x$ satisfying $a < x < b$ also satisfies $a < x \leq b$.

Finset.Ico_subset_Icc_self theorem

: Ico a b ⊆ Icc a b

Full source

theorem Ico_subset_Icc_self : IcoIco a b ⊆ Icc a b := by
  rw [← coe_subset, coe_Ico, coe_Icc]
  exact Set.Ico_subset_Icc_self

Inclusion of Closed-Open Interval in Closed Interval: $\text{Ico}(a, b) \subseteq \text{Icc}(a, b)$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the closed-open interval finset $\text{Ico}(a, b)$ is a subset of the closed interval finset $\text{Icc}(a, b)$. In other words, every element $x$ satisfying $a \leq x < b$ also satisfies $a \leq x \leq b$.

Finset.Ioc_subset_Icc_self theorem

: Ioc a b ⊆ Icc a b

Full source

theorem Ioc_subset_Icc_self : IocIoc a b ⊆ Icc a b := by
  rw [← coe_subset, coe_Ioc, coe_Icc]
  exact Set.Ioc_subset_Icc_self

Inclusion of Open-Closed Interval in Closed Interval Finset: $\text{Ioc}(a, b) \subseteq \text{Icc}(a, b)$

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$, the open-closed interval finset $\text{Ioc}(a, b)$ is a subset of the closed interval finset $\text{Icc}(a, b)$. In other words, every element $x$ satisfying $a < x \leq b$ also satisfies $a \leq x \leq b$.

Finset.Ioo_subset_Icc_self theorem

: Ioo a b ⊆ Icc a b

Full source

theorem Ioo_subset_Icc_self : IooIoo a b ⊆ Icc a b :=
  Ioo_subset_Ico_self.trans Ico_subset_Icc_self

Inclusion of Open Interval in Closed Interval: $\text{Ioo}(a, b) \subseteq \text{Icc}(a, b)$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the open interval finset $\text{Ioo}(a, b)$ is a subset of the closed interval finset $\text{Icc}(a, b)$. In other words, every element $x$ satisfying $a < x < b$ also satisfies $a \leq x \leq b$.

Finset.Icc_subset_Icc_iff theorem

(h₁ : a₁ ≤ b₁) : Icc a₁ b₁ ⊆ Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂

Full source

theorem Icc_subset_Icc_iff (h₁ : a₁ ≤ b₁) : IccIcc a₁ b₁ ⊆ Icc a₂ b₂Icc a₁ b₁ ⊆ Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂ := by
  rw [← coe_subset, coe_Icc, coe_Icc, Set.Icc_subset_Icc_iff h₁]

Subset Condition for Closed Interval Finsets: $\text{Icc}(a_1, b_1) \subseteq \text{Icc}(a_2, b_2) \iff a_2 \leq a_1 \leq b_1 \leq b_2$

Informal description

For any elements $a_1, b_1, a_2, b_2$ in a preorder $\alpha$ such that $a_1 \leq b_1$, the closed interval finset $\text{Icc}(a_1, b_1)$ is a subset of the closed interval finset $\text{Icc}(a_2, b_2)$ if and only if $a_2 \leq a_1$ and $b_1 \leq b_2$.

Finset.Icc_subset_Ioo_iff theorem

(h₁ : a₁ ≤ b₁) : Icc a₁ b₁ ⊆ Ioo a₂ b₂ ↔ a₂ < a₁ ∧ b₁ < b₂

Full source

theorem Icc_subset_Ioo_iff (h₁ : a₁ ≤ b₁) : IccIcc a₁ b₁ ⊆ Ioo a₂ b₂Icc a₁ b₁ ⊆ Ioo a₂ b₂ ↔ a₂ < a₁ ∧ b₁ < b₂ := by
  rw [← coe_subset, coe_Icc, coe_Ioo, Set.Icc_subset_Ioo_iff h₁]

Closed Finset Interval Subset of Open Finset Interval Criterion

Informal description

For any elements $a₁, b₁$ in a locally finite order with $a₁ \leq b₁$, the closed interval finset $\text{Icc}(a₁, b₁)$ is a subset of the open interval finset $\text{Ioo}(a₂, b₂)$ if and only if $a₂ < a₁$ and $b₁ < b₂$.

Finset.Icc_subset_Ico_iff theorem

(h₁ : a₁ ≤ b₁) : Icc a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ < b₂

Full source

theorem Icc_subset_Ico_iff (h₁ : a₁ ≤ b₁) : IccIcc a₁ b₁ ⊆ Ico a₂ b₂Icc a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ < b₂ := by
  rw [← coe_subset, coe_Icc, coe_Ico, Set.Icc_subset_Ico_iff h₁]

Subset Criterion for Closed Interval in Closed-Open Interval: $\text{Icc}(a₁, b₁) \subseteq \text{Ico}(a₂, b₂) \leftrightarrow a₂ \leq a₁ \land b₁ < b₂$

Informal description

For any elements $a₁, b₁, a₂, b₂$ in a locally finite order $\alpha$ with $a₁ \leq b₁$, the closed interval finset $\text{Icc}(a₁, b₁)$ is a subset of the closed-open interval finset $\text{Ico}(a₂, b₂)$ if and only if $a₂ \leq a₁$ and $b₁ < b₂$.

Finset.Icc_subset_Ioc_iff theorem

(h₁ : a₁ ≤ b₁) : Icc a₁ b₁ ⊆ Ioc a₂ b₂ ↔ a₂ < a₁ ∧ b₁ ≤ b₂

Full source

theorem Icc_subset_Ioc_iff (h₁ : a₁ ≤ b₁) : IccIcc a₁ b₁ ⊆ Ioc a₂ b₂Icc a₁ b₁ ⊆ Ioc a₂ b₂ ↔ a₂ < a₁ ∧ b₁ ≤ b₂ :=
  (Icc_subset_Ico_iff h₁.dual).trans and_comm

Subset Criterion for Closed Interval in Open-Closed Interval: $\text{Icc}(a₁, b₁) \subseteq \text{Ioc}(a₂, b₂) \leftrightarrow a₂ < a₁ \land b₁ \leq b₂$

Informal description

For any elements $a₁, b₁, a₂, b₂$ in a locally finite order $\alpha$ with $a₁ \leq b₁$, the closed interval finset $\text{Icc}(a₁, b₁)$ is a subset of the open-closed interval finset $\text{Ioc}(a₂, b₂)$ if and only if $a₂ < a₁$ and $b₁ \leq b₂$.

Finset.Icc_ssubset_Icc_left theorem

(hI : a₂ ≤ b₂) (ha : a₂ < a₁) (hb : b₁ ≤ b₂) : Icc a₁ b₁ ⊂ Icc a₂ b₂

Full source

theorem Icc_ssubset_Icc_left (hI : a₂ ≤ b₂) (ha : a₂ < a₁) (hb : b₁ ≤ b₂) :
    IccIcc a₁ b₁ ⊂ Icc a₂ b₂ := by
  rw [← coe_ssubset, coe_Icc, coe_Icc]
  exact Set.Icc_ssubset_Icc_left hI ha hb

Proper Subset Relation for Closed Intervals under Left Endpoint Strict Inequality

Informal description

For any elements $a_1, a_2, b_1, b_2$ in a locally finite order $\alpha$ with $a_2 \leq b_2$, if $a_2 < a_1$ and $b_1 \leq b_2$, then the closed interval $[a_1, b_1]$ is a proper subset of the closed interval $[a_2, b_2]$.

Finset.Icc_ssubset_Icc_right theorem

(hI : a₂ ≤ b₂) (ha : a₂ ≤ a₁) (hb : b₁ < b₂) : Icc a₁ b₁ ⊂ Icc a₂ b₂

Full source

theorem Icc_ssubset_Icc_right (hI : a₂ ≤ b₂) (ha : a₂ ≤ a₁) (hb : b₁ < b₂) :
    IccIcc a₁ b₁ ⊂ Icc a₂ b₂ := by
  rw [← coe_ssubset, coe_Icc, coe_Icc]
  exact Set.Icc_ssubset_Icc_right hI ha hb

Proper Subset Relation for Closed Intervals under Right Endpoint Strict Inequality

Informal description

For any elements $a₁, a₂, b₁, b₂$ in a preorder $\alpha$ such that $a₂ \leq b₂$, if $a₂ \leq a₁$ and $b₁ < b₂$, then the closed interval $[a₁, b₁]$ is a proper subset of the closed interval $[a₂, b₂]$. That is, $[a₁, b₁] \subsetneq [a₂, b₂]$.

Finset.Ioc_disjoint_Ioc_of_le theorem

{d : α} (hbc : b ≤ c) : Disjoint (Ioc a b) (Ioc c d)

Full source

@[simp]
theorem Ioc_disjoint_Ioc_of_le {d : α} (hbc : b ≤ c) : Disjoint (Ioc a b) (Ioc c d) :=
  disjoint_left.2 fun _ h1 h2 ↦ not_and_of_not_left _
    ((mem_Ioc.1 h1).2.trans hbc).not_lt (mem_Ioc.1 h2)

Disjointness of Open-Closed Intervals Under Order Condition

Informal description

For any elements $a, b, c, d$ in a locally finite order $\alpha$, if $b \leq c$, then the open-closed interval finsets $\text{Ioc}(a, b)$ and $\text{Ioc}(c, d)$ are disjoint. That is, $(a, b] \cap (c, d] = \emptyset$ when $b \leq c$.

Finset.Ico_self theorem

: Ico a a = ∅

Full source

theorem Ico_self : Ico a a = ∅ :=
  Ico_eq_empty <| lt_irrefl _

Empty Half-Open Interval at a Point

Informal description

For any element $a$ in a locally finite order, the half-open interval finset $[a, a)$ is empty, i.e., $\text{Ico}(a, a) = \emptyset$.

Finset.Ioc_self theorem

: Ioc a a = ∅

Full source

theorem Ioc_self : Ioc a a = ∅ :=
  Ioc_eq_empty <| lt_irrefl _

Empty Open-Closed Interval at a Point

Informal description

For any element $a$ in a locally finite order, the open-closed interval finset $\text{Ioc}(a, a)$ is empty, i.e., $(a, a] = \emptyset$.

Finset.Ioo_self theorem

: Ioo a a = ∅

Full source

theorem Ioo_self : Ioo a a = ∅ :=
  Ioo_eq_empty <| lt_irrefl _

Empty Open Interval at a Point

Informal description

For any element $a$ in a locally finite order, the open interval finset $\text{Ioo}(a, a)$ is empty, i.e., $\text{Ioo}(a, a) = \emptyset$.

Set.fintypeOfMemBounds definition

{s : Set α} [DecidablePred (· ∈ s)] (ha : a ∈ lowerBounds s) (hb : b ∈ upperBounds s) : Fintype s

Full source

/-- A set with upper and lower bounds in a locally finite order is a fintype -/
def _root_.Set.fintypeOfMemBounds {s : Set α} [DecidablePred (· ∈ s)] (ha : a ∈ lowerBounds s)
    (hb : b ∈ upperBounds s) : Fintype s :=
  Set.fintypeSubset (Set.Icc a b) fun _ hx => ⟨ha hx, hb hx⟩

Finiteness of bounded sets in locally finite orders

Informal description

For a set $s$ in a locally finite order $\alpha$, if $a$ is a lower bound and $b$ is an upper bound of $s$, then $s$ is a finite set. This is constructed by showing that $s$ is a subset of the finite interval $[a, b]$.

Finset.Ico_filter_lt_of_le_left theorem

[DecidablePred (· < c)] (hca : c ≤ a) : {x ∈ Ico a b | x < c} = ∅

Full source

theorem Ico_filter_lt_of_le_left [DecidablePred (· < c)] (hca : c ≤ a) :
    {x ∈ Ico a b | x < c} = ∅ :=
  filter_false_of_mem fun _ hx => (hca.trans (mem_Ico.1 hx).1).not_lt

Empty Filtered Closed-Open Interval for Left-Leaning Condition

Informal description

For a locally finite order $\alpha$ and elements $a, b, c \in \alpha$ with $c \leq a$, the set $\{x \in \text{Ico}(a, b) \mid x < c\}$ is empty.

Finset.Ico_filter_lt_of_right_le theorem

[DecidablePred (· < c)] (hbc : b ≤ c) : {x ∈ Ico a b | x < c} = Ico a b

Full source

theorem Ico_filter_lt_of_right_le [DecidablePred (· < c)] (hbc : b ≤ c) :
    {x ∈ Ico a b | x < c} = Ico a b :=
  filter_true_of_mem fun _ hx => (mem_Ico.1 hx).2.trans_le hbc

Filtered Closed-Open Interval Equals Original When Upper Bound is Below Filter Condition

Informal description

For a locally finite order $\alpha$ and elements $a, b, c \in \alpha$ with $b \leq c$, the filtered set $\{x \in \text{Ico}(a, b) \mid x < c\}$ is equal to the original interval $\text{Ico}(a, b)$.

Finset.Ico_filter_lt_of_le_right theorem

[DecidablePred (· < c)] (hcb : c ≤ b) : {x ∈ Ico a b | x < c} = Ico a c

Full source

theorem Ico_filter_lt_of_le_right [DecidablePred (· < c)] (hcb : c ≤ b) :
    {x ∈ Ico a b | x < c} = Ico a c := by
  ext x
  rw [mem_filter, mem_Ico, mem_Ico, and_right_comm]
  exact and_iff_left_of_imp fun h => h.2.trans_le hcb

Filtered Closed-Open Interval Equals Smaller Interval When Filter Condition is Met

Informal description

For a locally finite order $\alpha$ and elements $a, b, c \in \alpha$ with $c \leq b$, the set $\{x \in \text{Ico}(a, b) \mid x < c\}$ is equal to $\text{Ico}(a, c)$.

Finset.Ico_filter_le_of_le_left theorem

{a b c : α} [DecidablePred (c ≤ ·)] (hca : c ≤ a) : {x ∈ Ico a b | c ≤ x} = Ico a b

Full source

theorem Ico_filter_le_of_le_left {a b c : α} [DecidablePred (c ≤ ·)] (hca : c ≤ a) :
    {x ∈ Ico a b | c ≤ x} = Ico a b :=
  filter_true_of_mem fun _ hx => hca.trans (mem_Ico.1 hx).1

Filtering Closed-Open Interval with Lower Bound Below Interval Start

Informal description

Let $\alpha$ be a locally finite order with elements $a, b, c \in \alpha$. If $c \leq a$, then the set $\{x \in \text{Ico}(a, b) \mid c \leq x\}$ is equal to $\text{Ico}(a, b)$.

Finset.Ico_filter_le_of_right_le theorem

{a b : α} [DecidablePred (b ≤ ·)] : {x ∈ Ico a b | b ≤ x} = ∅

Full source

theorem Ico_filter_le_of_right_le {a b : α} [DecidablePred (b ≤ ·)] :
    {x ∈ Ico a b | b ≤ x} = ∅ :=
  filter_false_of_mem fun _ hx => (mem_Ico.1 hx).2.not_le

Emptyness of Closed-Open Interval Filtered by Upper Bound

Informal description

For any elements $a, b$ in a locally finite order $\alpha$, the set $\{x \in \text{Ico}(a, b) \mid b \leq x\}$ is empty.

Finset.Ico_filter_le_of_left_le theorem

{a b c : α} [DecidablePred (c ≤ ·)] (hac : a ≤ c) : {x ∈ Ico a b | c ≤ x} = Ico c b

Full source

theorem Ico_filter_le_of_left_le {a b c : α} [DecidablePred (c ≤ ·)] (hac : a ≤ c) :
    {x ∈ Ico a b | c ≤ x} = Ico c b := by
  ext x
  rw [mem_filter, mem_Ico, mem_Ico, and_comm, and_left_comm]
  exact and_iff_right_of_imp fun h => hac.trans h.1

Filtered Closed-Open Interval Equals Smaller Interval When Filter Bound is Within Original Bounds

Informal description

For any elements $a, b, c$ in a locally finite order $\alpha$ with a decidable predicate for elements greater than or equal to $c$, if $a \leq c$, then the filtered set $\{x \in \text{Ico}(a, b) \mid c \leq x\}$ is equal to $\text{Ico}(c, b)$.

Finset.Icc_filter_lt_of_lt_right theorem

{a b c : α} [DecidablePred (· < c)] (h : b < c) : {x ∈ Icc a b | x < c} = Icc a b

Full source

theorem Icc_filter_lt_of_lt_right {a b c : α} [DecidablePred (· < c)] (h : b < c) :
    {x ∈ Icc a b | x < c} = Icc a b :=
  filter_true_of_mem fun _ hx => lt_of_le_of_lt (mem_Icc.1 hx).2 h

Filtering Closed Interval by Less Than Condition Preserves Interval When Upper Bound is Less Than Filter Value

Informal description

For any elements $a, b, c$ in a locally finite order $\alpha$ with a decidable predicate for elements less than $c$, if $b < c$, then the set $\{x \in \text{Icc}(a, b) \mid x < c\}$ is equal to $\text{Icc}(a, b)$.

Finset.Ioc_filter_lt_of_lt_right theorem

{a b c : α} [DecidablePred (· < c)] (h : b < c) : {x ∈ Ioc a b | x < c} = Ioc a b

Full source

theorem Ioc_filter_lt_of_lt_right {a b c : α} [DecidablePred (· < c)] (h : b < c) :
    {x ∈ Ioc a b | x < c} = Ioc a b :=
  filter_true_of_mem fun _ hx => lt_of_le_of_lt (mem_Ioc.1 hx).2 h

Filtering Open-Closed Interval by Less Than Condition Preserves Interval

Informal description

For elements $a, b, c$ in a locally finite order $\alpha$ with a decidable predicate for elements less than $c$, if $b < c$, then the set $\{x \in \text{Ioc}(a, b) \mid x < c\}$ is equal to $\text{Ioc}(a, b)$.

Finset.Iic_filter_lt_of_lt_right theorem

 {α} [Preorder α] [LocallyFiniteOrderBot α] {a c : α} [DecidablePred (· < c)] (h : a < c) : {x ∈ Iic a | x < c} = Iic a

Full source

theorem Iic_filter_lt_of_lt_right {α} [Preorder α] [LocallyFiniteOrderBot α] {a c : α}
    [DecidablePred (· < c)] (h : a < c) : {x ∈ Iic a | x < c} = Iic a :=
  filter_true_of_mem fun _ hx => lt_of_le_of_lt (mem_Iic.1 hx) h

Filtering Lower-Closed Interval by Less Than Condition Preserves Interval

Informal description

Let $\alpha$ be a preorder with a locally finite order structure where all lower-bounded intervals are finite. For any elements $a, c \in \alpha$ with $a < c$, the filtered set $\{x \in \text{Iic}(a) \mid x < c\}$ is equal to $\text{Iic}(a)$.

Finset.filter_lt_lt_eq_Ioo theorem

[DecidablePred fun j => a < j ∧ j < b] : ({j | a < j ∧ j < b} : Finset _) = Ioo a b

Full source

theorem filter_lt_lt_eq_Ioo [DecidablePred fun j => a < j ∧ j < b] :
    ({j | a < j ∧ j < b} : Finset _) = Ioo a b := by ext; simp

Filtering Yields Open Interval Finset: $\{j \mid a < j < b\} = \text{Ioo}(a, b)$

Informal description

For a locally finite order $\alpha$ and elements $a, b \in \alpha$, the finset obtained by filtering elements $j$ such that $a < j < b$ is equal to the open interval finset $\text{Ioo}(a, b)$.

Finset.filter_lt_le_eq_Ioc theorem

[DecidablePred fun j => a < j ∧ j ≤ b] : ({j | a < j ∧ j ≤ b} : Finset _) = Ioc a b

Full source

theorem filter_lt_le_eq_Ioc [DecidablePred fun j => a < j ∧ j ≤ b] :
    ({j | a < j ∧ j ≤ b} : Finset _) = Ioc a b := by ext; simp

Filtering Elements Yields Open-Closed Interval Finset

Informal description

For a locally finite order $\alpha$ and elements $a, b \in \alpha$, the finset obtained by filtering elements $j$ such that $a < j \leq b$ is equal to the open-closed interval finset $\text{Ioc}(a, b)$.

Finset.filter_le_lt_eq_Ico theorem

[DecidablePred fun j => a ≤ j ∧ j < b] : ({j | a ≤ j ∧ j < b} : Finset _) = Ico a b

Full source

theorem filter_le_lt_eq_Ico [DecidablePred fun j => a ≤ j ∧ j < b] :
    ({j | a ≤ j ∧ j < b} : Finset _) = Ico a b := by ext; simp

Filtering Yields Closed-Open Interval Finset

Informal description

For a locally finite order $\alpha$ and elements $a, b \in \alpha$, the finset obtained by filtering elements $j$ such that $a \leq j < b$ is equal to the closed-open interval finset $\text{Ico}(a, b)$.

Finset.filter_le_le_eq_Icc theorem

[DecidablePred fun j => a ≤ j ∧ j ≤ b] : ({j | a ≤ j ∧ j ≤ b} : Finset _) = Icc a b

Full source

theorem filter_le_le_eq_Icc [DecidablePred fun j => a ≤ j ∧ j ≤ b] :
    ({j | a ≤ j ∧ j ≤ b} : Finset _) = Icc a b := by ext; simp

Filtered Elements Equal Closed Interval Finset

Informal description

For a locally finite order $\alpha$ and elements $a, b \in \alpha$, the finset obtained by filtering elements $j$ such that $a \leq j \leq b$ is equal to the closed interval finset $\text{Icc}(a, b)$.

Finset.Ioi_eq_empty theorem

: Ioi a = ∅ ↔ IsMax a

Full source

@[simp]
theorem Ioi_eq_empty : IoiIoi a = ∅ ↔ IsMax a := by
  rw [← coe_eq_empty, coe_Ioi, Set.Ioi_eq_empty_iff]

Empty Open Infinite Interval Characterizes Maximal Elements

Informal description

For an element $a$ in a locally finite order with finite intervals bounded below, the open infinite interval $(a, \infty)$ represented as a finset is empty if and only if $a$ is a maximal element.

Finset.Ioi_nonempty theorem

: (Ioi a).Nonempty ↔ ¬IsMax a

Full source

@[simp] lemma Ioi_nonempty : (Ioi a).Nonempty ↔ ¬ IsMax a := by simp [nonempty_iff_ne_empty]

Nonemptiness of Open Infinite Interval $(a, \infty)$ Equivalent to Non-Maximality of $a$

Informal description

For an element $a$ in a locally finite order with finite intervals bounded below, the open infinite interval $(a, \infty)$ represented as a finset is nonempty if and only if $a$ is not a maximal element.

Finset.Ioi_top theorem

[OrderTop α] : Ioi (⊤ : α) = ∅

Full source

theorem Ioi_top [OrderTop α] : Ioi (⊤ : α) = ∅ := Ioi_eq_empty.mpr isMax_top

Empty Open Infinite Interval at Top Element: $\text{Ioi}(\top) = \emptyset$

Informal description

In an order with a greatest element $\top$, the open infinite interval $(\top, \infty)$ is empty, i.e., $\text{Ioi}(\top) = \emptyset$.

Finset.Ici_bot theorem

[OrderBot α] [Fintype α] : Ici (⊥ : α) = univ

Full source

@[simp]
theorem Ici_bot [OrderBot α] [Fintype α] : Ici (⊥ : α) = univ := by
  ext a; simp only [mem_Ici, bot_le, mem_univ]

Closed-infinite interval at bottom equals universal set in finite order

Informal description

In a finite order `α` with a bottom element `⊥`, the closed-infinite interval `Ici(⊥)` consisting of all elements greater than or equal to `⊥` is equal to the entire set of elements in `α` (denoted by `univ`). That is, $\text{Ici}(\bot) = \text{univ}$.

Finset.nonempty_Ici theorem

: (Ici a).Nonempty

Full source

@[simp, aesop safe apply (rule_sets := [finsetNonempty])]
lemma nonempty_Ici : (Ici a).Nonempty := ⟨a, mem_Ici.2 le_rfl⟩

Nonemptiness of Closed-Infinite Interval $\text{Ici}(a)$

Informal description

For any element $a$ in a locally finite order with finite intervals bounded below, the closed-infinite interval $\text{Ici}(a) = \{x \mid a \leq x\}$ is nonempty.

Finset.nonempty_Ioi theorem

: (Ioi a).Nonempty ↔ ¬IsMax a

Full source

lemma nonempty_Ioi : (Ioi a).Nonempty ↔ ¬ IsMax a := by simp [Finset.Nonempty]

Nonemptiness of Open Infinite Interval Equivalent to Non-Maximality

Informal description

The open infinite interval $(a, \infty)$ is nonempty if and only if $a$ is not a maximal element in the order.

Finset.Ici_subset_Ici theorem

: Ici a ⊆ Ici b ↔ b ≤ a

Full source

@[simp]
theorem Ici_subset_Ici : IciIci a ⊆ Ici bIci a ⊆ Ici b ↔ b ≤ a := by
  simp [← coe_subset]

Subset Condition for Closed-Infinite Intervals: $[a, \infty) \subseteq [b, \infty) \leftrightarrow b \leq a$

Informal description

For any elements $a$ and $b$ in a locally finite order with finite intervals bounded below, the closed-infinite interval $[a, \infty)$ is a subset of $[b, \infty)$ if and only if $b \leq a$.

Finset.Ici_ssubset_Ici theorem

: Ici a ⊂ Ici b ↔ b < a

Full source

@[simp]
theorem Ici_ssubset_Ici : IciIci a ⊂ Ici bIci a ⊂ Ici b ↔ b < a := by
  simp [← coe_ssubset]

Strict subset relation between closed-infinite intervals: $[a, \infty) \subset [b, \infty) \leftrightarrow b < a$

Informal description

For elements $a$ and $b$ in a locally finite order with finite intervals bounded below, the closed-infinite interval $[a, \infty)$ is a strict subset of $[b, \infty)$ if and only if $b < a$.

Finset.Ioi_subset_Ioi theorem

(h : a ≤ b) : Ioi b ⊆ Ioi a

Full source

@[gcongr]
theorem Ioi_subset_Ioi (h : a ≤ b) : IoiIoi b ⊆ Ioi a := by
  simpa [← coe_subset] using Set.Ioi_subset_Ioi h

Monotonicity of Right-Infinite Open Intervals: $(b, \infty) \subseteq (a, \infty)$ when $a \leq b$

Informal description

For any elements $a$ and $b$ in a preorder, if $a \leq b$, then the open right-infinite interval $(b, \infty)$ is a subset of the open right-infinite interval $(a, \infty)$.

Finset.Ioi_ssubset_Ioi theorem

(h : a < b) : Ioi b ⊂ Ioi a

Full source

@[gcongr]
theorem Ioi_ssubset_Ioi (h : a < b) : IoiIoi b ⊂ Ioi a := by
  simpa [← coe_ssubset] using Set.Ioi_ssubset_Ioi h

Proper Subset Relation for Right-Infinite Open Intervals: $(b, \infty) \subset (a, \infty)$ when $a < b$

Informal description

For any elements $a$ and $b$ in a preorder, if $a < b$, then the open right-infinite interval $(b, \infty)$ is a proper subset of $(a, \infty)$.

Finset.Icc_subset_Ici_self theorem

: Icc a b ⊆ Ici a

Full source

theorem Icc_subset_Ici_self : IccIcc a b ⊆ Ici a := by
  simpa [← coe_subset] using Set.Icc_subset_Ici_self

Inclusion of Closed Interval in Left-Closed Right-Infinite Interval: $[a, b] \subseteq [a, \infty)$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the closed interval $[a, b]$ is a subset of the left-closed right-infinite interval $[a, \infty)$.

Finset.Ico_subset_Ici_self theorem

: Ico a b ⊆ Ici a

Full source

theorem Ico_subset_Ici_self : IcoIco a b ⊆ Ici a := by
  simpa [← coe_subset] using Set.Ico_subset_Ici_self

Inclusion of Closed-Open Interval in Closed-Infinite Interval: $[a, b) \subseteq [a, \infty)$

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$, the closed-open interval $[a, b)$ is a subset of the closed-infinite interval $[a, \infty)$. In other words, $[a, b) \subseteq [a, \infty)$.

Finset.Ioc_subset_Ioi_self theorem

: Ioc a b ⊆ Ioi a

Full source

theorem Ioc_subset_Ioi_self : IocIoc a b ⊆ Ioi a := by
  simpa [← coe_subset] using Set.Ioc_subset_Ioi_self

Inclusion of $(a, b]$ in $(a, \infty)$ for finsets in a locally finite order

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$, the open-closed interval finset $\text{Ioc}(a, b)$ is a subset of the open-infinite interval finset $\text{Ioi}(a)$. In other words, every element $x$ satisfying $a < x \leq b$ also satisfies $a < x$.

Finset.Ioo_subset_Ioi_self theorem

: Ioo a b ⊆ Ioi a

Full source

theorem Ioo_subset_Ioi_self : IooIoo a b ⊆ Ioi a := by
  simpa [← coe_subset] using Set.Ioo_subset_Ioi_self

Open Interval Subset of Left-Open Infinite Interval in Finsets

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$, the open interval finset $\text{Ioo}(a, b)$ is a subset of the left-open right-infinite interval finset $\text{Ioi}(a)$. In other words, every element $x$ satisfying $a < x < b$ also satisfies $a < x$.

Finset.Ioc_subset_Ici_self theorem

: Ioc a b ⊆ Ici a

Full source

theorem Ioc_subset_Ici_self : IocIoc a b ⊆ Ici a :=
  Ioc_subset_Icc_self.trans Icc_subset_Ici_self

Inclusion of Open-Closed Interval in Closed-Infinite Interval Finset: $\text{Ioc}(a, b) \subseteq \text{Ici}(a)$

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$, the open-closed interval finset $\text{Ioc}(a, b)$ is a subset of the closed-infinite interval finset $\text{Ici}(a)$. In other words, every element $x$ satisfying $a < x \leq b$ also satisfies $a \leq x$.

Finset.Ioo_subset_Ici_self theorem

: Ioo a b ⊆ Ici a

Full source

theorem Ioo_subset_Ici_self : IooIoo a b ⊆ Ici a :=
  Ioo_subset_Ico_self.trans Ico_subset_Ici_self

Inclusion of Open Interval in Closed-Infinite Interval: $(a, b) \subseteq [a, \infty)$

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$, the open interval $(a, b)$ is a subset of the closed-infinite interval $[a, \infty)$. In other words, every element $x$ satisfying $a < x < b$ also satisfies $a \leq x$.

Finset.Iio_eq_empty theorem

: Iio a = ∅ ↔ IsMin a

Full source

@[simp]
theorem Iio_eq_empty : IioIio a = ∅ ↔ IsMin a := Ioi_eq_empty (α := αᵒᵈ)

Empty Lower Interval Characterizes Minimal Elements

Informal description

For an element $a$ in a locally finite order with finite lower-bounded intervals, the open lower interval $\{x \mid x < a\}$ is empty if and only if $a$ is a minimal element.

Finset.Iio_nonempty theorem

: (Iio a).Nonempty ↔ ¬IsMin a

Full source

@[simp] lemma Iio_nonempty : (Iio a).Nonempty ↔ ¬ IsMin a := by simp [nonempty_iff_ne_empty]

Nonemptiness of Open Lower Interval Equivalent to Non-Minimality

Informal description

For an element $a$ in a locally finite order with finite lower-bounded intervals, the open lower interval $\text{Iio}(a)$ is nonempty if and only if $a$ is not a minimal element.

Finset.Iio_bot theorem

[OrderBot α] : Iio (⊥ : α) = ∅

Full source

theorem Iio_bot [OrderBot α] : Iio (⊥ : α) = ∅ := Iio_eq_empty.mpr isMin_bot

Empty Lower Interval at Bottom Element

Informal description

In an order with a bottom element $\bot$, the open lower interval $\text{Iio}(\bot)$ is empty.

Finset.Iic_top theorem

[OrderTop α] [Fintype α] : Iic (⊤ : α) = univ

Full source

@[simp]
theorem Iic_top [OrderTop α] [Fintype α] : Iic (⊤ : α) = univ := by
  ext a; simp only [mem_Iic, le_top, mem_univ]

Lower-Closed Interval at Top Equals Universal Set in Finite Order

Informal description

In a finite order with a greatest element $\top$, the lower-closed interval $\text{Iic}(\top)$ consisting of all elements less than or equal to $\top$ is equal to the entire set of elements (denoted by $\text{univ}$).

Finset.nonempty_Iic theorem

: (Iic a).Nonempty

Full source

@[simp, aesop safe apply (rule_sets := [finsetNonempty])]
lemma nonempty_Iic : (Iic a).Nonempty := ⟨a, mem_Iic.2 le_rfl⟩

Nonemptiness of Lower-Closed Interval Finset

Informal description

For any element $a$ in a locally finite order with finite lower-bounded intervals, the lower-closed interval $\text{Iic}(a)$ is nonempty.

Finset.nonempty_Iio theorem

: (Iio a).Nonempty ↔ ¬IsMin a

Full source

lemma nonempty_Iio : (Iio a).Nonempty ↔ ¬ IsMin a := by simp [Finset.Nonempty]

Nonempty Open Lower Interval Characterizes Non-Minimal Elements

Informal description

For an element $a$ in a locally finite order with finite lower-bounded intervals, the open lower interval $\text{Iio}(a)$ is nonempty if and only if $a$ is not a minimal element.

Finset.Iic_subset_Iic theorem

: Iic a ⊆ Iic b ↔ a ≤ b

Full source

@[simp]
theorem Iic_subset_Iic : IicIic a ⊆ Iic bIic a ⊆ Iic b ↔ a ≤ b := by
  simp [← coe_subset]

Subset Relation of Lower-Closed Intervals Characterizes Order Relation

Informal description

For any elements $a$ and $b$ in a locally finite order with finite lower-bounded intervals, the finset $\text{Iic}(a)$ is a subset of $\text{Iic}(b)$ if and only if $a \leq b$.

Finset.Iic_ssubset_Iic theorem

: Iic a ⊂ Iic b ↔ a < b

Full source

@[simp]
theorem Iic_ssubset_Iic : IicIic a ⊂ Iic bIic a ⊂ Iic b ↔ a < b := by
  simp [← coe_ssubset]

Strict Subset Characterization of Lower-Closed Intervals: $\operatorname{Iic}(a) \subset \operatorname{Iic}(b) \leftrightarrow a < b$

Informal description

For any elements $a$ and $b$ in a locally finite order with finite lower-bounded intervals, the finset $\operatorname{Iic}(a)$ is a strict subset of $\operatorname{Iic}(b)$ if and only if $a < b$.

Finset.Iio_subset_Iio theorem

(h : a ≤ b) : Iio a ⊆ Iio b

Full source

@[gcongr]
theorem Iio_subset_Iio (h : a ≤ b) : IioIio a ⊆ Iio b := by
  simpa [← coe_subset] using Set.Iio_subset_Iio h

Monotonicity of Finset Lower Intervals: $\operatorname{Iio}(a) \subseteq \operatorname{Iio}(b)$ when $a \leq b$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, if $a \leq b$, then the finset $\operatorname{Iio}(a)$ is a subset of the finset $\operatorname{Iio}(b)$, where $\operatorname{Iio}(x)$ denotes the finset of all elements less than $x$.

Finset.Iio_ssubset_Iio theorem

(h : a < b) : Iio a ⊂ Iio b

Full source

@[gcongr]
theorem Iio_ssubset_Iio (h : a < b) : IioIio a ⊂ Iio b := by
  simpa [← coe_ssubset] using Set.Iio_ssubset_Iio h

Proper Subset Relation for Open Lower Intervals: $a < b \Rightarrow \operatorname{Iio}(a) \subsetneq \operatorname{Iio}(b)$

Informal description

For any elements $a$ and $b$ in a preorder, if $a < b$, then the finset $\operatorname{Iio}(a)$ is a proper subset of $\operatorname{Iio}(b)$, where $\operatorname{Iio}(x) = \{y \mid y < x\}$.

Finset.Icc_subset_Iic_self theorem

: Icc a b ⊆ Iic b

Full source

theorem Icc_subset_Iic_self : IccIcc a b ⊆ Iic b := by
  simpa [← coe_subset] using Set.Icc_subset_Iic_self

Inclusion of Closed Interval in Lower-Closed Interval: $[a, b] \subseteq (-\infty, b]$

Informal description

For any elements $a$ and $b$ in a preorder, the closed interval finset $[a, b]$ is a subset of the lower-closed interval finset $(-\infty, b]$.

Finset.Ioc_subset_Iic_self theorem

: Ioc a b ⊆ Iic b

Full source

theorem Ioc_subset_Iic_self : IocIoc a b ⊆ Iic b := by
  simpa [← coe_subset] using Set.Ioc_subset_Iic_self

Inclusion of $(a, b]$ in $(-\infty, b]$ for finsets

Informal description

For any elements $a$ and $b$ in a locally finite order, the open-closed interval $(a, b]$ is a subset of the lower-closed interval $(-\infty, b]$.

Finset.Ico_subset_Iio_self theorem

: Ico a b ⊆ Iio b

Full source

theorem Ico_subset_Iio_self : IcoIco a b ⊆ Iio b := by
  simpa [← coe_subset] using Set.Ico_subset_Iio_self

Inclusion of Closed-Open Interval in Open Lower Interval: $\text{Ico}(a, b) \subseteq \text{Iio}(b)$

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$, the closed-open interval finset $\text{Ico}(a, b)$ is a subset of the open lower interval finset $\text{Iio}(b)$. In other words, every element $x$ satisfying $a \leq x < b$ also satisfies $x < b$.

Finset.Ioo_subset_Iio_self theorem

: Ioo a b ⊆ Iio b

Full source

theorem Ioo_subset_Iio_self : IooIoo a b ⊆ Iio b := by
  simpa [← coe_subset] using Set.Ioo_subset_Iio_self

Inclusion of Open Interval in Lower Interval: $\text{Ioo}(a,b) \subseteq \text{Iio}(b)$

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$, the open interval finset $\text{Ioo}(a, b)$ is a subset of the open lower interval finset $\text{Iio}(b)$. In other words, every element $x$ satisfying $a < x < b$ also satisfies $x < b$.

Finset.Ico_subset_Iic_self theorem

: Ico a b ⊆ Iic b

Full source

theorem Ico_subset_Iic_self : IcoIco a b ⊆ Iic b :=
  Ico_subset_Icc_self.trans Icc_subset_Iic_self

Inclusion of Closed-Open Interval in Lower-Closed Interval: $\text{Ico}(a, b) \subseteq \text{Iic}(b)$

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$, the closed-open interval finset $\text{Ico}(a, b)$ is a subset of the lower-closed interval finset $\text{Iic}(b)$. In other words, every element $x$ satisfying $a \leq x < b$ also satisfies $x \leq b$.

Finset.Ioo_subset_Iic_self theorem

: Ioo a b ⊆ Iic b

Full source

theorem Ioo_subset_Iic_self : IooIoo a b ⊆ Iic b :=
  Ioo_subset_Ioc_self.trans Ioc_subset_Iic_self

Inclusion of Open Interval in Lower-Closed Interval: $\text{Ioo}(a,b) \subseteq \text{Iic}(b)$

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$, the open interval finset $\text{Ioo}(a, b)$ is a subset of the lower-closed interval finset $\text{Iic}(b)$. In other words, every element $x$ satisfying $a < x < b$ also satisfies $x \leq b$.

Finset.Iic_disjoint_Ioc theorem

(h : a ≤ b) : Disjoint (Iic a) (Ioc b c)

Full source

theorem Iic_disjoint_Ioc (h : a ≤ b) : Disjoint (Iic a) (Ioc b c) :=
  disjoint_left.2 fun _ hax hbcx ↦ (mem_Iic.1 hax).not_lt <| lt_of_le_of_lt h (mem_Ioc.1 hbcx).1

Disjointness of Lower-Closed and Open-Closed Interval Finsets: $\text{Iic}(a) \cap \text{Ioc}(b, c) = \emptyset$ when $a \leq b$

Informal description

For any elements $a, b, c$ in a locally finite order $\alpha$ with $a \leq b$, the lower-closed interval finset $\text{Iic}(a)$ and the open-closed interval finset $\text{Ioc}(b, c)$ are disjoint. That is, $\text{Iic}(a) \cap \text{Ioc}(b, c) = \emptyset$.

Equiv.IicFinsetSet definition

(a : α) : Iic a ≃ Set.Iic a

Full source

/-- An equivalence between `Finset.Iic a` and `Set.Iic a`. -/
def _root_.Equiv.IicFinsetSet (a : α) : IicIic a ≃ Set.Iic a where
  toFun b := ⟨b.1, coe_Iic a ▸ mem_coe.2 b.2⟩
  invFun b := ⟨b.1, by rw [← mem_coe, coe_Iic a]; exact b.2⟩
  left_inv := fun _ ↦ rfl
  right_inv := fun _ ↦ rfl

Equivalence between finset and set lower-closed intervals

Informal description

For an element $a$ in a preorder $\alpha$ with a locally finite order structure, there is a natural equivalence between the finset $\text{Iic}(a)$ (the lower-closed interval as a finset) and the set $\text{Iic}(a)$ (the left-infinite right-closed interval $(-\infty, a]$). The equivalence maps an element $b$ in the finset $\text{Iic}(a)$ to the same element $b$ in the set $\text{Iic}(a)$, and vice versa, preserving the property that $b \leq a$.

Finset.Ioi_subset_Ici_self theorem

: Ioi a ⊆ Ici a

Full source

theorem Ioi_subset_Ici_self : IoiIoi a ⊆ Ici a := by
  simpa [← coe_subset] using Set.Ioi_subset_Ici_self

Inclusion of Open Interval in Closed Interval: $\text{Ioi}(a) \subseteq \text{Ici}(a)$

Informal description

For any element $a$ in a preorder $\alpha$ with a locally finite order structure, the finset $\text{Ioi}(a)$ (representing the open interval $(a, \infty)$) is a subset of the finset $\text{Ici}(a)$ (representing the closed interval $[a, \infty)$).

BddBelow.finite theorem

{s : Set α} (hs : BddBelow s) : s.Finite

Full source

theorem _root_.BddBelow.finite {s : Set α} (hs : BddBelow s) : s.Finite :=
  let ⟨a, ha⟩ := hs
  (Ici a).finite_toSet.subset fun _ hx => mem_Ici.2 <| ha hx

Finiteness of Bounded Below Sets in a Preorder

Informal description

For any subset $s$ of a preorder $\alpha$ that is bounded below, $s$ is finite.

Set.Infinite.not_bddBelow theorem

{s : Set α} : s.Infinite → ¬BddBelow s

Full source

theorem _root_.Set.Infinite.not_bddBelow {s : Set α} : s.Infinite → ¬BddBelow s :=
  mt BddBelow.finite

Infinite sets in a preorder are unbounded below

Informal description

For any subset $s$ of a preorder $\alpha$, if $s$ is infinite, then $s$ is not bounded below.

Finset.filter_lt_eq_Ioi theorem

[DecidablePred (a < ·)] : ({x | a < x} : Finset _) = Ioi a

Full source

theorem filter_lt_eq_Ioi [DecidablePred (a < ·)] : ({x | a < x} : Finset _) = Ioi a := by ext; simp

Equality of Filtered Finset and Open-Infinite Interval

Informal description

For a locally finite order with finite intervals bounded below and a decidable predicate `(a < ·)`, the finset obtained by filtering elements greater than $a$ is equal to the open-infinite interval $\text{Ioi}(a)$, which consists of all elements $x$ such that $a < x$.

Finset.filter_le_eq_Ici theorem

[DecidablePred (a ≤ ·)] : ({x | a ≤ x} : Finset _) = Ici a

Full source

theorem filter_le_eq_Ici [DecidablePred (a ≤ ·)] : ({x | a ≤ x} : Finset _) = Ici a := by ext; simp

Equality of Filtered Finset and Closed-Infinite Interval

Informal description

For a locally finite order with finite intervals bounded below and a decidable predicate `(a ≤ ·)`, the finset obtained by filtering elements greater than or equal to $a$ is equal to the closed-infinite interval $\text{Ici}(a)$, which consists of all elements $x$ such that $a \leq x$.

Finset.Iio_subset_Iic_self theorem

: Iio a ⊆ Iic a

Full source

theorem Iio_subset_Iic_self : IioIio a ⊆ Iic a := by
  simpa [← coe_subset] using Set.Iio_subset_Iic_self

Inclusion of Open Lower Interval in Closed Lower Interval: $\operatorname{Iio}(a) \subseteq \operatorname{Iic}(a)$

Informal description

For any element $a$ in a locally finite order with finite lower-bounded intervals, the open lower interval $\operatorname{Iio}(a)$ is a subset of the closed lower interval $\operatorname{Iic}(a)$. In other words, $\{x \mid x < a\} \subseteq \{x \mid x \leq a\}$.

BddAbove.finite theorem

{s : Set α} (hs : BddAbove s) : s.Finite

Full source

theorem _root_.BddAbove.finite {s : Set α} (hs : BddAbove s) : s.Finite :=
  hs.dual.finite

Finiteness of Bounded Above Sets in a Preorder

Informal description

For any subset $s$ of a preorder $\alpha$ that is bounded above, $s$ is finite.

Set.Infinite.not_bddAbove theorem

{s : Set α} : s.Infinite → ¬BddAbove s

Full source

theorem _root_.Set.Infinite.not_bddAbove {s : Set α} : s.Infinite → ¬BddAbove s :=
  mt BddAbove.finite

Infinite Sets in Preorders are Unbounded Above

Informal description

For any subset $s$ of a preorder $\alpha$, if $s$ is infinite, then $s$ is not bounded above.

Finset.filter_gt_eq_Iio theorem

[DecidablePred (· < a)] : ({x | x < a} : Finset _) = Iio a

Full source

theorem filter_gt_eq_Iio [DecidablePred (· < a)] : ({x | x < a} : Finset _) = Iio a := by ext; simp

Equality of Filtered Set and Open Lower Interval Finset: $\{x \mid x < a\} = \text{Iio}(a)$

Informal description

For any element $a$ in a locally finite order with finite lower-bounded intervals, the finset $\{x \mid x < a\}$ is equal to the open lower interval finset $\text{Iio}(a)$.

Finset.filter_ge_eq_Iic theorem

[DecidablePred (· ≤ a)] : ({x | x ≤ a} : Finset _) = Iic a

Full source

theorem filter_ge_eq_Iic [DecidablePred (· ≤ a)] : ({x | x ≤ a} : Finset _) = Iic a := by ext; simp

Equality of Filtered Set and Closed Lower Interval Finset: $\{x \mid x \leq a\} = \text{Iic}(a)$

Informal description

For any element $a$ in a locally finite order with finite lower-bounded intervals, the finset $\{x \mid x \leq a\}$ is equal to the closed lower interval finset $\text{Iic}(a)$.

Finset.Icc_bot theorem

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

Full source

@[simp]
theorem Icc_bot [OrderBot α] : Icc (⊥ : α) a = Iic a := rfl

Closed Interval at Bottom Equals Lower Interval: $\text{Icc}(\bot, a) = \text{Iic}(a)$

Informal description

For any element $a$ in a locally finite order $\alpha$ with a bottom element $\bot$, the closed interval finset $\text{Icc}(\bot, a)$ is equal to the closed lower interval finset $\text{Iic}(a)$.

Finset.Icc_top theorem

[OrderTop α] : Icc a (⊤ : α) = Ici a

Full source

@[simp]
theorem Icc_top [OrderTop α] : Icc a (⊤ : α) = Ici a := rfl

Closed Interval with Top Equals Closed-Infinite Interval: $\text{Icc}(a, \top) = \text{Ici}(a)$

Informal description

For any element $a$ in a locally finite order $\alpha$ with a top element $\top$, the closed interval finset $\text{Icc}(a, \top)$ is equal to the closed-infinite interval finset $\text{Ici}(a)$.

Finset.Ico_bot theorem

[OrderBot α] : Ico (⊥ : α) a = Iio a

Full source

@[simp]
theorem Ico_bot [OrderBot α] : Ico (⊥ : α) a = Iio a := rfl

Equality of Half-Open and Open Lower Intervals at Bottom: $\text{Ico}(\bot, a) = \text{Iio}(a)$

Informal description

For any element $a$ in a locally finite order $\alpha$ with a bottom element $\bot$, the half-open interval finset $\text{Ico}(\bot, a)$ is equal to the open lower interval finset $\text{Iio}(a)$.

Finset.Ioc_top theorem

[OrderTop α] : Ioc a (⊤ : α) = Ioi a

Full source

@[simp]
theorem Ioc_top [OrderTop α] : Ioc a (⊤ : α) = Ioi a := rfl

Equality of Open-Closed and Open Infinite Intervals at Top: $\text{Ioc}(a, \top) = \text{Ioi}(a)$

Informal description

For any element $a$ in a locally finite order $\alpha$ with a top element $\top$, the open-closed interval finset $\text{Ioc}(a, \top)$ is equal to the open infinite interval finset $\text{Ioi}(a)$. In other words, the set $\{x \in \alpha \mid a < x \leq \top\}$ equals the set $\{x \in \alpha \mid a < x\}$.

Finset.Icc_bot_top theorem

[BoundedOrder α] [Fintype α] : Icc (⊥ : α) (⊤ : α) = univ

Full source

theorem Icc_bot_top [BoundedOrder α] [Fintype α] : Icc (⊥ : α) (⊤ : α) = univ := by
  rw [Icc_bot, Iic_top]

Closed Interval from Bottom to Top Equals Universal Set in Finite Bounded Order

Informal description

In a finite bounded order $\alpha$, the closed interval from the bottom element $\bot$ to the top element $\top$ is equal to the entire set of elements in $\alpha$.

Finset.disjoint_Ioi_Iio theorem

(a : α) : Disjoint (Ioi a) (Iio a)

Full source

theorem disjoint_Ioi_Iio (a : α) : Disjoint (Ioi a) (Iio a) :=
  disjoint_left.2 fun _ hab hba => (mem_Ioi.1 hab).not_lt <| mem_Iio.1 hba

Disjointness of Open Infinite and Lower Intervals at $a$

Informal description

For any element $a$ in a locally finite order, the open infinite interval $(a, \infty)$ and the open lower interval $(-\infty, a)$ are disjoint as finsets. In other words, $\text{Ioi}(a) \cap \text{Iio}(a) = \emptyset$.

Finset.Icc_self theorem

(a : α) : Icc a a = { a }

Full source

@[simp]
theorem Icc_self (a : α) : Icc a a = {a} := by rw [← coe_eq_singleton, coe_Icc, Set.Icc_self]

Closed Interval at a Point is Singleton: $[a, a] = \{a\}$

Informal description

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

Finset.Icc_eq_singleton_iff theorem

: Icc a b = { c } ↔ a = c ∧ b = c

Full source

@[simp]
theorem Icc_eq_singleton_iff : IccIcc a b = {c} ↔ a = c ∧ b = c := by
  rw [← coe_eq_singleton, coe_Icc, Set.Icc_eq_singleton_iff]

Singleton Interval Characterization: $[a, b] = \{c\} \leftrightarrow a = c = b$

Informal description

For any elements $a, b, c$ in a preorder $\alpha$, the closed interval $[a, b]$ is equal to the singleton set $\{c\}$ if and only if $a = c$ and $b = c$.

Finset.Ico_disjoint_Ico_consecutive theorem

(a b c : α) : Disjoint (Ico a b) (Ico b c)

Full source

theorem Ico_disjoint_Ico_consecutive (a b c : α) : Disjoint (Ico a b) (Ico b c) :=
  disjoint_left.2 fun _ hab hbc => (mem_Ico.mp hab).2.not_le (mem_Ico.mp hbc).1

Disjointness of Consecutive Closed-Open Interval Finsets

Informal description

For any elements $a, b, c$ in a locally finite order $\alpha$, the closed-open interval finsets $\text{Ico}(a, b)$ and $\text{Ico}(b, c)$ are disjoint.

Finset.Ici_top theorem

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

Full source

@[simp]
theorem Ici_top [OrderTop α] : Ici (⊤ : α) = {⊤} := Icc_eq_singleton_iff.2 ⟨rfl, rfl⟩

Closed-Infinite Interval at Top is Singleton: $\text{Ici}(\top) = \{\top\}$

Informal description

In an order with a top element $\top$, the closed-infinite interval $\text{Ici}(\top)$ is equal to the singleton set $\{\top\}$.

Finset.Iic_bot theorem

[OrderBot α] : Iic (⊥ : α) = {⊥}

Full source

@[simp]
theorem Iic_bot [OrderBot α] : Iic (⊥ : α) = {⊥} := Icc_eq_singleton_iff.2 ⟨rfl, rfl⟩

Lower-Closed Interval at Bottom is Singleton

Informal description

In an order $\alpha$ with a bottom element $\bot$, the lower-closed interval finset $\text{Iic}(\bot)$ is equal to the singleton set $\{\bot\}$.

Finset.Icc_erase_left theorem

(a b : α) : (Icc a b).erase a = Ioc a b

Full source

@[simp]
theorem Icc_erase_left (a b : α) : (Icc a b).erase a = Ioc a b := by simp [← coe_inj]

Closed Interval Minus Left Endpoint Equals Left-Open Right-Closed Interval

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$, the finset obtained by removing the left endpoint $a$ from the closed interval finset $\text{Icc}(a, b)$ is equal to the left-open right-closed interval finset $\text{Ioc}(a, b)$. In other words, $\text{Icc}(a, b) \setminus \{a\} = \text{Ioc}(a, b)$.

Finset.Icc_erase_right theorem

(a b : α) : (Icc a b).erase b = Ico a b

Full source

@[simp]
theorem Icc_erase_right (a b : α) : (Icc a b).erase b = Ico a b := by simp [← coe_inj]

Closed Interval Minus Right Endpoint Equals Closed-Open Interval

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$, the finset obtained by removing the right endpoint $b$ from the closed interval finset $\text{Icc}(a, b)$ is equal to the closed-open interval finset $\text{Ico}(a, b)$. In other words, $\text{Icc}(a, b) \setminus \{b\} = \text{Ico}(a, b)$.

Finset.Ico_erase_left theorem

(a b : α) : (Ico a b).erase a = Ioo a b

Full source

@[simp]
theorem Ico_erase_left (a b : α) : (Ico a b).erase a = Ioo a b := by simp [← coe_inj]

Closed-Open Interval Minus Left Endpoint Equals Open Interval

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$, the finset obtained by removing the left endpoint $a$ from the closed-open interval finset $\text{Ico}(a, b)$ is equal to the open interval finset $\text{Ioo}(a, b)$. In other words, $\text{Ico}(a, b) \setminus \{a\} = \text{Ioo}(a, b)$.

Finset.Ioc_erase_right theorem

(a b : α) : (Ioc a b).erase b = Ioo a b

Full source

@[simp]
theorem Ioc_erase_right (a b : α) : (Ioc a b).erase b = Ioo a b := by simp [← coe_inj]

Open-closed interval minus right endpoint equals open interval

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$, the finset obtained by removing the right endpoint $b$ from the open-closed interval finset $\text{Ioc}(a, b)$ equals the open interval finset $\text{Ioo}(a, b)$. In other words, $\text{Ioc}(a, b) \setminus \{b\} = \text{Ioo}(a, b)$.

Finset.Icc_diff_both theorem

(a b : α) : Icc a b \ { a, b } = Ioo a b

Full source

@[simp]
theorem Icc_diff_both (a b : α) : IccIcc a b \ {a, b} = Ioo a b := by simp [← coe_inj]

Difference of Closed Interval Finset and Endpoints Equals Open Interval Finset: $\text{Icc}(a, b) \setminus \{a, b\} = \text{Ioo}(a, b)$

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$, the set difference between the closed interval finset $\text{Icc}(a, b)$ and the finset $\{a, b\}$ is equal to the open interval finset $\text{Ioo}(a, b)$. In other words, $\text{Icc}(a, b) \setminus \{a, b\} = \text{Ioo}(a, b)$.

Finset.Ico_insert_right theorem

(h : a ≤ b) : insert b (Ico a b) = Icc a b

Full source

@[simp]
theorem Ico_insert_right (h : a ≤ b) : insert b (Ico a b) = Icc a b := by
  rw [← coe_inj, coe_insert, coe_Icc, coe_Ico, Set.insert_eq, Set.union_comm, Set.Ico_union_right h]

Insertion of Right Endpoint into Closed-Open Interval Yields Closed Interval: $\text{Ico}(a, b) \cup \{b\} = \text{Icc}(a, b)$

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$ with $a \leq b$, inserting the element $b$ into the closed-open interval finset $\text{Ico}(a, b)$ yields the closed interval finset $\text{Icc}(a, b)$. That is, $\text{Ico}(a, b) \cup \{b\} = \text{Icc}(a, b)$.

Finset.Ioc_insert_left theorem

(h : a ≤ b) : insert a (Ioc a b) = Icc a b

Full source

@[simp]
theorem Ioc_insert_left (h : a ≤ b) : insert a (Ioc a b) = Icc a b := by
  rw [← coe_inj, coe_insert, coe_Ioc, coe_Icc, Set.insert_eq, Set.union_comm, Set.Ioc_union_left h]

Insertion of Left Endpoint into Open-Closed Interval Yields Closed Interval: $\text{Ioc}(a, b) \cup \{a\} = \text{Icc}(a, b)$

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$ with $a \leq b$, inserting the element $a$ into the open-closed interval finset $\text{Ioc}(a, b)$ yields the closed interval finset $\text{Icc}(a, b)$. That is, $\text{Ioc}(a, b) \cup \{a\} = \text{Icc}(a, b)$.

Finset.Ioo_insert_left theorem

(h : a < b) : insert a (Ioo a b) = Ico a b

Full source

@[simp]
theorem Ioo_insert_left (h : a < b) : insert a (Ioo a b) = Ico a b := by
  rw [← coe_inj, coe_insert, coe_Ioo, coe_Ico, Set.insert_eq, Set.union_comm, Set.Ioo_union_left h]

Insertion of Left Endpoint into Open Interval Yields Closed-Open Interval: $(a, b) \cup \{a\} = [a, b)$

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$ with $a < b$, inserting the element $a$ into the open interval finset $\text{Ioo}(a, b)$ yields the closed-open interval finset $\text{Ico}(a, b)$. That is, $(a, b) \cup \{a\} = [a, b)$.

Finset.Ioo_insert_right theorem

(h : a < b) : insert b (Ioo a b) = Ioc a b

Full source

@[simp]
theorem Ioo_insert_right (h : a < b) : insert b (Ioo a b) = Ioc a b := by
  rw [← coe_inj, coe_insert, coe_Ioo, coe_Ioc, Set.insert_eq, Set.union_comm, Set.Ioo_union_right h]

Insertion of Right Endpoint into Open Interval Yields Left-Open Right-Closed Interval

Informal description

For any two elements $a$ and $b$ in a locally finite order with $a < b$, inserting $b$ into the open interval finset $(a, b)$ yields the left-open right-closed interval finset $(a, b]$. That is, $\{b\} \cup (a, b) = (a, b]$.

Finset.Icc_diff_Ico_self theorem

(h : a ≤ b) : Icc a b \ Ico a b = { b }

Full source

@[simp]
theorem Icc_diff_Ico_self (h : a ≤ b) : IccIcc a b \ Ico a b = {b} := by simp [← coe_inj, h]

Difference of Closed and Half-Open Intervals at Right Endpoint: $[a, b] \setminus [a, b) = \{b\}$

Informal description

For any elements $a$ and $b$ in a locally finite order with $a \leq b$, the set difference between the closed interval $[a, b]$ and the half-open interval $[a, b)$ is the singleton set $\{b\}$. In other words, $[a, b] \setminus [a, b) = \{b\}$.

Finset.Icc_diff_Ioc_self theorem

(h : a ≤ b) : Icc a b \ Ioc a b = { a }

Full source

@[simp]
theorem Icc_diff_Ioc_self (h : a ≤ b) : IccIcc a b \ Ioc a b = {a} := by simp [← coe_inj, h]

Difference of Closed and Open-Closed Intervals Yields Left Endpoint: $[a, b] \setminus (a, b] = \{a\}$

Informal description

For any elements $a$ and $b$ in a locally finite order with $a \leq b$, the set difference between the closed interval $[a, b]$ and the open-closed interval $(a, b]$ is the singleton set $\{a\}$. In other words, $[a, b] \setminus (a, b] = \{a\}$.

Finset.Icc_diff_Ioo_self theorem

(h : a ≤ b) : Icc a b \ Ioo a b = { a, b }

Full source

@[simp]
theorem Icc_diff_Ioo_self (h : a ≤ b) : IccIcc a b \ Ioo a b = {a, b} := by simp [← coe_inj, h]

Difference of Closed and Open Finset Intervals Yields Endpoints: $\text{Icc}(a, b) \setminus \text{Ioo}(a, b) = \{a, b\}$

Informal description

For any elements $a$ and $b$ in a locally finite order with $a \leq b$, the set difference between the closed interval finset $\text{Icc}(a, b)$ and the open interval finset $\text{Ioo}(a, b)$ is the finset $\{a, b\}$. In other words, $\text{Icc}(a, b) \setminus \text{Ioo}(a, b) = \{a, b\}$.

Finset.Ico_diff_Ioo_self theorem

(h : a < b) : Ico a b \ Ioo a b = { a }

Full source

@[simp]
theorem Ico_diff_Ioo_self (h : a < b) : IcoIco a b \ Ioo a b = {a} := by simp [← coe_inj, h]

Difference of Closed-Open and Open Interval Finsets: $[a, b) \setminus (a, b) = \{a\}$ when $a < b$

Informal description

For any two elements $a$ and $b$ in a locally finite order with $a < b$, the set difference between the closed-open interval finset $[a, b)$ and the open interval finset $(a, b)$ is the singleton set $\{a\}$. In other words, $[a, b) \setminus (a, b) = \{a\}$.

Finset.Ioc_diff_Ioo_self theorem

(h : a < b) : Ioc a b \ Ioo a b = { b }

Full source

@[simp]
theorem Ioc_diff_Ioo_self (h : a < b) : IocIoc a b \ Ioo a b = {b} := by simp [← coe_inj, h]

Difference of finset intervals $(a, b] \setminus (a, b) = \{b\}$ for $a < b$

Informal description

For any elements $a$ and $b$ in a locally finite order with $a < b$, the set difference between the finset $\text{Ioc}(a, b)$ and the finset $\text{Ioo}(a, b)$ is the singleton set $\{b\}$. In other words, $(a, b] \setminus (a, b) = \{b\}$ where the intervals are represented as finsets.

Finset.Ico_inter_Ico_consecutive theorem

(a b c : α) : Ico a b ∩ Ico b c = ∅

Full source

@[simp]
theorem Ico_inter_Ico_consecutive (a b c : α) : IcoIco a b ∩ Ico b c = ∅ :=
  (Ico_disjoint_Ico_consecutive a b c).eq_bot

Empty Intersection of Consecutive Closed-Open Interval Finsets

Informal description

For any elements $a, b, c$ in a locally finite order $\alpha$, the intersection of the closed-open interval finsets $\text{Ico}(a, b)$ and $\text{Ico}(b, c)$ is empty.

Finset.Icc_eq_cons_Ico theorem

(h : a ≤ b) : Icc a b = (Ico a b).cons b right_not_mem_Ico

Full source

/-- `Finset.cons` version of `Finset.Ico_insert_right`. -/
theorem Icc_eq_cons_Ico (h : a ≤ b) : Icc a b = (Ico a b).cons b right_not_mem_Ico := by
  classical rw [cons_eq_insert, Ico_insert_right h]

Closed Interval as Insertion into Closed-Open Interval: $\text{Icc}(a, b) = \text{Ico}(a, b) \cup \{b\}$ for $a \leq b$

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$ with $a \leq b$, the closed interval finset $\text{Icc}(a, b)$ is equal to the finset obtained by inserting $b$ into the closed-open interval finset $\text{Ico}(a, b)$, where $b$ is not already in $\text{Ico}(a, b)$. In other words, $\text{Icc}(a, b) = \text{Ico}(a, b) \cup \{b\}$ when $a \leq b$.

Finset.Icc_eq_cons_Ioc theorem

(h : a ≤ b) : Icc a b = (Ioc a b).cons a left_not_mem_Ioc

Full source

/-- `Finset.cons` version of `Finset.Ioc_insert_left`. -/
theorem Icc_eq_cons_Ioc (h : a ≤ b) : Icc a b = (Ioc a b).cons a left_not_mem_Ioc := by
  classical rw [cons_eq_insert, Ioc_insert_left h]

Closed Interval as Cons of Open-Closed Interval: $\text{Icc}(a, b) = \{a\} \cup \text{Ioc}(a, b)$

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$ with $a \leq b$, the closed interval finset $\text{Icc}(a, b)$ is equal to the open-closed interval finset $\text{Ioc}(a, b)$ with the element $a$ consed (prepended), since $a \notin \text{Ioc}(a, b)$.

Finset.Ioc_eq_cons_Ioo theorem

(h : a < b) : Ioc a b = (Ioo a b).cons b right_not_mem_Ioo

Full source

/-- `Finset.cons` version of `Finset.Ioo_insert_right`. -/
theorem Ioc_eq_cons_Ioo (h : a < b) : Ioc a b = (Ioo a b).cons b right_not_mem_Ioo := by
  classical rw [cons_eq_insert, Ioo_insert_right h]

Construction of $(a, b]$ from $(a, b)$ via insertion of $b$

Informal description

For any two elements $a$ and $b$ in a locally finite order with $a < b$, the left-open right-closed interval $(a, b]$ can be constructed by inserting the element $b$ into the open interval $(a, b)$. That is, $(a, b] = \{b\} \cup (a, b)$.

Finset.Ico_eq_cons_Ioo theorem

(h : a < b) : Ico a b = (Ioo a b).cons a left_not_mem_Ioo

Full source

/-- `Finset.cons` version of `Finset.Ioo_insert_left`. -/
theorem Ico_eq_cons_Ioo (h : a < b) : Ico a b = (Ioo a b).cons a left_not_mem_Ioo := by
  classical rw [cons_eq_insert, Ioo_insert_left h]

Closed-open interval as insertion into open interval: $[a, b) = (a, b) \cup \{a\}$

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$ with $a < b$, the closed-open interval finset $\text{Ico}(a, b)$ is equal to the open interval finset $\text{Ioo}(a, b)$ with the element $a$ inserted (and $a \notin \text{Ioo}(a, b)$ by definition). That is, $[a, b) = (a, b) \cup \{a\}$.

Finset.Ico_filter_le_left theorem

{a b : α} [DecidablePred (· ≤ a)] (hab : a < b) : {x ∈ Ico a b | x ≤ a} = { a }

Full source

theorem Ico_filter_le_left {a b : α} [DecidablePred (· ≤ a)] (hab : a < b) :
    {x ∈ Ico a b | x ≤ a} = {a} := by
  ext x
  rw [mem_filter, mem_Ico, mem_singleton, and_right_comm, ← le_antisymm_iff, eq_comm]
  exact and_iff_left_of_imp fun h => h.le.trans_lt hab

Filtering Elements Below Left Endpoint in Closed-Open Interval

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$ with $a < b$, the set of elements $x$ in the closed-open interval $[a, b)$ that satisfy $x \leq a$ is exactly the singleton set $\{a\}$.

Finset.card_Ico_eq_card_Icc_sub_one theorem

(a b : α) : #(Ico a b) = #(Icc a b) - 1

Full source

theorem card_Ico_eq_card_Icc_sub_one (a b : α) : #(Ico a b) = #(Icc a b) - 1 := by
  classical
    by_cases h : a ≤ b
    · rw [Icc_eq_cons_Ico h, card_cons]
      exact (Nat.add_sub_cancel _ _).symm
    · rw [Ico_eq_empty fun h' => h h'.le, Icc_eq_empty h, card_empty, Nat.zero_sub]

Cardinality Relation Between Closed-Open and Closed Intervals: $|\text{Ico}(a, b)| = |\text{Icc}(a, b)| - 1$

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$, the cardinality of the closed-open interval $[a, b)$ is equal to the cardinality of the closed interval $[a, b]$ minus one. That is, $$|\text{Ico}(a, b)| = |\text{Icc}(a, b)| - 1.$$

Finset.card_Ioc_eq_card_Icc_sub_one theorem

(a b : α) : #(Ioc a b) = #(Icc a b) - 1

Full source

theorem card_Ioc_eq_card_Icc_sub_one (a b : α) : #(Ioc a b) = #(Icc a b) - 1 :=
  @card_Ico_eq_card_Icc_sub_one αᵒᵈ _ _ _ _

Cardinality Relation: $|\text{Ioc}(a, b)| = |\text{Icc}(a, b)| - 1$

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$, the cardinality of the open-closed interval $(a, b]$ is equal to the cardinality of the closed interval $[a, b]$ minus one, i.e., $$|\text{Ioc}(a, b)| = |\text{Icc}(a, b)| - 1.$$

Finset.card_Ioo_eq_card_Ico_sub_one theorem

(a b : α) : #(Ioo a b) = #(Ico a b) - 1

Full source

theorem card_Ioo_eq_card_Ico_sub_one (a b : α) : #(Ioo a b) = #(Ico a b) - 1 := by
  classical
    by_cases h : a < b
    · rw [Ico_eq_cons_Ioo h, card_cons]
      exact (Nat.add_sub_cancel _ _).symm
    · rw [Ioo_eq_empty h, Ico_eq_empty h, card_empty, Nat.zero_sub]

Cardinality Relation: $|\text{Ioo}(a, b)| = |\text{Ico}(a, b)| - 1$

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$, the cardinality of the open interval finset $\text{Ioo}(a, b)$ is equal to the cardinality of the closed-open interval finset $\text{Ico}(a, b)$ minus one, i.e., $|\text{Ioo}(a, b)| = |\text{Ico}(a, b)| - 1$.

Finset.card_Ioo_eq_card_Ioc_sub_one theorem

(a b : α) : #(Ioo a b) = #(Ioc a b) - 1

Full source

theorem card_Ioo_eq_card_Ioc_sub_one (a b : α) : #(Ioo a b) = #(Ioc a b) - 1 :=
  @card_Ioo_eq_card_Ico_sub_one αᵒᵈ _ _ _ _

Cardinality Relation: $|\text{Ioo}(a, b)| = |\text{Ioc}(a, b)| - 1$

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$, the cardinality of the open interval $\text{Ioo}(a, b)$ is equal to the cardinality of the open-closed interval $\text{Ioc}(a, b)$ minus one, i.e., $|\text{Ioo}(a, b)| = |\text{Ioc}(a, b)| - 1$.

Finset.card_Ioo_eq_card_Icc_sub_two theorem

(a b : α) : #(Ioo a b) = #(Icc a b) - 2

Full source

theorem card_Ioo_eq_card_Icc_sub_two (a b : α) : #(Ioo a b) = #(Icc a b) - 2 := by
  rw [card_Ioo_eq_card_Ico_sub_one, card_Ico_eq_card_Icc_sub_one]
  rfl

Cardinality Relation: $|\text{Ioo}(a, b)| = |\text{Icc}(a, b)| - 2$

Informal description

For any elements $a$ and $b$ in a locally finite order $\alpha$, the cardinality of the open interval $(a, b)$ is equal to the cardinality of the closed interval $[a, b]$ minus two, i.e., $$|\text{Ioo}(a, b)| = |\text{Icc}(a, b)| - 2.$$

Finset.uIcc_map_sectL theorem

 [Lattice α] [Lattice β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableLE (α × β)] (a b : α) (c : β) :
  (uIcc a b).map (.sectL _ c) = uIcc (a, c) (b, c)

Full source

lemma uIcc_map_sectL [Lattice α] [Lattice β] [LocallyFiniteOrder α] [LocallyFiniteOrder β]
    [DecidableLE (α × β)] (a b : α) (c : β) :
    (uIcc a b).map (.sectL _ c) = uIcc (a, c) (b, c) := by
  aesop (add safe forward [le_antisymm])

Image of Unordered Closed Interval under Section Map in Product Order

Informal description

Let $\alpha$ and $\beta$ be lattices with locally finite order structures, and let $\alpha \times \beta$ be equipped with the product order. For any elements $a, b \in \alpha$ and $c \in \beta$, the image of the unordered closed interval $\text{uIcc}(a, b)$ under the map $(x \mapsto (x, c))$ is equal to the unordered closed interval $\text{uIcc}((a, c), (b, c))$ in $\alpha \times \beta$.

Finset.Icc_map_sectL theorem

: (Icc a b).map (.sectL _ c) = Icc (a, c) (b, c)

Full source

lemma Icc_map_sectL : (Icc a b).map (.sectL _ c) = Icc (a, c) (b, c) := by
  aesop (add safe forward [le_antisymm])

Image of Closed Interval under Section Map in Product Order

Informal description

For a locally finite order $\alpha$ and elements $a, b \in \alpha$, and for any element $c$ in another locally finite order $\beta$, the image of the closed interval $[a, b]$ under the map $x \mapsto (x, c)$ is equal to the closed interval $[(a, c), (b, c)]$ in the product order $\alpha \times \beta$.

Finset.Ioc_map_sectL theorem

: (Ioc a b).map (.sectL _ c) = Ioc (a, c) (b, c)

Full source

lemma Ioc_map_sectL : (Ioc a b).map (.sectL _ c) = Ioc (a, c) (b, c) := by
  aesop (add safe forward [le_antisymm, le_of_lt])

Image of Open-Closed Interval under Section Map in Product Order: $(a, b].\text{map}(\text{sectL}_c) = ((a, c), (b, c)]$

Informal description

For a locally finite order $\alpha$ and elements $a, b \in \alpha$, and for any element $c$ in another locally finite order $\beta$, the image of the open-closed interval $(a, b]$ under the map $x \mapsto (x, c)$ is equal to the open-closed interval $((a, c), (b, c)]$ in the product order $\alpha \times \beta$.

Finset.Ico_map_sectL theorem

: (Ico a b).map (.sectL _ c) = Ico (a, c) (b, c)

Full source

lemma Ico_map_sectL : (Ico a b).map (.sectL _ c) = Ico (a, c) (b, c) := by
  aesop (add safe forward [le_antisymm, le_of_lt])

Image of Half-Open Interval under Section Map in Product Order

Informal description

For a locally finite order $\alpha$ and elements $a, b \in \alpha$, and for any element $c$ in another locally finite order $\beta$, the image of the half-open interval $[a, b)$ under the map $x \mapsto (x, c)$ is equal to the half-open interval $[(a, c), (b, c))$ in the product order $\alpha \times \beta$.

Finset.Ioo_map_sectL theorem

: (Ioo a b).map (.sectL _ c) = Ioo (a, c) (b, c)

Full source

lemma Ioo_map_sectL : (Ioo a b).map (.sectL _ c) = Ioo (a, c) (b, c) := by
  aesop (add safe forward [le_antisymm, le_of_lt])

Image of Open Interval under Section Map in Product Order: $(a, b).\text{map}(\text{sectL}_c) = ((a, c), (b, c))$

Informal description

For a locally finite order $\alpha$ and elements $a, b \in \alpha$, and for any element $c$ in another locally finite order $\beta$, the image of the open interval $(a, b)$ under the map $x \mapsto (x, c)$ is equal to the open interval $((a, c), (b, c))$ in the product order $\alpha \times \beta$.

Finset.uIcc_map_sectR theorem

 [Lattice α] [Lattice β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableLE (α × β)] (c : α) (a b : β) :
  (uIcc a b).map (.sectR c _) = uIcc (c, a) (c, b)

Full source

lemma uIcc_map_sectR [Lattice α] [Lattice β] [LocallyFiniteOrder α] [LocallyFiniteOrder β]
    [DecidableLE (α × β)] (c : α) (a b : β) :
    (uIcc a b).map (.sectR c _) = uIcc (c, a) (c, b) := by
  aesop (add safe forward [le_antisymm])

Image of Unordered Closed Interval under Right Section Map in Product Lattice

Informal description

Let $\alpha$ and $\beta$ be lattices equipped with locally finite order structures, and let $\alpha \times \beta$ be their product lattice with the induced order. For any fixed element $c \in \alpha$ and elements $a, b \in \beta$, the image of the unordered closed interval $\text{uIcc}(a, b)$ under the map $y \mapsto (c, y)$ is equal to the unordered closed interval $\text{uIcc}((c, a), (c, b))$ in $\alpha \times \beta$.

Finset.Icc_map_sectR theorem

: (Icc a b).map (.sectR c _) = Icc (c, a) (c, b)

Full source

lemma Icc_map_sectR : (Icc a b).map (.sectR c _) = Icc (c, a) (c, b) := by
  aesop (add safe forward [le_antisymm])

Image of Closed Interval under Section Map in Product Order: $\text{Icc}(a, b).\text{map}(\text{sectR}_c) = \text{Icc}((c, a), (c, b))$

Informal description

For a locally finite order $\alpha \times \beta$ and elements $a, b \in \beta$, the image of the closed interval $[a, b]$ under the map $\text{sectR}_c$ (where $c \in \alpha$ is fixed) is equal to the closed interval $[(c, a), (c, b)]$ in the product order $\alpha \times \beta$.

Finset.Ioc_map_sectR theorem

: (Ioc a b).map (.sectR c _) = Ioc (c, a) (c, b)

Full source

lemma Ioc_map_sectR : (Ioc a b).map (.sectR c _) = Ioc (c, a) (c, b) := by
  aesop (add safe forward [le_antisymm, le_of_lt])

Image of Open-Closed Interval under Section Map in Product Order

Informal description

For a locally finite order $\alpha \times \beta$ and elements $a, b \in \beta$, the image of the open-closed interval $(a, b]$ under the map $\text{sectR}_c$ (where $c \in \alpha$ is fixed) is equal to the open-closed interval $((c, a), (c, b)]$ in the product order $\alpha \times \beta$.

Finset.Ico_map_sectR theorem

: (Ico a b).map (.sectR c _) = Ico (c, a) (c, b)

Full source

lemma Ico_map_sectR : (Ico a b).map (.sectR c _) = Ico (c, a) (c, b) := by
  aesop (add safe forward [le_antisymm, le_of_lt])

Image of Closed-Open Interval under Section Map in Product Order: $\text{Ico}(a, b).\text{map}(\text{sectR}_c) = \text{Ico}((c, a), (c, b))$

Informal description

For a locally finite order $\alpha \times \beta$ and elements $a, b \in \beta$, the image of the closed-open interval $[a, b)$ under the map $\text{sectR}_c$ (where $c \in \alpha$ is fixed) is equal to the closed-open interval $[(c, a), (c, b))$ in the product order $\alpha \times \beta$.

Finset.Ioo_map_sectR theorem

: (Ioo a b).map (.sectR c _) = Ioo (c, a) (c, b)

Full source

lemma Ioo_map_sectR : (Ioo a b).map (.sectR c _) = Ioo (c, a) (c, b) := by
  aesop (add safe forward [le_antisymm, le_of_lt])

Image of Open Interval under Section Map in Product Order: $\text{Ioo}(a, b).\text{map}(\text{sectR}_c) = \text{Ioo}((c, a), (c, b))$

Informal description

For a locally finite order $\alpha \times \beta$ and elements $a, b \in \beta$, the image of the open interval $(a, b)$ under the map $\text{sectR}_c$ (where $c \in \alpha$ is fixed) is equal to the open interval $((c, a), (c, b))$ in the product order $\alpha \times \beta$.

Finset.Ici_erase theorem

[DecidableEq α] (a : α) : (Ici a).erase a = Ioi a

Full source

@[simp]
theorem Ici_erase [DecidableEq α] (a : α) : (Ici a).erase a = Ioi a := by
  ext
  simp_rw [Finset.mem_erase, mem_Ici, mem_Ioi, lt_iff_le_and_ne, and_comm, ne_comm]

Removing Endpoint from Closed Infinite Interval Yields Open Infinite Interval

Informal description

For any element $a$ in a locally finite order with finite intervals bounded below, the finset obtained by removing $a$ from the closed infinite interval $[a, \infty)$ is equal to the open infinite interval $(a, \infty)$. That is, $[a, \infty) \setminus \{a\} = (a, \infty)$.

Finset.Ioi_insert theorem

[DecidableEq α] (a : α) : insert a (Ioi a) = Ici a

Full source

@[simp]
theorem Ioi_insert [DecidableEq α] (a : α) : insert a (Ioi a) = Ici a := by
  ext
  simp_rw [Finset.mem_insert, mem_Ici, mem_Ioi, le_iff_lt_or_eq, or_comm, eq_comm]

Insertion into Open Infinite Interval Yields Closed Infinite Interval

Informal description

For any element $a$ in a locally finite order with finite intervals bounded below, the finset obtained by inserting $a$ into the open infinite interval $(a, \infty)$ is equal to the closed infinite interval $[a, \infty)$. That is, $\{a\} \cup (a, \infty) = [a, \infty)$.

Finset.not_mem_Ioi_self theorem

{b : α} : b ∉ Ioi b

Full source

theorem not_mem_Ioi_self {b : α} : b ∉ Ioi b := fun h => lt_irrefl _ (mem_Ioi.1 h)

Self-Exclusion from Open Infinite Interval: $b \notin (b, \infty)$

Informal description

For any element $b$ in a locally finite order with finite intervals bounded below, $b$ does not belong to the open infinite interval $(b, \infty)$.

Finset.Ici_eq_cons_Ioi theorem

(a : α) : Ici a = (Ioi a).cons a not_mem_Ioi_self

Full source

/-- `Finset.cons` version of `Finset.Ioi_insert`. -/
theorem Ici_eq_cons_Ioi (a : α) : Ici a = (Ioi a).cons a not_mem_Ioi_self := by
  classical rw [cons_eq_insert, Ioi_insert]

Closed Interval as Cons of Open Interval: $[a, \infty) = \{a\} \cup (a, \infty)$

Informal description

For any element $a$ in a locally finite order with finite intervals bounded below, the closed infinite interval $[a, \infty)$ is equal to the finset obtained by prepending $a$ to the open infinite interval $(a, \infty)$, noting that $a \notin (a, \infty)$. In symbols: $[a, \infty) = \{a\} \cup (a, \infty)$ where $a \notin (a, \infty)$.

Finset.card_Ioi_eq_card_Ici_sub_one theorem

(a : α) : #(Ioi a) = #(Ici a) - 1

Full source

theorem card_Ioi_eq_card_Ici_sub_one (a : α) : #(Ioi a) = #(Ici a) - 1 := by
  rw [Ici_eq_cons_Ioi, card_cons, Nat.add_sub_cancel_right]

Cardinality Relation Between Open and Closed Infinite Intervals: $|(a, \infty)| = |[a, \infty)| - 1$

Informal description

For any element $a$ in a locally finite order with finite intervals bounded below, the cardinality of the open infinite interval $(a, \infty)$ is equal to the cardinality of the closed infinite interval $[a, \infty)$ minus one. In symbols: $|(a, \infty)| = |[a, \infty)| - 1$.

Finset.Iic_erase theorem

[DecidableEq α] (b : α) : (Iic b).erase b = Iio b

Full source

@[simp]
theorem Iic_erase [DecidableEq α] (b : α) : (Iic b).erase b = Iio b := by
  ext
  simp_rw [Finset.mem_erase, mem_Iic, mem_Iio, lt_iff_le_and_ne, and_comm]

Removing Maximum Element from Closed Lower Interval Yields Open Lower Interval

Informal description

For any element $b$ in a locally finite order with finite lower-bounded intervals and decidable equality, the finset obtained by removing $b$ from the closed lower interval $\{x \mid x \leq b\}$ equals the open lower interval $\{x \mid x < b\}$. That is, $\text{Iic}(b) \setminus \{b\} = \text{Iio}(b)$.

Finset.Iio_insert theorem

[DecidableEq α] (b : α) : insert b (Iio b) = Iic b

Full source

@[simp]
theorem Iio_insert [DecidableEq α] (b : α) : insert b (Iio b) = Iic b := by
  ext
  simp_rw [Finset.mem_insert, mem_Iic, mem_Iio, le_iff_lt_or_eq, or_comm]

Insertion into Open Lower Interval Yields Closed Lower Interval

Informal description

For any element $b$ in a locally finite order with finite lower-bounded intervals, the finset obtained by inserting $b$ into the open lower interval $\text{Iio}(b)$ equals the closed lower interval $\text{Iic}(b)$. That is, $\text{insert}(b, \{x \mid x < b\}) = \{x \mid x \leq b\}$.

Finset.not_mem_Iio_self theorem

{b : α} : b ∉ Iio b

Full source

theorem not_mem_Iio_self {b : α} : b ∉ Iio b := fun h => lt_irrefl _ (mem_Iio.1 h)

Irreflexivity of Open Lower Interval: $b \notin \text{Iio}(b)$

Informal description

For any element $b$ in a locally finite order with finite lower-bounded intervals, $b$ does not belong to the open lower interval $\text{Iio}(b)$. That is, $b \not< b$.

Finset.Iic_eq_cons_Iio theorem

(b : α) : Iic b = (Iio b).cons b not_mem_Iio_self

Full source

/-- `Finset.cons` version of `Finset.Iio_insert`. -/
theorem Iic_eq_cons_Iio (b : α) : Iic b = (Iio b).cons b not_mem_Iio_self := by
  classical rw [cons_eq_insert, Iio_insert]

Closed Lower Interval as Cons of Open Lower Interval

Informal description

For any element $b$ in a locally finite order with finite lower-bounded intervals, the closed lower interval $\text{Iic}(b)$ is equal to the finset obtained by cons-ing $b$ onto the open lower interval $\text{Iio}(b)$, where $b \notin \text{Iio}(b)$. That is, $\{x \mid x \leq b\} = \text{cons}(b, \{x \mid x < b\})$.

Finset.card_Iio_eq_card_Iic_sub_one theorem

(a : α) : #(Iio a) = #(Iic a) - 1

Full source

theorem card_Iio_eq_card_Iic_sub_one (a : α) : #(Iio a) = #(Iic a) - 1 := by
  rw [Iic_eq_cons_Iio, card_cons, Nat.add_sub_cancel_right]

Cardinality Relation Between Open and Closed Lower Intervals: $|\text{Iio}(a)| = |\text{Iic}(a)| - 1$

Informal description

For any element $a$ in a locally finite order with finite lower-bounded intervals, the cardinality of the open lower interval $\{x \mid x < a\}$ is equal to the cardinality of the closed lower interval $\{x \mid x \leq a\}$ minus one. That is, $|\text{Iio}(a)| = |\text{Iic}(a)| - 1$.

Finset.sup'_Iic theorem

(a : α) : (Iic a).sup' nonempty_Iic id = a

Full source

lemma sup'_Iic (a : α) : (Iic a).sup' nonempty_Iic id = a :=
  le_antisymm (sup'_le _ _ fun _ ↦ mem_Iic.1) <| le_sup' (f := id) <| mem_Iic.2 <| le_refl a

Supremum of Lower-Closed Interval Equals its Upper Bound

Informal description

For any element $a$ in a locally finite order with finite lower-bounded intervals, the supremum of the lower-closed interval $\text{Iic}(a) = \{x \mid x \leq a\}$ (viewed as a finset) under the identity function equals $a$ itself. Here, $\text{sup'}$ is the supremum operation that requires a proof of nonemptiness of the finset.

Finset.sup_Iic theorem

[OrderBot α] (a : α) : (Iic a).sup id = a

Full source

@[simp] lemma sup_Iic [OrderBot α] (a : α) : (Iic a).sup id = a :=
  le_antisymm (Finset.sup_le fun _ ↦ mem_Iic.1) <| le_sup (f := id) <| mem_Iic.2 <| le_refl a

Supremum of Lower-Closed Interval Equals its Upper Bound

Informal description

Let $\alpha$ be an order with a bottom element $\bot$. For any element $a \in \alpha$, the supremum of the lower-closed interval $\{x \in \alpha \mid x \leq a\}$ (viewed as a finset) under the identity function is equal to $a$ itself. In other words, $\sup(\text{Iic}(a)) = a$.

Finset.image_subset_Iic_sup theorem

[OrderBot α] [DecidableEq α] (f : ι → α) (s : Finset ι) : s.image f ⊆ Iic (s.sup f)

Full source

lemma image_subset_Iic_sup [OrderBot α] [DecidableEq α] (f : ι → α) (s : Finset ι) :
    s.image f ⊆ Iic (s.sup f) := by
  refine fun i hi ↦ mem_Iic.2 ?_
  obtain ⟨j, hj, rfl⟩ := mem_image.1 hi
  exact le_sup hj

Image of Finite Set is Bounded by its Supremum in Lower-Closed Interval

Informal description

Let $\alpha$ be an order with a bottom element and decidable equality. For any function $f : \iota \to \alpha$ and any finite set $s$ of type $\iota$, the image of $s$ under $f$ is contained in the lower-closed interval $\text{Iic}(\sup f(s))$, i.e., $f(s) \subseteq \{x \in \alpha \mid x \leq \sup f(s)\}$.

Finset.subset_Iic_sup_id theorem

[OrderBot α] (s : Finset α) : s ⊆ Iic (s.sup id)

Full source

lemma subset_Iic_sup_id [OrderBot α] (s : Finset α) : s ⊆ Iic (s.sup id) :=
  fun _ h ↦ mem_Iic.2 <| le_sup (f := id) h

Finite Set is Contained in Lower Closure of its Supremum

Informal description

For any finite set $s$ in an order with a bottom element, every element of $s$ is less than or equal to the supremum of $s$ (with respect to the identity function), i.e., $s \subseteq \text{Iic}(\sup s)$.

Finset.inf'_Ici theorem

(a : α) : (Ici a).inf' nonempty_Ici id = a

Full source

lemma inf'_Ici (a : α) : (Ici a).inf' nonempty_Ici id = a :=
  ge_antisymm (le_inf' _ _ fun _ ↦ mem_Ici.1) <| inf'_le (f := id) <| mem_Ici.2 <| le_refl a

Infimum of Closed-Infinite Interval Equals Lower Bound

Informal description

For any element $a$ in a locally finite order with finite intervals bounded below, the infimum of the closed-infinite interval $\text{Ici}(a) = \{x \mid a \leq x\}$ under the identity function is equal to $a$, i.e., $\inf'(\text{Ici}(a)) = a$, where $\inf'$ denotes the infimum of a nonempty set.

Finset.inf_Ici theorem

[OrderTop α] (a : α) : (Ici a).inf id = a

Full source

@[simp] lemma inf_Ici [OrderTop α] (a : α) : (Ici a).inf id = a :=
  le_antisymm (inf_le (f := id) <| mem_Ici.2 <| le_refl a) <| Finset.le_inf fun _ ↦ mem_Ici.1

Infimum of Closed-Infinite Interval Equals Its Lower Bound

Informal description

For any element $a$ in an order with a top element, the infimum of the closed-infinite interval $\text{Ici}(a)$ under the identity function is equal to $a$, i.e., $\inf(\{x \mid a \leq x\}) = a$.

Finset.Ico_subset_Ico_iff theorem

{a₁ b₁ a₂ b₂ : α} (h : a₁ < b₁) : Ico a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂

Full source

theorem Ico_subset_Ico_iff {a₁ b₁ a₂ b₂ : α} (h : a₁ < b₁) :
    IcoIco a₁ b₁ ⊆ Ico a₂ b₂Ico a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂ := by
  rw [← coe_subset, coe_Ico, coe_Ico, Set.Ico_subset_Ico_iff h]

Subset Condition for Closed-Open Finset Intervals: $\text{Ico}(a₁, b₁) \subseteq \text{Ico}(a₂, b₂) \leftrightarrow a₂ \leq a₁ \land b₁ \leq b₂$

Informal description

For any elements $a₁, b₁, a₂, b₂$ in a locally finite order $\alpha$ with $a₁ < b₁$, the closed-open interval finset $\text{Ico}(a₁, b₁)$ is a subset of $\text{Ico}(a₂, b₂)$ if and only if $a₂ \leq a₁$ and $b₁ \leq b₂$.

Finset.Ico_union_Ico_eq_Ico theorem

{a b c : α} (hab : a ≤ b) (hbc : b ≤ c) : Ico a b ∪ Ico b c = Ico a c

Full source

theorem Ico_union_Ico_eq_Ico {a b c : α} (hab : a ≤ b) (hbc : b ≤ c) :
    IcoIco a b ∪ Ico b c = Ico a c := by
  rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico_eq_Ico hab hbc]

Union of Adjacent Closed-Open Intervals: $[a, b) \cup [b, c) = [a, c)$ when $a \leq b \leq c$

Informal description

For any elements $a$, $b$, and $c$ in a preorder $\alpha$ such that $a \leq b \leq c$, the union of the closed-open intervals $[a, b)$ and $[b, c)$ is equal to the closed-open interval $[a, c)$. That is, $$ [a, b) \cup [b, c) = [a, c). $$

Finset.Ioc_union_Ioc_eq_Ioc theorem

{a b c : α} (h₁ : a ≤ b) (h₂ : b ≤ c) : Ioc a b ∪ Ioc b c = Ioc a c

Full source

@[simp]
theorem Ioc_union_Ioc_eq_Ioc {a b c : α} (h₁ : a ≤ b) (h₂ : b ≤ c) :
    IocIoc a b ∪ Ioc b c = Ioc a c := by
  rw [← coe_inj, coe_union, coe_Ioc, coe_Ioc, coe_Ioc, Set.Ioc_union_Ioc_eq_Ioc h₁ h₂]

Union of Adjacent Open-Closed Intervals: $(a, b] \cup (b, c] = (a, c]$ when $a \leq b \leq c$

Informal description

For any elements $a$, $b$, and $c$ in a preorder $\alpha$ such that $a \leq b \leq c$, the union of the open-closed intervals $(a, b]$ and $(b, c]$ is equal to the open-closed interval $(a, c]$, i.e., $$ (a, b] \cup (b, c] = (a, c]. $$

Finset.Ico_subset_Ico_union_Ico theorem

{a b c : α} : Ico a c ⊆ Ico a b ∪ Ico b c

Full source

theorem Ico_subset_Ico_union_Ico {a b c : α} : IcoIco a c ⊆ Ico a b ∪ Ico b c := by
  rw [← coe_subset, coe_union, coe_Ico, coe_Ico, coe_Ico]
  exact Set.Ico_subset_Ico_union_Ico

Subset Property of Closed-Open Intervals: $[a, c) \subseteq [a, b) \cup [b, c)$

Informal description

For any elements $a$, $b$, and $c$ in a preorder $\alpha$, the closed-open interval $[a, c)$ is a subset of the union of the intervals $[a, b)$ and $[b, c)$. That is, $$ [a, c) \subseteq [a, b) \cup [b, c). $$

Finset.Ico_union_Ico' theorem

{a b c d : α} (hcb : c ≤ b) (had : a ≤ d) : Ico a b ∪ Ico c d = Ico (min a c) (max b d)

Full source

theorem Ico_union_Ico' {a b c d : α} (hcb : c ≤ b) (had : a ≤ d) :
    IcoIco a b ∪ Ico c d = Ico (min a c) (max b d) := by
  rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico' hcb had]

Union of Two Closed-Open Intervals Under Order Conditions: $[a, b) \cup [c, d) = [\min(a, c), \max(b, d))$

Informal description

For any elements $a, b, c, d$ in a locally finite order $\alpha$, if $c \leq b$ and $a \leq d$, then the union of the closed-open intervals $[a, b)$ and $[c, d)$ is equal to the closed-open interval $[\min(a, c), \max(b, d))$.

Finset.Ico_union_Ico theorem

 {a b c d : α} (h₁ : min a b ≤ max c d) (h₂ : min c d ≤ max a b) : Ico a b ∪ Ico c d = Ico (min a c) (max b d)

Full source

theorem Ico_union_Ico {a b c d : α} (h₁ : min a b ≤ max c d) (h₂ : min c d ≤ max a b) :
    IcoIco a b ∪ Ico c d = Ico (min a c) (max b d) := by
  rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico h₁ h₂]

Union of Closed-Open Intervals: $[a, b) \cup [c, d) = [\min(a, c), \max(b, d))$ under Overlap Conditions

Informal description

For any elements $a, b, c, d$ in a locally finite order $\alpha$, if $\min(a, b) \leq \max(c, d)$ and $\min(c, d) \leq \max(a, b)$, then the union of the closed-open intervals $[a, b)$ and $[c, d)$ is equal to the closed-open interval $[\min(a, c), \max(b, d))$.

Finset.Ico_inter_Ico theorem

{a b c d : α} : Ico a b ∩ Ico c d = Ico (max a c) (min b d)

Full source

theorem Ico_inter_Ico {a b c d : α} : IcoIco a b ∩ Ico c d = Ico (max a c) (min b d) := by
  rw [← coe_inj, coe_inter, coe_Ico, coe_Ico, coe_Ico, Set.Ico_inter_Ico]

Intersection of Closed-Open Interval Finsets: $\text{Ico}(a, b) \cap \text{Ico}(c, d) = \text{Ico}(\max(a, c), \min(b, d))$

Informal description

For any elements $a, b, c, d$ in a locally finite order $\alpha$, the intersection of the closed-open interval finsets $\text{Ico}(a, b)$ and $\text{Ico}(c, d)$ is equal to the closed-open interval finset $\text{Ico}(\max(a, c), \min(b, d))$. In symbols: \[ \text{Ico}(a, b) \cap \text{Ico}(c, d) = \text{Ico}(\max(a, c), \min(b, d)). \]

Finset.Ioc_inter_Ioc theorem

{a b c d : α} : Ioc a b ∩ Ioc c d = Ioc (max a c) (min b d)

Full source

theorem Ioc_inter_Ioc {a b c d : α} : IocIoc a b ∩ Ioc c d = Ioc (max a c) (min b d) := by
  rw [← coe_inj]
  push_cast
  exact Set.Ioc_inter_Ioc

Intersection of Open-Closed Interval Finsets: $\text{Ioc}(a, b) \cap \text{Ioc}(c, d) = \text{Ioc}(\max(a, c), \min(b, d))$

Informal description

For any elements $a, b, c, d$ in a locally finite order $\alpha$, the intersection of the open-closed interval finsets $\text{Ioc}(a, b)$ and $\text{Ioc}(c, d)$ is equal to the open-closed interval finset $\text{Ioc}(\max(a, c), \min(b, d))$. In symbols: \[ \text{Ioc}(a, b) \cap \text{Ioc}(c, d) = \text{Ioc}(\max(a, c), \min(b, d)). \]

Finset.Ico_filter_lt theorem

(a b c : α) : {x ∈ Ico a b | x < c} = Ico a (min b c)

Full source

@[simp]
theorem Ico_filter_lt (a b c : α) : {x ∈ Ico a b | x < c} = Ico a (min b c) := by
  cases le_total b c with
  | inl h => rw [Ico_filter_lt_of_right_le h, min_eq_left h]
  | inr h => rw [Ico_filter_lt_of_le_right h, min_eq_right h]

Filtered Closed-Open Interval Equality: $\{x \in [a,b) \mid x < c\} = [a, \min(b,c))$

Informal description

For any elements $a, b, c$ in a locally finite order $\alpha$, the finset of elements in the closed-open interval $[a, b)$ that are also less than $c$ is equal to the closed-open interval $[a, \min(b, c))$. In other words: $$\{x \in [a, b) \mid x < c\} = [a, \min(b, c))$$

Finset.Ico_filter_le theorem

(a b c : α) : {x ∈ Ico a b | c ≤ x} = Ico (max a c) b

Full source

@[simp]
theorem Ico_filter_le (a b c : α) : {x ∈ Ico a b | c ≤ x} = Ico (max a c) b := by
  cases le_total a c with
  | inl h => rw [Ico_filter_le_of_left_le h, max_eq_right h]
  | inr h => rw [Ico_filter_le_of_le_left h, max_eq_left h]

Filtered Closed-Open Interval Equality: $\{x \in [a,b) \mid c \leq x\} = [\max(a,c), b)$

Informal description

For any elements $a, b, c$ in a locally finite order $\alpha$, the filtered set $\{x \in [a, b) \mid c \leq x\}$ is equal to the interval $[\max(a, c), b)$. In other words: $$\{x \in \text{Ico}(a, b) \mid c \leq x\} = \text{Ico}(\max(a, c), b)$$

Finset.Ioo_filter_lt theorem

(a b c : α) : {x ∈ Ioo a b | x < c} = Ioo a (min b c)

Full source

@[simp]
theorem Ioo_filter_lt (a b c : α) : {x ∈ Ioo a b | x < c} = Ioo a (min b c) := by
  ext
  simp [and_assoc]

Filtered Open Interval Equality: $\{x \in (a,b) \mid x < c\} = (a, \min(b,c))$

Informal description

For any elements $a, b, c$ in a locally finite order $\alpha$, the finset of elements in the open interval $(a, b)$ that are also less than $c$ is equal to the open interval $(a, \min(b, c))$. In other words: $$\{x \in (a, b) \mid x < c\} = (a, \min(b, c))$$

Finset.Iio_filter_lt theorem

{α} [LinearOrder α] [LocallyFiniteOrderBot α] (a b : α) : {x ∈ Iio a | x < b} = Iio (min a b)

Full source

@[simp]
theorem Iio_filter_lt {α} [LinearOrder α] [LocallyFiniteOrderBot α] (a b : α) :
    {x ∈ Iio a | x < b} = Iio (min a b) := by
  ext
  simp [and_assoc]

Filtered Lower Interval Equality: $\{x < a \mid x < b\} = \{x < \min(a, b)\}$

Informal description

Let $\alpha$ be a linearly ordered type with a locally finite order where all lower-bounded intervals are finite. For any elements $a, b \in \alpha$, the finset of elements in the open lower interval $\text{Iio}(a)$ that are also less than $b$ is equal to the open lower interval $\text{Iio}(\min(a, b))$. In other words: $$\{x \in \text{Iio}(a) \mid x < b\} = \text{Iio}(\min(a, b))$$

Finset.Ico_diff_Ico_left theorem

(a b c : α) : Ico a b \ Ico a c = Ico (max a c) b

Full source

@[simp]
theorem Ico_diff_Ico_left (a b c : α) : IcoIco a b \ Ico a c = Ico (max a c) b := by
  cases le_total a c with
  | inl h =>
    ext x
    rw [mem_sdiff, mem_Ico, mem_Ico, mem_Ico, max_eq_right h, and_right_comm, not_and, not_lt]
    exact and_congr_left' ⟨fun hx => hx.2 hx.1, fun hx => ⟨h.trans hx, fun _ => hx⟩⟩
  | inr h => rw [Ico_eq_empty_of_le h, sdiff_empty, max_eq_left h]

Set Difference of Closed-Open Intervals: $[a, b) \setminus [a, c) = [\max(a, c), b)$

Informal description

For any elements $a, b, c$ in a locally finite order $\alpha$, the set difference between the closed-open intervals $[a, b)$ and $[a, c)$ is equal to the closed-open interval $[\max(a, c), b)$. In symbols: $$ [a, b) \setminus [a, c) = [\max(a, c), b). $$

Finset.Ico_diff_Ico_right theorem

(a b c : α) : Ico a b \ Ico c b = Ico a (min b c)

Full source

@[simp]
theorem Ico_diff_Ico_right (a b c : α) : IcoIco a b \ Ico c b = Ico a (min b c) := by
  cases le_total b c with
  | inl h => rw [Ico_eq_empty_of_le h, sdiff_empty, min_eq_left h]
  | inr h =>
    ext x
    rw [mem_sdiff, mem_Ico, mem_Ico, mem_Ico, min_eq_right h, and_assoc, not_and', not_le]
    exact and_congr_right' ⟨fun hx => hx.2 hx.1, fun hx => ⟨hx.trans_le h, fun _ => hx⟩⟩

Difference of Closed-Open Interval Finsets: $\text{Ico}(a, b) \setminus \text{Ico}(c, b) = \text{Ico}(a, \min(b, c))$

Informal description

For any elements $a, b, c$ in a locally finite order $\alpha$, the set difference between the closed-open interval finsets $\text{Ico}(a, b)$ and $\text{Ico}(c, b)$ is equal to the closed-open interval finset $\text{Ico}(a, \min(b, c))$. In symbols: $$ \text{Ico}(a, b) \setminus \text{Ico}(c, b) = \text{Ico}(a, \min(b, c)). $$

Finset.Ioc_disjoint_Ioc theorem

: Disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁

Full source

@[simp]
theorem Ioc_disjoint_Ioc : DisjointDisjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁ := by
  simp_rw [disjoint_iff_inter_eq_empty, Ioc_inter_Ioc, Ioc_eq_empty_iff, not_lt]

Disjointness Condition for Open-Closed Intervals: $\min(a₂, b₂) \leq \max(a₁, b₁)$

Informal description

For any elements $a₁, a₂, b₁, b₂$ in a locally finite order, the open-closed intervals $\text{Ioc}(a₁, a₂)$ and $\text{Ioc}(b₁, b₂)$ are disjoint if and only if the minimum of $a₂$ and $b₂$ is less than or equal to the maximum of $a₁$ and $b₁$. In symbols: \[ \text{Ioc}(a₁, a₂) \cap \text{Ioc}(b₁, b₂) = \emptyset \leftrightarrow \min(a₂, b₂) \leq \max(a₁, b₁). \]

Finset.Iic_diff_Ioc theorem

: Iic b \ Ioc a b = Iic (a ⊓ b)

Full source

theorem Iic_diff_Ioc : IicIic b \ Ioc a b = Iic (a ⊓ b) := by
  rw [← coe_inj]
  push_cast
  exact Set.Iic_diff_Ioc

Difference of Lower-Closed and Open-Closed Intervals Equals Lower-Closed Interval to Infimum

Informal description

For any elements $a$ and $b$ in a locally finite order, the set difference between the closed lower interval $(-\infty, b]$ and the open-closed interval $(a, b]$ is equal to the closed lower interval $(-\infty, a \sqcap b]$, where $\sqcap$ denotes the infimum of $a$ and $b$.

Finset.Iic_diff_Ioc_self_of_le theorem

(hab : a ≤ b) : Iic b \ Ioc a b = Iic a

Full source

theorem Iic_diff_Ioc_self_of_le (hab : a ≤ b) : IicIic b \ Ioc a b = Iic a := by
  rw [Iic_diff_Ioc, min_eq_left hab]

Difference of Lower and Open-Closed Intervals for $a \leq b$: $\text{Iic}(b) \setminus \text{Ioc}(a,b) = \text{Iic}(a)$

Informal description

For any elements $a$ and $b$ in a locally finite order with $a \leq b$, the set difference between the closed lower interval $(-\infty, b]$ and the open-closed interval $(a, b]$ is equal to the closed lower interval $(-\infty, a]$. In symbols: \[ \text{Iic}(b) \setminus \text{Ioc}(a,b) = \text{Iic}(a) \]

Finset.Iic_union_Ioc_eq_Iic theorem

(h : a ≤ b) : Iic a ∪ Ioc a b = Iic b

Full source

theorem Iic_union_Ioc_eq_Iic (h : a ≤ b) : IicIic a ∪ Ioc a b = Iic b := by
  rw [← coe_inj]
  push_cast
  exact Set.Iic_union_Ioc_eq_Iic h

Union of Lower and Open-Closed Intervals Equals Lower Interval: $\text{Iic}(a) \cup \text{Ioc}(a,b) = \text{Iic}(b)$ for $a \leq b$

Informal description

For any elements $a$ and $b$ in a locally finite order with $a \leq b$, the union of the finset $\text{Iic}(a)$ (all elements $\leq a$) and the finset $\text{Ioc}(a,b)$ (all elements in $(a,b]$) equals the finset $\text{Iic}(b)$ (all elements $\leq b$). In symbols: \[ \text{Iic}(a) \cup \text{Ioc}(a,b) = \text{Iic}(b) \]

Set.Infinite.exists_gt theorem

(hs : s.Infinite) : ∀ a, ∃ b ∈ s, a < b

Full source

theorem _root_.Set.Infinite.exists_gt (hs : s.Infinite) : ∀ a, ∃ b ∈ s, a < b :=
  not_bddAbove_iff.1 hs.not_bddAbove

Existence of Larger Element in Infinite Subset of Preorder

Informal description

For any infinite subset $s$ of a preorder $\alpha$ and any element $a \in \alpha$, there exists an element $b \in s$ such that $a < b$.

Set.infinite_iff_exists_gt theorem

[Nonempty α] : s.Infinite ↔ ∀ a, ∃ b ∈ s, a < b

Full source

theorem _root_.Set.infinite_iff_exists_gt [Nonempty α] : s.Infinite ↔ ∀ a, ∃ b ∈ s, a < b :=
  ⟨Set.Infinite.exists_gt, Set.infinite_of_forall_exists_gt⟩

Characterization of Infinite Subsets via Existence of Larger Elements

Informal description

For a nonempty preorder $\alpha$, a subset $s \subseteq \alpha$ is infinite if and only if for every element $a \in \alpha$, there exists an element $b \in s$ such that $a < b$.

Set.Infinite.exists_lt theorem

(hs : s.Infinite) : ∀ a, ∃ b ∈ s, b < a

Full source

theorem _root_.Set.Infinite.exists_lt (hs : s.Infinite) : ∀ a, ∃ b ∈ s, b < a :=
  not_bddBelow_iff.1 hs.not_bddBelow

Existence of Smaller Element in Infinite Subset of Preorder

Informal description

For any infinite subset $s$ of a preorder $\alpha$ and any element $a \in \alpha$, there exists an element $b \in s$ such that $b < a$.

Set.infinite_iff_exists_lt theorem

[Nonempty α] : s.Infinite ↔ ∀ a, ∃ b ∈ s, b < a

Full source

theorem _root_.Set.infinite_iff_exists_lt [Nonempty α] : s.Infinite ↔ ∀ a, ∃ b ∈ s, b < a :=
  ⟨Set.Infinite.exists_lt, Set.infinite_of_forall_exists_lt⟩

Characterization of Infinite Subsets via Existence of Smaller Elements

Informal description

For a nonempty preorder $\alpha$, a subset $s \subseteq \alpha$ is infinite if and only if for every element $a \in \alpha$, there exists an element $b \in s$ such that $b < a$.

Finset.Ioi_disjUnion_Iio theorem

(a : α) : (Ioi a).disjUnion (Iio a) (disjoint_Ioi_Iio a) = ({ a } : Finset α)ᶜ

Full source

theorem Ioi_disjUnion_Iio (a : α) :
    (Ioi a).disjUnion (Iio a) (disjoint_Ioi_Iio a) = ({a} : Finset α)ᶜ := by
  ext
  simp [eq_comm]

Disjoint Union of Open Intervals Equals Complement of Singleton: $\text{Ioi}(a) \sqcup \text{Iio}(a) = \{a\}^c$

Informal description

For any element $a$ in a locally finite order, the disjoint union of the open infinite interval $(a, \infty)$ and the open lower interval $(-\infty, a)$ is equal to the complement of the singleton set $\{a\}$ in the finset. In other words, $\text{Ioi}(a) \sqcup \text{Iio}(a) = \{a\}^c$.

Finset.uIcc_toDual theorem

(a b : α) : [[toDual a, toDual b]] = [[a, b]].map toDual.toEmbedding

Full source

theorem uIcc_toDual (a b : α) : [[toDual a, toDual b]] = [[a, b]].map toDual.toEmbedding :=
  Icc_toDual (a ⊔ b) (a ⊓ b)

Unordered Interval in Order Dual Equals Dual of Unordered Interval

Informal description

For any elements $a$ and $b$ in a lattice $\alpha$, the unordered closed interval $[[\text{toDual}(a), \text{toDual}(b)]]$ in the order dual $\alpha^\text{op}$ is equal to the image of the unordered closed interval $[[a, b]]$ in $\alpha$ under the order embedding $\text{toDual}$.

Finset.uIcc_of_le theorem

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

Full source

@[simp]
theorem 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$: $[[a, b]] = [a, 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]$, where $[[a, b]]$ denotes the finset of all elements between the infimum $a \sqcap b$ and the supremum $a \sqcup b$, and $[a, b]$ denotes the finset of all elements $x$ satisfying $a \leq x \leq b$.

Finset.uIcc_of_ge theorem

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

Full source

@[simp]
theorem 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$: $[[a, b]] = [b, 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]$, where $[[a, b]]$ denotes the finset of all elements between the infimum $a \sqcap b$ and the supremum $a \sqcup b$, and $[b, a]$ denotes the finset of all elements $x$ satisfying $b \leq x \leq a$.

Finset.uIcc_comm theorem

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

Full source

theorem uIcc_comm (a b : α) : [[a, b]] = [[b, a]] := by
  rw [uIcc, uIcc, inf_comm, sup_comm]

Commutativity of Unordered Closed Intervals: $[[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 the unordered closed interval $[[b, a]]$. Here, $[[a, b]]$ denotes the finset consisting of all elements between the infimum $a \sqcap b$ and the supremum $a \sqcup b$, inclusive.

Finset.uIcc_self theorem

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

Full source

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

Unordered Interval at a Point is Singleton: $[[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\}$.

Finset.nonempty_uIcc theorem

: Finset.Nonempty [[a, b]]

Full source

@[simp]
theorem nonempty_uIcc : Finset.Nonempty [[a, b]] :=
  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]]$ is nonempty.

Finset.Icc_subset_uIcc theorem

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

Full source

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

Inclusion of Ordered Closed Interval in Unordered Closed Interval

Informal description

For any elements $a$ and $b$ in a lattice $\alpha$, the closed interval finset $\text{Icc}(a, b)$ is a subset of the unordered closed interval finset $\text{uIcc}(a, b)$.

Finset.Icc_subset_uIcc' theorem

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

Full source

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

Inclusion of Reversed Closed Interval in Unordered Closed Interval

Informal description

For any elements $a$ and $b$ in a lattice $\alpha$, the closed interval finset $\text{Icc}(b, a)$ is a subset of the unordered closed interval finset $\text{uIcc}(a, b)$.

Finset.left_mem_uIcc theorem

: a ∈ [[a, b]]

Full source

theorem left_mem_uIcc : a ∈ [[a, b]] :=
  mem_Icc.2 ⟨inf_le_left, le_sup_left⟩

Left Endpoint Belongs to Unordered Closed Interval

Informal description

For any elements $a$ and $b$ in a lattice $\alpha$, the element $a$ belongs to the unordered closed interval finset $\text{uIcc}(a, b)$.

Finset.right_mem_uIcc theorem

: b ∈ [[a, b]]

Full source

theorem right_mem_uIcc : b ∈ [[a, b]] :=
  mem_Icc.2 ⟨inf_le_right, le_sup_right⟩

Right Endpoint Belongs to Unordered Closed Interval

Informal description

For any elements $a$ and $b$ in a lattice $\alpha$, the element $b$ belongs to the unordered closed interval finset $\text{uIcc}(a, b)$.

Finset.mem_uIcc_of_le theorem

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

Full source

theorem mem_uIcc_of_le (ha : a ≤ x) (hb : x ≤ b) : x ∈ [[a, b]] :=
  Icc_subset_uIcc <| mem_Icc.2 ⟨ha, hb⟩

Membership in Unordered Closed Interval via Bounds

Informal description

For any elements $a, b, x$ in a lattice $\alpha$, if $a \leq x$ and $x \leq b$, then $x$ belongs to the unordered closed interval finset $\text{uIcc}(a, b)$.

Finset.mem_uIcc_of_ge theorem

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

Full source

theorem mem_uIcc_of_ge (hb : b ≤ x) (ha : x ≤ a) : x ∈ [[a, b]] :=
  Icc_subset_uIcc' <| mem_Icc.2 ⟨hb, ha⟩

Membership in Unordered Closed Interval via Reverse Bounds

Informal description

For any elements $x, a, b$ in a lattice $\alpha$, if $b \leq x$ and $x \leq a$, then $x$ belongs to the unordered closed interval finset $\text{uIcc}(a, b)$.

Finset.uIcc_subset_uIcc theorem

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

Full source

theorem uIcc_subset_uIcc (h₁ : a₁ ∈ [[a₂, b₂]]) (h₂ : b₁ ∈ [[a₂, b₂]]) :
    [[a₁, b₁]][[a₁, b₁]] ⊆ [[a₂, b₂]] := by
  rw [mem_uIcc] at h₁ h₂
  exact Icc_subset_Icc (_root_.le_inf h₁.1 h₂.1) (_root_.sup_le h₁.2 h₂.2)

Subset Property of Unordered Closed Intervals: $\text{uIcc}(a₁, b₁) \subseteq \text{uIcc}(a₂, b₂)$ when $a₁, b₁ \in \text{uIcc}(a₂, b₂)$

Informal description

For any elements $a₁, a₂, b₁, b₂$ in a lattice $\alpha$, if $a₁$ and $b₁$ belong to the unordered closed interval finset $\text{uIcc}(a₂, b₂)$, then the unordered closed interval finset $\text{uIcc}(a₁, b₁)$ is a subset of $\text{uIcc}(a₂, b₂)$.

Finset.uIcc_subset_Icc theorem

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

Full source

theorem uIcc_subset_Icc (ha : a₁ ∈ Icc a₂ b₂) (hb : b₁ ∈ Icc a₂ b₂) : [[a₁, b₁]][[a₁, b₁]] ⊆ Icc a₂ b₂ := by
  rw [mem_Icc] at ha hb
  exact Icc_subset_Icc (_root_.le_inf ha.1 hb.1) (_root_.sup_le ha.2 hb.2)

Inclusion of Unordered Interval in Closed Interval: $\text{uIcc}(a₁, b₁) \subseteq \text{Icc}(a₂, b₂)$ when $a₁, b₁ \in \text{Icc}(a₂, b₂)$

Informal description

For any elements $a₁, a₂, b₁, b₂$ in a locally finite order $\alpha$, if $a₁$ and $b₁$ belong to the closed interval finset $\text{Icc}(a₂, b₂)$, then the unordered closed interval finset $\text{uIcc}(a₁, b₁)$ is a subset of $\text{Icc}(a₂, b₂)$.

Finset.uIcc_subset_uIcc_iff_mem theorem

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

Full source

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

Subset Criterion for Unordered Intervals via Membership

Informal description

For any elements $a₁, a₂, b₁, b₂$ in a lattice $\alpha$, the unordered closed interval $\text{uIcc}(a₁, b₁)$ is a subset of $\text{uIcc}(a₂, b₂)$ if and only if both $a₁$ and $b₁$ belong to $\text{uIcc}(a₂, b₂)$. In other words: \[ \text{uIcc}(a₁, b₁) \subseteq \text{uIcc}(a₂, b₂) \iff a₁ \in \text{uIcc}(a₂, b₂) \text{ and } b₁ \in \text{uIcc}(a₂, b₂). \]

Finset.uIcc_subset_uIcc_iff_le' theorem

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

Full source

theorem 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 Infima and Suprema

Informal description

For any elements $a_1, b_1, a_2, b_2$ in a lattice $\alpha$, the unordered closed interval $\text{uIcc}(a_1, b_1)$ is a subset of the unordered closed interval $\text{uIcc}(a_2, b_2)$ if and only if the infimum of $a_2$ and $b_2$ is less than or equal to the infimum of $a_1$ and $b_1$, and the supremum of $a_1$ and $b_1$ is less than or equal to the supremum of $a_2$ and $b_2$. In other words: \[ \text{uIcc}(a_1, b_1) \subseteq \text{uIcc}(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 \]

Finset.uIcc_subset_uIcc_right theorem

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

Full source

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

Right Subinterval Property: $\text{uIcc}(x, b) \subseteq \text{uIcc}(a, b)$ when $x \in \text{uIcc}(a, b)$

Informal description

For any elements $a, b, x$ in a lattice $\alpha$, if $x$ belongs to the unordered closed interval $\text{uIcc}(a, b)$, then the unordered closed interval $\text{uIcc}(x, b)$ is a subset of $\text{uIcc}(a, b)$.

Finset.uIcc_subset_uIcc_left theorem

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

Full source

theorem 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 Closed Intervals: $\text{uIcc}(a, x) \subseteq \text{uIcc}(a, b)$ when $x \in \text{uIcc}(a, b)$

Informal description

For any elements $a, b, x$ in a lattice $\alpha$, if $x$ belongs to the unordered closed interval $\text{uIcc}(a, b)$, then the unordered closed interval $\text{uIcc}(a, x)$ is a subset of $\text{uIcc}(a, b)$.

Finset.uIcc_injective_right theorem

(a : α) : Injective fun b => [[b, a]]

Full source

theorem uIcc_injective_right (a : α) : Injective fun b => [[b, a]] := fun b c h => by
  rw [Finset.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 Closed Interval Construction

Informal description

For any element $a$ in a lattice $\alpha$, the function $b \mapsto [[b, a]]$ is injective, meaning that if $[[b_1, a]] = [[b_2, a]]$ for some $b_1, b_2 \in \alpha$, then $b_1 = b_2$.

Finset.uIcc_injective_left theorem

(a : α) : Injective (uIcc a)

Full source

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

Left-Injectivity of Unordered Closed Interval Construction

Informal description

For any element $a$ in a lattice $\alpha$, the function $b \mapsto [[a, b]]$ is injective, meaning that if $[[a, b_1]] = [[a, b_2]]$ for some $b_1, b_2 \in \alpha$, then $b_1 = b_2$.

Finset.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

Closed Interval Equals Unordered Interval via Min/Max

Informal description

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

Finset.uIcc_of_not_le theorem

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

Full source

theorem uIcc_of_not_le (h : ¬a ≤ b) : [[a, b]] = Icc b a :=
  uIcc_of_ge <| le_of_not_ge h

Unordered Interval Equals Ordered Interval When $a \nleq b$: $[[a, b]] = [b, a]$

Informal description

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

Finset.uIcc_of_not_ge theorem

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

Full source

theorem uIcc_of_not_ge (h : ¬b ≤ a) : [[a, b]] = Icc a b :=
  uIcc_of_le <| le_of_not_ge h

Unordered Interval Equals Ordered Interval When $b \nleq a$: $[[a, b]] = [a, b]$

Informal description

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

Finset.uIcc_eq_union theorem

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

Full source

theorem uIcc_eq_union : [[a, b]] = IccIcc a b ∪ Icc b a :=
  coe_injective <| by
    push_cast
    exact Set.uIcc_eq_union

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]. $$

Finset.mem_uIcc' theorem

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

Full source

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

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

Informal description

An 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$.

Finset.not_mem_uIcc_of_lt theorem

: c < a → c < b → c ∉ [[a, b]]

Full source

theorem not_mem_uIcc_of_lt : c < a → c < b → c ∉ [[a, b]] := by
  rw [mem_uIcc]
  exact Set.not_mem_uIcc_of_lt

Non-membership in Unordered Interval for Elements Below Both Endpoints

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]]$.

Finset.not_mem_uIcc_of_gt theorem

: a < c → b < c → c ∉ [[a, b]]

Full source

theorem not_mem_uIcc_of_gt : a < c → b < c → c ∉ [[a, b]] := by
  rw [mem_uIcc]
  exact Set.not_mem_uIcc_of_gt

Non-membership in Unordered Interval for Elements Above Both Endpoints

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]]$.

Finset.uIcc_subset_uIcc_iff_le theorem

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

Full source

theorem 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 lattice $\alpha$, the unordered closed interval $[[a_1, b_1]]$ is a subset of the unordered closed 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$. That is: \[ [[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). \]

Finset.uIcc_subset_uIcc_union_uIcc theorem

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

Full source

/-- A sort of triangle inequality. -/
theorem uIcc_subset_uIcc_union_uIcc : [[a, c]][[a, c]] ⊆ [[a, b]] ∪ [[b, c]] :=
  coe_subset.1 <| by
    push_cast
    exact Set.uIcc_subset_uIcc_union_uIcc

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]]$. That is, every element lying between $a$ and $c$ also lies between $a$ and $b$ or between $b$ and $c$.

transGen_wcovBy_of_le theorem

[Preorder α] [LocallyFiniteOrder α] {x y : α} (hxy : x ≤ y) : TransGen (· ⩿ ·) x y

Full source

lemma transGen_wcovBy_of_le [Preorder α] [LocallyFiniteOrder α] {x y : α} (hxy : x ≤ y) :
    TransGen (· ⩿ ·) x y := by
  -- We proceed by well-founded induction on the cardinality of `Icc x y`.
  -- It's impossible for the cardinality to be zero since `x ≤ y`
  have : #(Ico x y) < #(Icc x y) := card_lt_card <|
    ⟨Ico_subset_Icc_self, not_subset.mpr ⟨y, ⟨right_mem_Icc.mpr hxy, right_not_mem_Ico⟩⟩⟩
  by_cases hxy' : y ≤ x
  -- If `y ≤ x`, then `x ⩿ y`
  · exact .single <| wcovBy_of_le_of_le hxy hxy'
  /- and if `¬ y ≤ x`, then `x < y`, not because it is a linear order, but because `x ≤ y`
  already. In that case, since `z` is maximal in `Ico x y`, then `z ⩿ y` and we can use the
  induction hypothesis to show that `Relation.TransGen (· ⩿ ·) x z`. -/
  · have h_non : (Ico x y).Nonempty := ⟨x, mem_Ico.mpr ⟨le_rfl, lt_of_le_not_le hxy hxy'⟩⟩
    obtain ⟨z, z_mem, hz⟩ := (Ico x y).exists_maximal h_non
    have z_card := calc
      #(Icc x z) ≤ #(Ico x y) := card_le_card <| Icc_subset_Ico_right (mem_Ico.mp z_mem).2
      _          < #(Icc x y) := this
    have h₁ := transGen_wcovBy_of_le (mem_Ico.mp z_mem).1
    have h₂ : z ⩿ y := by
      refine ⟨(mem_Ico.mp z_mem).2.le, fun c hzc hcy ↦ hz c ?_ hzc⟩
      exact mem_Ico.mpr <| ⟨(mem_Ico.mp z_mem).1.trans hzc.le, hcy⟩
    exact .tail h₁ h₂
termination_by #(Icc x y)

Transitive Generation of Weak Covering Relation from Inequality in Locally Finite Orders

Informal description

Let $\alpha$ be a preorder with a locally finite order structure. For any two elements $x, y \in \alpha$ such that $x \leq y$, there exists a transitive generation of the weak covering relation $\cdot \ ⩿ \ \cdot$ connecting $x$ to $y$. In other words, $x \leq y$ implies that $x$ is transitively weakly covered by $y$.

le_iff_transGen_wcovBy theorem

[Preorder α] [LocallyFiniteOrder α] {x y : α} : x ≤ y ↔ TransGen (· ⩿ ·) x y

Full source

/-- In a locally finite preorder, `≤` is the transitive closure of `⩿`. -/
lemma le_iff_transGen_wcovBy [Preorder α] [LocallyFiniteOrder α] {x y : α} :
    x ≤ y ↔ TransGen (· ⩿ ·) x y := by
  refine ⟨transGen_wcovBy_of_le, fun h ↦ ?_⟩
  induction h with
  | single h => exact h.le
  | tail _ h₁ h₂ => exact h₂.trans h₁.le

Characterization of $\leq$ as Transitive Closure of Weak Covering in Locally Finite Orders

Informal description

Let $\alpha$ be a preorder equipped with a locally finite order structure. For any two elements $x, y \in \alpha$, the relation $x \leq y$ holds if and only if there exists a transitive generation of the weak covering relation $\cdot \ ⩿ \ \cdot$ connecting $x$ to $y$.

le_iff_reflTransGen_covBy theorem

[PartialOrder α] [LocallyFiniteOrder α] {x y : α} : x ≤ y ↔ ReflTransGen (· ⋖ ·) x y

Full source

/-- In a locally finite partial order, `≤` is the reflexive transitive closure of `⋖`. -/
lemma le_iff_reflTransGen_covBy [PartialOrder α] [LocallyFiniteOrder α] {x y : α} :
    x ≤ y ↔ ReflTransGen (· ⋖ ·) x y := by
  rw [le_iff_transGen_wcovBy, wcovBy_eq_reflGen_covBy, transGen_reflGen]

Characterization of $\leq$ as Reflexive Transitive Closure of Covering Relation in Locally Finite Orders

Informal description

Let $\alpha$ be a partially ordered set with a locally finite order structure. For any two elements $x, y \in \alpha$, the relation $x \leq y$ holds if and only if there exists a reflexive transitive closure of the covering relation $\cdot \lessdot \cdot$ connecting $x$ to $y$.

transGen_covBy_of_lt theorem

[Preorder α] [LocallyFiniteOrder α] {x y : α} (hxy : x < y) : TransGen (· ⋖ ·) x y

Full source

lemma transGen_covBy_of_lt [Preorder α] [LocallyFiniteOrder α] {x y : α} (hxy : x < y) :
    TransGen (· ⋖ ·) x y := by
  -- We proceed by well-founded induction on the cardinality of `Ico x y`.
  -- It's impossible for the cardinality to be zero since `x < y`
  have h_non : (Ico x y).Nonempty := ⟨x, mem_Ico.mpr ⟨le_rfl, hxy⟩⟩
  -- `Ico x y` is a nonempty finset and so contains a maximal element `z` and
  -- `Ico x z` has cardinality strictly less than the cardinality of `Ico x y`
  obtain ⟨z, z_mem, hz⟩ := (Ico x y).exists_maximal h_non
  have z_card : #(Ico x z) < #(Ico x y) := card_lt_card <| ssubset_iff_of_subset
    (Ico_subset_Ico le_rfl (mem_Ico.mp z_mem).2.le) |>.mpr ⟨z, z_mem, right_not_mem_Ico⟩
  /- Since `z` is maximal in `Ico x y`, `z ⋖ y`. -/
  have hzy : z ⋖ y := by
    refine ⟨(mem_Ico.mp z_mem).2, fun c hc hcy ↦ ?_⟩
    exact hz _ (mem_Ico.mpr ⟨((mem_Ico.mp z_mem).1.trans_lt hc).le, hcy⟩) hc
  by_cases hxz : x < z
  /- when `x < z`, then we may use the induction hypothesis to get a chain
  `Relation.TransGen (· ⋖ ·) x z`, which we can extend with `Relation.TransGen.tail`. -/
  · exact .tail (transGen_covBy_of_lt hxz) hzy
  /- when `¬ x < z`, then actually `z ≤ x` (not because it's a linear order, but because
  `x ≤ z`), and since `z ⋖ y` we conclude that `x ⋖ y` , then `Relation.TransGen.single`. -/
  · simp only [lt_iff_le_not_le, not_and, not_not] at hxz
    exact .single (hzy.of_le_of_lt (hxz (mem_Ico.mp z_mem).1) hxy)
termination_by #(Ico x y)

Transitive Generation of Covering Relation from Strict Inequality in Locally Finite Orders

Informal description

Let $\alpha$ be a preorder with a locally finite order structure. For any two elements $x, y \in \alpha$ such that $x < y$, there exists a transitive generation of the covering relation $\cdot \lessdot \cdot$ from $x$ to $y$. In other words, $x < y$ implies that $y$ can be reached from $x$ through a finite sequence of covering relations.

lt_iff_transGen_covBy theorem

[Preorder α] [LocallyFiniteOrder α] {x y : α} : x < y ↔ TransGen (· ⋖ ·) x y

Full source

/-- In a locally finite preorder, `<` is the transitive closure of `⋖`. -/
lemma lt_iff_transGen_covBy [Preorder α] [LocallyFiniteOrder α] {x y : α} :
    x < y ↔ TransGen (· ⋖ ·) x y := by
  refine ⟨transGen_covBy_of_lt, fun h ↦ ?_⟩
  induction h with
  | single hx => exact hx.1
  | tail _ hb ih => exact ih.trans hb.1

Characterization of Strict Inequality via Covering Relation in Locally Finite Orders

Informal description

Let $\alpha$ be a preorder equipped with a locally finite order structure. For any two elements $x, y \in \alpha$, the strict inequality $x < y$ holds if and only if there exists a finite sequence of covering relations (denoted by $\cdot \lessdot \cdot$) that transitively connects $x$ to $y$.

monotone_iff_forall_wcovBy theorem

 [Preorder α] [LocallyFiniteOrder α] [Preorder β] (f : α → β) : Monotone f ↔ ∀ a b : α, a ⩿ b → f a ≤ f b

Full source

/-- A function from a locally finite preorder is monotone if and only if it is monotone when
restricted to pairs satisfying `a ⩿ b`. -/
lemma monotone_iff_forall_wcovBy [Preorder α] [LocallyFiniteOrder α] [Preorder β]
    (f : α → β) : MonotoneMonotone f ↔ ∀ a b : α, a ⩿ b → f a ≤ f b := by
  refine ⟨fun hf _ _ h ↦ hf h.le, fun h a b hab ↦ ?_⟩
  simpa [transGen_eq_self (r := ((· : β) ≤ ·)) transitive_le]
    using TransGen.lift f h <| le_iff_transGen_wcovBy.mp hab

Characterization of Monotone Functions via Weak Covering Relation in Locally Finite Orders

Informal description

Let $\alpha$ be a preorder with a locally finite order structure and $\beta$ be a preorder. A function $f \colon \alpha \to \beta$ is monotone if and only if for every pair of elements $a, b \in \alpha$ such that $a$ is weakly covered by $b$ (denoted $a \ ⩿ \ b$), we have $f(a) \leq f(b)$.

monotone_iff_forall_covBy theorem

 [PartialOrder α] [LocallyFiniteOrder α] [Preorder β] (f : α → β) : Monotone f ↔ ∀ a b : α, a ⋖ b → f a ≤ f b

Full source

/-- A function from a locally finite partial order is monotone if and only if it is monotone when
restricted to pairs satisfying `a ⋖ b`. -/
lemma monotone_iff_forall_covBy [PartialOrder α] [LocallyFiniteOrder α] [Preorder β]
    (f : α → β) : MonotoneMonotone f ↔ ∀ a b : α, a ⋖ b → f a ≤ f b := by
  refine ⟨fun hf _ _ h ↦ hf h.le, fun h a b hab ↦ ?_⟩
  simpa [reflTransGen_eq_self (r := ((· : β) ≤ ·)) IsRefl.reflexive transitive_le]
    using ReflTransGen.lift f h <| le_iff_reflTransGen_covBy.mp hab

Characterization of Monotone Functions via Covering Relation in Locally Finite Orders

Informal description

Let $\alpha$ be a partially ordered set with a locally finite order structure and $\beta$ be a preordered set. A function $f \colon \alpha \to \beta$ is monotone if and only if for every pair of elements $a, b \in \alpha$ such that $a$ is covered by $b$ (denoted $a \lessdot b$), we have $f(a) \leq f(b)$.

strictMono_iff_forall_covBy theorem

 [Preorder α] [LocallyFiniteOrder α] [Preorder β] (f : α → β) : StrictMono f ↔ ∀ a b : α, a ⋖ b → f a < f b

Full source

/-- A function from a locally finite preorder is strictly monotone if and only if it is strictly
monotone when restricted to pairs satisfying `a ⋖ b`. -/
lemma strictMono_iff_forall_covBy [Preorder α] [LocallyFiniteOrder α] [Preorder β]
    (f : α → β) : StrictMonoStrictMono f ↔ ∀ a b : α, a ⋖ b → f a < f b := by
  refine ⟨fun hf _ _ h ↦ hf h.lt, fun h a b hab ↦ ?_⟩
  have := Relation.TransGen.lift f h (a := a) (b := b)
  rw [← lt_iff_transGen_covBy, transGen_eq_self (@lt_trans β _)] at this
  exact this hab

Characterization of Strictly Monotone Functions via Covering Relation in Locally Finite Orders

Informal description

Let $\alpha$ be a preorder with a locally finite order structure and $\beta$ be a preorder. A function $f \colon \alpha \to \beta$ is strictly monotone if and only if for every pair of elements $a, b \in \alpha$ such that $a$ is covered by $b$ (denoted $a \lessdot b$), we have $f(a) < f(b)$.

antitone_iff_forall_wcovBy theorem

 [Preorder α] [LocallyFiniteOrder α] [Preorder β] (f : α → β) : Antitone f ↔ ∀ a b : α, a ⩿ b → f b ≤ f a

Full source

/-- A function from a locally finite preorder is antitone if and only if it is antitone when
restricted to pairs satisfying `a ⩿ b`. -/
lemma antitone_iff_forall_wcovBy [Preorder α] [LocallyFiniteOrder α] [Preorder β]
    (f : α → β) : AntitoneAntitone f ↔ ∀ a b : α, a ⩿ b → f b ≤ f a :=
  monotone_iff_forall_wcovBy (β := βᵒᵈ) f

Characterization of Antitone Functions via Weak Covering Relation in Locally Finite Orders

Informal description

Let $\alpha$ be a preorder with a locally finite order structure and $\beta$ be a preorder. A function $f \colon \alpha \to \beta$ is antitone if and only if for every pair of elements $a, b \in \alpha$ such that $a$ is weakly covered by $b$ (denoted $a \ ⩿ \ b$), we have $f(b) \leq f(a)$.

antitone_iff_forall_covBy theorem

 [PartialOrder α] [LocallyFiniteOrder α] [Preorder β] (f : α → β) : Antitone f ↔ ∀ a b : α, a ⋖ b → f b ≤ f a

Full source

/-- A function from a locally finite partial order is antitone if and only if it is antitone when
restricted to pairs satisfying `a ⋖ b`. -/
lemma antitone_iff_forall_covBy [PartialOrder α] [LocallyFiniteOrder α] [Preorder β]
    (f : α → β) : AntitoneAntitone f ↔ ∀ a b : α, a ⋖ b → f b ≤ f a :=
  monotone_iff_forall_covBy (β := βᵒᵈ) f

Characterization of Antitone Functions via Covering Relation in Locally Finite Orders

Informal description

Let $\alpha$ be a partially ordered set with a locally finite order structure and $\beta$ be a preordered set. A function $f \colon \alpha \to \beta$ is antitone if and only if for every pair of elements $a, b \in \alpha$ such that $a$ is covered by $b$ (denoted $a \lessdot b$), we have $f(b) \leq f(a)$.

strictAnti_iff_forall_covBy theorem

 [Preorder α] [LocallyFiniteOrder α] [Preorder β] (f : α → β) : StrictAnti f ↔ ∀ a b : α, a ⋖ b → f b < f a

Full source

/-- A function from a locally finite preorder is strictly antitone if and only if it is strictly
antitone when restricted to pairs satisfying `a ⋖ b`. -/
lemma strictAnti_iff_forall_covBy [Preorder α] [LocallyFiniteOrder α] [Preorder β]
    (f : α → β) : StrictAntiStrictAnti f ↔ ∀ a b : α, a ⋖ b → f b < f a :=
  strictMono_iff_forall_covBy (β := βᵒᵈ) f

Characterization of Strictly Antitone Functions via Covering Relation in Locally Finite Orders

Informal description

Let $\alpha$ be a preorder with a locally finite order structure and $\beta$ be a preorder. A function $f \colon \alpha \to \beta$ is strictly antitone if and only if for every pair of elements $a, b \in \alpha$ such that $a$ is covered by $b$ (denoted $a \lessdot b$), we have $f(b) < f(a)$.

TODO