Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Violeta Hernández Palacios
! This file was ported from Lean 3 source module order.bounded
! leanprover-community/mathlib commit aba57d4d3dae35460225919dcd82fe91355162f9
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Order.RelClasses
import Mathlib.Data.Set.Intervals.Basic

/-!
# Bounded and unbounded sets
We prove miscellaneous lemmas about bounded and unbounded sets. Many of these are just variations on
the same ideas, or similar results with a few minor differences. The file is divided into these
different general ideas.
-/

namespace Set

variable {α: Type ?u.2α : Type _: Type (?u.17+1)Type _} {r: α → α → Propr : α: Type ?u.2α → α: Type ?u.10568α → Prop: TypeProp} {s: Set αs t: Set αt : Set: Type ?u.14 → Type ?u.14Set α: Type ?u.2α}

/-! ### Subsets of bounded and unbounded sets -/

theorem Bounded.mono: ∀ {α : Type u_1} {r : α → α → Prop} {s t : Set α}, s ⊆ t → Bounded r t → Bounded r sBounded.mono (hst: s ⊆ thst : s: Set αs ⊆ t: Set αt) (hs: Bounded r ths : Bounded: {α : Type ?u.51} → (α → α → Prop) → Set α → PropBounded r: α → α → Propr t: Set αt) : Bounded: {α : Type ?u.62} → (α → α → Prop) → Set α → PropBounded r: α → α → Propr s: Set αs :=
hs: Bounded r ths.imp: ∀ {α : Sort ?u.76} {p q : α → Prop}, (∀ (a : α), p a → q a) → (∃ a, p a) → ∃ a, q aimp fun _: ?m.94_ ha: ?m.97ha b: ?m.100b hb: ?m.103hb => ha: ?m.97ha b: ?m.100b (hst: s ⊆ thst hb: ?m.103hb)
#align set.bounded.mono Set.Bounded.mono: ∀ {α : Type u_1} {r : α → α → Prop} {s t : Set α}, s ⊆ t → Bounded r t → Bounded r sSet.Bounded.mono

theorem Unbounded.mono: ∀ {α : Type u_1} {r : α → α → Prop} {s t : Set α}, s ⊆ t → Unbounded r s → Unbounded r tUnbounded.mono (hst: s ⊆ thst : s: Set αs ⊆ t: Set αt) (hs: Unbounded r shs : Unbounded: {α : Type ?u.180} → (α → α → Prop) → Set α → PropUnbounded r: α → α → Propr s: Set αs) : Unbounded: {α : Type ?u.191} → (α → α → Prop) → Set α → PropUnbounded r: α → α → Propr t: Set αt := fun a: ?m.206a =>
let ⟨b: αb, hb: b ∈ shb, hb': ¬r b ahb'⟩ := hs: Unbounded r shs a: ?m.206a
⟨b: αb, hst: s ⊆ thst hb: b ∈ shb, hb': ¬r b ahb'⟩
#align set.unbounded.mono Set.Unbounded.mono: ∀ {α : Type u_1} {r : α → α → Prop} {s t : Set α}, s ⊆ t → Unbounded r s → Unbounded r tSet.Unbounded.mono

/-! ### Alternate characterizations of unboundedness on orders -/

theorem unbounded_le_of_forall_exists_lt: ∀ [inst : Preorder α], (∀ (a : α), ∃ b, b ∈ s ∧ a < b) → Unbounded (fun x x_1 => x ≤ x_1) sunbounded_le_of_forall_exists_lt [Preorder: Type ?u.404 → Type ?u.404Preorder α: Type ?u.389α] (h: ∀ (a : α), ∃ b, b ∈ s ∧ a < bh : ∀ a: ?m.408a, ∃ b: ?m.414b ∈ s: Set αs, a: ?m.408a < b: ?m.414b) :
Unbounded: {α : Type ?u.451} → (α → α → Prop) → Set α → PropUnbounded (· ≤ ·): α → α → Prop(· ≤ ·) s: Set αs := fun a: ?m.527a =>
let ⟨b: αb, hb: b ∈ shb, hb': a < bhb'⟩ := h: ∀ (a : α), ∃ b, b ∈ s ∧ a < bh a: ?m.527a
⟨b: αb, hb: b ∈ shb, fun hba: ?m.595hba => hba: ?m.595hba.not_lt: ∀ {α : Type ?u.597} [inst : Preorder α] {a b : α}, a ≤ b → ¬b < anot_lt hb': a < bhb'⟩
#align set.unbounded_le_of_forall_exists_lt Set.unbounded_le_of_forall_exists_lt: ∀ {α : Type u_1} {s : Set α} [inst : Preorder α], (∀ (a : α), ∃ b, b ∈ s ∧ a < b) → Unbounded (fun x x_1 => x ≤ x_1) sSet.unbounded_le_of_forall_exists_lt

theorem unbounded_le_iff: ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α], Unbounded (fun x x_1 => x ≤ x_1) s ↔ ∀ (a : α), ∃ b, b ∈ s ∧ a < bunbounded_le_iff [LinearOrder: Type ?u.741 → Type ?u.741LinearOrder α: Type ?u.726α] : Unbounded: {α : Type ?u.744} → (α → α → Prop) → Set α → PropUnbounded (· ≤ ·): α → α → Prop(· ≤ ·) s: Set αs ↔ ∀ a: ?m.805a, ∃ b: ?m.811b ∈ s: Set αs, a: ?m.805a < b: ?m.811b := byGoals accomplished! 🐙
α: Type u_1r: α → α → Props, t: Set αinst✝: LinearOrder αUnbounded (fun x x_1 => x ≤ x_1) s ↔ ∀ (a : α), ∃ b, b ∈ s ∧ a < bsimp only [Unbounded: {α : Type ?u.1012} → (α → α → Prop) → Set α → PropUnbounded, not_le: ∀ {α : Type ?u.1014} [inst : LinearOrder α] {a b : α}, ¬a ≤ b ↔ b < anot_le]Goals accomplished! 🐙
#align set.unbounded_le_iff Set.unbounded_le_iff: ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α], Unbounded (fun x x_1 => x ≤ x_1) s ↔ ∀ (a : α), ∃ b, b ∈ s ∧ a < bSet.unbounded_le_iff

theorem unbounded_lt_of_forall_exists_le: ∀ {α : Type u_1} {s : Set α} [inst : Preorder α], (∀ (a : α), ∃ b, b ∈ s ∧ a ≤ b) → Unbounded (fun x x_1 => x < x_1) sunbounded_lt_of_forall_exists_le [Preorder: Type ?u.1309 → Type ?u.1309Preorder α: Type ?u.1294α] (h: ∀ (a : α), ∃ b, b ∈ s ∧ a ≤ bh : ∀ a: ?m.1313a, ∃ b: ?m.1319b ∈ s: Set αs, a: ?m.1313a ≤ b: ?m.1319b) :
Unbounded: {α : Type ?u.1356} → (α → α → Prop) → Set α → PropUnbounded (· < ·): α → α → Prop(· < ·) s: Set αs := fun a: ?m.1423a =>
let ⟨b: αb, hb: b ∈ shb, hb': a ≤ bhb'⟩ := h: ∀ (a : α), ∃ b, b ∈ s ∧ a ≤ bh a: ?m.1423a
⟨b: αb, hb: b ∈ shb, fun hba: ?m.1491hba => hba: ?m.1491hba.not_le: ∀ {α : Type ?u.1493} [inst : Preorder α] {a b : α}, a < b → ¬b ≤ anot_le hb': a ≤ bhb'⟩
#align set.unbounded_lt_of_forall_exists_le Set.unbounded_lt_of_forall_exists_le: ∀ {α : Type u_1} {s : Set α} [inst : Preorder α], (∀ (a : α), ∃ b, b ∈ s ∧ a ≤ b) → Unbounded (fun x x_1 => x < x_1) sSet.unbounded_lt_of_forall_exists_le

theorem unbounded_lt_iff: ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α], Unbounded (fun x x_1 => x < x_1) s ↔ ∀ (a : α), ∃ b, b ∈ s ∧ a ≤ bunbounded_lt_iff [LinearOrder: Type ?u.1637 → Type ?u.1637LinearOrder α: Type ?u.1622α] : Unbounded: {α : Type ?u.1640} → (α → α → Prop) → Set α → PropUnbounded (· < ·): α → α → Prop(· < ·) s: Set αs ↔ ∀ a: ?m.1692a, ∃ b: ?m.1698b ∈ s: Set αs, a: ?m.1692a ≤ b: ?m.1698b := byGoals accomplished! 🐙
α: Type u_1r: α → α → Props, t: Set αinst✝: LinearOrder αUnbounded (fun x x_1 => x < x_1) s ↔ ∀ (a : α), ∃ b, b ∈ s ∧ a ≤ bsimp only [Unbounded: {α : Type ?u.1899} → (α → α → Prop) → Set α → PropUnbounded, not_lt: ∀ {α : Type ?u.1901} [inst : LinearOrder α] {a b : α}, ¬a < b ↔ b ≤ anot_lt]Goals accomplished! 🐙
#align set.unbounded_lt_iff Set.unbounded_lt_iff: ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α], Unbounded (fun x x_1 => x < x_1) s ↔ ∀ (a : α), ∃ b, b ∈ s ∧ a ≤ bSet.unbounded_lt_iff

theorem unbounded_ge_of_forall_exists_gt: ∀ {α : Type u_1} {s : Set α} [inst : Preorder α], (∀ (a : α), ∃ b, b ∈ s ∧ b < a) → Unbounded (fun x x_1 => x ≥ x_1) sunbounded_ge_of_forall_exists_gt [Preorder: Type ?u.2196 → Type ?u.2196Preorder α: Type ?u.2181α] (h: ∀ (a : α), ∃ b, b ∈ s ∧ b < ah : ∀ a: ?m.2200a, ∃ b: ?m.2206b ∈ s: Set αs, b: ?m.2206b < a: ?m.2200a) :
Unbounded: {α : Type ?u.2243} → (α → α → Prop) → Set α → PropUnbounded (· ≥ ·): α → α → Prop(· ≥ ·) s: Set αs :=
@unbounded_le_of_forall_exists_lt: ∀ {α : Type ?u.2318} {s : Set α} [inst : Preorder α],
(∀ (a : α), ∃ b, b ∈ s ∧ a < b) → Unbounded (fun x x_1 => x ≤ x_1) sunbounded_le_of_forall_exists_lt α: Type ?u.2181αᵒᵈ _: Set αᵒᵈ_ _ h: ∀ (a : α), ∃ b, b ∈ s ∧ b < ah
#align set.unbounded_ge_of_forall_exists_gt Set.unbounded_ge_of_forall_exists_gt: ∀ {α : Type u_1} {s : Set α} [inst : Preorder α], (∀ (a : α), ∃ b, b ∈ s ∧ b < a) → Unbounded (fun x x_1 => x ≥ x_1) sSet.unbounded_ge_of_forall_exists_gt

theorem unbounded_ge_iff: ∀ [inst : LinearOrder α], Unbounded (fun x x_1 => x ≥ x_1) s ↔ ∀ (a : α), ∃ b, b ∈ s ∧ b < aunbounded_ge_iff [LinearOrder: Type ?u.2381 → Type ?u.2381LinearOrder α: Type ?u.2366α] : Unbounded: {α : Type ?u.2384} → (α → α → Prop) → Set α → PropUnbounded (· ≥ ·): α → α → Prop(· ≥ ·) s: Set αs ↔ ∀ a: ?m.2445a, ∃ b: ?m.2451b ∈ s: Set αs, b: ?m.2451b < a: ?m.2445a :=
⟨fun h: ?m.2649h a: ?m.2652a =>
let ⟨b: αb, hb: b ∈ shb, hba: ¬(fun x x_1 => x ≥ x_1) b ahba⟩ := h: ?m.2649h a: ?m.2652a
⟨b: αb, hb: b ∈ shb, lt_of_not_ge: ∀ {α : Type ?u.2727} [inst : LinearOrder α] {a b : α}, ¬a ≥ b → a < blt_of_not_ge hba: ¬(fun x x_1 => x ≥ x_1) b ahba⟩,
unbounded_ge_of_forall_exists_gt: ∀ {α : Type ?u.2854} {s : Set α} [inst : Preorder α],
(∀ (a : α), ∃ b, b ∈ s ∧ b < a) → Unbounded (fun x x_1 => x ≥ x_1) sunbounded_ge_of_forall_exists_gt⟩
#align set.unbounded_ge_iff Set.unbounded_ge_iff: ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α], Unbounded (fun x x_1 => x ≥ x_1) s ↔ ∀ (a : α), ∃ b, b ∈ s ∧ b < aSet.unbounded_ge_iff

theorem unbounded_gt_of_forall_exists_ge: ∀ {α : Type u_1} {s : Set α} [inst : Preorder α], (∀ (a : α), ∃ b, b ∈ s ∧ b ≤ a) → Unbounded (fun x x_1 => x > x_1) sunbounded_gt_of_forall_exists_ge [Preorder: Type ?u.3016 → Type ?u.3016Preorder α: Type ?u.3001α] (h: ∀ (a : α), ∃ b, b ∈ s ∧ b ≤ ah : ∀ a: ?m.3020a, ∃ b: ?m.3026b ∈ s: Set αs, b: ?m.3026b ≤ a: ?m.3020a) :
Unbounded: {α : Type ?u.3063} → (α → α → Prop) → Set α → PropUnbounded (· > ·): α → α → Prop(· > ·) s: Set αs := fun a: ?m.3130a =>
let ⟨b: αb, hb: b ∈ shb, hb': b ≤ ahb'⟩ := h: ∀ (a : α), ∃ b, b ∈ s ∧ b ≤ ah a: ?m.3130a
⟨b: αb, hb: b ∈ shb, fun hba: ?m.3198hba => not_le_of_gt: ∀ {α : Type ?u.3200} [inst : Preorder α] {a b : α}, a > b → ¬a ≤ bnot_le_of_gt hba: ?m.3198hba hb': b ≤ ahb'⟩
#align set.unbounded_gt_of_forall_exists_ge Set.unbounded_gt_of_forall_exists_ge: ∀ {α : Type u_1} {s : Set α} [inst : Preorder α], (∀ (a : α), ∃ b, b ∈ s ∧ b ≤ a) → Unbounded (fun x x_1 => x > x_1) sSet.unbounded_gt_of_forall_exists_ge

