/-
Copyright (c) 2022 Violeta Hernández Palacios. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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: α → α → Prop
r : 
α: Type ?u.2
α → 
α: Type ?u.10568
α → 
Prop: Type
Prop} {
s: Set α
s 
t: Set α
t : 
Set: Type ?u.14 → Type ?u.14
Set 
α: 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 s
Bounded.mono (
hst: s ⊆ t
hst : 
s: Set α
s ⊆ 
t: Set α
t) (
hs: Bounded r t
hs : 
Bounded: {α : Type ?u.51} → (α → α → Prop) → Set α → Prop
Bounded 
r: α → α → Prop
r 
t: Set α
t) : 
Bounded: {α : Type ?u.62} → (α → α → Prop) → Set α → Prop
Bounded 
r: α → α → Prop
r 
s: Set α
s :=
  
hs: Bounded r t
hs.
imp: ∀ {α : Sort ?u.76} {p q : α → Prop}, (∀ (a : α), p a → q a) → (∃ a, p a) → ∃ a, q a
imp fun 
_: ?m.94
_ 
ha: ?m.97
ha 
b: ?m.100
b 
hb: ?m.103
hb => 
ha: ?m.97
ha 
b: ?m.100
b (
hst: s ⊆ t
hst 
hb: ?m.103
hb)
#align set.bounded.mono 
Set.Bounded.mono: ∀ {α : Type u_1} {r : α → α → Prop} {s t : Set α}, s ⊆ t → Bounded r t → Bounded r s
Set.Bounded.mono

theorem 
Unbounded.mono: ∀ {α : Type u_1} {r : α → α → Prop} {s t : Set α}, s ⊆ t → Unbounded r s → Unbounded r t
Unbounded.mono (
hst: s ⊆ t
hst : 
s: Set α
s ⊆ 
t: Set α
t) (
hs: Unbounded r s
hs : 
Unbounded: {α : Type ?u.180} → (α → α → Prop) → Set α → Prop
Unbounded 
r: α → α → Prop
r 
s: Set α
s) : 
Unbounded: {α : Type ?u.191} → (α → α → Prop) → Set α → Prop
Unbounded 
r: α → α → Prop
r 
t: Set α
t := fun 
a: ?m.206
a =>
  let ⟨
b: α
b, 
hb: b ∈ s
hb, 
hb': ¬r b a
hb'⟩ := 
hs: Unbounded r s
hs 
a: ?m.206
a
  ⟨
b: α
b, 
hst: s ⊆ t
hst 
hb: b ∈ s
hb, 
hb': ¬r b a
hb'⟩
#align set.unbounded.mono 
Set.Unbounded.mono: ∀ {α : Type u_1} {r : α → α → Prop} {s t : Set α}, s ⊆ t → Unbounded r s → Unbounded r t
Set.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) s
unbounded_le_of_forall_exists_lt [
Preorder: Type ?u.404 → Type ?u.404
Preorder 
α: Type ?u.389
α] (
h: ∀ (a : α), ∃ b, b ∈ s ∧ a < b
h : ∀ 
a: ?m.408
a, ∃ 
b: ?m.414
b ∈ 
s: Set α
s, 
a: ?m.408
a < 
b: ?m.414
b) :
    
Unbounded: {α : Type ?u.451} → (α → α → Prop) → Set α → Prop
Unbounded 
(· ≤ ·): α → α → Prop
(· ≤ ·) 
s: Set α
s := fun 
a: ?m.527
a =>
  let ⟨
b: α
b, 
hb: b ∈ s
hb, 
hb': a < b
hb'⟩ := 
h: ∀ (a : α), ∃ b, b ∈ s ∧ a < b
h 
a: ?m.527
a
  ⟨
b: α
b, 
hb: b ∈ s
hb, fun 
hba: ?m.595
hba => 
hba: ?m.595
hba.
not_lt: ∀ {α : Type ?u.597} [inst : Preorder α] {a b : α}, a ≤ b → ¬b < a
not_lt 
hb': a < b
hb'⟩
#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) s
Set.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 < b
unbounded_le_iff [
LinearOrder: Type ?u.741 → Type ?u.741
LinearOrder 
α: Type ?u.726
α] : 
Unbounded: {α : Type ?u.744} → (α → α → Prop) → Set α → Prop
Unbounded 
(· ≤ ·): α → α → Prop
(· ≤ ·) 
s: Set α
s ↔ ∀ 
a: ?m.805
a, ∃ 
b: ?m.811
b ∈ 
s: Set α
s, 
a: ?m.805
a < 
b: ?m.811
b := by
Goals accomplished! 🐙
  
α: Type u_1

r: α → α → Prop

s, 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 α → Prop
Unbounded, 
not_le: ∀ {α : Type ?u.1014} [inst : LinearOrder α] {a b : α}, ¬a ≤ b ↔ b < a
not_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 < b
Set.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) s
unbounded_lt_of_forall_exists_le [
Preorder: Type ?u.1309 → Type ?u.1309
Preorder 
α: Type ?u.1294
α] (
h: ∀ (a : α), ∃ b, b ∈ s ∧ a ≤ b
h : ∀ 
a: ?m.1313
a, ∃ 
b: ?m.1319
b ∈ 
s: Set α
s, 
a: ?m.1313
a ≤ 
b: ?m.1319
b) :
    
Unbounded: {α : Type ?u.1356} → (α → α → Prop) → Set α → Prop
Unbounded 
(· < ·): α → α → Prop
(· < ·) 
s: Set α
s := fun 
a: ?m.1423
a =>
  let ⟨
b: α
b, 
hb: b ∈ s
hb, 
hb': a ≤ b
hb'⟩ := 
h: ∀ (a : α), ∃ b, b ∈ s ∧ a ≤ b
h 
a: ?m.1423
a
  ⟨
b: α
b, 
hb: b ∈ s
hb, fun 
hba: ?m.1491
hba => 
hba: ?m.1491
hba.
not_le: ∀ {α : Type ?u.1493} [inst : Preorder α] {a b : α}, a < b → ¬b ≤ a
not_le 
hb': a ≤ b
hb'⟩
#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) s
Set.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 ≤ b
unbounded_lt_iff [
LinearOrder: Type ?u.1637 → Type ?u.1637
LinearOrder 
α: Type ?u.1622
α] : 
Unbounded: {α : Type ?u.1640} → (α → α → Prop) → Set α → Prop
Unbounded 
(· < ·): α → α → Prop
(· < ·) 
s: Set α
s ↔ ∀ 
a: ?m.1692
a, ∃ 
b: ?m.1698
b ∈ 
s: Set α
s, 
a: ?m.1692
a ≤ 
b: ?m.1698
b := by
Goals accomplished! 🐙
  
α: Type u_1

r: α → α → Prop

s, 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 α → Prop
Unbounded, 
not_lt: ∀ {α : Type ?u.1901} [inst : LinearOrder α] {a b : α}, ¬a < b ↔ b ≤ a
not_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 ≤ b
Set.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) s
unbounded_ge_of_forall_exists_gt [
Preorder: Type ?u.2196 → Type ?u.2196
Preorder 
α: Type ?u.2181
α] (
h: ∀ (a : α), ∃ b, b ∈ s ∧ b < a
h : ∀ 
a: ?m.2200
a, ∃ 
b: ?m.2206
b ∈ 
s: Set α
s, 
b: ?m.2206
b < 
a: ?m.2200
a) :
    
