/-
Copyright (c) 2022 Sébastien Gouëzel. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sébastien Gouëzel, Yury Kudryashov

! This file was ported from Lean 3 source module order.monotone.extension
! leanprover-community/mathlib commit 422e70f7ce183d2900c586a8cda8381e788a0c62
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Order.ConditionallyCompleteLattice.Basic

/-!
# Extension of a monotone function from a set to the whole space

In this file we prove that if a function is monotone and is bounded on a set `s`, then it admits a
monotone extension to the whole space.
-/


open Set

variable {
α: Type ?u.25
α 
β: Type ?u.6648
β : 
Type _: Type (?u.5+1)
Type _} [
LinearOrder: Type ?u.8 → Type ?u.8
LinearOrder 
α: Type ?u.2
α] [
ConditionallyCompleteLinearOrder: Type ?u.11 → Type ?u.11
ConditionallyCompleteLinearOrder 
β: Type ?u.28
β] {
f: α → β
f : 
α: Type ?u.2
α → 
β: Type ?u.5
β} {
s: Set α
s : 
Set: Type ?u.18 → Type ?u.18
Set 
α: Type ?u.2
α}
  {
a: α
a 
b: α
b : 
α: Type ?u.2
α}

/-- If a function is monotone and is bounded on a set `s`, then it admits a monotone extension to
the whole space. -/
theorem 
MonotoneOn.exists_monotone_extension: ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β] {f : α → β}
  {s : Set α}, MonotoneOn f s → BddBelow (f '' s) → BddAbove (f '' s) → ∃ g, Monotone g ∧ EqOn f g s
MonotoneOn.exists_monotone_extension (
h: MonotoneOn f s
h : 
MonotoneOn: {α : Type ?u.49} → {β : Type ?u.48} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Set α → Prop
MonotoneOn 
f: α → β
f 
s: Set α
s) (
hl: BddBelow (f '' s)
hl : 
BddBelow: {α : Type ?u.336} → [inst : Preorder α] → Set α → Prop
BddBelow (
f: α → β
f '' 
s: Set α
s))
    (
hu: BddAbove (f '' s)
hu : 
BddAbove: {α : Type ?u.368} → [inst : Preorder α] → Set α → Prop
BddAbove (
f: α → β
f '' 
s: Set α
s)) : ∃ 
g: α → β
g : 
α: Type ?u.25
α → 
β: Type ?u.28
β, 
Monotone: {α : Type ?u.407} → {β : Type ?u.406} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Monotone 
g: α → β
g ∧ 
EqOn: {α : Type ?u.416} → {β : Type ?u.415} → (α → β) → (α → β) → Set α → Prop
EqOn 
f: α → β
f 
g: α → β
g 
s: Set α
s := by
Goals accomplished! 🐙
  
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a, b: α

h: MonotoneOn f s

hl: BddBelow (f '' s)

hu: BddAbove (f '' s)

∃ g, Monotone g ∧ EqOn f g sclassical
    /- The extension is defined by `f x = f a` for `x ≤ a`, and `f x` is the supremum of the values
      of `f`  to the left of `x` for `x ≥ a`. -/
    
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a, b: α

h: MonotoneOn f s

hl: BddBelow (f '' s)

hu: BddAbove (f '' s)

∃ g, Monotone g ∧ EqOn f g srcases 
hl: BddBelow (f '' s)
hl with 
⟨a, ha⟩: BddBelow (f '' s)
⟨
a: β
a
⟨a, ha⟩: BddBelow (f '' s)
, 
ha: a ∈ lowerBounds (f '' s)
ha
⟨a, ha⟩: BddBelow (f '' s)
⟩
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

intro
∃ g, Monotone g ∧ EqOn f g s
    
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a, b: α

h: MonotoneOn f s

hl: BddBelow (f '' s)

hu: BddAbove (f '' s)

∃ g, Monotone g ∧ EqOn f g shave 
hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
hu' : ∀ 
x: ?m.469
x, 
BddAbove: {α : Type ?u.472} → [inst : Preorder α] → Set α → Prop
BddAbove (
f: α → β
f '' (
Iic: {α : Type ?u.507} → [inst : Preorder α] → α → Set α
Iic 
x: ?m.469
x ∩ 
s: Set α
s)) := fun 
x: ?m.782
x =>
      