theorem unbounded_gt_iff: ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α], Unbounded (fun x x_1 => x > x_1) s ↔ ∀ (a : α), ∃ b, b ∈ s ∧ b ≤ aunbounded_gt_iff [LinearOrder: Type ?u.3342 → Type ?u.3342LinearOrder α: Type ?u.3327α] : Unbounded: {α : Type ?u.3345} → (α → α → Prop) → Set α → PropUnbounded (· > ·): α → α → Prop(· > ·) s: Set αs ↔ ∀ a: ?m.3397a, ∃ b: ?m.3403b ∈ s: Set αs, b: ?m.3403b ≤ a: ?m.3397a :=
⟨fun h: ?m.3601h a: ?m.3604a =>
let ⟨b: αb, hb: b ∈ shb, hba: ¬(fun x x_1 => x > x_1) b ahba⟩ := h: ?m.3601h a: ?m.3604a
⟨b: αb, hb: b ∈ shb, le_of_not_gt: ∀ {α : Type ?u.3679} [inst : LinearOrder α] {a b : α}, ¬a > b → a ≤ ble_of_not_gt hba: ¬(fun x x_1 => x > x_1) b ahba⟩,
unbounded_gt_of_forall_exists_ge: ∀ {α : Type ?u.3806} {s : Set α} [inst : Preorder α],
(∀ (a : α), ∃ b, b ∈ s ∧ b ≤ a) → Unbounded (fun x x_1 => x > x_1) sunbounded_gt_of_forall_exists_ge⟩
#align set.unbounded_gt_iff Set.unbounded_gt_iff: ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α], Unbounded (fun x x_1 => x > x_1) s ↔ ∀ (a : α), ∃ b, b ∈ s ∧ b ≤ aSet.unbounded_gt_iff

/-! ### Relation between boundedness by strict and nonstrict orders. -/

/-! #### Less and less or equal -/

theorem Bounded.rel_mono: ∀ {r' : α → α → Prop}, Bounded r s → r ≤ r' → Bounded r' sBounded.rel_mono {r': α → α → Propr' : α: Type ?u.3953α → α: Type ?u.3953α → Prop: TypeProp} (h: Bounded r sh : Bounded: {α : Type ?u.3974} → (α → α → Prop) → Set α → PropBounded r: α → α → Propr s: Set αs) (hrr': r ≤ r'hrr' : r: α → α → Propr ≤ r': α → α → Propr') : Bounded: {α : Type ?u.4049} → (α → α → Prop) → Set α → PropBounded r': α → α → Propr' s: Set αs :=
let ⟨a: αa, ha: ∀ (b : α), b ∈ s → r b aha⟩ := h: Bounded r sh
⟨a: αa, fun b: ?m.4121b hb: ?m.4124hb => hrr': r ≤ r'hrr' b: ?m.4121b a: αa (ha: ∀ (b : α), b ∈ s → r b aha b: ?m.4121b hb: ?m.4124hb)⟩
#align set.bounded.rel_mono Set.Bounded.rel_mono: ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {r' : α → α → Prop}, Bounded r s → r ≤ r' → Bounded r' sSet.Bounded.rel_mono

