Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: 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.8LinearOrder α: Type ?u.2α] [ConditionallyCompleteLinearOrder: Type ?u.11 → Type ?u.11ConditionallyCompleteLinearOrder β: Type ?u.28β] {f: α → βf : α: Type ?u.2α → β: Type ?u.5β} {s: Set αs : Set: Type ?u.18 → Type ?u.18Set α: 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 sMonotoneOn.exists_monotone_extension (h: MonotoneOn f sh : MonotoneOn: {α : Type ?u.49} → {β : Type ?u.48} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Set α → PropMonotoneOn f: α → βf s: Set αs) (hl: BddBelow (f '' s)hl : BddBelow: {α : Type ?u.336} → [inst : Preorder α] → Set α → PropBddBelow (f: α → βf '' s: Set αs))
(hu: BddAbove (f '' s)hu : BddAbove: {α : Type ?u.368} → [inst : Preorder α] → Set α → PropBddAbove (f: α → βf '' s: Set αs)) : ∃ g: α → βg : α: Type ?u.25α → β: Type ?u.28β, Monotone: {α : Type ?u.407} → {β : Type ?u.406} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropMonotone g: α → βg ∧ EqOn: {α : Type ?u.416} → {β : Type ?u.415} → (α → β) → (α → β) → Set α → PropEqOn f: α → βf g: α → βg s: Set αs := byGoals accomplished! 🐙
α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa, b: αh: MonotoneOn f shl: 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_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa, b: αh: MonotoneOn f shl: 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_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: BddAbove (f '' s)a: βha: a ∈ lowerBounds (f '' s)intro∃ g, Monotone g ∧ EqOn f g s
α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa, b: αh: MonotoneOn f shl: BddBelow (f '' s)hu: BddAbove (f '' s)∃ g, Monotone g ∧ EqOn f g shave hu': ∀ (x : α), BddAbove (f '' (Iic x ∩ s))hu' : ∀ x: ?m.469x, BddAbove: {α : Type ?u.472} → [inst : Preorder α] → Set α → PropBddAbove (f: α → βf '' (Iic: {α : Type ?u.507} → [inst : Preorder α] → α → Set αIic x: ?m.469x ∩ s: Set αs)) := fun x: ?m.782x =>
hu: BddAbove (f '' s)hu.mono: ∀ {α : Type ?u.784} [inst : Preorder α] ⦃s t : Set α⦄, s ⊆ t → BddAbove t → BddAbove smono (image_subset: ∀ {α : Type ?u.814} {β : Type ?u.815} {a b : Set α} (f : α → β), a ⊆ b → f '' a ⊆ f '' bimage_subset _: ?m.816 → ?m.817_ (inter_subset_right: ∀ {α : Type ?u.835} (s t : Set α), s ∩ t ⊆ tinter_subset_right _: Set ?m.836_ _: Set ?m.836_))α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa, b: αh: MonotoneOn f shl: 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.862x => if Disjoint: {α : Type ?u.864} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → PropDisjoint (Iic: {α : Type ?u.868} → [inst : Preorder α] → α → Set αIic x: ?m.862x) 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.862x ∩ s: Set αs))α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa, b: αh: MonotoneOn f shl: BddBelow (f '' s)hu: BddAbove (f '' s)∃ g, Monotone g ∧ EqOn f g shave hgs: EqOn f g shgs : EqOn: {α : Type ?u.1042} → {β : Type ?u.1041} → (α → β) → (α → β) → Set α → PropEqOn f: α → βf g: α → βg s: Set αs := α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 sbyGoals accomplished! 🐙
α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 ∈ shxα: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 ∈ sf x = g x
α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 ∈ sf x = if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 α → α → PropIsGreatest (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 aright_mem_Iic, hx: x ∈ shx⟩, fun y: ?m.1530y hy: ?m.1533hy => hy: ?m.1533hy.1: ∀ {a b : Prop}, a ∧ b → a1⟩α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 ∈ sthis: IsGreatest (Iic x ∩ s) xf x = if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 ∈ sthis: IsGreatest (Iic x ∩ s) xf 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) = eif_neg this: IsGreatest (Iic x ∩ s) xthis.nonempty: ∀ {α : Type ?u.1548} [inst : Preorder α] {s : Set α} {a : α}, IsGreatest s a → Set.Nonempty snonempty.not_disjoint: ∀ {α : Type ?u.1558} {s t : Set α}, Set.Nonempty (s ∩ t) → ¬Disjoint s tnot_disjoint,α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 ∈ sthis: IsGreatest (Iic x ∩ s) xf x = sSup (f '' (Iic x ∩ s))
α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 ∈ sthis: IsGreatest (Iic x ∩ s) xf x = if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))((h: MonotoneOn f sh.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 ⊆ tinter_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) xthis).csSup_eq: ∀ {α : Type ?u.1648} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α}, IsGreatest s a → sSup s = acsSup_eqα: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 ∈ sthis: IsGreatest (Iic x ∩ s) xf x = f x]Goals accomplished! 🐙
α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa, b: αh: MonotoneOn f shl: BddBelow (f '' s)hu: BddAbove (f '' s)∃ g, Monotone g ∧ EqOn f g srefine' ⟨g: α → βg, fun x: ?m.1708x y: ?m.1711y hxy: ?m.1714hxy => _: g x ≤ g y_, hgs: EqOn f g shgs⟩α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 sx, y: αhxy: x ≤ yintrog x ≤ g y
α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa, b: αh: MonotoneOn f shl: BddBelow (f '' s)hu: BddAbove (f '' s)∃ g, Monotone g ∧ EqOn f g sby_cases hx: ?m.1996hx : Disjoint: {α : Type ?u.1729} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → PropDisjoint (Iic: {α : Type ?u.1733} → [inst : Preorder α] → α → Set αIic x: ?m.1708x) s: Set αsα: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 sx, y: αhxy: x ≤ yhx: Disjoint (Iic x) sposg x ≤ g yα: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 sx, y: αhxy: x ≤ yhx: ¬Disjoint (Iic x) snegg x ≤ g y α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 sx, y: αhxy: x ≤ yintrog x ≤ g y<;>α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 sx, y: αhxy: x ≤ yhx: Disjoint (Iic x) sposg x ≤ g yα: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 sx, y: αhxy: x ≤ yhx: ¬Disjoint (Iic x) snegg x ≤ g y α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 sx, y: αhxy: x ≤ yintrog x ≤ g yby_cases hy: ?m.2565hy : Disjoint: {α : Type ?u.2291} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → PropDisjoint (Iic: {α : Type ?u.2295} → [inst : Preorder α] → α → Set αIic y: ?m.1711y) s: Set αsα: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 sx, y: αhxy: x ≤ yhx: ¬Disjoint (Iic x) shy: Disjoint (Iic y) sposg x ≤ g yα: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 sx, y: αhxy: x ≤ yhx: ¬Disjoint (Iic x) shy: ¬Disjoint (Iic y) snegg x ≤ g y α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 sx, y: αhxy: x ≤ yintrog x ≤ g y<;>α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 sx, y: αhxy: x ≤ yhx: Disjoint (Iic x) shy: Disjoint (Iic y) sposg x ≤ g yα: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 sx, y: αhxy: x ≤ yhx: Disjoint (Iic x) shy: ¬Disjoint (Iic y) snegg x ≤ g yα: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 sx, y: αhxy: x ≤ yhx: ¬Disjoint (Iic x) shy: Disjoint (Iic y) sposg x ≤ g yα: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 sx, y: αhxy: x ≤ yhx: ¬Disjoint (Iic x) shy: ¬Disjoint (Iic y) snegg x ≤ g y
α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 sx, y: αhxy: x ≤ yintrog x ≤ g ysimp only [if_pos: ∀ {c : Prop} {h : Decidable c}, c → ∀ {α : Sort ?u.4378} {t e : α}, (if c then t else e) = tif_pos, if_neg: ∀ {c : Prop} {h : Decidable c}, ¬c → ∀ {α : Sort ?u.4392} {t e : α}, (if c then t else e) = eif_neg, not_false_iff: ¬False ↔ Truenot_false_iff, *, refl: ∀ {α : Type ?u.5150} {r : α → α → Prop} [inst : IsRefl α r] (a : α), r a arefl]α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 sx, y: αhxy: x ≤ yhx: ¬Disjoint (Iic x) shy: Disjoint (Iic y) spossSup (f '' (Iic x ∩ s)) ≤ a
α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa, b: αh: MonotoneOn f shl: BddBelow (f '' s)hu: BddAbove (f '' s)∃ g, Monotone g ∧ EqOn f g s·α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 sx, y: αhxy: x ≤ yhx: Disjoint (Iic x) shy: ¬Disjoint (Iic y) snega ≤ sSup (f '' (Iic y ∩ s)) α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 sx, y: αhxy: x ≤ yhx: Disjoint (Iic x) shy: ¬Disjoint (Iic y) snega ≤ sSup (f '' (Iic y ∩ s))α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 sx, y: αhxy: x ≤ yhx: ¬Disjoint (Iic x) shy: Disjoint (Iic y) spossSup (f '' (Iic x ∩ s)) ≤ aα: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 sx, y: αhxy: x ≤ yhx: ¬Disjoint (Iic x) shy: ¬Disjoint (Iic y) snegsSup (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 → b1 hy: ?m.2284hy with ⟨z, hz⟩: Set.Nonempty (Iic y ∩ s)⟨z: αz⟨z, hz⟩: Set.Nonempty (Iic y ∩ s), hz: z ∈ Iic y ∩ shz⟨z, hz⟩: Set.Nonempty (Iic y ∩ s)⟩α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 sx, y: αhxy: x ≤ yhx: Disjoint (Iic x) shy: ¬Disjoint (Iic y) sz: αhz: z ∈ Iic y ∩ sneg.introa ≤ sSup (f '' (Iic y ∩ s))
α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 sx, y: αhxy: x ≤ yhx: Disjoint (Iic x) shy: ¬Disjoint (Iic y) snega ≤ 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 sle_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 '' amem_image_of_mem _: ?m.6051 → ?m.6052_ hz: z ∈ Iic y ∩ shz) (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 '' amem_image_of_mem _: ?m.6071 → ?m.6072_ hz: z ∈ Iic y ∩ shz.2: ∀ {a b : Prop}, a ∧ b → b2)Goals accomplished! 🐙
α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa, b: αh: MonotoneOn f shl: BddBelow (f '' s)hu: BddAbove (f '' s)∃ g, Monotone g ∧ EqOn f g s·α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 sx, y: αhxy: x ≤ yhx: ¬Disjoint (Iic x) shy: Disjoint (Iic y) spossSup (f '' (Iic x ∩ s)) ≤ a α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 sx, y: αhxy: x ≤ yhx: ¬Disjoint (Iic x) shy: Disjoint (Iic y) spossSup (f '' (Iic x ∩ s)) ≤ aα: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 sx, y: αhxy: x ≤ yhx: ¬Disjoint (Iic x) shy: ¬Disjoint (Iic y) snegsSup (f '' (Iic x ∩ s)) ≤ sSup (f '' (Iic y ∩ s))exact (hx: ?m.2003hx <| hy: ?m.2558hy.mono_left: ∀ {α : Type ?u.6081} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b c : α}, a ≤ b → Disjoint b c → Disjoint a cmono_left <| Iic_subset_Iic: ∀ {α : Type ?u.6141} [inst : Preorder α] {a b : α}, Iic a ⊆ Iic b ↔ a ≤ bIic_subset_Iic.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 hxy: ?m.1714hxy).elim: ∀ {C : Sort ?u.6251}, False → CelimGoals accomplished! 🐙
α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa, b: αh: MonotoneOn f shl: BddBelow (f '' s)hu: BddAbove (f '' s)∃ g, Monotone g ∧ EqOn f g s·α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 sx, y: αhxy: x ≤ yhx: ¬Disjoint (Iic x) shy: ¬Disjoint (Iic y) snegsSup (f '' (Iic x ∩ s)) ≤ sSup (f '' (Iic y ∩ s)) α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 sx, y: αhxy: x ≤ yhx: ¬Disjoint (Iic x) shy: ¬Disjoint (Iic y) snegsSup (f '' (Iic x ∩ s)) ≤ sSup (f '' (Iic y ∩ s))rw [α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 sx, y: αhxy: x ≤ yhx: ¬Disjoint (Iic x) shy: ¬Disjoint (Iic y) snegsSup (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_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 sx, y: αhxy: x ≤ yhx: Set.Nonempty (Iic x ∩ s)hy: Set.Nonempty (Iic y ∩ s)negsSup (f '' (Iic x ∩ s)) ≤ sSup (f '' (Iic y ∩ s))]α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 sx, y: αhxy: x ≤ yhx: Set.Nonempty (Iic x ∩ s)hy: Set.Nonempty (Iic y ∩ s)negsSup (f '' (Iic x ∩ s)) ≤ sSup (f '' (Iic y ∩ s)) at hx: ?m.2003hx hy: ¬Disjoint (Iic y) shyα: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 sx, y: αhxy: x ≤ yhx: Set.Nonempty (Iic x ∩ s)hy: Set.Nonempty (Iic y ∩ s)negsSup (f '' (Iic x ∩ s)) ≤ sSup (f '' (Iic y ∩ s))
α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 sx, y: αhxy: x ≤ yhx: ¬Disjoint (Iic x) shy: ¬Disjoint (Iic y) snegsSup (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 tcsSup_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 '' bimage_subset _: ?m.6548 → ?m.6549_ _: ?m.6550 ⊆ ?m.6551_)α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 sx, y: αhxy: x ≤ yhx: Set.Nonempty (Iic x ∩ s)hy: Set.Nonempty (Iic y ∩ s)negIic x ∩ s ⊆ Iic y ∩ s
α: Type u_1β: Type u_2inst✝¹: LinearOrder αinst✝: ConditionallyCompleteLinearOrder βf: α → βs: Set αa✝, b: αh: MonotoneOn f shu: 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 sx, y: αhxy: x ≤ yhx: ¬Disjoint (Iic x) shy: ¬Disjoint (Iic y) snegsSup (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 ∩ uinter_subset_inter_left _: Set ?m.6561_ (Iic_subset_Iic: ∀ {α : Type ?u.6574} [inst : Preorder α] {a b : α}, Iic a ⊆ Iic b ↔ a ≤ bIic_subset_Iic.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 hxy: ?m.1714hxy)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 sMonotoneOn.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 sAntitoneOn.exists_antitone_extension (h: AntitoneOn f sh : AntitoneOn: {α : Type ?u.6669} → {β : Type ?u.6668} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Set α → PropAntitoneOn f: α → βf s: Set αs) (hl: BddBelow (f '' s)hl : BddBelow: {α : Type ?u.6956} → [inst : Preorder α] → Set α → PropBddBelow (f: α → βf '' s: Set αs))
(hu: BddAbove (f '' s)hu : BddAbove: {α : Type ?u.6988} → [inst : Preorder α] → Set α → PropBddAbove (f: α → βf '' s: Set αs)) : ∃ g: α → βg : α: Type ?u.6645α → β: Type ?u.6648β, Antitone: {α : Type ?u.7027} → {β : Type ?u.7026} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropAntitone g: α → βg ∧ EqOn: {α : Type ?u.7036} → {β : Type ?u.7035} → (α → β) → (α → β) → Set α → PropEqOn f: α → βf g: α → βg s: Set αs :=
h: AntitoneOn f sh.dual_right: ∀ {α : Type ?u.7053} {β : Type ?u.7052} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
AntitoneOn f s → MonotoneOn (↑OrderDual.toDual ∘ f) sdual_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 sexists_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 sAntitoneOn.exists_antitone_extension
```