Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(order/monotone): Functions from/to subsingletons are monotone #10903

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - feat(order/monotone): Functions from/to subsingletons are monotone #10903

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
36 changes: 29 additions & 7 deletions src/order/monotone.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -98,7 +98,7 @@ def strict_anti_on (f : α → β) (s : set α) : Prop :=

end monotone_def

/-! #### Monotonicity on the dual order
/-! ### Monotonicity on the dual order

Strictly many of the `*_on.dual` lemmas in this section should use `of_dual ⁻¹' s` instead of `s`,
but right now this is not possible as `set.preimage` is not defined yet, and importing it creates
Expand Down Expand Up @@ -189,7 +189,7 @@ protected lemma strict_anti_on.dual_right (hf : strict_anti_on f s) :

end order_dual

/-! #### Monotonicity in function spaces -/
/-! ### Monotonicity in function spaces -/

section preorder
variables [preorder α]
Expand Down Expand Up @@ -219,7 +219,7 @@ lemma function.monotone_eval {ι : Type u} {α : ι → Type v} [∀ i, preorder
monotone (function.eval i : (Π i, α i) → α i) :=
λ f g H, H i

/-! #### Monotonicity hierarchy -/
/-! ### Monotonicity hierarchy -/

section preorder
variables [preorder α]
Expand Down Expand Up @@ -284,7 +284,29 @@ hf.dual_right.monotone.dual_right

end partial_order

/-! #### Miscellaneous monotonicity results -/
/-! ### Monotonicity from and to subsingletons -/

namespace subsingleton
variables [preorder α] [preorder β]

protected lemma monotone [subsingleton α] (f : α → β) : monotone f :=
λ a b _, (congr_arg _ $ subsingleton.elim _ _).le

protected lemma antitone [subsingleton α] (f : α → β) : antitone f :=
λ a b _, (congr_arg _ $ subsingleton.elim _ _).le

lemma monotone' [subsingleton β] (f : α → β) : monotone f := λ a b _, (subsingleton.elim _ _).le
lemma antitone' [subsingleton β] (f : α → β) : antitone f := λ a b _, (subsingleton.elim _ _).le

protected lemma strict_mono [subsingleton α] (f : α → β) : strict_mono f :=
λ a b h, (h.ne $ subsingleton.elim _ _).elim

protected lemma strict_anti [subsingleton α] (f : α → β) : strict_anti f :=
λ a b h, (h.ne $ subsingleton.elim _ _).elim

end subsingleton

/-! ### Miscellaneous monotonicity results -/

lemma monotone_id [preorder α] : monotone (id : α → α) := λ a b, id

Expand Down Expand Up @@ -348,7 +370,7 @@ hf.ite' hg hp $ λ x y hx hy h, (hfg y).trans_lt (hf h)

end preorder

/-! #### Monotonicity under composition -/
/-! ### Monotonicity under composition -/

section composition
variables [preorder α] [preorder β] [preorder γ] {g : β → γ} {f : α → β} {s : set α}
Expand Down Expand Up @@ -426,7 +448,7 @@ lemma strict_anti.comp_strict_mono_on (hg : strict_anti g) (hf : strict_mono_on

end composition

/-! #### Monotonicity in linear orders -/
/-! ### Monotonicity in linear orders -/

section linear_order
variables [linear_order α]
Expand Down Expand Up @@ -534,7 +556,7 @@ lemma antitone.strict_anti_iff_injective (hf : antitone f) :
end partial_order
end linear_order

/-! #### Monotonicity in `ℕ` and `ℤ` -/
/-! ### Monotonicity in `ℕ` and `ℤ` -/

section preorder
variables [preorder α]
Expand Down