Unbounded: {α : Type ?u.2243} → (α → α → Prop) → Set α → Prop
Unbounded 
(· ≥ ·): α → α → 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) s
unbounded_le_of_forall_exists_lt 
α: Type ?u.2181
αᵒᵈ 
_: Set αᵒᵈ
_ _ 
h: ∀ (a : α), ∃ b, b ∈ s ∧ b < a
h
#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) s
Set.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 < a
unbounded_ge_iff [
LinearOrder: Type ?u.2381 → Type ?u.2381
LinearOrder 
α: Type ?u.2366
α] : 
Unbounded: {α : Type ?u.2384} → (α → α → Prop) → Set α → Prop
Unbounded 
(· ≥ ·): α → α → Prop
(· ≥ ·) 
s: Set α
s ↔ ∀ 
a: ?m.2445
a, ∃ 
b: ?m.2451
b ∈ 
s: Set α
s, 
b: ?m.2451
b < 
a: ?m.2445
a :=
  ⟨fun 
h: ?m.2649
h 
a: ?m.2652
a =>
    let ⟨
b: α
b, 
hb: b ∈ s
hb, 
hba: ¬(fun x x_1 => x ≥ x_1) b a
hba⟩ := 
h: ?m.2649
h 
a: ?m.2652
a
    ⟨
b: α
b, 
hb: b ∈ s
hb, 
lt_of_not_ge: ∀ {α : Type ?u.2727} [inst : LinearOrder α] {a b : α}, ¬a ≥ b → a < b
lt_of_not_ge 
hba: ¬(fun x x_1 => x ≥ x_1) b a
hba⟩,
    
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) s
unbounded_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 < a
Set.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) s
unbounded_gt_of_forall_exists_ge [
Preorder: Type ?u.3016 → Type ?u.3016
Preorder 
α: Type ?u.3001
α] (
h: ∀ (a : α), ∃ b, b ∈ s ∧ b ≤ a
h : ∀ 
a: ?m.3020
a, ∃ 
b: ?m.3026
b ∈ 
s: Set α
s, 
b: ?m.3026
b ≤ 
a: ?m.3020
a) :
    
Unbounded: {α : Type ?u.3063} → (α → α → Prop) → Set α → Prop
Unbounded 
(· > ·): α → α → Prop
(· > ·) 
s: Set α
s := fun 
a: ?m.3130
a =>
  let ⟨
b: α
b, 
hb: b ∈ s
hb, 
hb': b ≤ a
hb'⟩ := 
h: ∀ (a : α), ∃ b, b ∈ s ∧ b ≤ a
h 
a: ?m.3130
a
  ⟨
b: α
b, 
hb: b ∈ s
hb, fun 
hba: ?m.3198
hba => 
not_le_of_gt: ∀ {α : Type ?u.3200} [inst : Preorder α] {a b : α}, a > b → ¬a ≤ b
not_le_of_gt 
hba: ?m.3198
hba 
hb': b ≤ a
hb'⟩
#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) s
Set.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 ≤ a
unbounded_gt_iff [
LinearOrder: Type ?u.3342 → Type ?u.3342
LinearOrder 
α: Type ?u.3327
α] : 
Unbounded: {α : Type ?u.3345} → (α → α → Prop) → Set α → Prop
Unbounded 
(· > ·): α → α → Prop
(· > ·) 
s: Set α
s ↔ ∀ 
a: ?m.3397
a, ∃ 
b: ?m.3403
b ∈ 
s: Set α
s, 
b: ?m.3403
b ≤ 
a: ?m.3397
a :=
  ⟨fun 
h: ?m.3601
h 
a: ?m.3604
a =>
    let ⟨
b: α
b, 
hb: b ∈ s
hb, 
hba: ¬(fun x x_1 => x > x_1) b a
hba⟩ := 
h: ?m.3601
h 
a: ?m.3604
a
    ⟨
b: α
b, 
hb: b ∈ s
hb, 
le_of_not_gt: ∀ {α : Type ?u.3679} [inst : LinearOrder α] {a b : α}, ¬a > b → a ≤ b
le_of_not_gt 
hba: ¬(fun x x_1 => x > x_1) b a
hba⟩,
    
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) s
unbounded_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 ≤ a
Set.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' s
Bounded.rel_mono {
r': α → α → Prop
r' : 
α: Type ?u.3953
α → 
α: Type ?u.3953
α → 
Prop: Type
Prop} (
h: Bounded r s
h : 
Bounded: {α : Type ?u.3974} → (α → α → Prop) → Set α → Prop
Bounded 
r: α → α → Prop
r 
s: Set α
s) (
hrr': r ≤ r'
hrr' : 
r: α → α → Prop
r ≤ 
r': α → α → Prop
r') : 
Bounded: {α : Type ?u.4049} → (α → α → Prop) → Set α → Prop
Bounded 
r': α → α → Prop
r' 
s: Set α
s :=
  let ⟨
a: α
a, 
ha: ∀ (b : α), b ∈ s → r b a
ha⟩ := 
h: Bounded r s
h
  ⟨
a: α
a, fun 
b: ?m.4121
b 
hb: ?m.4124
hb => 
hrr': r ≤ r'
hrr' 
b: ?m.4121
b 
a: α
a (
ha: ∀ (b : α), b ∈ s → r b a
ha 
b: ?m.4121
b 
hb: ?m.4124
hb)⟩
#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' s
Set.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) s
bounded_le_of_bounded_lt [
Preorder: Type ?u.4257 → Type ?u.4257
Preorder 
α: Type ?u.4242
α] (
h: Bounded (fun x x_1 => x < x_1) s
h : 
Bounded: {α : Type ?u.4260} → (α → α → Prop) → Set α → Prop
Bounded 
(· < ·): α → α → Prop
(· < ·) 
s: Set α
s) : 
Bounded: {α : Type ?u.4313} → (α → α → Prop) → Set α → Prop
Bounded 
(· ≤ ·): α → α → Prop
(· ≤ ·) 
s: Set α
s :=
  
h: Bounded (fun x x_1 => x < x_1) s
h.
rel_mono: ∀ {α : Type ?u.4402} {r : α → α → Prop} {s : Set α} {r' : α → α → Prop}, Bounded r s → r ≤ r' → Bounded r' s
rel_mono fun 
_: ?m.4429
_ 
_: ?m.4432
_ => 
le_of_lt: ∀ {α : Type ?u.4434} [inst : Preorder α] {a b : α}, a < b → a ≤ b
le_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) s
Set.bounded_le_of_bounded_lt