hu: BddAbove (f '' s)
hu.
mono: ∀ {α : Type ?u.784} [inst : Preorder α] ⦃s t : Set α⦄, s ⊆ t → BddAbove t → BddAbove s
mono (
image_subset: ∀ {α : Type ?u.814} {β : Type ?u.815} {a b : Set α} (f : α → β), a ⊆ b → f '' a ⊆ f '' b
image_subset 
_: ?m.816 → ?m.817
_ (
inter_subset_right: ∀ {α : Type ?u.835} (s t : Set α), s ∩ t ⊆ t
inter_subset_right 
_: Set ?m.836
_ 
_: Set ?m.836
_))
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

intro
∃ g, Monotone g ∧ EqOn f g s
    
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a, b: α

h: MonotoneOn f s

hl: BddBelow (f '' s)

hu: BddAbove (f '' s)

∃ g, Monotone g ∧ EqOn f g slet 
g: α → β
g : 
α: Type u_1
α → 
β: Type u_2
β := fun 
x: ?m.862
x => if 
Disjoint: {α : Type ?u.864} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → Prop
Disjoint (
Iic: {α : Type ?u.868} → [inst : Preorder α] → α → Set α
Iic 
x: ?m.862
x) 
s: Set α
s then 
a: β
a else 
sSup: {α : Type ?u.964} → [self : SupSet α] → Set α → α
sSup (
f: α → β
f '' (
Iic: {α : Type ?u.998} → [inst : Preorder α] → α → Set α
Iic 
x: ?m.862
x ∩ 
s: Set α
s))
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

intro
∃ g, Monotone g ∧ EqOn f g s
    
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a, b: α

h: MonotoneOn f s

hl: BddBelow (f '' s)

hu: BddAbove (f '' s)

∃ g, Monotone g ∧ EqOn f g shave 
hgs: EqOn f g s
hgs : 
EqOn: {α : Type ?u.1042} → {β : Type ?u.1041} → (α → β) → (α → β) → Set α → Prop
EqOn 
f: α → β
f 
g: α → β
g 
s: Set α
s := 
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

intro
∃ g, Monotone g ∧ EqOn f g sby
Goals accomplished! 🐙
      
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

EqOn f g sintro 
x: α
x 
hx: x ∈ s
hx
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

x: α

hx: x ∈ s

f x = g x
      
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

EqOn f g ssimp only []
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

x: α

hx: x ∈ s

f x = if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
      
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

EqOn f g shave : 
IsGreatest: {α : Type ?u.1438} → [inst : Preorder α] → Set α → α → Prop
IsGreatest (
Iic: {α : Type ?u.1464} → [inst : Preorder α] → α → Set α
Iic 
x: α
x ∩ 
s: Set α
s) 
x: α
x := ⟨⟨
right_mem_Iic: ∀ {α : Type ?u.1501} [inst : Preorder α] {a : α}, a ∈ Iic a
right_mem_Iic, 
hx: x ∈ s
hx⟩, fun 
y: ?m.1530
y 
hy: ?m.1533
hy => 
hy: ?m.1533
hy.
1: ∀ {a b : Prop}, a ∧ b → a
1⟩
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

x: α

hx: x ∈ s

this: IsGreatest (Iic x ∩ s) x

f x = if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
      
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

EqOn f g srw [
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

x: α

hx: x ∈ s

this: IsGreatest (Iic x ∩ s) x

f x = if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
if_neg: ∀ {c : Prop} {h : Decidable c}, ¬c → ∀ {α : Sort ?u.1545} {t e : α}, (if c then t else e) = e
if_neg 
this: IsGreatest (Iic x ∩ s) x
this.
nonempty: ∀ {α : Type ?u.1548} [inst : Preorder α] {s : Set α} {a : α}, IsGreatest s a → Set.Nonempty s
nonempty.
not_disjoint: ∀ {α : Type ?u.1558} {s t : Set α}, Set.Nonempty (s ∩ t) → ¬Disjoint s t
not_disjoint,
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

x: α

hx: x ∈ s

this: IsGreatest (Iic x ∩ s) x

f x = sSup (f '' (Iic x ∩ s))
        
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

x: α

hx: x ∈ s

this: IsGreatest (Iic x ∩ s) x

f x = if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))((
h: MonotoneOn f s
h.
mono: ∀ {α : Type ?u.1593} {β : Type ?u.1594} {s s₂ : Set α} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β],
  MonotoneOn f s → s₂ ⊆ s → MonotoneOn f s₂
mono <| 
inter_subset_right: ∀ {α : Type ?u.1625} (s t : Set α), s ∩ t ⊆ t
inter_subset_right 
_: Set ?m.1626
_ 
_: Set ?m.1626
_).
map_isGreatest: ∀ {α : Type ?u.1630} {β : Type ?u.1629} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {t : Set α},
  MonotoneOn f t → ∀ {a : α}, IsGreatest t a → IsGreatest (f '' t) (f a)