theorem bounded_le_of_bounded_lt: ∀ [inst : Preorder α], Bounded (fun x x_1 => x < x_1) s → Bounded (fun x x_1 => x ≤ x_1) sbounded_le_of_bounded_lt [Preorder: Type ?u.4257 → Type ?u.4257Preorder α: Type ?u.4242α] (h: Bounded (fun x x_1 => x < x_1) sh : Bounded: {α : Type ?u.4260} → (α → α → Prop) → Set α → PropBounded (· < ·): α → α → Prop(· < ·) s: Set αs) : Bounded: {α : Type ?u.4313} → (α → α → Prop) → Set α → PropBounded (· ≤ ·): α → α → Prop(· ≤ ·) s: Set αs :=
h: Bounded (fun x x_1 => x < x_1) sh.rel_mono: ∀ {α : Type ?u.4402} {r : α → α → Prop} {s : Set α} {r' : α → α → Prop}, Bounded r s → r ≤ r' → Bounded r' srel_mono fun _: ?m.4429_ _: ?m.4432_ => le_of_lt: ∀ {α : Type ?u.4434} [inst : Preorder α] {a b : α}, a < b → a ≤ ble_of_lt
#align set.bounded_le_of_bounded_lt Set.bounded_le_of_bounded_lt: ∀ {α : Type u_1} {s : Set α} [inst : Preorder α], Bounded (fun x x_1 => x < x_1) s → Bounded (fun x x_1 => x ≤ x_1) sSet.bounded_le_of_bounded_lt

theorem Unbounded.rel_mono: ∀ {r' : α → α → Prop}, r' ≤ r → Unbounded r s → Unbounded r' sUnbounded.rel_mono {r': α → α → Propr' : α: Type ?u.4475α → α: Type ?u.4475α → Prop: TypeProp} (hr: r' ≤ rhr : r': α → α → Propr' ≤ r: α → α → Propr) (h: Unbounded r sh : Unbounded: {α : Type ?u.4559} → (α → α → Prop) → Set α → PropUnbounded r: α → α → Propr s: Set αs) : Unbounded: {α : Type ?u.4571} → (α → α → Prop) → Set α → PropUnbounded r': α → α → Propr' s: Set αs :=
fun a: ?m.4588a =>
let ⟨b: αb, hb: b ∈ shb, hba: ¬r b ahba⟩ := h: Unbounded r sh a: ?m.4588a
⟨b: αb, hb: b ∈ shb, fun hba': ?m.4652hba' => hba: ¬r b ahba (hr: r' ≤ rhr b: αb a: ?m.4588a hba': ?m.4652hba')⟩
#align set.unbounded.rel_mono Set.Unbounded.rel_mono: ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {r' : α → α → Prop}, r' ≤ r → Unbounded r s → Unbounded r' sSet.Unbounded.rel_mono

theorem unbounded_lt_of_unbounded_le: ∀ [inst : Preorder α], Unbounded (fun x x_1 => x ≤ x_1) s → Unbounded (fun x x_1 => x < x_1) sunbounded_lt_of_unbounded_le [Preorder: Type ?u.4778 → Type ?u.4778Preorder α: Type ?u.4763α] (h: Unbounded (fun x x_1 => x ≤ x_1) sh : Unbounded: {α : Type ?u.4781} → (α → α → Prop) → Set α → PropUnbounded (· ≤ ·): α → α → Prop(· ≤ ·) s: Set αs) : Unbounded: {α : Type ?u.4843} → (α → α → Prop) → Set α → PropUnbounded (· < ·): α → α → Prop(· < ·) s: Set αs :=
h: Unbounded (fun x x_1 => x ≤ x_1) sh.rel_mono: ∀ {α : Type ?u.4923} {r : α → α → Prop} {s : Set α} {r' : α → α → Prop}, r' ≤ r → Unbounded r s → Unbounded r' srel_mono fun _: ?m.4948_ _: ?m.4951_ => le_of_lt: ∀ {α : Type ?u.4953} [inst : Preorder α] {a b : α}, a < b → a ≤ ble_of_lt
#align set.unbounded_lt_of_unbounded_le Set.unbounded_lt_of_unbounded_le: ∀ {α : Type u_1} {s : Set α} [inst : Preorder α],
Unbounded (fun x x_1 => x ≤ x_1) s → Unbounded (fun x x_1 => x < x_1) sSet.unbounded_lt_of_unbounded_le

theorem bounded_le_iff_bounded_lt: ∀ [inst : Preorder α] [inst_1 : NoMaxOrder α], Bounded (fun x x_1 => x ≤ x_1) s ↔ Bounded (fun x x_1 => x < x_1) sbounded_le_iff_bounded_lt [Preorder: Type ?u.5016 → Type ?u.5016Preorder α: Type ?u.5001α] [NoMaxOrder: (α : Type ?u.5019) → [inst : LT α] → PropNoMaxOrder α: Type ?u.5001α] :
Bounded: {α : Type ?u.5033} → (α → α → Prop) → Set α → PropBounded (· ≤ ·): α → α → Prop(· ≤ ·) s: Set αs ↔ Bounded: {α : Type ?u.5093} → (α → α → Prop) → Set α → PropBounded (· < ·): α → α → Prop(· < ·) s: Set αs := byGoals accomplished! 🐙
α: Type u_1r: α → α → Props, t: Set αinst✝¹: Preorder αinst✝: NoMaxOrder αBounded (fun x x_1 => x ≤ x_1) s ↔ Bounded (fun x x_1 => x < x_1) srefine' ⟨fun h: ?m.5177h => _: ?m.5173_, bounded_le_of_bounded_lt: ∀ {α : Type ?u.5183} {s : Set α} [inst : Preorder α],
Bounded (fun x x_1 => x < x_1) s → Bounded (fun x x_1 => x ≤ x_1) sbounded_le_of_bounded_lt⟩α: Type u_1r: α → α → Props, t: Set αinst✝¹: Preorder αinst✝: NoMaxOrder αh: Bounded (fun x x_1 => x ≤ x_1) sBounded (fun x x_1 => x < x_1) s
α: Type u_1r: α → α → Props, t: Set αinst✝¹: Preorder αinst✝: NoMaxOrder αBounded (fun x x_1 => x ≤ x_1) s ↔ Bounded (fun x x_1 => x < x_1) scases' h: ?m.5177h with a: ?m.5239a ha: ?m.5240 ahaα: Type u_1r: α → α → Props, t: Set αinst✝¹: Preorder αinst✝: NoMaxOrder αa: αha: ∀ (b : α), b ∈ s → (fun x x_1 => x ≤ x_1) b aintroBounded (fun x x_1 => x < x_1) s
α: Type u_1r: α → α → Props, t: Set αinst✝¹: Preorder αinst✝: NoMaxOrder αBounded (fun x x_1 => x ≤ x_1) s ↔ Bounded (fun x x_1 => x < x_1) scases' exists_gt: ∀ {α : Type ?u.5272} [inst : LT α] [self : NoMaxOrder α] (a : α), ∃ b, a < bexists_gt a: ?m.5239a with b: ?m.5317b hb: ?m.5318 bhbα: Type u_1r: α → α → Props, t: Set αinst✝¹: Preorder αinst✝: NoMaxOrder αa: αha: ∀ (b : α), b ∈ s → (fun x x_1 => x ≤ x_1) b ab: αhb: a < bintro.introBounded (fun x x_1 => x < x_1) s
α: Type u_1r: α → α → Props, t: Set αinst✝¹: Preorder αinst✝: NoMaxOrder αBounded (fun x x_1 => x ≤ x_1) s ↔ Bounded (fun x x_1 => x < x_1) sexact ⟨b: ?m.5317b, fun c: ?m.5359c hc: ?m.5362hc => lt_of_le_of_lt: ∀ {α : Type ?u.5364} [inst : Preorder α] {a b c : α}, a ≤ b → b < c → a < clt_of_le_of_lt (ha: ?m.5240 aha c: ?m.5359c hc: ?m.5362hc) hb: ?m.5318 bhb⟩Goals accomplished! 🐙
#align set.bounded_le_iff_bounded_lt Set.bounded_le_iff_bounded_lt: ∀ {α : Type u_1} {s : Set α} [inst : Preorder α] [inst_1 : NoMaxOrder α],
Bounded (fun x x_1 => x ≤ x_1) s ↔ Bounded (fun x x_1 => x < x_1) sSet.bounded_le_iff_bounded_lt

theorem unbounded_lt_iff_unbounded_le: ∀ [inst : Preorder α] [inst_1 : NoMaxOrder α], Unbounded (fun x x_1 => x < x_1) s ↔ Unbounded (fun x x_1 => x ≤ x_1) sunbounded_lt_iff_unbounded_le [Preorder: Type ?u.5439 → Type ?u.5439Preorder α: Type ?u.5424α] [NoMaxOrder: (α : Type ?u.5442) → [inst : LT α] → PropNoMaxOrder α: Type ?u.5424α] :
Unbounded: {α : Type ?u.5456} → (α → α → Prop) → Set α → PropUnbounded (· < ·): α → α → Prop(· < ·) s: Set αs ↔ Unbounded: {α : Type ?u.5507} → (α → α → Prop) → Set α → PropUnbounded (· ≤ ·): α → α → Prop(· ≤ ·) s: Set αs := byGoals accomplished! 🐙
α: Type u_1r: α → α → Props, t: Set αinst✝¹: Preorder αinst✝: NoMaxOrder αUnbounded (fun x x_1 => x < x_1) s ↔ Unbounded (fun x x_1 => x ≤ x_1) ssimp_rw [α: Type u_1r: α → α → Props, t: Set αinst✝¹: Preorder αinst✝: NoMaxOrder αUnbounded (fun x x_1 => x < x_1) s ↔ Unbounded (fun x x_1 => x ≤ x_1) s← not_bounded_iff: ∀ {α : Type ?u.5672} {r : α → α → Prop} (s : Set α), ¬Bounded r s ↔ Unbounded r snot_bounded_iff,α: Type u_1r: α → α → Props, t: Set αinst✝¹: Preorder αinst✝: NoMaxOrder α¬Bounded (fun x x_1 => x < x_1) s ↔ ¬Bounded (fun x x_1 => x ≤ x_1) s α: Type u_1r: α → α → Props, t: Set αinst✝¹: Preorder αinst✝: NoMaxOrder αUnbounded (fun x x_1 => x < x_1) s ↔ Unbounded (fun x x_1 => x ≤ x_1) sbounded_le_iff_bounded_ltGoals accomplished! 🐙]Goals accomplished! 🐙
#align set.unbounded_lt_iff_unbounded_le Set.unbounded_lt_iff_unbounded_le: ∀ {α : Type u_1} {s : Set α} [inst : Preorder α] [inst_1 : NoMaxOrder α],
Unbounded (fun x x_1 => x < x_1) s ↔ Unbounded (fun x x_1 => x ≤ x_1) sSet.unbounded_lt_iff_unbounded_le

/-! #### Greater and greater or equal -/

theorem bounded_ge_of_bounded_gt: ∀ {α : Type u_1} {s : Set α} [inst : Preorder α], Bounded (fun x x_1 => x > x_1) s → Bounded (fun x x_1 => x ≥ x_1) sbounded_ge_of_bounded_gt [Preorder: Type ?u.5969 → Type ?u.5969Preorder α: Type ?u.5954α] (h: Bounded (fun x x_1 => x > x_1) sh : Bounded: {α : Type ?u.5972} → (α → α → Prop) → Set α → PropBounded (· > ·): α → α → Prop(· > ·) s: Set αs) : Bounded: {α : Type ?u.6025} → (α → α → Prop) → Set α → PropBounded (· ≥ ·): α → α → Prop(· ≥ ·) s: Set αs :=
let ⟨a: αa, ha: ∀ (b : α), b ∈ s → (fun x x_1 => x > x_1) b aha⟩ := h: Bounded (fun x x_1 => x > x_1) sh
⟨a: αa, fun b: ?m.6190b hb: ?m.6193hb => le_of_lt: ∀ {α : Type ?u.6195} [inst : Preorder α] {a b : α}, a < b → a ≤ ble_of_lt (ha: ∀ (b : α), b ∈ s → (fun x x_1 => x > x_1) b aha b: ?m.6190b hb: ?m.6193hb)⟩
#align set.bounded_ge_of_bounded_gt Set.bounded_ge_of_bounded_gt: ∀ {α : Type u_1} {s : Set α} [inst : Preorder α], Bounded (fun x x_1 => x > x_1) s → Bounded (fun x x_1 => x ≥ x_1) sSet.bounded_ge_of_bounded_gt

theorem unbounded_gt_of_unbounded_ge: ∀ {α : Type u_1} {s : Set α} [inst : Preorder α],
Unbounded (fun x x_1 => x ≥ x_1) s → Unbounded (fun x x_1 => x > x_1) sunbounded_gt_of_unbounded_ge [Preorder: Type ?u.6369 → Type ?u.6369Preorder α: Type ?u.6354α] (h: Unbounded (fun x x_1 => x ≥ x_1) sh : Unbounded: {α : Type ?u.6372} → (α → α → Prop) → Set α → PropUnbounded (· ≥ ·): α → α → Prop(· ≥ ·) s: Set αs) : Unbounded: {α : Type ?u.6434} → (α → α → Prop) → Set α → PropUnbounded (· > ·): α → α → Prop(· > ·) s: Set αs :=
fun a: ?m.6515a =>
let ⟨b: αb, hb: b ∈ shb, hba: ¬(fun x x_1 => x ≥ x_1) b ahba⟩ := h: Unbounded (fun x x_1 => x ≥ x_1) sh a: ?m.6515a
⟨b: αb, hb: b ∈ shb, fun hba': ?m.6595hba' => hba: ¬(fun x x_1 => x ≥ x_1) b ahba (le_of_lt: ∀ {α : Type ?u.6597} [inst : Preorder α] {a b : α}, a < b → a ≤ ble_of_lt hba': ?m.6595hba')⟩
#align set.unbounded_gt_of_unbounded_ge Set.unbounded_gt_of_unbounded_ge: ∀ {α : Type u_1} {s : Set α} [inst : Preorder α],
Unbounded (fun x x_1 => x ≥ x_1) s → Unbounded (fun x x_1 => x > x_1) sSet.unbounded_gt_of_unbounded_ge

theorem bounded_ge_iff_bounded_gt: ∀ [inst : Preorder α] [inst_1 : NoMinOrder α], Bounded (fun x x_1 => x ≥ x_1) s ↔ Bounded (fun x x_1 => x > x_1) sbounded_ge_iff_bounded_gt [Preorder: Type ?u.6750 → Type ?u.6750Preorder α: Type ?u.6735α] [NoMinOrder: (α : Type ?u.6753) → [inst : LT α] → PropNoMinOrder α: Type ?u.6735α] :
Bounded: {α : Type ?u.6767} → (α → α → Prop) → Set α → PropBounded (· ≥ ·): α → α → Prop(· ≥ ·) s: Set αs ↔ Bounded: {α : Type ?u.6827} → (α → α → Prop) → Set α → PropBounded (· > ·): α → α → Prop(· > ·) s: Set αs :=
@bounded_le_iff_bounded_lt: ∀ {α : Type ?u.6900} {s : Set α} [inst : Preorder α] [inst_1 : NoMaxOrder α],
Bounded (fun x x_1 => x ≤ x_1) s ↔ Bounded (fun x x_1 => x < x_1) sbounded_le_iff_bounded_lt α: Type ?u.6735αᵒᵈ _: Set αᵒᵈ_ _ _
#align set.bounded_ge_iff_bounded_gt Set.bounded_ge_iff_bounded_gt: ∀ {α : Type u_1} {s : Set α} [inst : Preorder α] [inst_1 : NoMinOrder α],
Bounded (fun x x_1 => x ≥ x_1) s ↔ Bounded (fun x x_1 => x > x_1) sSet.bounded_ge_iff_bounded_gt

theorem unbounded_gt_iff_unbounded_ge: ∀ {α : Type u_1} {s : Set α} [inst : Preorder α] [inst_1 : NoMinOrder α],
Unbounded (fun x x_1 => x > x_1) s ↔ Unbounded (fun x x_1 => x ≥ x_1) sunbounded_gt_iff_unbounded_ge [Preorder: Type ?u.6967 → Type ?u.6967Preorder α: Type ?u.6952α] [NoMinOrder: (α : Type ?u.6970) → [inst : LT α] → PropNoMinOrder α: Type ?u.6952α] :
Unbounded: {α : Type ?u.6984} → (α → α → Prop) → Set α → PropUnbounded (· > ·): α → α → Prop(· > ·) s: Set αs ↔ Unbounded: {α : Type ?u.7035} → (α → α → Prop) → Set α → PropUnbounded (· ≥ ·): α → α → Prop(· ≥ ·) s: Set αs :=
@unbounded_lt_iff_unbounded_le: ∀ {α : Type ?u.7117} {s : Set α} [inst : Preorder α] [inst_1 : NoMaxOrder α],
Unbounded (fun x x_1 => x < x_1) s ↔ Unbounded (fun x x_1 => x ≤ x_1) sunbounded_lt_iff_unbounded_le α: Type ?u.6952αᵒᵈ _: Set αᵒᵈ_ _ _
#align set.unbounded_gt_iff_unbounded_ge Set.unbounded_gt_iff_unbounded_ge: ∀ {α : Type u_1} {s : Set α} [inst : Preorder α] [inst_1 : NoMinOrder α],
Unbounded (fun x x_1 => x > x_1) s ↔ Unbounded (fun x x_1 => x ≥ x_1) sSet.unbounded_gt_iff_unbounded_ge

/-! ### The universal set -/

theorem unbounded_le_univ: ∀ [inst : LE α] [inst_1 : NoTopOrder α], Unbounded (fun x x_1 => x ≤ x_1) univunbounded_le_univ [LE: Type ?u.7184 → Type ?u.7184LE α: Type ?u.7169α] [NoTopOrder: (α : Type ?u.7187) → [inst : LE α] → PropNoTopOrder α: Type ?u.7169α] : Unbounded: {α : Type ?u.7195} → (α → α → Prop) → Set α → PropUnbounded (· ≤ ·): α → α → Prop(· ≤ ·) (@Set.univ: {α : Type ?u.7249} → Set αSet.univ α: Type ?u.7169α) := fun a: ?m.7264a =>
let ⟨b: αb, hb: ¬b ≤ ahb⟩ := exists_not_le: ∀ {α : Type ?u.7266} [inst : LE α] [self : NoTopOrder α] (a : α), ∃ b, ¬b ≤ aexists_not_le a: ?m.7264a
⟨b: αb, ⟨⟩: True⟨⟩, hb: ¬b ≤ ahb⟩
#align set.unbounded_le_univ Set.unbounded_le_univ: ∀ {α : Type u_1} [inst : LE α] [inst_1 : NoTopOrder α], Unbounded (fun x x_1 => x ≤ x_1) univSet.unbounded_le_univ

theorem unbounded_lt_univ: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : NoTopOrder α], Unbounded (fun x x_1 => x < x_1) univunbounded_lt_univ [Preorder: Type ?u.7421 → Type ?u.7421Preorder α: Type ?u.7406α] [NoTopOrder: (α : Type ?u.7424) → [inst : LE α] → PropNoTopOrder α: Type ?u.7406α] : Unbounded: {α : Type ?u.7438} → (α → α → Prop) → Set α → PropUnbounded (· < ·): α → α → Prop(· < ·) (@Set.univ: {α : Type ?u.7486} → Set αSet.univ α: Type ?u.7406α) :=
unbounded_lt_of_unbounded_le: ∀ {α : Type ?u.7505} {s : Set α} [inst : Preorder α],
Unbounded (fun x x_1 => x ≤ x_1) s → Unbounded (fun x x_1 => x < x_1) sunbounded_lt_of_unbounded_le unbounded_le_univ: ∀ {α : Type ?u.7536} [inst : LE α] [inst_1 : NoTopOrder α], Unbounded (fun x x_1 => x ≤ x_1) univunbounded_le_univ
#align set.unbounded_lt_univ Set.unbounded_lt_univ: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : NoTopOrder α], Unbounded (fun x x_1 => x < x_1) univSet.unbounded_lt_univ

theorem unbounded_ge_univ: ∀ {α : Type u_1} [inst : LE α] [inst_1 : NoBotOrder α], Unbounded (fun x x_1 => x ≥ x_1) univunbounded_ge_univ [LE: Type ?u.7601 → Type ?u.7601LE α: Type ?u.7586α] [NoBotOrder: (α : Type ?u.7604) → [inst : LE α] → PropNoBotOrder α: Type ?u.7586α] : Unbounded: {α : Type ?u.7612} → (α → α → Prop) → Set α → PropUnbounded (· ≥ ·): α → α → Prop(· ≥ ·) (@Set.univ: {α : Type ?u.7666} → Set αSet.univ α: Type ?u.7586α) := fun a: ?m.7681a =>
let ⟨b: αb, hb: ¬a ≤ bhb⟩ := exists_not_ge: ∀ {α : Type ?u.7683} [inst : LE α] [self : NoBotOrder α] (a : α), ∃ b, ¬a ≤ bexists_not_ge a: ?m.7681a
⟨b: αb, ⟨⟩: True⟨⟩, hb: ¬a ≤ bhb⟩
#align set.unbounded_ge_univ Set.unbounded_ge_univ: ∀ {α : Type u_1} [inst : LE α] [inst_1 : NoBotOrder α], Unbounded (fun x x_1 => x ≥ x_1) univSet.unbounded_ge_univ

theorem unbounded_gt_univ: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : NoBotOrder α], Unbounded (fun x x_1 => x > x_1) univunbounded_gt_univ [Preorder: Type ?u.7838 → Type ?u.7838Preorder α: Type ?u.7823α] [NoBotOrder: (α : Type ?u.7841) → [inst : LE α] → PropNoBotOrder α: Type ?u.7823α] : Unbounded: {α : Type ?u.7855} → (α → α → Prop) → Set α → PropUnbounded (· > ·): α → α → Prop(· > ·) (@Set.univ: {α : Type ?u.7903} → Set αSet.univ α: Type ?u.7823α) :=
unbounded_gt_of_unbounded_ge: ∀ {α : Type ?u.7922} {s : Set α} [inst : Preorder α],
Unbounded (fun x x_1 => x ≥ x_1) s → Unbounded (fun x x_1 => x > x_1) sunbounded_gt_of_unbounded_ge unbounded_ge_univ: ∀ {α : Type ?u.7953} [inst : LE α] [inst_1 : NoBotOrder α], Unbounded (fun x x_1 => x ≥ x_1) univunbounded_ge_univ
#align set.unbounded_gt_univ Set.unbounded_gt_univ: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : NoBotOrder α], Unbounded (fun x x_1 => x > x_1) univSet.unbounded_gt_univ

/-! ### Bounded and unbounded intervals -/

theorem bounded_self: ∀ (a : α), Bounded r { b | r b a }bounded_self (a: αa : α: Type ?u.8003α) : Bounded: {α : Type ?u.8020} → (α → α → Prop) → Set α → PropBounded r: α → α → Propr { b: ?m.8033b | r: α → α → Propr b: ?m.8033b a: αa } :=
⟨a: αa, fun _: ?m.8056_ => id: ∀ {α : Sort ?u.8058}, α → αid⟩
#align set.bounded_self Set.bounded_self: ∀ {α : Type u_1} {r : α → α → Prop} (a : α), Bounded r { b | r b a }Set.bounded_self

/-! #### Half-open bounded intervals -/

theorem bounded_lt_Iio: ∀ {α : Type u_1} [inst : Preorder α] (a : α), Bounded (fun x x_1 => x < x_1) (Iio a)bounded_lt_Iio [Preorder: Type ?u.8092 → Type ?u.8092Preorder α: Type ?u.8077α] (a: αa : α: Type ?u.8077α) : Bounded: {α : Type ?u.8097} → (α → α → Prop) → Set α → PropBounded (· < ·): α → α → Prop(· < ·) (Iio: {α : Type ?u.8145} → [inst : Preorder α] → α → Set αIio a: αa) :=
bounded_self: ∀ {α : Type ?u.8184} {r : α → α → Prop} (a : α), Bounded r { b | r b a }bounded_self a: αa
#align set.bounded_lt_Iio Set.bounded_lt_Iio: ∀ {α : Type u_1} [inst : Preorder α] (a : α), Bounded (fun x x_1 => x < x_1) (Iio a)Set.bounded_lt_Iio

theorem bounded_le_Iio: ∀ [inst : Preorder α] (a : α), Bounded (fun x x_1 => x ≤ x_1) (Iio a)bounded_le_Iio [Preorder: Type ?u.8220 → Type ?u.8220Preorder α: Type ?u.8205α] (a: αa : α: Type ?u.8205α) : Bounded: {α : Type ?u.8225} → (α → α → Prop) → Set α → PropBounded (· ≤ ·): α → α → Prop(· ≤ ·) (Iio: {α : Type ?u.8282} → [inst : Preorder α] → α → Set αIio a: αa) :=
bounded_le_of_bounded_lt: ∀ {α : Type ?u.8321} {s : Set α} [inst : Preorder α],
Bounded (fun x x_1 => x < x_1) s → Bounded (fun x x_1 => x ≤ x_1) sbounded_le_of_bounded_lt (bounded_lt_Iio: ∀ {α : Type ?u.8351} [inst : Preorder α] (a : α), Bounded (fun x x_1 => x < x_1) (Iio a)bounded_lt_Iio a: αa)
#align set.bounded_le_Iio Set.bounded_le_Iio: ∀ {α : Type u_1} [inst : Preorder α] (a : α), Bounded (fun x x_1 => x ≤ x_1) (Iio a)Set.bounded_le_Iio

theorem bounded_le_Iic: ∀ [inst : Preorder α] (a : α), Bounded (fun x x_1 => x ≤ x_1) (Iic a)bounded_le_Iic [Preorder: Type ?u.8374 → Type ?u.8374Preorder α: Type ?u.8359α] (a: αa : α: Type ?u.8359α) : Bounded: {α : Type ?u.8379} → (α → α → Prop) → Set α → PropBounded (· ≤ ·): α → α → Prop(· ≤ ·) (Iic: {α : Type ?u.8436} → [inst : Preorder α] → α → Set αIic a: αa) :=
bounded_self: ∀ {α : Type ?u.8475} {r : α → α → Prop} (a : α), Bounded r { b | r b a }bounded_self a: αa
#align set.bounded_le_Iic Set.bounded_le_Iic: ∀ {α : Type u_1} [inst : Preorder α] (a : α), Bounded (fun x x_1 => x ≤ x_1) (Iic a)Set.bounded_le_Iic

theorem bounded_lt_Iic: ∀ [inst : Preorder α] [inst_1 : NoMaxOrder α] (a : α), Bounded (fun x x_1 => x < x_1) (Iic a)bounded_lt_Iic [Preorder: Type ?u.8511 → Type ?u.8511Preorder α: Type ?u.8496α] [NoMaxOrder: (α : Type ?u.8514) → [inst : LT α] → PropNoMaxOrder α: Type ?u.8496α] (a: αa : α: Type ?u.8496α) : Bounded: {α : Type ?u.8530} → (α → α → Prop) → Set α → PropBounded (· < ·): α → α → Prop(· < ·) (Iic: {α : Type ?u.8578} → [inst : Preorder α] → α → Set αIic a: αa) := byGoals accomplished! 🐙
α: Type u_1r: α → α → Props, t: Set αinst✝¹: Preorder αinst✝: NoMaxOrder αa: αBounded (fun x x_1 => x < x_1) (Iic a)simp only [← bounded_le_iff_bounded_lt: ∀ {α : Type ?u.8627} {s : Set α} [inst : Preorder α] [inst_1 : NoMaxOrder α],
Bounded (fun x x_1 => x ≤ x_1) s ↔ Bounded (fun x x_1 => x < x_1) sbounded_le_iff_bounded_lt, bounded_le_Iic: ∀ {α : Type ?u.8653} [inst : Preorder α] (a : α), Bounded (fun x x_1 => x ≤ x_1) (Iic a)bounded_le_Iic]Goals accomplished! 🐙
#align set.bounded_lt_Iic Set.bounded_lt_Iic: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : NoMaxOrder α] (a : α), Bounded (fun x x_1 => x < x_1) (Iic a)Set.bounded_lt_Iic

theorem bounded_gt_Ioi: ∀ {α : Type u_1} [inst : Preorder α] (a : α), Bounded (fun x x_1 => x > x_1) (Ioi a)bounded_gt_Ioi [Preorder: Type ?u.8793 → Type ?u.8793Preorder α: Type ?u.8778α] (a: αa : α: Type ?u.8778α) : Bounded: {α : Type ?u.8798} → (α → α → Prop) → Set α → PropBounded (· > ·): α → α → Prop(· > ·) (Ioi: {α : Type ?u.8846} → [inst : Preorder α] → α → Set αIoi a: αa) :=
bounded_self: ∀ {α : Type ?u.8885} {r : α → α → Prop} (a : α), Bounded r { b | r b a }bounded_self a: αa
#align set.bounded_gt_Ioi Set.bounded_gt_Ioi: ∀ {α : Type u_1} [inst : Preorder α] (a : α), Bounded (fun x x_1 => x > x_1) (Ioi a)Set.bounded_gt_Ioi

theorem bounded_ge_Ioi: ∀ [inst : Preorder α] (a : α), Bounded (fun x x_1 => x ≥ x_1) (Ioi a)bounded_ge_Ioi [Preorder: Type ?u.8921 → Type ?u.8921Preorder α: Type ?u.8906α] (a: αa : α: Type ?u.8906α) : Bounded: {α : Type ?u.8926} → (α → α → Prop) → Set α → PropBounded (· ≥ ·): α → α → Prop(· ≥ ·) (Ioi: {α : Type ?u.8983} → [inst : Preorder α] → α → Set αIoi a: αa) :=
bounded_ge_of_bounded_gt: ∀ {α : Type ?u.9022} {s : Set α} [inst : Preorder α],
Bounded (fun x x_1 => x > x_1) s → Bounded (fun x x_1 => x ≥ x_1) sbounded_ge_of_bounded_gt (bounded_gt_Ioi: ∀ {α : Type ?u.9052} [inst : Preorder α] (a : α), Bounded (fun x x_1 => x > x_1) (Ioi a)bounded_gt_Ioi a: αa)
#align set.bounded_ge_Ioi Set.bounded_ge_Ioi: ∀ {α : Type u_1} [inst : Preorder α] (a : α), Bounded (fun x x_1 => x ≥ x_1) (Ioi a)Set.bounded_ge_Ioi

theorem bounded_ge_Ici: ∀ [inst : Preorder α] (a : α), Bounded (fun x x_1 => x ≥ x_1) (Ici a)bounded_ge_Ici [Preorder: Type ?u.9075 → Type ?u.9075Preorder α: Type ?u.9060α] (a: αa : α: Type ?u.9060α) : Bounded: {α : Type ?u.9080} → (α → α → Prop) → Set α → PropBounded (· ≥ ·): α → α → Prop(· ≥ ·) (Ici: {α : Type ?u.9137} → [inst : Preorder α] → α → Set αIci a: αa) :=
bounded_self: ∀ {α : Type ?u.9176} {r : α → α → Prop} (a : α), Bounded r { b | r b a }bounded_self a: αa
#align set.bounded_ge_Ici Set.bounded_ge_Ici: ∀ {α : Type u_1} [inst : Preorder α] (a : α), Bounded (fun x x_1 => x ≥ x_1) (Ici a)Set.bounded_ge_Ici

theorem bounded_gt_Ici: ∀ [inst : Preorder α] [inst_1 : NoMinOrder α] (a : α), Bounded (fun x x_1 => x > x_1) (Ici a)bounded_gt_Ici [Preorder: Type ?u.9212 → Type ?u.9212Preorder α: Type ?u.9197α] [NoMinOrder: (α : Type ?u.9215) → [inst : LT α] → PropNoMinOrder α: Type ?u.9197α] (a: αa : α: Type ?u.9197α) : Bounded: {α : Type ?u.9231} → (α → α → Prop) → Set α → PropBounded (· > ·): α → α → Prop(· > ·) (Ici: {α : Type ?u.9279} → [inst : Preorder α] → α → Set αIci a: αa) := byGoals accomplished! 🐙
α: Type u_1r: α → α → Props, t: Set αinst✝¹: Preorder αinst✝: NoMinOrder αa: αBounded (fun x x_1 => x > x_1) (Ici a)simp only [← bounded_ge_iff_bounded_gt: ∀ {α : Type ?u.9328} {s : Set α} [inst : Preorder α] [inst_1 : NoMinOrder α],
Bounded (fun x x_1 => x ≥ x_1) s ↔ Bounded (fun x x_1 => x > x_1) sbounded_ge_iff_bounded_gt, bounded_ge_Ici: ∀ {α : Type ?u.9352} [inst : Preorder α] (a : α), Bounded (fun x x_1 => x ≥ x_1) (Ici a)bounded_ge_Ici]Goals accomplished! 🐙
#align set.bounded_gt_Ici Set.bounded_gt_Ici: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : NoMinOrder α] (a : α), Bounded (fun x x_1 => x > x_1) (Ici a)Set.bounded_gt_Ici

/-! #### Other bounded intervals -/

theorem bounded_lt_Ioo: ∀ {α : Type u_1} [inst : Preorder α] (a b : α), Bounded (fun x x_1 => x < x_1) (Ioo a b)bounded_lt_Ioo [Preorder: Type ?u.9507 → Type ?u.9507Preorder α: Type ?u.9492α] (a: αa b: αb : α: Type ?u.9492α) : Bounded: {α : Type ?u.9514} → (α → α → Prop) → Set α → PropBounded (· < ·): α → α → Prop(· < ·) (Ioo: {α : Type ?u.9562} → [inst : Preorder α] → α → α → Set αIoo a: αa b: αb) :=
(bounded_lt_Iio: ∀ {α : Type ?u.9603} [inst : Preorder α] (a : α), Bounded (fun x x_1 => x < x_1) (Iio a)bounded_lt_Iio b: αb).mono: ∀ {α : Type ?u.9609} {r : α → α → Prop} {s t : Set α}, s ⊆ t → Bounded r t → Bounded r smono Set.Ioo_subset_Iio_self: ∀ {α : Type ?u.9631} [inst : Preorder α] {a b : α}, Ioo a b ⊆ Iio bSet.Ioo_subset_Iio_self
#align set.bounded_lt_Ioo Set.bounded_lt_Ioo: ∀ {α : Type u_1} [inst : Preorder α] (a b : α), Bounded (fun x x_1 => x < x_1) (Ioo a b)Set.bounded_lt_Ioo

theorem bounded_lt_Ico: ∀ [inst : Preorder α] (a b : α), Bounded (fun x x_1 => x < x_1) (Ico a b)bounded_lt_Ico [Preorder: Type ?u.9678 → Type ?u.9678Preorder α: Type ?u.9663α] (a: αa b: αb : α: Type ?u.9663α) : Bounded: {α : Type ?u.9685} → (α → α → Prop) → Set α → PropBounded (· < ·): α → α → Prop(· < ·) (Ico: {α : Type ?u.9733} → [inst : Preorder α] → α → α → Set αIco a: αa b: αb) :=
(bounded_lt_Iio: ∀ {α : Type ?u.9774} [inst : Preorder α] (a : α), Bounded (fun x x_1 => x < x_1) (Iio a)bounded_lt_Iio b: αb).mono: ∀ {α : Type ?u.9780} {r : α → α → Prop} {s t : Set α}, s ⊆ t → Bounded r t → Bounded r smono Set.Ico_subset_Iio_self: ∀ {α : Type ?u.9802} [inst : Preorder α] {a b : α}, Ico a b ⊆ Iio bSet.Ico_subset_Iio_self
#align set.bounded_lt_Ico Set.bounded_lt_Ico: ∀ {α : Type u_1} [inst : Preorder α] (a b : α), Bounded (fun x x_1 => x < x_1) (Ico a b)Set.bounded_lt_Ico

theorem bounded_lt_Ioc: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : NoMaxOrder α] (a b : α), Bounded (fun x x_1 => x < x_1) (Ioc a b)bounded_lt_Ioc [Preorder: Type ?u.9849 → Type ?u.9849Preorder α: Type ?u.9834α] [NoMaxOrder: (α : Type ?u.9852) → [inst : LT α] → PropNoMaxOrder α: Type ?u.9834α] (a: αa b: αb : α: Type ?u.9834α) : Bounded: {α : Type ?u.9870} → (α → α → Prop) → Set α → PropBounded (· < ·): α → α → Prop(· < ·) (Ioc: {α : Type ?u.9918} → [inst : Preorder α] → α → α → Set αIoc a: αa b: αb) :=
(bounded_lt_Iic: ∀ {α : Type ?u.9956} [inst : Preorder α] [inst_1 : NoMaxOrder α] (a : α), Bounded (fun x x_1 => x < x_1) (Iic a)bounded_lt_Iic b: αb).mono: ∀ {α : Type ?u.9966} {r : α → α → Prop} {s t : Set α}, s ⊆ t → Bounded r t → Bounded r smono Set.Ioc_subset_Iic_self: ∀ {α : Type ?u.9988} [inst : Preorder α] {a b : α}, Ioc a b ⊆ Iic bSet.Ioc_subset_Iic_self
#align set.bounded_lt_Ioc Set.bounded_lt_Ioc: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : NoMaxOrder α] (a b : α), Bounded (fun x x_1 => x < x_1) (Ioc a b)Set.bounded_lt_Ioc