theorem 
Unbounded.rel_mono: ∀ {r' : α → α → Prop}, r' ≤ r → Unbounded r s → Unbounded r' s
Unbounded.rel_mono {
r': α → α → Prop
r' : 
α: Type ?u.4475
α → 
α: Type ?u.4475
α → 
Prop: Type
Prop} (
hr: r' ≤ r
hr : 
r': α → α → Prop
r' ≤ 
r: α → α → Prop
r) (
h: Unbounded r s
h : 
Unbounded: {α : Type ?u.4559} → (α → α → Prop) → Set α → Prop
Unbounded 
r: α → α → Prop
r 
s: Set α
s) : 
Unbounded: {α : Type ?u.4571} → (α → α → Prop) → Set α → Prop
Unbounded 
r': α → α → Prop
r' 
s: Set α
s :=
  fun 
a: ?m.4588
a =>
  let ⟨
b: α
b, 
hb: b ∈ s
hb, 
hba: ¬r b a
hba⟩ := 
h: Unbounded r s
h 
a: ?m.4588
a
  ⟨
b: α
b, 
hb: b ∈ s
hb, fun 
hba': ?m.4652
hba' => 
hba: ¬r b a
hba (
hr: r' ≤ r
hr 
b: α
b 
a: ?m.4588
a 
hba': ?m.4652
hba')⟩
#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' s
Set.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) s
unbounded_lt_of_unbounded_le [
Preorder: Type ?u.4778 → Type ?u.4778
Preorder 
α: Type ?u.4763
α] (
h: Unbounded (fun x x_1 => x ≤ x_1) s
h : 
Unbounded: {α : Type ?u.4781} → (α → α → Prop) → Set α → Prop
Unbounded 
(· ≤ ·): α → α → Prop
(· ≤ ·) 
s: Set α
s) : 
Unbounded: {α : Type ?u.4843} → (α → α → Prop) → Set α → Prop
Unbounded 
(· < ·): α → α → Prop
(· < ·) 
s: Set α
s :=
  
h: Unbounded (fun x x_1 => x ≤ x_1) s
h.
rel_mono: ∀ {α : Type ?u.4923} {r : α → α → Prop} {s : Set α} {r' : α → α → Prop}, r' ≤ r → Unbounded r s → Unbounded r' s
rel_mono fun 
_: ?m.4948
_ 
_: ?m.4951
_ => 
le_of_lt: ∀ {α : Type ?u.4953} [inst : Preorder α] {a b : α}, a < b → a ≤ b
le_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) s
Set.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) s
bounded_le_iff_bounded_lt [
Preorder: Type ?u.5016 → Type ?u.5016
Preorder 
α: Type ?u.5001
α] [
NoMaxOrder: (α : Type ?u.5019) → [inst : LT α] → Prop
NoMaxOrder 
α: Type ?u.5001
α] :
    
Bounded: {α : Type ?u.5033} → (α → α → Prop) → Set α → Prop
Bounded 
(· ≤ ·): α → α → Prop
(· ≤ ·) 
s: Set α
s ↔ 
Bounded: {α : Type ?u.5093} → (α → α → Prop) → Set α → Prop
Bounded 
(· < ·): α → α → Prop
(· < ·) 
s: Set α
s := by
Goals accomplished! 🐙
  
α: Type u_1

r: α → α → Prop

s, 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.5177
h => 
_: ?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) s
bounded_le_of_bounded_lt⟩
α: Type u_1

r: α → α → Prop

s, t: Set α

inst✝¹: Preorder α

inst✝: NoMaxOrder α

h: Bounded (fun x x_1 => x ≤ x_1) s

Bounded (fun x x_1 => x < x_1) s
  
α: Type u_1

r: α → α → Prop

s, 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.5177
h with 
a: ?m.5239
a 
ha: ?m.5240 a
ha
α: Type u_1

r: α → α → Prop

s, t: Set α

inst✝¹: Preorder α

inst✝: NoMaxOrder α

a: α

ha: ∀ (b : α), b ∈ s → (fun x x_1 => x ≤ x_1) b a

intro
Bounded (fun x x_1 => x < x_1) s
  
α: Type u_1

r: α → α → Prop

s, 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 < b
exists_gt 
a: ?m.5239
a with 
b: ?m.5317
b 
hb: ?m.5318 b
hb
α: Type u_1

r: α → α → Prop

s, t: Set α

inst✝¹: Preorder α

inst✝: NoMaxOrder α

a: α

ha: ∀ (b : α), b ∈ s → (fun x x_1 => x ≤ x_1) b a

b: α

hb: a < b

intro.intro
Bounded (fun x x_1 => x < x_1) s
  
α: Type u_1

r: α → α → Prop

s, 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.5317
b, fun 
c: ?m.5359
c 
hc: ?m.5362
hc => 
lt_of_le_of_lt: ∀ {α : Type ?u.5364} [inst : Preorder α] {a b c : α}, a ≤ b → b < c → a < c
lt_of_le_of_lt (
ha: ?m.5240 a
ha 
c: ?m.5359
c 
hc: ?m.5362
hc) 
hb: ?m.5318 b
hb⟩
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) s
Set.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) s
unbounded_lt_iff_unbounded_le [
Preorder: Type ?u.5439 → Type ?u.5439
Preorder 
α: Type ?u.5424
α] [
NoMaxOrder: (α : Type ?u.5442) → [inst : LT α] → Prop
NoMaxOrder 
α: Type ?u.5424
α] :
    
Unbounded: {α : Type ?u.5456} → (α → α → Prop) → Set α → Prop
Unbounded 
(· < ·): α → α → Prop
(· < ·) 
s: Set α
s ↔ 
Unbounded: {α : Type ?u.5507} → (α → α → Prop) → Set α → Prop
Unbounded 
(· ≤ ·): α → α → Prop
(· ≤ ·) 
s: Set α
s := by
Goals accomplished! 🐙
  
α: Type u_1

r: α → α → Prop

s, 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_1

r: α → α → Prop

s, 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 s
not_bounded_iff,
α: Type u_1

r: α → α → Prop

s, 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_1

r: α → α → Prop

s, 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_lt
Goals 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) s
Set.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) s
bounded_ge_of_bounded_gt [
Preorder: Type ?u.5969 → Type ?u.5969
Preorder 
α: Type ?u.5954
α] (
h: Bounded (fun x x_1 => x > x_1) s
h : 
Bounded: {α : Type ?u.5972} → (α → α → Prop) → Set α → Prop
Bounded 
(· > ·): α → α → Prop
(· > ·) 
s: Set α
s) : 
Bounded: {α : Type ?u.6025} → (α → α → Prop) → Set α → Prop
Bounded 
(· ≥ ·): α → α → Prop
(· ≥ ·) 
s: Set α
s :=
  let ⟨
a: α
a, 
ha: ∀ (b : α), b ∈ s → (fun x x_1 => x > x_1) b a
ha⟩ := 
h: Bounded (fun x x_1 => x > x_1) s
h
  ⟨
a: α
a, fun 
b: ?m.6190
b 
hb: ?m.6193
hb => 
le_of_lt: ∀ {α : Type ?u.6195} [inst : Preorder α] {a b : α}, a < b → a ≤ b
le_of_lt (
ha: ∀ (b : α), b ∈ s → (fun x x_1 => x > x_1) b a
ha 
b: ?m.6190
b 
hb: ?m.6193
hb)⟩
#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) s
Set.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) s
unbounded_gt_of_unbounded_ge [
Preorder: Type ?u.6369 → Type ?u.6369
Preorder 
α: Type ?u.6354
α] (
h: Unbounded (fun x x_1 => x ≥ x_1) s
h : 
Unbounded: {α : Type ?u.6372} → (α → α → Prop) → Set α → Prop
Unbounded 
(· ≥ ·): α → α → Prop
(· ≥ ·) 
s: Set α
s) : 
Unbounded: {α : Type ?u.6434} → (α → α → Prop) → Set α → Prop
Unbounded 
(· > ·): α → α → Prop
(· > ·) 
s: Set α
s :=
  fun 
a: ?m.6515
a =>
  let ⟨
b: α
b, 
hb: b ∈ s
hb, 
hba: ¬(fun x x_1 => x ≥ x_1) b a
hba⟩ := 
h: Unbounded (fun x x_1 => x ≥ x_1) s
h 
a: ?m.6515
a
  ⟨
b: α
b, 
hb: b ∈ s
hb, fun 
hba': ?m.6595
hba' => 
hba: ¬(fun x x_1 => x ≥ x_1) b a
hba (
le_of_lt: ∀ {α : Type ?u.6597} [inst : Preorder α] {a b : α}, a < b → a ≤ b
le_of_lt 
hba': ?m.6595
hba')⟩
#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) s
Set.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) s
bounded_ge_iff_bounded_gt [
Preorder: Type ?u.6750 → Type ?u.6750
Preorder 
α: Type ?u.6735
α] [
NoMinOrder: (α : Type ?u.6753) → [inst : LT α] → Prop
NoMinOrder 
α: Type ?u.6735
α] :
    