map_isGreatest 
this: IsGreatest (Iic x ∩ s) x
this).
csSup_eq: ∀ {α : Type ?u.1648} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α}, IsGreatest s a → sSup s = a
csSup_eq
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

x: α

hx: x ∈ s

this: IsGreatest (Iic x ∩ s) x

f x = f x]
Goals accomplished! 🐙
    
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a, b: α

h: MonotoneOn f s

hl: BddBelow (f '' s)

hu: BddAbove (f '' s)

∃ g, Monotone g ∧ EqOn f g srefine' ⟨
g: α → β
g, fun 
x: ?m.1708
x 
y: ?m.1711
y 
hxy: ?m.1714
hxy => 
_: g x ≤ g y
_, 
hgs: EqOn f g s
hgs⟩
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

hgs: EqOn f g s

x, y: α

hxy: x ≤ y

intro
g x ≤ g y
    
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a, b: α

h: MonotoneOn f s

hl: BddBelow (f '' s)

hu: BddAbove (f '' s)

∃ g, Monotone g ∧ EqOn f g sby_cases 
hx: ?m.1996
hx : 
Disjoint: {α : Type ?u.1729} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → Prop
Disjoint (
Iic: {α : Type ?u.1733} → [inst : Preorder α] → α → Set α
Iic 
x: ?m.1708
x) 
s: Set α
s
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

hgs: EqOn f g s

x, y: α

hxy: x ≤ y

hx: Disjoint (Iic x) s

pos
g x ≤ g y
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

hgs: EqOn f g s

x, y: α

hxy: x ≤ y

hx: ¬Disjoint (Iic x) s

neg
g x ≤ g y 
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

hgs: EqOn f g s

x, y: α

hxy: x ≤ y

intro
g x ≤ g y<;>
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

hgs: EqOn f g s

x, y: α

hxy: x ≤ y

hx: Disjoint (Iic x) s

pos
g x ≤ g y
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

hgs: EqOn f g s

x, y: α

hxy: x ≤ y

hx: ¬Disjoint (Iic x) s

neg
g x ≤ g y 
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

hgs: EqOn f g s

x, y: α

hxy: x ≤ y

intro
g x ≤ g yby_cases 
hy: ?m.2565
hy : 
Disjoint: {α : Type ?u.2291} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → Prop
Disjoint (
Iic: {α : Type ?u.2295} → [inst : Preorder α] → α → Set α
Iic 
y: ?m.1711
y) 
s: Set α
s
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

hgs: EqOn f g s

x, y: α

hxy: x ≤ y

hx: ¬Disjoint (Iic x) s

hy: Disjoint (Iic y) s

pos
g x ≤ g y
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

hgs: EqOn f g s

x, y: α

hxy: x ≤ y

hx: ¬Disjoint (Iic x) s

hy: ¬Disjoint (Iic y) s

neg
g x ≤ g y 
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

hgs: EqOn f g s

x, y: α

hxy: x ≤ y

intro
g x ≤ g y<;>
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

hgs: EqOn f g s

x, y: α

hxy: x ≤ y

hx: Disjoint (Iic x) s

hy: Disjoint (Iic y) s

pos
g x ≤ g y
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

hgs: EqOn f g s

x, y: α

hxy: x ≤ y

hx: Disjoint (Iic x) s

hy: ¬Disjoint (Iic y) s

neg
g x ≤ g y
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

hgs: EqOn f g s

x, y: α

hxy: x ≤ y

hx: ¬Disjoint (Iic x) s

hy: Disjoint (Iic y) s

pos
g x ≤ g y
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

hgs: EqOn f g s

x, y: α

hxy: x ≤ y

hx: ¬Disjoint (Iic x) s

hy: ¬Disjoint (Iic y) s

neg
g x ≤ g y
      
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

hgs: EqOn f g s

x, y: α

hxy: x ≤ y

