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.
/-
Copyright (c) 2021 Yaël Dillies. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yaël Dillies
! This file was ported from Lean 3 source module order.monotone.monovary
! leanprover-community/mathlib commit 6cb77a8eaff0ddd100e87b1591c6d3ad319514ff
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Set.Image
/-!
# Monovariance of functions
Two functions *vary together* if a strict change in the first implies a change in the second.
This is in some sense a way to say that two functions `f : ι → α`, `g : ι → β` are "monotone
together", without actually having an order on `ι`.
This condition comes up in the rearrangement inequality. See `Algebra.Order.Rearrangement`.
## Main declarations
* `Monovary f g`: `f` monovaries with `g`. If `g i < g j`, then `f i ≤ f j`.
* `Antivary f g`: `f` antivaries with `g`. If `g i < g j`, then `f j ≤ f i`.
* `MonovaryOn f g s`: `f` monovaries with `g` on `s`.
* `MonovaryOn f g s`: `f` antivaries with `g` on `s`.
-/
open Function Set
variable {ι ι' α β γ : Type _: Type (?u.12668+1)
Monovary: (ι → α) → (ι → β) → Prop
Antivary: (ι → α) → (ι → β) → Prop
MonovaryOn: (ι → α) → (ι → β) → Set ι → Prop
AntivaryOn: (ι → α) → (ι → β) → Set ι → Prop
monovary_const_left: ∀ (g : ι → β) (a : α), Monovary (const ι a) g
const: {α : Sort ?u.2358} → (β : Sort ?u.2357) → α → β → α
const: {α : Sort ?u.2520} → (β : Sort ?u.2519) → α → β → α
const: {α : Sort ?u.2685} → (β : Sort ?u.2684) → α → β → α
rfl: ∀ {α : Sort ?u.2733} {a : α}, a = a
antivary_const_right: ∀ (f : ι → α) (b : β), Antivary f (const ι b)
const: {α : Sort ?u.2848} → (β : Sort ?u.2847) → α → β → α
rfl: ∀ {α : Sort ?u.2896} {a : α}, a = a
le_of_lt: ∀ {α : Type ?u.3024} [inst : Preorder α] {a b : α}, a < b → a ≤ b
le_of_lt: ∀ {α : Type ?u.3173} [inst : Preorder α] {a b : α}, a < b → a ≤ b
ne_of_apply_ne: ∀ {α : Sort ?u.3332} {β : Sort ?u.3333} (f : α → β) {x y : α}, f x ≠ f y → x ≠ y
ne_of_apply_ne: ∀ {α : Sort ?u.3540} {β : Sort ?u.3541} (f : α → β) {x y : α}, f x ≠ f y → x ≠ y
ne_of_apply_ne: ∀ {α : Sort ?u.3761} {β : Sort ?u.3762} (f : α → β) {x y : α}, f x ≠ f y → x ≠ y
ne_of_apply_ne: ∀ {α : Sort ?u.3987} {β : Sort ?u.3988} (f : α → β) {x y : α}, f x ≠ f y → x ≠ y
const: {α : Sort ?u.4169} → (β : Sort ?u.4168) → α → β → α
const: {α : Sort ?u.4351} → (β : Sort ?u.4350) → α → β → α
const: {α : Sort ?u.4536} → (β : Sort ?u.4535) → α → β → α
rfl: ∀ {α : Sort ?u.4594} {a : α}, a = a
const: {α : Sort ?u.4717} → (β : Sort ?u.4716) → α → β → α
rfl: ∀ {α : Sort ?u.4775} {a : α}, a = a
toDual: {α : Type ?u.7807} → α ≃ αᵒᵈ
toDual: {α : Type ?u.7886} → α ≃ αᵒᵈ
swap: ∀ {α : Sort ?u.7977} {β : Sort ?u.7976} {φ : α → β → Sort ?u.7975},
(∀ (x : α) (y : β), φ x y) → ∀ (y : β) (x : α), φ x y
toDual: {α : Type ?u.8146} → α ≃ αᵒᵈ
toDual: {α : Type ?u.8225} → α ≃ αᵒᵈ
swap: ∀ {α : Sort ?u.8316} {β : Sort ?u.8315} {φ : α → β → Sort ?u.8314},
(∀ (x : α) (y : β), φ x y) → ∀ (y : β) (x : α), φ x y
toDual: {α : Type ?u.8485} → α ≃ αᵒᵈ
id: ∀ {α : Sort ?u.8569}, α → α
toDual: {α : Type ?u.8722} → α ≃ αᵒᵈ
id: ∀ {α : Sort ?u.8806}, α → α
toDual: {α : Type ?u.8962} → α ≃ αᵒᵈ
swap: ∀ {α : Sort ?u.9045} {β : Sort ?u.9044} {φ : α → β → Sort ?u.9043},
(∀ (x : α) (y : β), φ x y) → ∀ (y : β) (x : α), φ x y
toDual: {α : Type ?u.9215} → α ≃ αᵒᵈ
swap: ∀ {α : Sort ?u.9298} {β : Sort ?u.9297} {φ : α → β → Sort ?u.9296},
(∀ (x : α) (y : β), φ x y) → ∀ (y : β) (x : α), φ x y
toDual: {α : Type ?u.9467} → α ≃ αᵒᵈ
toDual: {α : Type ?u.9546} → α ≃ αᵒᵈ
swap₂: ∀ {ι₁ : Sort ?u.9640} {ι₂ : Sort ?u.9639} {κ₁ : ι₁ → Sort ?u.9638} {κ₂ : ι₂ → Sort ?u.9637}
{φ : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → Sort ?u.9636},
(∀ (i₁ : ι₁) (j₁ : κ₁ i₁) (i₂ : ι₂) (j₂ : κ₂ i₂), φ i₁ j₁ i₂ j₂) →
∀ (i₂ : ι₂) (j₂ : κ₂ i₂) (i₁ : ι₁) (j₁ : κ₁ i₁), φ i₁ j₁ i₂ j₂
toDual: {α : Type ?u.9834} → α ≃ αᵒᵈ
toDual: {α : Type ?u.9913} → α ≃ αᵒᵈ
swap₂: ∀ {ι₁ : Sort ?u.10007} {ι₂ : Sort ?u.10006} {κ₁ : ι₁ → Sort ?u.10005} {κ₂ : ι₂ → Sort ?u.10004}
{φ : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → Sort ?u.10003},
(∀ (i₁ : ι₁) (j₁ : κ₁ i₁) (i₂ : ι₂) (j₂ : κ₂ i₂), φ i₁ j₁ i₂ j₂) →
∀ (i₂ : ι₂) (j₂ : κ₂ i₂) (i₁ : ι₁) (j₁ : κ₁ i₁), φ i₁ j₁ i₂ j₂
toDual: {α : Type ?u.10201} → α ≃ αᵒᵈ
id: ∀ {α : Sort ?u.10286}, α → α
toDual: {α : Type ?u.10446} → α ≃ αᵒᵈ
id: ∀ {α : Sort ?u.10531}, α → α
toDual: {α : Type ?u.10694} → α ≃ αᵒᵈ
swap₂: ∀ {ι₁ : Sort ?u.10780} {ι₂ : Sort ?u.10779} {κ₁ : ι₁ → Sort ?u.10778} {κ₂ : ι₂ → Sort ?u.10777}
{φ : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → Sort ?u.10776},
(∀ (i₁ : ι₁) (j₁ : κ₁ i₁) (i₂ : ι₂) (j₂ : κ₂ i₂), φ i₁ j₁ i₂ j₂) →
∀ (i₂ : ι₂) (j₂ : κ₂ i₂) (i₁ : ι₁) (j₁ : κ₁ i₁), φ i₁ j₁ i₂ j₂
toDual: {α : Type ?u.10975} → α ≃ αᵒᵈ
swap₂: ∀ {ι₁ : Sort ?u.11061} {ι₂ : Sort ?u.11060} {κ₁ : ι₁ → Sort ?u.11059} {κ₂ : ι₂ → Sort ?u.11058}
{φ : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → Sort ?u.11057},
(∀ (i₁ : ι₁) (j₁ : κ₁ i₁) (i₂ : ι₂) (j₂ : κ₂ i₂), φ i₁ j₁ i₂ j₂) →
∀ (i₂ : ι₂) (j₂ : κ₂ i₂) (i₁ : ι₁) (j₁ : κ₁ i₁), φ i₁ j₁ i₂ j₂
toDual: {α : Type ?u.11183} → α ≃ αᵒᵈ
Iff.rfl: ∀ {a : Prop}, a ↔ a
toDual: {α : Type ?u.11428} → α ≃ αᵒᵈ
forall_swap: ∀ {α : Sort ?u.11530} {β : Sort ?u.11531} {p : α → β → Prop}, (∀ (x : α) (y : β), p x y) ↔ ∀ (y : β) (x : α), p x y
toDual: {α : Type ?u.11681} → α ≃ αᵒᵈ
Iff.rfl: ∀ {a : Prop}, a ↔ a
toDual: {α : Type ?u.11926} → α ≃ αᵒᵈ
forall_swap: ∀ {α : Sort ?u.12028} {β : Sort ?u.12029} {p : α → β → Prop}, (∀ (x : α) (y : β), p x y) ↔ ∀ (y : β) (x : α), p x y
toDual: {α : Type ?u.12179} → α ≃ αᵒᵈ
Iff.rfl: ∀ {a : Prop}, a ↔ a
toDual: {α : Type ?u.12437} → α ≃ αᵒᵈ
forall₂_swap: ∀ {ι₁ : Sort ?u.12542} {ι₂ : Sort ?u.12543} {κ₁ : ι₁ → Sort ?u.12544} {κ₂ : ι₂ → Sort ?u.12545}
{p : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → Prop},
(∀ (i₁ : ι₁) (j₁ : κ₁ i₁) (i₂ : ι₂) (j₂ : κ₂ i₂), p i₁ j₁ i₂ j₂) ↔ ∀ (i₂ : ι₂) (j₂ : κ₂ i₂) (i₁ : ι₁) (j₁ : κ₁ i₁), p i₁ j₁ i₂ j₂
toDual: {α : Type ?u.12721} → α ≃ αᵒᵈ
Iff.rfl: ∀ {a : Prop}, a ↔ a
toDual: {α : Type ?u.12979} → α ≃ αᵒᵈ
forall₂_swap: ∀ {ι₁ : Sort ?u.13084} {ι₂ : Sort ?u.13085} {κ₁ : ι₁ → Sort ?u.13086} {κ₂ : ι₂ → Sort ?u.13087}
{p : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → Prop},
(∀ (i₁ : ι₁) (j₁ : κ₁ i₁) (i₂ : ι₂) (j₂ : κ₂ i₂), p i₁ j₁ i₂ j₂) ↔ ∀ (i₂ : ι₂) (j₂ : κ₂ i₂) (i₁ : ι₁) (j₁ : κ₁ i₁), p i₁ j₁ i₂ j₂
PartialOrder: Type ?u.13502 → Type ?u.13502
id: {α : Sort ?u.13310} → α → α
symm: ∀ {a b : Prop}, (a ↔ b) → (b ↔ a)
id: {α : Sort ?u.13516} → α → α
symm: ∀ {a b : Prop}, (a ↔ b) → (b ↔ a)
id: {α : Sort ?u.13722} → α → α
symm: ∀ {a b : Prop}, (a ↔ b) → (b ↔ a)
id: {α : Sort ?u.13954} → α → α
symm: ∀ {a b : Prop}, (a ↔ b) → (b ↔ a)
LinearOrder: Type ?u.16213 → Type ?u.16213
le: ∀ {α : Type ?u.14478} [inst : Preorder α] {a b : α}, a < b → a ≤ b
le: ∀ {α : Type ?u.16487} [inst : Preorder α] {a b : α}, a < b → a ≤ b
LinearOrder: Type ?u.18288 → Type ?u.18288
mem_image_of_mem: ∀ {α : Type ?u.18660} {β : Type ?u.18661} (f : α → β) {x : α} {a : Set α}, x ∈ a → f x ∈ f '' a
mem_image_of_mem: ∀ {α : Type ?u.18681} {β : Type ?u.18682} (f : α → β) {x : α} {a : Set α}, x ∈ a → f x ∈ f '' a
mem_image_of_mem: ∀ {α : Type ?u.19069} {β : Type ?u.19070} (f : α → β) {x : α} {a : Set α}, x ∈ a → f x ∈ f '' a
mem_image_of_mem: ∀ {α : Type ?u.19090} {β : Type ?u.19091} (f : α → β) {x : α} {a : Set α}, x ∈ a → f x ∈ f '' a
mem_image_of_mem: ∀ {α : Type ?u.19478} {β : Type ?u.19479} (f : α → β) {x : α} {a : Set α}, x ∈ a → f x ∈ f '' a
mem_image_of_mem: ∀ {α : Type ?u.19499} {β : Type ?u.19500} (f : α → β) {x : α} {a : Set α}, x ∈ a → f x ∈ f '' a