Bounded: {α : Type ?u.6767} → (α → α → Prop) → Set α → Prop
Bounded 
(· ≥ ·): α → α → Prop
(· ≥ ·) 
s: Set α
s ↔ 
Bounded: {α : Type ?u.6827} → (α → α → Prop) → Set α → Prop
Bounded 
(· > ·): α → α → 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) s
bounded_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) s
Set.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) s
unbounded_gt_iff_unbounded_ge [
Preorder: Type ?u.6967 → Type ?u.6967
Preorder 
α: Type ?u.6952
α] [
NoMinOrder: (α : Type ?u.6970) → [inst : LT α] → Prop
NoMinOrder 
α: Type ?u.6952
α] :
    
Unbounded: {α : Type ?u.6984} → (α → α → Prop) → Set α → Prop
Unbounded 
(· > ·): α → α → Prop
(· > ·) 
s: Set α
s ↔ 
Unbounded: {α : Type ?u.7035} → (α → α → Prop) → Set α → Prop
Unbounded 
(· ≥ ·): α → α → 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) s
unbounded_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) s
Set.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) univ
unbounded_le_univ [
LE: Type ?u.7184 → Type ?u.7184
LE 
α: Type ?u.7169
α] [
NoTopOrder: (α : Type ?u.7187) → [inst : LE α] → Prop
NoTopOrder 
α: Type ?u.7169
α] : 
Unbounded: {α : Type ?u.7195} → (α → α → Prop) → Set α → Prop
Unbounded 
(· ≤ ·): α → α → Prop
(· ≤ ·) (@
Set.univ: {α : Type ?u.7249} → Set α
Set.univ 
α: Type ?u.7169
α) := fun 
a: ?m.7264
a =>
  let ⟨
b: α
b, 
hb: ¬b ≤ a
hb⟩ := 
exists_not_le: ∀ {α : Type ?u.7266} [inst : LE α] [self : NoTopOrder α] (a : α), ∃ b, ¬b ≤ a
exists_not_le 
a: ?m.7264
a
  ⟨
b: α
b, 
⟨⟩: True
⟨⟩, 
hb: ¬b ≤ a
hb⟩
#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) univ
Set.unbounded_le_univ

theorem 
unbounded_lt_univ: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : NoTopOrder α], Unbounded (fun x x_1 => x < x_1) univ
unbounded_lt_univ [
Preorder: Type ?u.7421 → Type ?u.7421
Preorder 
α: Type ?u.7406
α] [
NoTopOrder: (α : Type ?u.7424) → [inst : LE α] → Prop
NoTopOrder 
α: Type ?u.7406
α] : 
Unbounded: {α : Type ?u.7438} → (α → α → Prop) → Set α → Prop
Unbounded 
(· < ·): α → α → 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) s
unbounded_lt_of_unbounded_le 
unbounded_le_univ: ∀ {α : Type ?u.7536} [inst : LE α] [inst_1 : NoTopOrder α], Unbounded (fun x x_1 => x ≤ x_1) univ
unbounded_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) univ
Set.unbounded_lt_univ

theorem 
unbounded_ge_univ: ∀ {α : Type u_1} [inst : LE α] [inst_1 : NoBotOrder α], Unbounded (fun x x_1 => x ≥ x_1) univ
unbounded_ge_univ [
LE: Type ?u.7601 → Type ?u.7601
LE 
α: Type ?u.7586
α] [
NoBotOrder: (α : Type ?u.7604) → [inst : LE α] → Prop
NoBotOrder 
α: Type ?u.7586
α] : 
Unbounded: {α : Type ?u.7612} → (α → α → Prop) → Set α → Prop
Unbounded 
(· ≥ ·): α → α → Prop
(· ≥ ·) (@
Set.univ: {α : Type ?u.7666} → Set α
Set.univ 
α: Type ?u.7586
α) := fun 
a: ?m.7681
a =>
  let ⟨
b: α
b, 
hb: ¬a ≤ b
hb⟩ := 
exists_not_ge: ∀ {α : Type ?u.7683} [inst : LE α] [self : NoBotOrder α] (a : α), ∃ b, ¬a ≤ b
exists_not_ge 
a: ?m.7681
a
  ⟨
b: α
b, 
⟨⟩: True
⟨⟩, 
hb: ¬a ≤ b
hb⟩
#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) univ
Set.unbounded_ge_univ

theorem 
unbounded_gt_univ: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : NoBotOrder α], Unbounded (fun x x_1 => x > x_1) univ
unbounded_gt_univ [
Preorder: Type ?u.7838 → Type ?u.7838
Preorder 
α: Type ?u.7823
α] [
NoBotOrder: (α : Type ?u.7841) → [inst : LE α] → Prop
NoBotOrder 
α: Type ?u.7823
α] : 
Unbounded: {α : Type ?u.7855} → (α → α → Prop) → Set α → Prop
Unbounded 
(· > ·): α → α → 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) s
unbounded_gt_of_unbounded_ge 
unbounded_ge_univ: ∀ {α : Type ?u.7953} [inst : LE α] [inst_1 : NoBotOrder α], Unbounded (fun x x_1 => x ≥ x_1) univ
unbounded_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) univ
Set.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 α → Prop
Bounded 
r: α → α → Prop
r { 
b: ?m.8033
b | 
r: α → α → Prop
r 
b: ?m.8033
b 
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.8092
Preorder 
α: Type ?u.8077
α] (
a: α
a : 
α: Type ?u.8077
α) : 
Bounded: {α : Type ?u.8097} → (α → α → Prop) → Set α → Prop
Bounded 
(· < ·): α → α → 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.8220
Preorder 
α: Type ?u.8205
α] (
a: α
a : 
α: Type ?u.8205
α) : 
Bounded: {α : Type ?u.8225} → (α → α → Prop) → Set α → Prop
Bounded 
(· ≤ ·): α → α → 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) s
bounded_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.8374
Preorder 
α: Type ?u.8359
α] (
a: α
a : 
α: Type ?u.8359
α) : 
Bounded: {α : Type ?u.8379} → (α → α → Prop) → Set α → Prop
Bounded 
(· ≤ ·): α → α → 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.8511
Preorder 
α: Type ?u.8496
α] [
NoMaxOrder: (α : Type ?u.8514) → [inst : LT α] → Prop
NoMaxOrder 
α: Type ?u.8496
α] (
a: α
a : 
α: Type ?u.8496
α) : 
Bounded: {α : Type ?u.8530} → (α → α → Prop) → Set α → Prop
Bounded 
(· < ·): α → α → Prop
(· < ·) (
Iic: {α : Type ?u.8578} → [inst : Preorder α] → α → Set α
Iic 
a: α
a) := by
Goals accomplished! 🐙
  
α: Type u_1

r: α → α → Prop