intro
g x ≤ g ysimp only [
if_pos: ∀ {c : Prop} {h : Decidable c}, c → ∀ {α : Sort ?u.4378} {t e : α}, (if c then t else e) = t
if_pos, 
if_neg: ∀ {c : Prop} {h : Decidable c}, ¬c → ∀ {α : Sort ?u.4392} {t e : α}, (if c then t else e) = e
if_neg, 
not_false_iff: ¬False ↔ True
not_false_iff, *, 
refl: ∀ {α : Type ?u.5150} {r : α → α → Prop} [inst : IsRefl α r] (a : α), r a a
refl]
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

hgs: EqOn f g s

x, y: α

hxy: x ≤ y

hx: ¬Disjoint (Iic x) s

hy: Disjoint (Iic y) s

pos
sSup (f '' (Iic x ∩ s)) ≤ a
    
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a, b: α

h: MonotoneOn f s

hl: BddBelow (f '' s)

hu: BddAbove (f '' s)

∃ g, Monotone g ∧ EqOn f g s·
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

hgs: EqOn f g s

x, y: α

hxy: x ≤ y

hx: Disjoint (Iic x) s

hy: ¬Disjoint (Iic y) s

neg
a ≤ sSup (f '' (Iic y ∩ s)) 
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

hgs: EqOn f g s

x, y: α

hxy: x ≤ y

hx: Disjoint (Iic x) s

hy: ¬Disjoint (Iic y) s

neg
a ≤ sSup (f '' (Iic y ∩ s))
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

hgs: EqOn f g s

x, y: α

hxy: x ≤ y

hx: ¬Disjoint (Iic x) s

hy: Disjoint (Iic y) s

pos
sSup (f '' (Iic x ∩ s)) ≤ a
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

hgs: EqOn f g s

x, y: α

hxy: x ≤ y

hx: ¬Disjoint (Iic x) s

hy: ¬Disjoint (Iic y) s

neg
sSup (f '' (Iic x ∩ s)) ≤ sSup (f '' (Iic y ∩ s))rcases 
not_disjoint_iff_nonempty_inter: ∀ {α : Type ?u.5934} {s t : Set α}, ¬Disjoint s t ↔ Set.Nonempty (s ∩ t)
not_disjoint_iff_nonempty_inter.
1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 
hy: ?m.2284
hy with 
⟨z, hz⟩: Set.Nonempty (Iic y ∩ s)
⟨
z: α
z
⟨z, hz⟩: Set.Nonempty (Iic y ∩ s)
, 
hz: z ∈ Iic y ∩ s
hz
⟨z, hz⟩: Set.Nonempty (Iic y ∩ s)
⟩
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

hgs: EqOn f g s

x, y: α

hxy: x ≤ y

hx: Disjoint (Iic x) s

hy: ¬Disjoint (Iic y) s

z: α

hz: z ∈ Iic y ∩ s

neg.intro
a ≤ sSup (f '' (Iic y ∩ s))
      
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

hgs: EqOn f g s

x, y: α

hxy: x ≤ y

hx: Disjoint (Iic x) s

hy: ¬Disjoint (Iic y) s

neg
a ≤ sSup (f '' (Iic y ∩ s))exact 
le_csSup_of_le: ∀ {α : Type ?u.5993} [inst : ConditionallyCompleteLattice α] {s : Set α} {a b : α},
  BddAbove s → b ∈ s → a ≤ b → a ≤ sSup s
le_csSup_of_le (
hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
hu' 
_: α
_) (
mem_image_of_mem: ∀ {α : Type ?u.6049} {β : Type ?u.6050} (f : α → β) {x : α} {a : Set α}, x ∈ a → f x ∈ f '' a
mem_image_of_mem 
_: ?m.6051 → ?m.6052
_ 
hz: z ∈ Iic y ∩ s
hz) (
ha: a ∈ lowerBounds (f '' s)
ha <| 
mem_image_of_mem: ∀ {α : Type ?u.6069} {β : Type ?u.6070} (f : α → β) {x : α} {a : Set α}, x ∈ a → f x ∈ f '' a
mem_image_of_mem 
_: ?m.6071 → ?m.6072
_ 
hz: z ∈ Iic y ∩ s
hz.
2: ∀ {a b : Prop}, a ∧ b → b
2)
Goals accomplished! 🐙
    
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a, b: α

h: MonotoneOn f s

hl: BddBelow (f '' s)

hu: BddAbove (f '' s)

∃ g, Monotone g ∧ EqOn f g s·
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

hgs: EqOn f g s

x, y: α

hxy: x ≤ y

hx: ¬Disjoint (Iic x) s

hy: Disjoint (Iic y) s

pos
sSup (f '' (Iic x ∩ s)) ≤ a 
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