theorem bounded_lt_Icc: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : NoMaxOrder α] (a b : α), Bounded (fun x x_1 => x < x_1) (Icc a b)bounded_lt_Icc [Preorder: Type ?u.10036 → Type ?u.10036Preorder α: Type ?u.10021α] [NoMaxOrder: (α : Type ?u.10039) → [inst : LT α] → PropNoMaxOrder α: Type ?u.10021α] (a: αa b: αb : α: Type ?u.10021α) : Bounded: {α : Type ?u.10057} → (α → α → Prop) → Set α → PropBounded (· < ·): α → α → Prop(· < ·) (Icc: {α : Type ?u.10105} → [inst : Preorder α] → α → α → Set αIcc a: αa b: αb) :=
(bounded_lt_Iic: ∀ {α : Type ?u.10143} [inst : Preorder α] [inst_1 : NoMaxOrder α] (a : α), Bounded (fun x x_1 => x < x_1) (Iic a)bounded_lt_Iic b: αb).mono: ∀ {α : Type ?u.10153} {r : α → α → Prop} {s t : Set α}, s ⊆ t → Bounded r t → Bounded r smono Set.Icc_subset_Iic_self: ∀ {α : Type ?u.10175} [inst : Preorder α] {a b : α}, Icc a b ⊆ Iic bSet.Icc_subset_Iic_self
#align set.bounded_lt_Icc Set.bounded_lt_Icc: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : NoMaxOrder α] (a b : α), Bounded (fun x x_1 => x < x_1) (Icc a b)Set.bounded_lt_Icc