s, 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) s
bounded_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.8793
Preorder 
α: Type ?u.8778
α] (
a: α
a : 
α: Type ?u.8778
α) : 
Bounded: {α : Type ?u.8798} → (α → α → Prop) → Set α → Prop
Bounded 
(· > ·): α → α → 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.8921
Preorder 
α: Type ?u.8906
α] (
a: α
a : 
α: Type ?u.8906
α) : 
Bounded: {α : Type ?u.8926} → (α → α → Prop) → Set α → Prop
Bounded 
(· ≥ ·): α → α → 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) s
bounded_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.9075
Preorder 
α: Type ?u.9060
α] (
a: α
a : 
α: Type ?u.9060
α) : 
Bounded: {α : Type ?u.9080} → (α → α → Prop) → Set α → Prop
Bounded 
(· ≥ ·): α → α → 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.9212
Preorder 
α: Type ?u.9197
α] [
NoMinOrder: (α : Type ?u.9215) → [inst : LT α] → Prop
NoMinOrder 
α: Type ?u.9197
α] (
a: α
a : 
α: Type ?u.9197
α) : 
Bounded: {α : Type ?u.9231} → (α → α → Prop) → Set α → Prop
Bounded 
(· > ·): α → α → Prop
(· > ·) (
Ici: {α : Type ?u.9279} → [inst : Preorder α] → α → Set α
Ici 
a: α
a) := by
Goals accomplished! 🐙
  
α: Type u_1

r: α → α → Prop

s, 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) s
bounded_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.9507
Preorder 
α: Type ?u.9492
α] (
a: α
a 
b: α
b : 
α: Type ?u.9492
α) : 
Bounded: {α : Type ?u.9514} → (α → α → Prop) → Set α → Prop
Bounded 
(· < ·): α → α → 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 s
mono 
Set.Ioo_subset_Iio_self: ∀ {α : Type ?u.9631} [inst : Preorder α] {a b : α}, Ioo a b ⊆ Iio b
Set.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.9678
Preorder 
α: Type ?u.9663
α] (
a: α
a 
b: α
b : 
α: Type ?u.9663
α) : 
Bounded: {α : Type ?u.9685} → (α → α → Prop) → Set α → Prop
Bounded 
(· < ·): α → α → 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 s
mono 
Set.Ico_subset_Iio_self: ∀ {α : Type ?u.9802} [inst : Preorder α] {a b : α}, Ico a b ⊆ Iio b
Set.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.9849
Preorder 
α: Type ?u.9834
α] [
NoMaxOrder: (α : Type ?u.9852) → [inst : LT α] → Prop
NoMaxOrder 
α: Type ?u.9834
α] (
a: α
a 
b: α
b : 
α: Type ?u.9834
α) : 
Bounded: {α : Type ?u.9870} → (α → α → Prop) → Set α → Prop
Bounded 
(· < ·): α → α → 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 s
mono 
Set.Ioc_subset_Iic_self: ∀ {α : Type ?u.9988} [inst : Preorder α] {a b : α}, Ioc a b ⊆ Iic b
Set.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.10036
Preorder 
α: Type ?u.10021
α] [
NoMaxOrder: (α : Type ?u.10039) → [inst : LT α] → Prop
NoMaxOrder 
α: Type ?u.10021
α] (
a: α
a 
b: α
b : 
α: Type ?u.10021
α) : 
Bounded: {α : Type ?u.10057} → (α → α → Prop) → Set α → Prop
Bounded 
(· < ·): α → α → 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 s
mono 
Set.Icc_subset_Iic_self: ∀ {α : Type ?u.10175} [inst : Preorder α] {a b : α}, Icc a b ⊆ Iic b
Set.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.10223
Preorder 
α: Type ?u.10208
α] (
a: α
a 
b: α
b : 
α: Type ?u.10208
α) : 
Bounded: {α : Type ?u.10230} → (α → α → Prop) → Set α → Prop
Bounded 
(· ≤ ·): α → α → 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 s
mono 
Set.Ioo_subset_Iio_self: ∀ {α : Type ?u.10356} [inst : Preorder α] {a b : α}, Ioo a b ⊆ Iio b
Set.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.10403
Preorder 
α: Type ?u.10388
α] (
a: α
a 
b: α
b : 
α: Type ?u.10388
α) : 
Bounded: {α : Type ?u.10410} → (α → α → Prop) → Set α → Prop
Bounded 
(· ≤ ·): α → α → 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 s
mono 
Set.Ico_subset_Iio_self: ∀ {α : Type ?u.10536} [inst : Preorder α] {a b : α}, Ico a b ⊆ Iio b
Set.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.10583
Preorder 
α: Type ?u.10568
α] (
a: α
a 
b: α
b : 
α: Type ?u.10568
α) : 
Bounded: {α : Type ?u.10590} → (α → α → Prop) → Set α → Prop
Bounded 
(· ≤ ·): α → α → 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 s
mono 
Set.Ioc_subset_Iic_self: ∀ {α : Type ?u.10716} [inst : Preorder α] {a b : α}, Ioc a b ⊆ Iic b
Set.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.10763
Preorder 
α: Type ?u.10748
α] (
a: α
a 
b: α
b : 
α: Type ?u.10748
α) : 
Bounded: {α : Type ?u.10770} → (α → α → Prop) → Set α → Prop
Bounded 
(· ≤ ·): α → α → 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 s
mono 
Set.Icc_subset_Iic_self: ∀ {α : Type ?u.10896} [inst : Preorder α] {a b : α}, Icc a b ⊆ Iic b
Set.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.10943
Preorder 
α: Type ?u.10928
α] (
a: α
a 
b: α
b : 
α: Type ?u.10928
α) : 
Bounded: {α : Type ?u.10950} → (α → α → Prop) → Set α → Prop
Bounded 
(· > ·): α → α → 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 s
mono 
Set.Ioo_subset_Ioi_self: ∀ {α : Type ?u.11067} [inst : Preorder α] {a b : α}, Ioo a b ⊆ Ioi a
Set.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.11114
Preorder 
α: Type ?u.11099
α] (
a: α
a 
b: α
b : 
α: Type ?u.11099
α) : 
Bounded: {α : Type ?u.11121} → (α → α → Prop) → Set α → Prop
Bounded 
(· > ·): α → α → 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 s
mono 
Set.Ioc_subset_Ioi_self: ∀ {α : Type ?u.11238} [inst : Preorder α] {a b : α}, Ioc a b ⊆ Ioi a
Set.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.11285
Preorder 
α: Type ?u.11270
α] [
NoMinOrder: (α : Type ?u.11288) → [inst : LT α] → Prop
NoMinOrder 
α: Type ?u.11270
α] (
a: α
a 
b: α
b : 
α: Type ?u.11270
α) : 
Bounded: {α : Type ?u.11306} → (α → α → Prop) → Set α → Prop
Bounded 
(· > ·): α → α → 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 s
mono 
Set.Ico_subset_Ici_self: ∀ {α : Type ?u.11424} [inst : Preorder α] {a b : α}, Ico a b ⊆ Ici a
Set.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.11472
Preorder 
α: Type ?u.11457
α] [
NoMinOrder: (α : Type ?u.11475) → [inst : LT α] → Prop
NoMinOrder 
α: Type ?u.11457
α] (
a: α
a 
b: α
b : 
α: Type ?u.11457
α) : 
Bounded: {α : Type ?u.11493} → (α → α → Prop) → Set α → Prop
Bounded 
(· > ·): α → α → 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 s
mono 
Set.Icc_subset_Ici_self: ∀ {α : Type ?u.11611} [inst : Preorder α] {a b : α}, Icc a b ⊆ Ici a
Set.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.11659
Preorder 
α: Type ?u.11644
α] (
a: α
a 
b: α
b : 
α: Type ?u.11644
α) : 
Bounded: {α : Type ?u.11666} → (α → α → Prop) → Set α → Prop
Bounded 
(· ≥ ·): α → α → 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 s
mono 
Set.Ioo_subset_Ioi_self: ∀ {α : Type ?u.11792} [inst : Preorder α] {a b : α}, Ioo a b ⊆ Ioi a
Set.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.11839
Preorder 
α: Type ?u.11824
α] (
a: α
a 
b: α
b : 
α: Type ?u.11824
α) : 
Bounded: {α : Type ?u.11846} → (α → α → Prop) → Set α → Prop
Bounded 
(· ≥ ·): α → α → 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 s
mono 
Set.Ioc_subset_Ioi_self: ∀ {α : Type ?u.11972} [inst : Preorder α] {a b : α}, Ioc a b ⊆ Ioi a
Set.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.12019
Preorder 
α: Type ?u.12004
α] (
a: α
a 
b: α
b : 
α: Type ?u.12004
α) : 
Bounded: {α : Type ?u.12026} → (α → α → Prop) → Set α → Prop
Bounded 
(· ≥ ·): α → α → 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 s
mono 
Set.Ico_subset_Ici_self: ∀ {α : Type ?u.12152} [inst : Preorder α] {a b : α}, Ico a b ⊆ Ici a
Set.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.12199
Preorder 
α: Type ?u.12184
α] (
a: α
a 
b: α
b : 
α: Type ?u.12184
α) : 
Bounded: {α : Type ?u.12206} → (α → α → Prop) → Set α → Prop
Bounded 
(· ≥ ·): α → α → 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 s
mono 
Set.Icc_subset_Ici_self: ∀ {α : Type ?u.12332} [inst : Preorder α] {a b : α}, Icc a b ⊆ Ici a
Set.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.12379
SemilatticeSup 
α: Type ?u.12364
α] [
NoMaxOrder: (α : Type ?u.12382) → [inst : LT α] → Prop
NoMaxOrder 
α: Type ?u.12364
α] (
a: α
a : 
α: Type ?u.12364
α) :
    