hgs: EqOn f g s

x, y: α

hxy: x ≤ y

hx: ¬Disjoint (Iic x) s

hy: Disjoint (Iic y) s

pos
sSup (f '' (Iic x ∩ s)) ≤ a
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

hgs: EqOn f g s

x, y: α

hxy: x ≤ y

hx: ¬Disjoint (Iic x) s

hy: ¬Disjoint (Iic y) s

neg
sSup (f '' (Iic x ∩ s)) ≤ sSup (f '' (Iic y ∩ s))exact (
hx: ?m.2003
hx <| 
hy: ?m.2558
hy.
mono_left: ∀ {α : Type ?u.6081} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b c : α}, a ≤ b → Disjoint b c → Disjoint a c
mono_left <| 
Iic_subset_Iic: ∀ {α : Type ?u.6141} [inst : Preorder α] {a b : α}, Iic a ⊆ Iic b ↔ a ≤ b
Iic_subset_Iic.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 
hxy: ?m.1714
hxy).
elim: ∀ {C : Sort ?u.6251}, False → C
elim
Goals accomplished! 🐙
    
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a, b: α

h: MonotoneOn f s

hl: BddBelow (f '' s)

hu: BddAbove (f '' s)

∃ g, Monotone g ∧ EqOn f g s·
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

hgs: EqOn f g s

x, y: α

hxy: x ≤ y

hx: ¬Disjoint (Iic x) s

hy: ¬Disjoint (Iic y) s

neg
sSup (f '' (Iic x ∩ s)) ≤ sSup (f '' (Iic y ∩ s)) 
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

hgs: EqOn f g s

x, y: α

hxy: x ≤ y

hx: ¬Disjoint (Iic x) s

hy: ¬Disjoint (Iic y) s

neg
sSup (f '' (Iic x ∩ s)) ≤ sSup (f '' (Iic y ∩ s))rw [
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

hgs: EqOn f g s

x, y: α

hxy: x ≤ y

hx: ¬Disjoint (Iic x) s

hy: ¬Disjoint (Iic y) s

neg
sSup (f '' (Iic x ∩ s)) ≤ sSup (f '' (Iic y ∩ s))
not_disjoint_iff_nonempty_inter: ∀ {α : Type ?u.6408} {s t : Set α}, ¬Disjoint s t ↔ Set.Nonempty (s ∩ t)
not_disjoint_iff_nonempty_inter
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

hgs: EqOn f g s

x, y: α

hxy: x ≤ y

hx: Set.Nonempty (Iic x ∩ s)

hy: Set.Nonempty (Iic y ∩ s)

neg
sSup (f '' (Iic x ∩ s)) ≤ sSup (f '' (Iic y ∩ s))]
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

hgs: EqOn f g s

x, y: α

hxy: x ≤ y

hx: Set.Nonempty (Iic x ∩ s)

hy: Set.Nonempty (Iic y ∩ s)

neg
sSup (f '' (Iic x ∩ s)) ≤ sSup (f '' (Iic y ∩ s)) at 
hx: ?m.2003
hx 
hy: ¬Disjoint (Iic y) s
hy
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

hgs: EqOn f g s

x, y: α

hxy: x ≤ y

hx: Set.Nonempty (Iic x ∩ s)

hy: Set.Nonempty (Iic y ∩ s)

neg
sSup (f '' (Iic x ∩ s)) ≤ sSup (f '' (Iic y ∩ s))
      
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

hgs: EqOn f g s

x, y: α

hxy: x ≤ y

hx: ¬Disjoint (Iic x) s

hy: ¬Disjoint (Iic y) s

neg
sSup (f '' (Iic x ∩ s)) ≤ sSup (f '' (Iic y ∩ s))refine' 
csSup_le_csSup: ∀ {α : Type ?u.6505} [inst : ConditionallyCompleteLattice α] {s t : Set α},
  BddAbove t → Set.Nonempty s → s ⊆ t → sSup s ≤ sSup t
csSup_le_csSup (
hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
hu' 
_: α
_) (
hx: Set.Nonempty (Iic x ∩ s)
hx.
image: ∀ {α : Type ?u.6528} {β : Type ?u.6529} (f : α → β) {s : Set α}, Set.Nonempty s → Set.Nonempty (f '' s)
image 
_: ?m.6535 → ?m.6536
_) (
image_subset: ∀ {α : Type ?u.6546} {β : Type ?u.6547} {a b : Set α} (f : α → β), a ⊆ b → f '' a ⊆ f '' b
image_subset 
_: ?m.6548 → ?m.6549
_ 
_: ?m.6550 ⊆ ?m.6551
_)
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