theorem bounded_le_Ioo: ∀ [inst : Preorder α] (a b : α), Bounded (fun x x_1 => x ≤ x_1) (Ioo a b)bounded_le_Ioo [Preorder: Type ?u.10223 → Type ?u.10223Preorder α: Type ?u.10208α] (a: αa b: αb : α: Type ?u.10208α) : Bounded: {α : Type ?u.10230} → (α → α → Prop) → Set α → PropBounded (· ≤ ·): α → α → Prop(· ≤ ·) (Ioo: {α : Type ?u.10287} → [inst : Preorder α] → α → α → Set αIoo a: αa b: αb) :=
(bounded_le_Iio: ∀ {α : Type ?u.10328} [inst : Preorder α] (a : α), Bounded (fun x x_1 => x ≤ x_1) (Iio a)bounded_le_Iio b: αb).mono: ∀ {α : Type ?u.10334} {r : α → α → Prop} {s t : Set α}, s ⊆ t → Bounded r t → Bounded r smono Set.Ioo_subset_Iio_self: ∀ {α : Type ?u.10356} [inst : Preorder α] {a b : α}, Ioo a b ⊆ Iio bSet.Ioo_subset_Iio_self
#align set.bounded_le_Ioo Set.bounded_le_Ioo: ∀ {α : Type u_1} [inst : Preorder α] (a b : α), Bounded (fun x x_1 => x ≤ x_1) (Ioo a b)Set.bounded_le_Ioo

theorem bounded_le_Ico: ∀ [inst : Preorder α] (a b : α), Bounded (fun x x_1 => x ≤ x_1) (Ico a b)bounded_le_Ico [Preorder: Type ?u.10403 → Type ?u.10403Preorder α: Type ?u.10388α] (a: αa b: αb : α: Type ?u.10388α) : Bounded: {α : Type ?u.10410} → (α → α → Prop) → Set α → PropBounded (· ≤ ·): α → α → Prop(· ≤ ·) (Ico: {α : Type ?u.10467} → [inst : Preorder α] → α → α → Set αIco a: αa b: αb) :=
(bounded_le_Iio: ∀ {α : Type ?u.10508} [inst : Preorder α] (a : α), Bounded (fun x x_1 => x ≤ x_1) (Iio a)bounded_le_Iio b: αb).mono: ∀ {α : Type ?u.10514} {r : α → α → Prop} {s t : Set α}, s ⊆ t → Bounded r t → Bounded r smono Set.Ico_subset_Iio_self: ∀ {α : Type ?u.10536} [inst : Preorder α] {a b : α}, Ico a b ⊆ Iio bSet.Ico_subset_Iio_self
#align set.bounded_le_Ico Set.bounded_le_Ico: ∀ {α : Type u_1} [inst : Preorder α] (a b : α), Bounded (fun x x_1 => x ≤ x_1) (Ico a b)Set.bounded_le_Ico

theorem bounded_le_Ioc: ∀ [inst : Preorder α] (a b : α), Bounded (fun x x_1 => x ≤ x_1) (Ioc a b)bounded_le_Ioc [Preorder: Type ?u.10583 → Type ?u.10583Preorder α: Type ?u.10568α] (a: αa b: αb : α: Type ?u.10568α) : Bounded: {α : Type ?u.10590} → (α → α → Prop) → Set α → PropBounded (· ≤ ·): α → α → Prop(· ≤ ·) (Ioc: {α : Type ?u.10647} → [inst : Preorder α] → α → α → Set αIoc a: αa b: αb) :=
(bounded_le_Iic: ∀ {α : Type ?u.10688} [inst : Preorder α] (a : α), Bounded (fun x x_1 => x ≤ x_1) (Iic a)bounded_le_Iic b: αb).mono: ∀ {α : Type ?u.10694} {r : α → α → Prop} {s t : Set α}, s ⊆ t → Bounded r t → Bounded r smono Set.Ioc_subset_Iic_self: ∀ {α : Type ?u.10716} [inst : Preorder α] {a b : α}, Ioc a b ⊆ Iic bSet.Ioc_subset_Iic_self
#align set.bounded_le_Ioc Set.bounded_le_Ioc: ∀ {α : Type u_1} [inst : Preorder α] (a b : α), Bounded (fun x x_1 => x ≤ x_1) (Ioc a b)Set.bounded_le_Ioc

theorem bounded_le_Icc: ∀ [inst : Preorder α] (a b : α), Bounded (fun x x_1 => x ≤ x_1) (Icc a b)bounded_le_Icc [Preorder: Type ?u.10763 → Type ?u.10763Preorder α: Type ?u.10748α] (a: αa b: αb : α: Type ?u.10748α) : Bounded: {α : Type ?u.10770} → (α → α → Prop) → Set α → PropBounded (· ≤ ·): α → α → Prop(· ≤ ·) (Icc: {α : Type ?u.10827} → [inst : Preorder α] → α → α → Set αIcc a: αa b: αb) :=
(bounded_le_Iic: ∀ {α : Type ?u.10868} [inst : Preorder α] (a : α), Bounded (fun x x_1 => x ≤ x_1) (Iic a)bounded_le_Iic b: αb).mono: ∀ {α : Type ?u.10874} {r : α → α → Prop} {s t : Set α}, s ⊆ t → Bounded r t → Bounded r smono Set.Icc_subset_Iic_self: ∀ {α : Type ?u.10896} [inst : Preorder α] {a b : α}, Icc a b ⊆ Iic bSet.Icc_subset_Iic_self
#align set.bounded_le_Icc Set.bounded_le_Icc: ∀ {α : Type u_1} [inst : Preorder α] (a b : α), Bounded (fun x x_1 => x ≤ x_1) (Icc a b)Set.bounded_le_Icc

theorem bounded_gt_Ioo: ∀ {α : Type u_1} [inst : Preorder α] (a b : α), Bounded (fun x x_1 => x > x_1) (Ioo a b)bounded_gt_Ioo [Preorder: Type ?u.10943 → Type ?u.10943Preorder α: Type ?u.10928α] (a: αa b: αb : α: Type ?u.10928α) : Bounded: {α : Type ?u.10950} → (α → α → Prop) → Set α → PropBounded (· > ·): α → α → Prop(· > ·) (Ioo: {α : Type ?u.10998} → [inst : Preorder α] → α → α → Set αIoo a: αa b: αb) :=
(bounded_gt_Ioi: ∀ {α : Type ?u.11039} [inst : Preorder α] (a : α), Bounded (fun x x_1 => x > x_1) (Ioi a)bounded_gt_Ioi a: αa).mono: ∀ {α : Type ?u.11045} {r : α → α → Prop} {s t : Set α}, s ⊆ t → Bounded r t → Bounded r smono Set.Ioo_subset_Ioi_self: ∀ {α : Type ?u.11067} [inst : Preorder α] {a b : α}, Ioo a b ⊆ Ioi aSet.Ioo_subset_Ioi_self
#align set.bounded_gt_Ioo Set.bounded_gt_Ioo: ∀ {α : Type u_1} [inst : Preorder α] (a b : α), Bounded (fun x x_1 => x > x_1) (Ioo a b)Set.bounded_gt_Ioo

theorem bounded_gt_Ioc: ∀ {α : Type u_1} [inst : Preorder α] (a b : α), Bounded (fun x x_1 => x > x_1) (Ioc a b)bounded_gt_Ioc [Preorder: Type ?u.11114 → Type ?u.11114Preorder α: Type ?u.11099α] (a: αa b: αb : α: Type ?u.11099α) : Bounded: {α : Type ?u.11121} → (α → α → Prop) → Set α → PropBounded (· > ·): α → α → Prop(· > ·) (Ioc: {α : Type ?u.11169} → [inst : Preorder α] → α → α → Set αIoc a: αa b: αb) :=
(bounded_gt_Ioi: ∀ {α : Type ?u.11210} [inst : Preorder α] (a : α), Bounded (fun x x_1 => x > x_1) (Ioi a)bounded_gt_Ioi a: αa).mono: ∀ {α : Type ?u.11216} {r : α → α → Prop} {s t : Set α}, s ⊆ t → Bounded r t → Bounded r smono Set.Ioc_subset_Ioi_self: ∀ {α : Type ?u.11238} [inst : Preorder α] {a b : α}, Ioc a b ⊆ Ioi aSet.Ioc_subset_Ioi_self
#align set.bounded_gt_Ioc Set.bounded_gt_Ioc: ∀ {α : Type u_1} [inst : Preorder α] (a b : α), Bounded (fun x x_1 => x > x_1) (Ioc a b)Set.bounded_gt_Ioc

theorem bounded_gt_Ico: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : NoMinOrder α] (a b : α), Bounded (fun x x_1 => x > x_1) (Ico a b)bounded_gt_Ico [Preorder: Type ?u.11285 → Type ?u.11285Preorder α: Type ?u.11270α] [NoMinOrder: (α : Type ?u.11288) → [inst : LT α] → PropNoMinOrder α: Type ?u.11270α] (a: αa b: αb : α: Type ?u.11270α) : Bounded: {α : Type ?u.11306} → (α → α → Prop) → Set α → PropBounded (· > ·): α → α → Prop(· > ·) (Ico: {α : Type ?u.11354} → [inst : Preorder α] → α → α → Set αIco a: αa b: αb) :=
(bounded_gt_Ici: ∀ {α : Type ?u.11392} [inst : Preorder α] [inst_1 : NoMinOrder α] (a : α), Bounded (fun x x_1 => x > x_1) (Ici a)bounded_gt_Ici a: αa).mono: ∀ {α : Type ?u.11402} {r : α → α → Prop} {s t : Set α}, s ⊆ t → Bounded r t → Bounded r smono Set.Ico_subset_Ici_self: ∀ {α : Type ?u.11424} [inst : Preorder α] {a b : α}, Ico a b ⊆ Ici aSet.Ico_subset_Ici_self
#align set.bounded_gt_Ico Set.bounded_gt_Ico: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : NoMinOrder α] (a b : α), Bounded (fun x x_1 => x > x_1) (Ico a b)Set.bounded_gt_Ico

theorem bounded_gt_Icc: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : NoMinOrder α] (a b : α), Bounded (fun x x_1 => x > x_1) (Icc a b)bounded_gt_Icc [Preorder: Type ?u.11472 → Type ?u.11472Preorder α: Type ?u.11457α] [NoMinOrder: (α : Type ?u.11475) → [inst : LT α] → PropNoMinOrder α: Type ?u.11457α] (a: αa b: αb : α: Type ?u.11457α) : Bounded: {α : Type ?u.11493} → (α → α → Prop) → Set α → PropBounded (· > ·): α → α → Prop(· > ·) (Icc: {α : Type ?u.11541} → [inst : Preorder α] → α → α → Set αIcc a: αa b: αb) :=
(bounded_gt_Ici: ∀ {α : Type ?u.11579} [inst : Preorder α] [inst_1 : NoMinOrder α] (a : α), Bounded (fun x x_1 => x > x_1) (Ici a)bounded_gt_Ici a: αa).mono: ∀ {α : Type ?u.11589} {r : α → α → Prop} {s t : Set α}, s ⊆ t → Bounded r t → Bounded r smono Set.Icc_subset_Ici_self: ∀ {α : Type ?u.11611} [inst : Preorder α] {a b : α}, Icc a b ⊆ Ici aSet.Icc_subset_Ici_self
#align set.bounded_gt_Icc Set.bounded_gt_Icc: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : NoMinOrder α] (a b : α), Bounded (fun x x_1 => x > x_1) (Icc a b)Set.bounded_gt_Icc

theorem bounded_ge_Ioo: ∀ {α : Type u_1} [inst : Preorder α] (a b : α), Bounded (fun x x_1 => x ≥ x_1) (Ioo a b)bounded_ge_Ioo [Preorder: Type ?u.11659 → Type ?u.11659Preorder α: Type ?u.11644α] (a: αa b: αb : α: Type ?u.11644α) : Bounded: {α : Type ?u.11666} → (α → α → Prop) → Set α → PropBounded (· ≥ ·): α → α → Prop(· ≥ ·) (Ioo: {α : Type ?u.11723} → [inst : Preorder α] → α → α → Set αIoo a: αa b: αb) :=
(bounded_ge_Ioi: ∀ {α : Type ?u.11764} [inst : Preorder α] (a : α), Bounded (fun x x_1 => x ≥ x_1) (Ioi a)bounded_ge_Ioi a: αa).mono: ∀ {α : Type ?u.11770} {r : α → α → Prop} {s t : Set α}, s ⊆ t → Bounded r t → Bounded r smono Set.Ioo_subset_Ioi_self: ∀ {α : Type ?u.11792} [inst : Preorder α] {a b : α}, Ioo a b ⊆ Ioi aSet.Ioo_subset_Ioi_self
#align set.bounded_ge_Ioo Set.bounded_ge_Ioo: ∀ {α : Type u_1} [inst : Preorder α] (a b : α), Bounded (fun x x_1 => x ≥ x_1) (Ioo a b)Set.bounded_ge_Ioo

theorem bounded_ge_Ioc: ∀ {α : Type u_1} [inst : Preorder α] (a b : α), Bounded (fun x x_1 => x ≥ x_1) (Ioc a b)bounded_ge_Ioc [Preorder: Type ?u.11839 → Type ?u.11839Preorder α: Type ?u.11824α] (a: αa b: αb : α: Type ?u.11824α) : Bounded: {α : Type ?u.11846} → (α → α → Prop) → Set α → PropBounded (· ≥ ·): α → α → Prop(· ≥ ·) (Ioc: {α : Type ?u.11903} → [inst : Preorder α] → α → α → Set αIoc a: αa b: αb) :=
(bounded_ge_Ioi: ∀ {α : Type ?u.11944} [inst : Preorder α] (a : α), Bounded (fun x x_1 => x ≥ x_1) (Ioi a)bounded_ge_Ioi a: αa).mono: ∀ {α : Type ?u.11950} {r : α → α → Prop} {s t : Set α}, s ⊆ t → Bounded r t → Bounded r smono Set.Ioc_subset_Ioi_self: ∀ {α : Type ?u.11972} [inst : Preorder α] {a b : α}, Ioc a b ⊆ Ioi aSet.Ioc_subset_Ioi_self
#align set.bounded_ge_Ioc Set.bounded_ge_Ioc: ∀ {α : Type u_1} [inst : Preorder α] (a b : α), Bounded (fun x x_1 => x ≥ x_1) (Ioc a b)Set.bounded_ge_Ioc

theorem bounded_ge_Ico: ∀ [inst : Preorder α] (a b : α), Bounded (fun x x_1 => x ≥ x_1) (Ico a b)bounded_ge_Ico [Preorder: Type ?u.12019 → Type ?u.12019Preorder α: Type ?u.12004α] (a: αa b: αb : α: Type ?u.12004α) : Bounded: {α : Type ?u.12026} → (α → α → Prop) → Set α → PropBounded (· ≥ ·): α → α → Prop(· ≥ ·) (Ico: {α : Type ?u.12083} → [inst : Preorder α] → α → α → Set αIco a: αa b: αb) :=
(bounded_ge_Ici: ∀ {α : Type ?u.12124} [inst : Preorder α] (a : α), Bounded (fun x x_1 => x ≥ x_1) (Ici a)bounded_ge_Ici a: αa).mono: ∀ {α : Type ?u.12130} {r : α → α → Prop} {s t : Set α}, s ⊆ t → Bounded r t → Bounded r smono Set.Ico_subset_Ici_self: ∀ {α : Type ?u.12152} [inst : Preorder α] {a b : α}, Ico a b ⊆ Ici aSet.Ico_subset_Ici_self
#align set.bounded_ge_Ico Set.bounded_ge_Ico: ∀ {α : Type u_1} [inst : Preorder α] (a b : α), Bounded (fun x x_1 => x ≥ x_1) (Ico a b)Set.bounded_ge_Ico

theorem bounded_ge_Icc: ∀ [inst : Preorder α] (a b : α), Bounded (fun x x_1 => x ≥ x_1) (Icc a b)bounded_ge_Icc [Preorder: Type ?u.12199 → Type ?u.12199Preorder α: Type ?u.12184α] (a: αa b: αb : α: Type ?u.12184α) : Bounded: {α : Type ?u.12206} → (α → α → Prop) → Set α → PropBounded (· ≥ ·): α → α → Prop(· ≥ ·) (Icc: {α : Type ?u.12263} → [inst : Preorder α] → α → α → Set αIcc a: αa b: αb) :=
(bounded_ge_Ici: ∀ {α : Type ?u.12304} [inst : Preorder α] (a : α), Bounded (fun x x_1 => x ≥ x_1) (Ici a)bounded_ge_Ici a: αa).mono: ∀ {α : Type ?u.12310} {r : α → α → Prop} {s t : Set α}, s ⊆ t → Bounded r t → Bounded r smono Set.Icc_subset_Ici_self: ∀ {α : Type ?u.12332} [inst : Preorder α] {a b : α}, Icc a b ⊆ Ici aSet.Icc_subset_Ici_self
#align set.bounded_ge_Icc Set.bounded_ge_Icc: ∀ {α : Type u_1} [inst : Preorder α] (a b : α), Bounded (fun x x_1 => x ≥ x_1) (Icc a b)Set.bounded_ge_Icc

/-! #### Unbounded intervals -/

theorem unbounded_le_Ioi: ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : NoMaxOrder α] (a : α), Unbounded (fun x x_1 => x ≤ x_1) (Ioi a)unbounded_le_Ioi [SemilatticeSup: Type ?u.12379 → Type ?u.12379SemilatticeSup α: Type ?u.12364α] [NoMaxOrder: (α : Type ?u.12382) → [inst : LT α] → PropNoMaxOrder α: Type ?u.12364α] (a: αa : α: Type ?u.12364α) :
Unbounded: {α : Type ?u.12484} → (α → α → Prop) → Set α → PropUnbounded (· ≤ ·): α → α → Prop(· ≤ ·) (Ioi: {α : Type ?u.12541} → [inst : Preorder α] → α → Set αIoi a: αa) := fun b: ?m.12710b =>
let ⟨c: αc, hc: a ⊔ b < chc⟩ := exists_gt: ∀ {α : Type ?u.12712} [inst : LT α] [self : NoMaxOrder α] (a : α), ∃ b, a < bexists_gt (a: αa ⊔ b: ?m.12710b)
⟨c: αc, le_sup_left: ∀ {α : Type ?u.12889} [inst : SemilatticeSup α] {a b : α}, a ≤ a ⊔ ble_sup_left.trans_lt: ∀ {α : Type ?u.12904} [inst : Preorder α] {a b c : α}, a ≤ b → b < c → a < ctrans_lt hc: a ⊔ b < chc, (le_sup_right: ∀ {α : Type ?u.13038} [inst : SemilatticeSup α] {a b : α}, b ≤ a ⊔ ble_sup_right.trans_lt: ∀ {α : Type ?u.13053} [inst : Preorder α] {a b c : α}, a ≤ b → b < c → a < ctrans_lt hc: a ⊔ b < chc).not_le: ∀ {α : Type ?u.13105} [inst : Preorder α] {a b : α}, a < b → ¬b ≤ anot_le⟩
#align set.unbounded_le_Ioi Set.unbounded_le_Ioi: ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : NoMaxOrder α] (a : α), Unbounded (fun x x_1 => x ≤ x_1) (Ioi a)Set.unbounded_le_Ioi

theorem unbounded_le_Ici: ∀ [inst : SemilatticeSup α] [inst_1 : NoMaxOrder α] (a : α), Unbounded (fun x x_1 => x ≤ x_1) (Ici a)unbounded_le_Ici [SemilatticeSup: Type ?u.13210 → Type ?u.13210SemilatticeSup α: Type ?u.13195α] [NoMaxOrder: (α : Type ?u.13213) → [inst : LT α] → PropNoMaxOrder α: Type ?u.13195α] (a: αa : α: Type ?u.13195α) :
Unbounded: {α : Type ?u.13315} → (α → α → Prop) → Set α → PropUnbounded (· ≤ ·): α → α → Prop(· ≤ ·) (Ici: {α : Type ?u.13372} → [inst : Preorder α] → α → Set αIci a: αa) :=
(unbounded_le_Ioi: ∀ {α : Type ?u.13540} [inst : SemilatticeSup α] [inst_1 : NoMaxOrder α] (a : α),
Unbounded (fun x x_1 => x ≤ x_1) (Ioi a)unbounded_le_Ioi a: αa).mono: ∀ {α : Type ?u.13551} {r : α → α → Prop} {s t : Set α}, s ⊆ t → Unbounded r s → Unbounded r tmono Set.Ioi_subset_Ici_self: ∀ {α : Type ?u.13575} [inst : Preorder α] {a : α}, Ioi a ⊆ Ici aSet.Ioi_subset_Ici_self
#align set.unbounded_le_Ici Set.unbounded_le_Ici: ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : NoMaxOrder α] (a : α), Unbounded (fun x x_1 => x ≤ x_1) (Ici a)Set.unbounded_le_Ici

theorem unbounded_lt_Ioi: ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : NoMaxOrder α] (a : α), Unbounded (fun x x_1 => x < x_1) (Ioi a)unbounded_lt_Ioi [SemilatticeSup: Type ?u.13712 → Type ?u.13712SemilatticeSup α: Type ?u.13697α] [NoMaxOrder: (α : Type ?u.13715) → [inst : LT α] → PropNoMaxOrder α: Type ?u.13697α] (a: αa : α: Type ?u.13697α) :
Unbounded: {α : Type ?u.13817} → (α → α → Prop) → Set α → PropUnbounded (· < ·): α → α → Prop(· < ·) (Ioi: {α : Type ?u.13865} → [inst : Preorder α] → α → Set αIoi a: αa) :=
unbounded_lt_of_unbounded_le: ∀ {α : Type ?u.14031} {s : Set α} [inst : Preorder α],
Unbounded (fun x x_1 => x ≤ x_1) s → Unbounded (fun x x_1 => x < x_1) sunbounded_lt_of_unbounded_le (unbounded_le_Ioi: ∀ {α : Type ?u.14151} [inst : SemilatticeSup α] [inst_1 : NoMaxOrder α] (a : α),
Unbounded (fun x x_1 => x ≤ x_1) (Ioi a)unbounded_le_Ioi a: αa)
#align set.unbounded_lt_Ioi Set.unbounded_lt_Ioi: ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : NoMaxOrder α] (a : α), Unbounded (fun x x_1 => x < x_1) (Ioi a)Set.unbounded_lt_Ioi

theorem unbounded_lt_Ici: ∀ [inst : SemilatticeSup α] (a : α), Unbounded (fun x x_1 => x < x_1) (Ici a)unbounded_lt_Ici [SemilatticeSup: Type ?u.14182 → Type ?u.14182SemilatticeSup α: Type ?u.14167α] (a: αa : α: Type ?u.14167α) : Unbounded: {α : Type ?u.14187} → (α → α → Prop) → Set α → PropUnbounded (· < ·): α → α → Prop(· < ·) (Ici: {α : Type ?u.14235} → [inst : Preorder α] → α → Set αIci a: αa) := fun b: ?m.14427b =>
⟨a: αa ⊔ b: ?m.14427b, le_sup_left: ∀ {α : Type ?u.14473} [inst : SemilatticeSup α] {a b : α}, a ≤ a ⊔ ble_sup_left, le_sup_right: ∀ {α : Type ?u.14498} [inst : SemilatticeSup α] {a b : α}, b ≤ a ⊔ ble_sup_right.not_lt: ∀ {α : Type ?u.14513} [inst : Preorder α] {a b : α}, a ≤ b → ¬b < anot_lt⟩
#align set.unbounded_lt_Ici Set.unbounded_lt_Ici: ∀ {α : Type u_1} [inst : SemilatticeSup α] (a : α), Unbounded (fun x x_1 => x < x_1) (Ici a)Set.unbounded_lt_Ici

/-! ### Bounded initial segments -/

theorem bounded_inter_not: ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α},
(∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m) → ∀ (a : α), Bounded r (s ∩ { b | ¬r b a }) ↔ Bounded r sbounded_inter_not (H: ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c mH : ∀ a: ?m.14689a b: ?m.14692b, ∃ m: ?m.14698m, ∀ c: ?m.14701c, r: α → α → Propr c: ?m.14701c a: ?m.14689a ∨ r: α → α → Propr c: ?m.14701c b: ?m.14692b → r: α → α → Propr c: ?m.14701c m: ?m.14698m) (a: αa : α: Type ?u.14673α) :
Bounded: {α : Type ?u.14716} → (α → α → Prop) → Set α → PropBounded r: α → α → Propr (s: Set αs ∩ { b: ?m.14738b | ¬r: α → α → Propr b: ?m.14738b a: αa }) ↔ Bounded: {α : Type ?u.14750} → (α → α → Prop) → Set α → PropBounded r: α → α → Propr s: Set αs := byGoals accomplished! 🐙
α: Type u_1r: α → α → Props, t: Set αH: ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c ma: αBounded r (s ∩ { b | ¬r b a }) ↔ Bounded r srefine' ⟨_: ?m.14768 → ?m.14769_, Bounded.mono: ∀ {α : Type ?u.14773} {r : α → α → Prop} {s t : Set α}, s ⊆ t → Bounded r t → Bounded r sBounded.mono (Set.inter_subset_left: ∀ {α : Type ?u.14789} (s t : Set α), s ∩ t ⊆ sSet.inter_subset_left s: Set αs _: Set ?m.14790_)⟩α: Type u_1r: α → α → Props, t: Set αH: ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c ma: αBounded r (s ∩ { b | ¬r b a }) → Bounded r s
α: Type u_1r: α → α → Props, t: Set αH: ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c ma: αBounded r (s ∩ { b | ¬r b a }) ↔ Bounded r srintro ⟨b, hb⟩: ?m.14768⟨b: αb⟨b, hb⟩: ?m.14768, hb: ∀ (b_1 : α), b_1 ∈ s ∩ { b | ¬r b a } → r b_1 bhb⟨b, hb⟩: ?m.14768⟩α: Type u_1r: α → α → Props, t: Set αH: ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c ma, b: αhb: ∀ (b_1 : α), b_1 ∈ s ∩ { b | ¬r b a } → r b_1 bintroBounded r s
α: Type u_1r: α → α → Props, t: Set αH: ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c ma: αBounded r (s ∩ { b | ¬r b a }) ↔ Bounded r scases' H: ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c mH a: αa b: αb with m: ?m.14860m hm: ?m.14861 mhmα: Type u_1r: α → α → Props, t: Set αH: ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c ma, b: αhb: ∀ (b_1 : α), b_1 ∈ s ∩ { b | ¬r b a } → r b_1 bm: αhm: ∀ (c : α), r c a ∨ r c b → r c mintro.introBounded r s
α: Type u_1r: α → α → Props, t: Set αH: ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c ma: αBounded r (s ∩ { b | ¬r b a }) ↔ Bounded r sexact ⟨m: ?m.14860m, fun c: ?m.14905c hc: ?m.14908hc => hm: ?m.14861 mhm c: ?m.14905c (or_iff_not_imp_left: ∀ {a b : Prop}, a ∨ b ↔ ¬a → bor_iff_not_imp_left.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 fun hca: ?m.14918hca => hb: ∀ (b_1 : α), b_1 ∈ s ∩ { b | ¬r b a } → r b_1 bhb c: ?m.14905c ⟨hc: ?m.14908hc, hca: ?m.14918hca⟩)⟩Goals accomplished! 🐙
#align set.bounded_inter_not Set.bounded_inter_not: ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α},
(∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m) → ∀ (a : α), Bounded r (s ∩ { b | ¬r b a }) ↔ Bounded r sSet.bounded_inter_not

theorem unbounded_inter_not: ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α},
(∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m) → ∀ (a : α), Unbounded r (s ∩ { b | ¬r b a }) ↔ Unbounded r sunbounded_inter_not (H: ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c mH : ∀ a: ?m.14989a b: ?m.14992b, ∃ m: ?m.14998m, ∀ c: ?m.15001c, r: α → α → Propr c: ?m.15001c a: ?m.14989a ∨ r: α → α → Propr c: ?m.15001c b: ?m.14992b → r: α → α → Propr c: ?m.15001c m: ?m.14998m) (a: αa : α: Type ?u.14973α) :
Unbounded: {α : Type ?u.15016} → (α → α → Prop) → Set α → PropUnbounded r: α → α → Propr (s: Set αs ∩ { b: ?m.15038b | ¬r: α → α → Propr b: ?m.15038b a: αa }) ↔ Unbounded: {α : Type ?u.15050} → (α → α → Prop) → Set α → PropUnbounded r: α → α → Propr s: Set αs := byGoals accomplished! 🐙
α: Type u_1r: α → α → Props, t: Set αH: ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c ma: αUnbounded r (s ∩ { b | ¬r b a }) ↔ Unbounded r ssimp_rw [α: Type u_1r: α → α → Props, t: Set αH: ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c ma: αUnbounded r (s ∩ { b | ¬r b a }) ↔ Unbounded r s← not_bounded_iff: ∀ {α : Type ?u.15136} {r : α → α → Prop} (s : Set α), ¬Bounded r s ↔ Unbounded r snot_bounded_iff,α: Type u_1r: α → α → Props, t: Set αH: ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c ma: α¬Bounded r (s ∩ { b | ¬r b a }) ↔ ¬Bounded r s α: Type u_1r: α → α → Props, t: Set αH: ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c ma: αUnbounded r (s ∩ { b | ¬r b a }) ↔ Unbounded r sbounded_inter_not: ∀ {α : Type ?u.15219} {r : α → α → Prop} {s : Set α},
(∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m) → ∀ (a : α), Bounded r (s ∩ { b | ¬r b a }) ↔ Bounded r sbounded_inter_not H: ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c mHGoals accomplished! 🐙]Goals accomplished! 🐙
#align set.unbounded_inter_not Set.unbounded_inter_not: ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α},
(∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m) → ∀ (a : α), Unbounded r (s ∩ { b | ¬r b a }) ↔ Unbounded r sSet.unbounded_inter_not

/-! #### Less or equal -/

theorem bounded_le_inter_not_le: ∀ {α : Type u_1} {s : Set α} [inst : SemilatticeSup α] (a : α),
Bounded (fun x x_1 => x ≤ x_1) (s ∩ { b | ¬b ≤ a }) ↔ Bounded (fun x x_1 => x ≤ x_1) sbounded_le_inter_not_le [SemilatticeSup: Type ?u.15310 → Type ?u.15310SemilatticeSup α: Type ?u.15295α] (a: αa : α: Type ?u.15295α) :
Bounded: {α : Type ?u.15315} → (α → α → Prop) → Set α → PropBounded (· ≤ ·): α → α → Prop(· ≤ ·) (s: Set αs ∩ { b: ?m.15387b | ¬b: ?m.15387b ≤ a: αa }) ↔ Bounded: {α : Type ?u.15498} → (α → α → Prop) → Set α → PropBounded (· ≤ ·): α → α → Prop(· ≤ ·) s: Set αs :=
bounded_inter_not: ∀ {α : Type ?u.15568} {r : α → α → Prop} {s : Set α},
(∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m) → ∀ (a : α), Bounded r (s ∩ { b | ¬r b a }) ↔ Bounded r sbounded_inter_not (fun x: ?m.15573x y: ?m.15576y => ⟨x: ?m.15573x ⊔ y: ?m.15576y, fun _: ?m.15632_ h: ?m.15635h => h: ?m.15635h.elim: ∀ {a b c : Prop}, a ∨ b → (a → c) → (b → c) → celim le_sup_of_le_left: ∀ {α : Type ?u.15648} [inst : SemilatticeSup α] {a b c : α}, c ≤ a → c ≤ a ⊔ ble_sup_of_le_left le_sup_of_le_right: ∀ {α : Type ?u.16500} [inst : SemilatticeSup α] {a b c : α}, c ≤ b → c ≤ a ⊔ ble_sup_of_le_right⟩) a: αa
#align set.bounded_le_inter_not_le Set.bounded_le_inter_not_le: ∀ {α : Type u_1} {s : Set α} [inst : SemilatticeSup α] (a : α),
Bounded (fun x x_1 => x ≤ x_1) (s ∩ { b | ¬b ≤ a }) ↔ Bounded (fun x x_1 => x ≤ x_1) sSet.bounded_le_inter_not_le

theorem unbounded_le_inter_not_le: ∀ {α : Type u_1} {s : Set α} [inst : SemilatticeSup α] (a : α),
Unbounded (fun x x_1 => x ≤ x_1) (s ∩ { b | ¬b ≤ a }) ↔ Unbounded (fun x x_1 => x ≤ x_1) sunbounded_le_inter_not_le [SemilatticeSup: Type ?u.17514 → Type ?u.17514SemilatticeSup α: Type ?u.17499α] (a: αa : α: Type ?u.17499α) :
Unbounded: {α : Type ?u.17519} → (α → α → Prop) → Set α → PropUnbounded (· ≤ ·): α → α → Prop(· ≤ ·) (s: Set αs ∩ { b: ?m.17591b | ¬b: ?m.17591b ≤ a: αa }) ↔ Unbounded: {α : Type ?u.17702} → (α → α → Prop) → Set α → PropUnbounded (· ≤ ·): α → α → Prop(· ≤ ·) s: Set αs := byGoals accomplished! 🐙
α: Type u_1r: α → α → Props, t: Set αinst✝: SemilatticeSup αa: αUnbounded (fun x x_1 => x ≤ x_1) (s ∩ { b | ¬b ≤ a }) ↔ Unbounded (fun x x_1 => x ≤ x_1) srw [α: Type u_1r: α → α → Props, t: Set αinst✝: SemilatticeSup αa: αUnbounded (fun x x_1 => x ≤ x_1) (s ∩ { b | ¬b ≤ a }) ↔ Unbounded (fun x x_1 => x ≤ x_1) s← not_bounded_iff: ∀ {α : Type ?u.17774} {r : α → α → Prop} (s : Set α), ¬Bounded r s ↔ Unbounded r snot_bounded_iff,α: Type u_1r: α → α → Props, t: Set αinst✝: SemilatticeSup αa: α¬Bounded (fun x x_1 => x ≤ x_1) (s ∩ { b | ¬b ≤ a }) ↔ Unbounded (fun x x_1 => x ≤ x_1) s α: Type u_1r: α → α → Props, t: Set αinst✝: SemilatticeSup αa: αUnbounded (fun x x_1 => x ≤ x_1) (s ∩ { b | ¬b ≤ a }) ↔ Unbounded (fun x x_1 => x ≤ x_1) s← not_bounded_iff: ∀ {α : Type ?u.17801} {r : α → α → Prop} (s : Set α), ¬Bounded r s ↔ Unbounded r snot_bounded_iff,α: Type u_1r: α → α → Props, t: Set αinst✝: SemilatticeSup αa: α¬Bounded (fun x x_1 => x ≤ x_1) (s ∩ { b | ¬b ≤ a }) ↔ ¬Bounded (fun x x_1 => x ≤ x_1) s α: Type u_1r: α → α → Props, t: Set αinst✝: SemilatticeSup αa: αUnbounded (fun x x_1 => x ≤ x_1) (s ∩ { b | ¬b ≤ a }) ↔ Unbounded (fun x x_1 => x ≤ x_1) snot_iff_not: ∀ {a b : Prop}, (¬a ↔ ¬b) ↔ (a ↔ b)not_iff_notα: Type u_1r: α → α → Props, t: Set αinst✝: SemilatticeSup αa: αBounded (fun x x_1 => x ≤ x_1) (s ∩ { b | ¬b ≤ a }) ↔ Bounded (fun x x_1 => x ≤ x_1) s]α: Type u_1r: α → α → Props, t: Set αinst✝: SemilatticeSup αa: αBounded (fun x x_1 => x ≤ x_1) (s ∩ { b | ¬b ≤ a }) ↔ Bounded (fun x x_1 => x ≤ x_1) s
α: Type u_1r: α → α → Props, t: Set αinst✝: SemilatticeSup αa: αUnbounded (fun x x_1 => x ≤ x_1) (s ∩ { b | ¬b ≤ a }) ↔ Unbounded (fun x x_1 => x ≤ x_1) sexact bounded_le_inter_not_le: ∀ {α : Type ?u.17844} {s : Set α} [inst : SemilatticeSup α] (a : α),
Bounded (fun x x_1 => x ≤ x_1) (s ∩ { b | ¬b ≤ a }) ↔ Bounded (fun x x_1 => x ≤ x_1) sbounded_le_inter_not_le a: αaGoals accomplished! 🐙
#align set.unbounded_le_inter_not_le Set.unbounded_le_inter_not_le: ∀ {α : Type u_1} {s : Set α} [inst : SemilatticeSup α] (a : α),
Unbounded (fun x x_1 => x ≤ x_1) (s ∩ { b | ¬b ≤ a }) ↔ Unbounded (fun x x_1 => x ≤ x_1) sSet.unbounded_le_inter_not_le

theorem bounded_le_inter_lt: ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α] (a : α),
Bounded (fun x x_1 => x ≤ x_1) (s ∩ { b | a < b }) ↔ Bounded (fun x x_1 => x ≤ x_1) sbounded_le_inter_lt [LinearOrder: Type ?u.17891 → Type ?u.17891LinearOrder α: Type ?u.17876α] (a: αa : α: Type ?u.17876α) :
Bounded: {α : Type ?u.17896} → (α → α → Prop) → Set α → PropBounded (· ≤ ·): α → α → Prop(· ≤ ·) (s: Set αs ∩ { b: ?m.17968b | a: αa < b: ?m.17968b }) ↔ Bounded: {α : Type ?u.18074} → (α → α → Prop) → Set α → PropBounded (· ≤ ·): α → α → Prop(· ≤ ·) s: Set αs := byGoals accomplished! 🐙
α: Type u_1r: α → α → Props, t: Set αinst✝: LinearOrder αa: αBounded (fun x x_1 => x ≤ x_1) (s ∩ { b | a < b }) ↔ Bounded (fun x x_1 => x ≤ x_1) ssimp_rw [α: Type u_1r: α → α → Props, t: Set αinst✝: LinearOrder αa: αBounded (fun x x_1 => x ≤ x_1) (s ∩ { b | a < b }) ↔ Bounded (fun x x_1 => x ≤ x_1) s← not_le: ∀ {α : Type ?u.18345} [inst : LinearOrder α] {a b : α}, ¬a ≤ b ↔ b < anot_le,α: Type u_1r: α → α → Props, t: Set αinst✝: LinearOrder αa: αBounded (fun x x_1 => x ≤ x_1) (s ∩ { b | ¬b ≤ a }) ↔ Bounded (fun x x_1 => x ≤ x_1) s α: Type u_1r: α → α → Props, t: Set αinst✝: LinearOrder αa: αBounded (fun x x_1 => x ≤ x_1) (s ∩ { b | a < b }) ↔ Bounded (fun x x_1 => x ≤ x_1) sbounded_le_inter_not_leGoals accomplished! 🐙]Goals accomplished! 🐙
#align set.bounded_le_inter_lt Set.bounded_le_inter_lt: ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α] (a : α),
Bounded (fun x x_1 => x ≤ x_1) (s ∩ { b | a < b }) ↔ Bounded (fun x x_1 => x ≤ x_1) sSet.bounded_le_inter_lt

theorem unbounded_le_inter_lt: ∀ [inst : LinearOrder α] (a : α),
Unbounded (fun x x_1 => x ≤ x_1) (s ∩ { b | a < b }) ↔ Unbounded (fun x x_1 => x ≤ x_1) sunbounded_le_inter_lt [LinearOrder: Type ?u.18812 → Type ?u.18812LinearOrder α: Type ?u.18797α] (a: αa : α: Type ?u.18797α) :
Unbounded: {α : Type ?u.18817} → (α → α → Prop) → Set α → PropUnbounded (· ≤ ·): α → α → Prop(· ≤ ·) (s: Set αs ∩ { b: ?m.18889b | a: αa < b: ?m.18889b }) ↔ Unbounded: {α : Type ?u.18995} → (α → α → Prop) → Set α → PropUnbounded (· ≤ ·): α → α → Prop(· ≤ ·) s: Set αs := byGoals accomplished! 🐙
α: Type u_1r: α → α → Props, t: Set αinst✝: LinearOrder αa: αUnbounded (fun x x_1 => x ≤ x_1) (s ∩ { b | a < b }) ↔ Unbounded (fun x x_1 => x ≤ x_1) sconvert @unbounded_le_inter_not_le: ∀ {α : Type ?u.19134} {s : Set α} [inst : SemilatticeSup α] (a : α),
Unbounded (fun x x_1 => x ≤ x_1) (s ∩ { b | ¬b ≤ a }) ↔ Unbounded (fun x x_1 => x ≤ x_1) sunbounded_le_inter_not_le _: Type ?u.19134_ s: Set αs _ a: αaα: Type u_1r: α → α → Props, t: Set αinst✝: LinearOrder αa, x✝: αh.e'_1.h.e'_3.h.e'_4.h.e'_2.h.aa < x✝ ↔ ¬x✝ ≤ a
α: Type u_1r: α → α → Props, t: Set αinst✝: LinearOrder αa: αUnbounded (fun x x_1 => x ≤ x_1) (s ∩ { b | a < b }) ↔ Unbounded (fun x x_1 => x ≤ x_1) sexact lt_iff_not_le: ∀ {α : Type ?u.21930} [inst : LinearOrder α] {x y : α}, x < y ↔ ¬y ≤ xlt_iff_not_leGoals accomplished! 🐙
#align set.unbounded_le_inter_lt Set.unbounded_le_inter_lt: ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α] (a : α),
Unbounded (fun x x_1 => x ≤ x_1) (s ∩ { b | a < b }) ↔ Unbounded (fun x x_1 => x ≤ x_1) sSet.unbounded_le_inter_lt

theorem bounded_le_inter_le: ∀ [inst : LinearOrder α] (a : α), Bounded (fun x x_1 => x ≤ x_1) (s ∩ { b | a ≤ b }) ↔ Bounded (fun x x_1 => x ≤ x_1) sbounded_le_inter_le [LinearOrder: Type ?u.22048 → Type ?u.22048LinearOrder α: Type ?u.22033α] (a: αa : α: Type ?u.22033α) :
Bounded: {α : Type ?u.22053} → (α → α → Prop) → Set α → PropBounded (· ≤ ·): α → α → Prop(· ≤ ·) (s: Set αs ∩ { b: ?m.22125b | a: αa ≤ b: ?m.22125b }) ↔ Bounded: {α : Type ?u.22231} → (α → α → Prop) → Set α → PropBounded (· ≤ ·): α → α → Prop(· ≤ ·) s: Set αs := byGoals accomplished! 🐙
α: Type u_1r: α → α → Props, t: Set αinst✝: LinearOrder αa: αBounded (fun x x_1 => x ≤ x_1) (s ∩ { b | a ≤ b }) ↔ Bounded (fun x x_1 => x ≤ x_1) srefine' ⟨_: ?m.22307 → ?m.22308_, Bounded.mono: ∀ {α : Type ?u.22312} {r : α → α → Prop} {s t : Set α}, s ⊆ t → Bounded r t → Bounded r sBounded.mono (Set.inter_subset_left: ∀ {α : Type ?u.22330} (s t : Set α), s ∩ t ⊆ sSet.inter_subset_left s: Set αs _: Set ?m.22331_)⟩α: Type u_1r: α → α → Props, t: Set αinst✝: LinearOrder αa: αBounded (fun x x_1 => x ≤ x_1) (s ∩ { b | a ≤ b }) → Bounded (fun x x_1 => x ≤ x_1) s
α: Type u_1r: α → α → Props, t: Set αinst✝: LinearOrder αa: αBounded (fun x x_1 => x ≤ x_1) (s ∩ { b | a ≤ b }) ↔ Bounded (fun x x_1 => x ≤ x_1) srw [α: Type u_1r: α → α → Props, t: Set αinst✝: LinearOrder αa: αBounded (fun x x_1 => x ≤ x_1) (s ∩ { b | a ≤ b }) → Bounded (fun x x_1 => x ≤ x_1) s← @bounded_le_inter_lt: ∀ {α : Type ?u.22346} {s : Set α} [inst : LinearOrder α] (a : α),
Bounded (fun x x_1 => x ≤ x_1) (s ∩ { b | a < b }) ↔ Bounded (fun x x_1 => x ≤ x_1) sbounded_le_inter_lt _: Type ?u.22346_ s: Set αs _ a: αaα: Type u_1r: α → α → Props, t: Set αinst✝: LinearOrder αa: αBounded (fun x x_1 => x ≤ x_1) (s ∩ { b | a ≤ b }) → Bounded (fun x x_1 => x ≤ x_1) (s ∩ { b | a < b })]α: Type u_1r: α → α → Props, t: Set αinst✝: LinearOrder αa: αBounded (fun x x_1 => x ≤ x_1) (s ∩ { b | a ≤ b }) → Bounded (fun x x_1 => x ≤ x_1) (s ∩ { b | a < b })
α: Type u_1r: α → α → Props, t: Set αinst✝: LinearOrder αa: αBounded (fun x x_1 => x ≤ x_1) (s ∩ { b | a ≤ b }) ↔ Bounded (fun x x_1 => x ≤ x_1) sexact Bounded.mono: ∀ {α : Type ?u.22381} {r : α → α → Prop} {s t : Set α}, s ⊆ t → Bounded r t → Bounded r sBounded.mono fun x: ?m.22391x ⟨hx: x ∈ shx, hx': x ∈ { b | a < b }hx'⟩ => ⟨hx: x ∈ shx, le_of_lt: ∀ {α : Type ?u.22430} [inst : Preorder α] {a b : α}, a < b → a ≤ ble_of_lt hx': x ∈ { b | a < b }hx'⟩Goals accomplished! 🐙
#align set.bounded_le_inter_le Set.bounded_le_inter_le: ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α] (a : α),
Bounded (fun x x_1 => x ≤ x_1) (s ∩ { b | a ≤ b }) ↔ Bounded (fun x x_1 => x ≤ x_1) sSet.bounded_le_inter_le

theorem unbounded_le_inter_le: ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α] (a : α),
Unbounded (fun x x_1 => x ≤ x_1) (s ∩ { b | a ≤ b }) ↔ Unbounded (fun x x_1 => x ≤ x_1) sunbounded_le_inter_le [LinearOrder: Type ?u.22651 → Type ?u.22651LinearOrder α: Type ?u.22636α] (a: αa : α: Type ?u.22636α) :
Unbounded: {α : Type ?u.22656} → (α → α → Prop) → Set α → PropUnbounded (· ≤ ·): α → α → Prop(· ≤ ·) (s: Set αs ∩ { b: ?m.22728b | a: αa ≤ b: ?m.22728b }) ↔ Unbounded: {α : Type ?u.22834} → (α → α → Prop) → Set α → PropUnbounded (· ≤ ·): α → α → Prop(· ≤ ·) s: Set αs := byGoals accomplished! 🐙
α: Type u_1r: α → α → Props, t: Set αinst✝: LinearOrder αa: αUnbounded (fun x x_1 => x ≤ x_1) (s ∩ { b | a ≤ b }) ↔ Unbounded (fun x x_1 => x ≤ x_1) srw [α: Type u_1r: α → α → Props, t: Set αinst✝: LinearOrder αa: αUnbounded (fun x x_1 => x ≤ x_1) (s ∩ { b | a ≤ b }) ↔ Unbounded (fun x x_1 => x ≤ x_1) s← not_bounded_iff: ∀ {α : Type ?u.22906} {r : α → α → Prop} (s : Set α), ¬Bounded r s ↔ Unbounded r snot_bounded_iff,α: Type u_1r: α → α → Props, t: Set αinst✝: LinearOrder αa: α¬Bounded (fun x x_1 => x ≤ x_1) (s ∩ { b | a ≤ b }) ↔ Unbounded (fun x x_1 => x ≤ x_1) s α: Type u_1r: α → α → Props, t: Set αinst✝: LinearOrder αa: αUnbounded (fun x x_1 => x ≤ x_1) (s ∩ { b | a ≤ b }) ↔ Unbounded (fun x x_1 => x ≤ x_1) s← not_bounded_iff: ∀ {α : Type ?u.22933} {r : α → α → Prop} (s : Set α), ¬Bounded r s ↔ Unbounded r snot_bounded_iff,α: Type u_1r: α → α → Props, t: Set αinst✝: LinearOrder αa: α¬Bounded (fun x x_1 => x ≤ x_1) (s ∩ { b | a ≤ b }) ↔ ¬Bounded (fun x x_1 => x ≤ x_1) s α: Type u_1r: α → α → Props, t: Set αinst✝: LinearOrder αa: αUnbounded (fun x x_1 => x ≤ x_1) (s ∩ { b | a ≤ b }) ↔ Unbounded (fun x x_1 => x ≤ x_1) snot_iff_not: ∀ {a b : Prop}, (¬a ↔ ¬b) ↔ (a ↔ b)not_iff_notα: Type u_1r: α → α → Props, t: Set αinst✝: LinearOrder αa: αBounded (fun x x_1 => x ≤ x_1) (s ∩ { b | a ≤ b }) ↔ Bounded (fun x x_1 => x ≤ x_1) s]α: Type u_1r: α → α → Props, t: Set αinst✝: LinearOrder αa: αBounded (fun x x_1 => x ≤ x_1) (s ∩ { b | a ≤ b }) ↔ Bounded (fun x x_1 => x ≤ x_1) s
α: Type u_1r: α → α → Props, t: Set αinst✝: LinearOrder αa: αUnbounded (fun x x_1 => x ≤ x_1) (s ∩ { b | a ≤ b }) ↔ Unbounded (fun x x_1 => x ≤ x_1) sexact bounded_le_inter_le: ∀ {α : Type ?u.22976} {s : Set α} [inst : LinearOrder α] (a : α),
Bounded (fun x x_1 => x ≤ x_1) (s ∩ { b | a ≤ b }) ↔ Bounded (fun x x_1 => x ≤ x_1) sbounded_le_inter_le a: αaGoals accomplished! 🐙
#align set.unbounded_le_inter_le Set.unbounded_le_inter_le: ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α] (a : α),
Unbounded (fun x x_1 => x ≤ x_1) (s ∩ { b | a ≤ b }) ↔ Unbounded (fun x x_1 => x ≤ x_1) sSet.unbounded_le_inter_le

/-! #### Less than -/

theorem bounded_lt_inter_not_lt: ∀ {α : Type u_1} {s : Set α} [inst : SemilatticeSup α] (a : α),
Bounded (fun x x_1 => x < x_1) (s ∩ { b | ¬b < a }) ↔ Bounded (fun x x_1 => x < x_1) sbounded_lt_inter_not_lt [SemilatticeSup: Type ?u.23022 → Type ?u.23022SemilatticeSup α: Type ?u.23007α] (a: αa : α: Type ?u.23007α) :
Bounded: {α : Type ?u.23027} → (α → α → Prop) → Set α → PropBounded (· < ·): α → α → Prop(· < ·) (s: Set αs ∩ { b: ?m.23090b | ¬b: ?m.23090b < a: αa }) ↔ Bounded: {α : Type ?u.23201} → (α → α → Prop) → Set α → PropBounded (· < ·): α → α → Prop(· < ·) s: Set αs :=
bounded_inter_not: ∀ {α : Type ?u.23262} {r : α → α → Prop} {s : Set α},
(∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m) → ∀ (a : α), Bounded r (s ∩ { b | ¬r b a }) ↔ Bounded r sbounded_inter_not (fun x: ?m.23267x y: ?m.23270y => ⟨x: ?m.23267x ⊔ y: ?m.23270y, fun _: ?m.23326_ h: ?m.23329h => h: ?m.23329h.elim: ∀ {a b c : Prop}, a ∨ b → (a → c) → (b → c) → celim lt_sup_of_lt_left: ∀ {α : Type ?u.23342} [inst : SemilatticeSup α] {a b c : α}, c < a → c < a ⊔ blt_sup_of_lt_left lt_sup_of_lt_right: ∀ {α : Type ?u.24194} [inst : SemilatticeSup α] {a b c : α}, c < b → c < a ⊔ blt_sup_of_lt_right⟩) a: αa
#align set.bounded_lt_inter_not_lt Set.bounded_lt_inter_not_lt: ∀ {α : Type u_1} {s : Set α} [inst : SemilatticeSup α] (a : α),
Bounded (fun x x_1 => x < x_1) (s ∩ { b | ¬b < a }) ↔ Bounded (fun x x_1 => x < x_1) sSet.bounded_lt_inter_not_lt

theorem unbounded_lt_inter_not_lt: ∀ {α : Type u_1} {s : Set α} [inst : SemilatticeSup α] (a : α),
Unbounded (fun x x_1 => x < x_1) (s ∩ { b | ¬b < a }) ↔ Unbounded (fun x x_1 => x < x_1) sunbounded_lt_inter_not_lt [SemilatticeSup: Type ?u.25208 → Type ?u.25208SemilatticeSup α: Type ?u.25193α] (a: αa : α: Type ?u.25193α) :
Unbounded: {α : Type ?u.25213} → (α → α → Prop) → Set α → PropUnbounded (· < ·): α → α → Prop(· < ·) (s: Set αs ∩ { b: ?m.25276b | ¬b: ?m.25276b < a: αa }) ↔ Unbounded: {α : Type ?u.25387} → (α → α → Prop) → Set α → PropUnbounded (· < ·): α → α → Prop(· < ·) s: Set αs := byGoals accomplished! 🐙
α: Type u_1r: α → α → Props, t: Set αinst✝: SemilatticeSup αa: αUnbounded (fun x x_1 => x < x_1) (s ∩ { b | ¬b < a }) ↔ Unbounded (fun x x_1 => x < x_1) srw [α: Type u_1r: α → α → Props, t: Set αinst✝: SemilatticeSup αa: αUnbounded (fun x x_1 => x < x_1) (s ∩ { b | ¬b < a }) ↔ Unbounded (fun x x_1 => x < x_1) s← not_bounded_iff: ∀ {α : Type ?u.25450} {r : α → α → Prop} (s : Set α), ¬Bounded r s ↔ Unbounded r snot_bounded_iff,α: Type u_1r: α → α → Props, t: Set αinst✝: SemilatticeSup αa: α¬Bounded (fun x x_1 => x < x_1) (s ∩ { b | ¬b < a }) ↔ Unbounded (fun x x_1 => x < x_1) s α: Type u_1r: α → α → Props, t: Set αinst✝: SemilatticeSup αa: αUnbounded (fun x x_1 => x < x_1) (s ∩ { b | ¬b < a }) ↔ Unbounded (fun x x_1 => x < x_1) s← not_bounded_iff: ∀ {α : Type ?u.25477} {r : α → α → Prop} (s : Set α), ¬Bounded r s ↔ Unbounded r snot_bounded_iff,α: Type u_1r: α → α → Props, t: Set αinst✝: SemilatticeSup αa: α¬Bounded (fun x x_1 => x < x_1) (s ∩ { b | ¬b < a }) ↔ ¬Bounded (fun x x_1 => x < x_1) s α: Type u_1r: α → α → Props, t: Set αinst✝: SemilatticeSup αa: αUnbounded (fun x x_1 => x < x_1) (s ∩ { b | ¬b < a }) ↔ Unbounded (fun x x_1 => x < x_1) snot_iff_not: ∀ {a b : Prop}, (¬a ↔ ¬b) ↔ (a ↔ b)not_iff_notα: Type u_1r: α → α → Props, t: Set αinst✝: SemilatticeSup αa: αBounded (fun x x_1 => x < x_1) (s ∩ { b | ¬b < a }) ↔ Bounded (fun x x_1 => x < x_1) s]α: Type u_1r: α → α → Props, t: Set αinst✝: SemilatticeSup αa: αBounded (fun x x_1 => x < x_1) (s ∩ { b | ¬b < a }) ↔ Bounded (fun x x_1 => x < x_1) s
α: Type u_1r: α → α → Props, t: Set αinst✝: SemilatticeSup αa: αUnbounded (fun x x_1 => x < x_1) (s ∩ { b | ¬b < a }) ↔ Unbounded (fun x x_1 => x < x_1) sexact bounded_lt_inter_not_lt: ∀ {α : Type ?u.25520} {s : Set α} [inst : SemilatticeSup α] (a : α),
Bounded (fun x x_1 => x < x_1) (s ∩ { b | ¬b < a }) ↔ Bounded (fun x x_1 => x < x_1) sbounded_lt_inter_not_lt a: αaGoals accomplished! 🐙
#align set.unbounded_lt_inter_not_lt Set.unbounded_lt_inter_not_lt: ∀ {α : Type u_1} {s : Set α} [inst : SemilatticeSup α] (a : α),
Unbounded (fun x x_1 => x < x_1) (s ∩ { b | ¬b < a }) ↔ Unbounded (fun x x_1 => x < x_1) sSet.unbounded_lt_inter_not_lt

theorem bounded_lt_inter_le: ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α] (a : α),
Bounded (fun x x_1 => x < x_1) (s ∩ { b | a ≤ b }) ↔ Bounded (fun x x_1 => x < x_1) sbounded_lt_inter_le [LinearOrder: Type ?u.25567 → Type ?u.25567LinearOrder α: Type ?u.25552α] (a: αa : α: Type ?u.25552α) :
Bounded: {α : Type ?u.25572} → (α → α → Prop) → Set α → PropBounded (· < ·): α → α → Prop(· < ·) (s: ```