Unbounded: {α : Type ?u.12484} → (α → α → Prop) → Set α → Prop
Unbounded 
(· ≤ ·): α → α → Prop
(· ≤ ·) (
Ioi: {α : Type ?u.12541} → [inst : Preorder α] → α → Set α
Ioi 
a: α
a) := fun 
b: ?m.12710
b =>
  let ⟨
c: α
c, 
hc: a ⊔ b < c
hc⟩ := 
exists_gt: ∀ {α : Type ?u.12712} [inst : LT α] [self : NoMaxOrder α] (a : α), ∃ b, a < b
exists_gt (
a: α
a ⊔ 
b: ?m.12710
b)
  ⟨
c: α
c, 
le_sup_left: ∀ {α : Type ?u.12889} [inst : SemilatticeSup α] {a b : α}, a ≤ a ⊔ b
le_sup_left.
trans_lt: ∀ {α : Type ?u.12904} [inst : Preorder α] {a b c : α}, a ≤ b → b < c → a < c
trans_lt 
hc: a ⊔ b < c
hc, (
le_sup_right: ∀ {α : Type ?u.13038} [inst : SemilatticeSup α] {a b : α}, b ≤ a ⊔ b
le_sup_right.
trans_lt: ∀ {α : Type ?u.13053} [inst : Preorder α] {a b c : α}, a ≤ b → b < c → a < c
trans_lt 
hc: a ⊔ b < c
hc).
not_le: ∀ {α : Type ?u.13105} [inst : Preorder α] {a b : α}, a < b → ¬b ≤ a
not_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.13210
SemilatticeSup 
α: Type ?u.13195
α] [
NoMaxOrder: (α : Type ?u.13213) → [inst : LT α] → Prop
NoMaxOrder 
α: Type ?u.13195
α] (
a: α
a : 
α: Type ?u.13195
α) :
    
Unbounded: {α : Type ?u.13315} → (α → α → Prop) → Set α → Prop
Unbounded 
(· ≤ ·): α → α → 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 t
mono 
Set.Ioi_subset_Ici_self: ∀ {α : Type ?u.13575} [inst : Preorder α] {a : α}, Ioi a ⊆ Ici a
Set.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.13712
SemilatticeSup 
α: Type ?u.13697
α] [
NoMaxOrder: (α : Type ?u.13715) → [inst : LT α] → Prop
NoMaxOrder 
α: Type ?u.13697
α] (
a: α
a : 
α: Type ?u.13697
α) :
    
Unbounded: {α : Type ?u.13817} → (α → α → Prop) → Set α → Prop
Unbounded 
(· < ·): α → α → 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) s
unbounded_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.14182
SemilatticeSup 
α: Type ?u.14167
α] (
a: α
a : 
α: Type ?u.14167
α) : 
Unbounded: {α : Type ?u.14187} → (α → α → Prop) → Set α → Prop
Unbounded 
(· < ·): α → α → Prop
(· < ·) (
Ici: {α : Type ?u.14235} → [inst : Preorder α] → α → Set α
Ici 
a: α
a) := fun 
b: ?m.14427
b =>
  ⟨
a: α
a ⊔ 
b: ?m.14427
b, 
le_sup_left: ∀ {α : Type ?u.14473} [inst : SemilatticeSup α] {a b : α}, a ≤ a ⊔ b
le_sup_left, 
le_sup_right: ∀ {α : Type ?u.14498} [inst : SemilatticeSup α] {a b : α}, b ≤ a ⊔ b
le_sup_right.
not_lt: ∀ {α : Type ?u.14513} [inst : Preorder α] {a b : α}, a ≤ b → ¬b < a
not_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 s
bounded_inter_not (
H: ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m
H : ∀ 
a: ?m.14689
a 
b: ?m.14692
b, ∃ 
m: ?m.14698
m, ∀ 
c: ?m.14701
c, 
r: α → α → Prop
r 
c: ?m.14701
c 
a: ?m.14689
a ∨ 
r: α → α → Prop
r 
c: ?m.14701
c 
b: ?m.14692
b → 
r: α → α → Prop
r 
c: ?m.14701
c 
m: ?m.14698
m) (
a: α
a : 
α: Type ?u.14673
α) :
    
Bounded: {α : Type ?u.14716} → (α → α → Prop) → Set α → Prop
Bounded 
r: α → α → Prop
r (
s: Set α
s ∩ { 
b: ?m.14738
b | ¬
r: α → α → Prop
r 
b: ?m.14738
b 
a: α
a }) ↔ 
Bounded: {α : Type ?u.14750} → (α → α → Prop) → Set α → Prop
Bounded 
r: α → α → Prop
r 
s: Set α
s := by
Goals accomplished! 🐙
  
α: Type u_1

r: α → α → Prop

s, t: Set α

H: ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m

a: α

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 s
Bounded.mono (
Set.inter_subset_left: ∀ {α : Type ?u.14789} (s t : Set α), s ∩ t ⊆ s
Set.inter_subset_left 
s: Set α
s 
_: Set ?m.14790
_)⟩
α: Type u_1

r: α → α → Prop

s, t: Set α

H: ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m

a: α

Bounded r (s ∩ { b | ¬r b a }) → Bounded r s
  
α: Type u_1

r: α → α → Prop

s, t: Set α

H: ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m

a: α

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 b
hb
⟨b, hb⟩: ?m.14768
⟩
α: Type u_1

r: α → α → Prop

s, t: Set α

H: ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m

a, b: α

hb: ∀ (b_1 : α), b_1 ∈ s ∩ { b | ¬r b a } → r b_1 b

intro
Bounded r s
  
α: Type u_1

r: α → α → Prop

s, t: Set α

H: ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m

a: α