hgs: EqOn f g s

x, y: α

hxy: x ≤ y

hx: Set.Nonempty (Iic x ∩ s)

hy: Set.Nonempty (Iic y ∩ s)

neg
Iic x ∩ s ⊆ Iic y ∩ s
      
α: Type u_1

β: Type u_2

inst✝¹: LinearOrder α

inst✝: ConditionallyCompleteLinearOrder β

f: α → β

s: Set α

a✝, b: α

h: MonotoneOn f s

hu: BddAbove (f '' s)

a: β

ha: a ∈ lowerBounds (f '' s)

hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

g:= fun x => if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s)): α → β

hgs: EqOn f g s

x, y: α

hxy: x ≤ y

hx: ¬Disjoint (Iic x) s

hy: ¬Disjoint (Iic y) s

neg
sSup (f '' (Iic x ∩ s)) ≤ sSup (f '' (Iic y ∩ s))exact 
inter_subset_inter_left: ∀ {α : Type ?u.6560} {s t : Set α} (u : Set α), s ⊆ t → s ∩ u ⊆ t ∩ u
inter_subset_inter_left 
_: Set ?m.6561
_ (
Iic_subset_Iic: ∀ {α : Type ?u.6574} [inst : Preorder α] {a b : α}, Iic a ⊆ Iic b ↔ a ≤ b
Iic_subset_Iic.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 
hxy: ?m.1714
hxy)
Goals accomplished! 🐙
#align monotone_on.exists_monotone_extension 
MonotoneOn.exists_monotone_extension: ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β] {f : α → β}
  {s : Set α}, MonotoneOn f s → BddBelow (f '' s) → BddAbove (f '' s) → ∃ g, Monotone g ∧ EqOn f g s
MonotoneOn.exists_monotone_extension

/-- If a function is antitone and is bounded on a set `s`, then it admits an antitone extension to
the whole space. -/
theorem 
AntitoneOn.exists_antitone_extension: ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β] {f : α → β}
  {s : Set α}, AntitoneOn f s → BddBelow (f '' s) → BddAbove (f '' s) → ∃ g, Antitone g ∧ EqOn f g s
AntitoneOn.exists_antitone_extension (
h: AntitoneOn f s
h : 
AntitoneOn: {α : Type ?u.6669} → {β : Type ?u.6668} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Set α → Prop
AntitoneOn 
f: α → β
f 
s: Set α
s) (
hl: BddBelow (f '' s)
hl : 
BddBelow: {α : Type ?u.6956} → [inst : Preorder α] → Set α → Prop
BddBelow (
f: α → β
f '' 
s: Set α
s))
    (
hu: BddAbove (f '' s)
hu : 
BddAbove: {α : Type ?u.6988} → [inst : Preorder α] → Set α → Prop
BddAbove (
f: α → β
f '' 
s: Set α
s)) : ∃ 
g: α → β
g : 
α: Type ?u.6645
α → 
β: Type ?u.6648
β, 
Antitone: {α : Type ?u.7027} → {β : Type ?u.7026} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Antitone 
g: α → β
g ∧ 
EqOn: {α : Type ?u.7036} → {β : Type ?u.7035} → (α → β) → (α → β) → Set α → Prop
EqOn 
f: α → β
f 
g: α → β
g 
s: Set α
s :=
  
h: AntitoneOn f s
h.
dual_right: ∀ {α : Type ?u.7053} {β : Type ?u.7052} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  AntitoneOn f s → MonotoneOn (↑OrderDual.toDual ∘ f) s
dual_right.
exists_monotone_extension: ∀ {α : Type ?u.7315} {β : Type ?u.7316} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β] {f : α → β}
  {s : Set α}, MonotoneOn f s → BddBelow (f '' s) → BddAbove (f '' s) → ∃ g, Monotone g ∧ EqOn f g s
exists_monotone_extension 
hu: BddAbove (f '' s)
hu 
hl: BddBelow (f '' s)
hl
#align antitone_on.exists_antitone_extension 
AntitoneOn.exists_antitone_extension: ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β] {f : α → β}
  {s : Set α}, AntitoneOn f s → BddBelow (f '' s) → BddAbove (f '' s) → ∃ g, Antitone g ∧ EqOn f g s
AntitoneOn.exists_antitone_extension