Bounded r (s ∩ { b | ¬r b a }) ↔ Bounded r scases' 
H: ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m
H 
a: α
a 
b: α
b with 
m: ?m.14860
m 
hm: ?m.14861 m
hm
α: Type u_1

r: α → α → Prop

s, t: Set α

H: ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m

a, b: α

hb: ∀ (b_1 : α), b_1 ∈ s ∩ { b | ¬r b a } → r b_1 b

m: α

hm: ∀ (c : α), r c a ∨ r c b → r c m

intro.intro
Bounded r s
  
α: Type u_1

r: α → α → Prop

s, t: Set α

H: ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m

a: α

Bounded r (s ∩ { b | ¬r b a }) ↔ Bounded r sexact ⟨
m: ?m.14860
m, fun 
c: ?m.14905
c 
hc: ?m.14908
hc => 
hm: ?m.14861 m
hm 
c: ?m.14905
c (
or_iff_not_imp_left: ∀ {a b : Prop}, a ∨ b ↔ ¬a → b
or_iff_not_imp_left.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 fun 
hca: ?m.14918
hca => 
hb: ∀ (b_1 : α), b_1 ∈ s ∩ { b | ¬r b a } → r b_1 b
hb 
c: ?m.14905
c ⟨
hc: ?m.14908
hc, 
hca: ?m.14918
hca⟩)⟩
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 s
Set.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 s
unbounded_inter_not (
H: ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m
H : ∀ 
a: ?m.14989
a 
b: ?m.14992
b, ∃ 
m: ?m.14998
m, ∀ 
c: ?m.15001
c, 
r: α → α → Prop
r 
c: ?m.15001
c 
a: ?m.14989
a ∨ 
r: α → α → Prop
r 
c: ?m.15001
c 
b: ?m.14992
b → 
r: α → α → Prop
r 
c: ?m.15001
c 
m: ?m.14998
m) (
a: α
a : 
α: Type ?u.14973
α) :
    
Unbounded: {α : Type ?u.15016} → (α → α → Prop) → Set α → Prop
Unbounded 
r: α → α → Prop
r (
s: Set α
s ∩ { 
b: ?m.15038
b | ¬
r: α → α → Prop
r 
b: ?m.15038
b 
a: α
a }) ↔ 
Unbounded: {α : Type ?u.15050} → (α → α → Prop) → Set α → Prop
Unbounded 
r: α → α → Prop
r 
s: Set α
s := by
Goals accomplished! 🐙
  
α: Type u_1

r: α → α → Prop

s, t: Set α

H: ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m

a: α

Unbounded r (s ∩ { b | ¬r b a }) ↔ Unbounded r ssimp_rw [
α: Type u_1

r: α → α → Prop

s, t: Set α

H: ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m

a: α

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 s
not_bounded_iff,
α: Type u_1

r: α → α → Prop

s, t: Set α

H: ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m

a: α

¬Bounded r (s ∩ { b | ¬r b a }) ↔ ¬Bounded r s 
α: Type u_1

r: α → α → Prop

s, t: Set α

H: ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m

a: α

Unbounded r (s ∩ { b | ¬r b a }) ↔ Unbounded r s
bounded_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 s
bounded_inter_not 
H: ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m
H
Goals 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 s
Set.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) s
bounded_le_inter_not_le [
SemilatticeSup: Type ?u.15310 → Type ?u.15310
SemilatticeSup 
α: Type ?u.15295
α] (
a: α
a : 
α: Type ?u.15295
α) :
    
Bounded: {α : Type ?u.15315} → (α → α → Prop) → Set α → Prop
Bounded 
(· ≤ ·): α → α → Prop
(· ≤ ·) (
s: Set α
s ∩ { 
b: ?m.15387
b | ¬
b: ?m.15387
b ≤ 
a: α
a }) ↔ 
Bounded: {α : Type ?u.15498} → (α → α → Prop) → Set α → Prop
Bounded 
(· ≤ ·): α → α → 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 s
bounded_inter_not (fun 
x: ?m.15573
x 
y: ?m.15576
y => ⟨
x: ?m.15573
x ⊔ 
y: ?m.15576
y, fun 
_: ?m.15632
_ 
h: ?m.15635
h => 
h: ?m.15635
h.
elim: ∀ {a b c : Prop}, a ∨ b → (a → c) → (b → c) → c
elim 
le_sup_of_le_left: ∀ {α : Type ?u.15648} [inst : SemilatticeSup α] {a b c : α}, c ≤ a → c ≤ a ⊔ b
le_sup_of_le_left 
le_sup_of_le_right: ∀ {α : Type ?u.16500} [inst : SemilatticeSup α] {a b c : α}, c ≤ b → c ≤ a ⊔ b
le_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) s
Set.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) s
unbounded_le_inter_not_le [
SemilatticeSup: Type ?u.17514 → Type ?u.17514
SemilatticeSup 
α: Type ?u.17499
α] (
a: α
a : 
α: Type ?u.17499
α) :
    
Unbounded: {α : Type ?u.17519} → (α → α → Prop) → Set α → Prop
Unbounded 
(· ≤ ·): α → α → Prop
(· ≤ ·) (
s: Set α
s ∩ { 
b: ?m.17591
b | ¬
b: ?m.17591
b ≤ 
a: α
a }) ↔ 
Unbounded: {α : Type ?u.17702} → (α → α → Prop) → Set α → Prop
Unbounded 
(· ≤ ·): α → α → Prop
(· ≤ ·) 
s: Set α
s := by
Goals accomplished! 🐙
  
α: Type u_1

r: α → α → Prop

s, 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_1

r: α → α → Prop

s, 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 s
not_bounded_iff,
α: Type u_1

r: α → α → Prop

s, 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_1

r: α → α → Prop

s, 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 s
not_bounded_iff,
α: Type u_1

r: α → α → Prop

s, 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_1

r: α → α → Prop

s, 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_iff_not: ∀ {a b : Prop}, (¬a ↔ ¬b) ↔ (a ↔ b)
not_iff_not
α: Type u_1

r: α → α → Prop

s, 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_1

r: α → α → Prop

s, 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_1

r: α → α → Prop

s, 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) s
bounded_le_inter_not_le 
a: α
a
Goals 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) s
Set.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) s
bounded_le_inter_lt [
LinearOrder: Type ?u.17891 → Type ?u.17891
LinearOrder 
α: Type ?u.17876
α] (
a: α
a : 
α: Type ?u.17876
α) :
    
Bounded: {α : Type ?u.17896} → (α → α → Prop) → Set α → Prop
Bounded 
(· ≤ ·): α → α → Prop
(· ≤ ·) (
s: Set α
s ∩ { 
b: ?m.17968
b | 
a: α
a < 
b: ?m.17968
b }) ↔ 
Bounded: {α : Type ?u.18074} → (α → α → Prop) → Set α → Prop
Bounded 
(· ≤ ·): α → α → Prop
(· ≤ ·) 
s: Set α
s := by
Goals accomplished! 🐙
  
α: Type u_1

r: α → α → Prop

s, 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_1

r: α → α → Prop

s, 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 < a
not_le,
α: Type u_1

r: α → α → Prop

s, 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_1

r: α → α → Prop

s, 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_le
Goals 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) s
Set.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) s
unbounded_le_inter_lt [
LinearOrder: Type ?u.18812 → Type ?u.18812
LinearOrder 
α: Type ?u.18797
α] (
a: α
a : 
α: Type ?u.18797
α) :
    
Unbounded: {α : Type ?u.18817} → (α → α → Prop) → Set α → Prop
Unbounded 
(· ≤ ·): α → α → Prop
(· ≤ ·) (
s: Set α
s ∩ { 
b: ?m.18889
b | 
a: α
a < 
b: ?m.18889
b }) ↔ 
Unbounded: {α : Type ?u.18995} → (α → α → Prop) → Set α → Prop
Unbounded 
(· ≤ ·): α → α → Prop
(· ≤ ·) 
s: Set α
s := by
Goals accomplished! 🐙
  
α: Type u_1

r: α → α → Prop

s, 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) s
unbounded_le_inter_not_le 
_: Type ?u.19134
_ 
s: Set α
s _ 
a: α
a
α: Type u_1

r: α → α → Prop

s, t: Set α

inst✝: LinearOrder α

a, x✝: α

h.e'_1.h.e'_3.h.e'_4.h.e'_2.h.a
a < x✝ ↔ ¬x✝ ≤ a
  
α: Type u_1

r: α → α → Prop

s, 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 ≤ x
lt_iff_not_le
Goals 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) s
Set.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) s
bounded_le_inter_le [
LinearOrder: Type ?u.22048 → Type ?u.22048
LinearOrder 
α: Type ?u.22033
α] (
a: α
a : 
α: Type ?u.22033
α) :
    
Bounded: {α : Type ?u.22053} → (α → α → Prop) → Set α → Prop
Bounded 
(· ≤ ·): α → α → Prop
(· ≤ ·) (
s: Set α
s ∩ { 
b: ?m.22125
b | 
a: α
a ≤ 
b: ?m.22125
b }) ↔ 
Bounded: {α : Type ?u.22231} → (α → α → Prop) → Set α → Prop
Bounded 
(· ≤ ·): α → α → Prop
(· ≤ ·) 
s: Set α
s := by
Goals accomplished! 🐙
  
α: Type u_1

r: α → α → Prop

s, 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 s
Bounded.mono (
Set.inter_subset_left: ∀ {α : Type ?u.22330} (s t : Set α), s ∩ t ⊆ s
Set.inter_subset_left 
s: Set α
s 
_: Set ?m.22331
_)⟩
α: Type u_1

r: α → α → Prop

s, 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_1

r: α → α → Prop

s, 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_1

r: α → α → Prop

s, 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) s
bounded_le_inter_lt 
_: Type ?u.22346
_ 
s: Set α
s _ 
a: α
a
α: Type u_1

r: α → α → Prop

s, 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_1

r: α → α → Prop

s, 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_1

r: α → α → Prop

s, 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 s
Bounded.mono fun 
x: ?m.22391
x ⟨
hx: x ∈ s
hx, 
hx': x ∈ { b | a < b }
hx'⟩ => ⟨
hx: x ∈ s
hx, 
le_of_lt: ∀ {α : Type ?u.22430} [inst : Preorder α] {a b : α}, a < b → a ≤ b
le_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) s
Set.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) s
unbounded_le_inter_le [
LinearOrder: Type ?u.22651 → Type ?u.22651
LinearOrder 
α: Type ?u.22636
α] (
a: α
a : 
α: Type ?u.22636
α) :
    
Unbounded: {α : Type ?u.22656} → (α → α → Prop) → Set α → Prop
Unbounded 
(· ≤ ·): α → α → Prop
(· ≤ ·) (
s: Set α
s ∩ { 
b: ?m.22728
b | 
a: α
a ≤ 
b: ?m.22728
b }) ↔ 
Unbounded: {α : Type ?u.22834} → (α → α → Prop) → Set α → Prop
Unbounded 
(· ≤ ·): α → α → Prop
(· ≤ ·) 
s: Set α
s := by
Goals accomplished! 🐙
  
α: Type u_1

r: α → α → Prop

s, 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_1

r: α → α → Prop

s, 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 s
not_bounded_iff,
α: Type u_1

r: α → α → Prop

s, 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_1

r: α → α → Prop

s, 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 s
not_bounded_iff,
α: Type u_1

r: α → α → Prop

s, 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_1

r: α → α → Prop

s, 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_iff_not: ∀ {a b : Prop}, (¬a ↔ ¬b) ↔ (a ↔ b)
not_iff_not
α: Type u_1

r: α → α → Prop

s, 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_1

r: α → α → Prop

s, 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_1

r: α → α → Prop

s, 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) s
bounded_le_inter_le 
a: α
a
Goals 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) s
Set.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) s
bounded_lt_inter_not_lt [
SemilatticeSup: Type ?u.23022 → Type ?u.23022
SemilatticeSup 
α: Type ?u.23007
α] (
a: α
a : 
α: Type ?u.23007
α) :
    
Bounded: {α : Type ?u.23027} → (α → α → Prop) → Set α → Prop
Bounded 
(· < ·): α → α → Prop
(· < ·) (
s: Set α
s ∩ { 
b: ?m.23090
b | ¬
b: ?m.23090
b < 
a: α
a }) ↔ 
Bounded: {α : Type ?u.23201} → (α → α → Prop) → Set α → Prop
Bounded 
(· < ·): α → α → 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 s
bounded_inter_not (fun 
x: ?m.23267
x 
y: ?m.23270
y => ⟨
x: ?m.23267
x ⊔ 
y: ?m.23270
y, fun 
_: ?m.23326
_ 
h: ?m.23329
h => 
h: ?m.23329
h.
elim: ∀ {a b c : Prop}, a ∨ b → (a → c) → (b → c) → c
elim 
lt_sup_of_lt_left: ∀ {α : Type ?u.23342} [inst : SemilatticeSup α] {a b c : α}, c < a → c < a ⊔ b
lt_sup_of_lt_left 
lt_sup_of_lt_right: ∀ {α : Type ?u.24194} [inst : SemilatticeSup α] {a b c : α}, c < b → c < a ⊔ b
lt_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) s
Set.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) s
unbounded_lt_inter_not_lt [
SemilatticeSup: Type ?u.25208 → Type ?u.25208
SemilatticeSup 
α: Type ?u.25193
α] (
a: α
a : 
α: Type ?u.25193
α) :
    
Unbounded: {α : Type ?u.25213} → (α → α → Prop) → Set α → Prop
Unbounded 
(· < ·): α → α → Prop
(· < ·) (
s: Set α
s ∩ { 
b: ?m.25276
b | ¬
b: ?m.25276
b < 
a: α
a }) ↔ 
Unbounded: {α : Type ?u.25387} → (α → α → Prop) → Set α → Prop
Unbounded 
(· < ·): α → α → Prop
(· < ·) 
s: Set α
s := by
Goals accomplished! 🐙
  
α: Type u_1

r: α → α → Prop

s, 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_1

r: α → α → Prop

s, 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 s
not_bounded_iff,
α: Type u_1

r: α → α → Prop

s, 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_1

r: α → α → Prop

s, 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 s
not_bounded_iff,
α: Type u_1

r: α → α → Prop

s, 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_1

r: α → α → Prop

s, 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_iff_not: ∀ {a b : Prop}, (¬a ↔ ¬b) ↔ (a ↔ b)
not_iff_not
α: Type u_1

r: α → α → Prop

s, 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_1

r: α → α → Prop

s, 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_1

r: α → α → Prop

s, 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) s
bounded_lt_inter_not_lt 
a: α
a
Goals 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) s
Set.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) s
bounded_lt_inter_le [
LinearOrder: Type ?u.25567 → Type ?u.25567
LinearOrder 
α: Type ?u.25552
α] (
a: α
a : 
α: Type ?u.25552
α) :
    
Bounded: {α : Type ?u.25572} → (α → α → Prop) → Set α → Prop
Bounded 
(· < ·): α → α → Prop
(· < ·) (
s: