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: Yaël Dillies

! This file was ported from Lean 3 source module order.monotone.monovary
! 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 ?u.2ι ι': Type ?u.5ι' α: Type ?u.8835α β: Type ?u.11β γ: Type ?u.14γ : Type _: Type (?u.12668+1)Type _}

section Preorder

variable [Preorder: Type ?u.5032 → Type ?u.5032Preorder α: Type ?u.6429α] [Preorder: Type ?u.6930 → Type ?u.6930Preorder β: Type ?u.6921β] [Preorder: Type ?u.3082 → Type ?u.3082Preorder γ: Type ?u.5485γ] {f: ι → αf : ι: Type ?u.10069ι → α: Type ?u.69α} {f': α → γf' : α: Type ?u.23α → γ: Type ?u.29γ} {g: ι → βg : ι: Type ?u.63ι → β: Type ?u.6921β} {g': β → γg' : β: Type ?u.6921β → γ: Type ?u.29γ}
{s: Set ιs t: Set ιt : Set: Type ?u.6232 → Type ?u.6232Set ι: Type ?u.17ι}

/-- `f` monovaries with `g` if `g i < g j` implies `f i ≤ f j`. -/
def Monovary: (ι → α) → (ι → β) → PropMonovary (f: ι → αf : ι: Type ?u.63ι → α: Type ?u.69α) (g: ι → βg : ι: Type ?u.63ι → β: Type ?u.72β) : Prop: TypeProp :=
∀ ⦃i: ?m.121i j: ?m.124j⦄, g: ι → βg i: ?m.121i < g: ι → βg j: ?m.124j → f: ι → αf i: ?m.121i ≤ f: ι → αf j: ?m.124j
#align monovary Monovary: {ι : Type u_1} → {α : Type u_2} → {β : Type u_3} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropMonovary

/-- `f` antivaries with `g` if `g i < g j` implies `f j ≤ f i`. -/
def Antivary: (ι → α) → (ι → β) → PropAntivary (f: ι → αf : ι: Type ?u.183ι → α: Type ?u.189α) (g: ι → βg : ι: Type ?u.183ι → β: Type ?u.192β) : Prop: TypeProp :=
∀ ⦃i: ?m.241i j: ?m.244j⦄, g: ι → βg i: ?m.241i < g: ι → βg j: ?m.244j → f: ι → αf j: ?m.244j ≤ f: ι → αf i: ?m.241i
#align antivary Antivary: {ι : Type u_1} → {α : Type u_2} → {β : Type u_3} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropAntivary

/-- `f` monovaries with `g` on `s` if `g i < g j` implies `f i ≤ f j` for all `i, j ∈ s`. -/
def MonovaryOn: (ι → α) → (ι → β) → Set ι → PropMonovaryOn (f: ι → αf : ι: Type ?u.303ι → α: Type ?u.309α) (g: ι → βg : ι: Type ?u.303ι → β: Type ?u.312β) (s: Set ιs : Set: Type ?u.357 → Type ?u.357Set ι: Type ?u.303ι) : Prop: TypeProp :=
∀ ⦃i: ?m.365i⦄ (_: i ∈ s_ : i: ?m.365i ∈ s: Set ιs) ⦃j: ?m.397j⦄ (_: j ∈ s_ : j: ?m.397j ∈ s: Set ιs), g: ι → βg i: ?m.365i < g: ι → βg j: ?m.397j → f: ι → αf i: ?m.365i ≤ f: ι → αf j: ?m.397j
#align monovary_on MonovaryOn: {ι : Type u_1} →
{α : Type u_2} → {β : Type u_3} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropMonovaryOn

/-- `f` antivaries with `g` on `s` if `g i < g j` implies `f j ≤ f i` for all `i, j ∈ s`. -/
def AntivaryOn: (ι → α) → (ι → β) → Set ι → PropAntivaryOn (f: ι → αf : ι: Type ?u.490ι → α: Type ?u.496α) (g: ι → βg : ι: Type ?u.490ι → β: Type ?u.499β) (s: Set ιs : Set: Type ?u.544 → Type ?u.544Set ι: Type ?u.490ι) : Prop: TypeProp :=
∀ ⦃i: ?m.552i⦄ (_: i ∈ s_ : i: ?m.552i ∈ s: Set ιs) ⦃j: ?m.584j⦄ (_: j ∈ s_ : j: ?m.584j ∈ s: Set ιs), g: ι → βg i: ?m.552i < g: ι → βg j: ?m.584j → f: ι → αf j: ?m.584j ≤ f: ι → αf i: ?m.552i
#align antivary_on AntivaryOn: {ι : Type u_1} →
{α : Type u_2} → {β : Type u_3} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropAntivaryOn

protected theorem Monovary.monovaryOn: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
Monovary f g → ∀ (s : Set ι), MonovaryOn f g sMonovary.monovaryOn (h: Monovary f gh : Monovary: {ι : Type ?u.725} →
{α : Type ?u.724} → {β : Type ?u.723} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropMonovary f: ι → αf g: ι → βg) (s: Set ιs : Set: Type ?u.769 → Type ?u.769Set ι: Type ?u.677ι) : MonovaryOn: {ι : Type ?u.774} →
{α : Type ?u.773} → {β : Type ?u.772} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropMonovaryOn f: ι → αf g: ι → βg s: Set ιs :=
fun _: ?m.816_ _: ?m.819_ _: ?m.822_ _: ?m.825_ hij: ?m.828hij => h: Monovary f gh hij: ?m.828hij
#align monovary.monovary_on Monovary.monovaryOn: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
Monovary f g → ∀ (s : Set ι), MonovaryOn f g sMonovary.monovaryOn

protected theorem Antivary.antivaryOn: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
Antivary f g → ∀ (s : Set ι), AntivaryOn f g sAntivary.antivaryOn (h: Antivary f gh : Antivary: {ι : Type ?u.907} →
{α : Type ?u.906} → {β : Type ?u.905} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropAntivary f: ι → αf g: ι → βg) (s: Set ιs : Set: Type ?u.951 → Type ?u.951Set ι: Type ?u.859ι) : AntivaryOn: {ι : Type ?u.956} →
{α : Type ?u.955} → {β : Type ?u.954} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropAntivaryOn f: ι → αf g: ι → βg s: Set ιs :=
fun _: ?m.998_ _: ?m.1001_ _: ?m.1004_ _: ?m.1007_ hij: ?m.1010hij => h: Antivary f gh hij: ?m.1010hij
#align antivary.antivary_on Antivary.antivaryOn: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
Antivary f g → ∀ (s : Set ι), AntivaryOn f g sAntivary.antivaryOn

@[simp]
theorem MonovaryOn.empty: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
MonovaryOn f g ∅MonovaryOn.empty : MonovaryOn: {ι : Type ?u.1089} →
{α : Type ?u.1088} → {β : Type ?u.1087} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropMonovaryOn f: ι → αf g: ι → βg ∅: ?m.1124∅ := fun _: ?m.1177_ => False.elim: ∀ {C : Sort ?u.1179}, False → CFalse.elim
#align monovary_on.empty MonovaryOn.empty: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
MonovaryOn f g ∅MonovaryOn.empty

@[simp]
theorem AntivaryOn.empty: AntivaryOn f g ∅AntivaryOn.empty : AntivaryOn: {ι : Type ?u.1291} →
{α : Type ?u.1290} → {β : Type ?u.1289} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropAntivaryOn f: ι → αf g: ι → βg ∅: ?m.1326∅ := fun _: ?m.1379_ => False.elim: ∀ {C : Sort ?u.1381}, False → CFalse.elim
#align antivary_on.empty AntivaryOn.empty: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
AntivaryOn f g ∅AntivaryOn.empty

@[simp]
theorem monovaryOn_univ: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
MonovaryOn f g univ ↔ Monovary f gmonovaryOn_univ : MonovaryOn: {ι : Type ?u.1493} →
{α : Type ?u.1492} → {β : Type ?u.1491} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropMonovaryOn f: ι → αf g: ι → βg univ: {α : Type ?u.1505} → Set αuniv ↔ Monovary: {ι : Type ?u.1519} →
{α : Type ?u.1518} → {β : Type ?u.1517} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropMonovary f: ι → αf g: ι → βg :=
⟨fun h: ?m.1541h _: ?m.1544_ _: ?m.1547_ => h: ?m.1541h trivial: Truetrivial trivial: Truetrivial, fun h: ?m.1566h _: ?m.1569_ _: ?m.1572_ _: ?m.1575_ _: ?m.1578_ hij: ?m.1581hij => h: ?m.1566h hij: ?m.1581hij⟩
#align monovary_on_univ monovaryOn_univ: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
MonovaryOn f g univ ↔ Monovary f gmonovaryOn_univ

@[simp]
theorem antivaryOn_univ: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
AntivaryOn f g univ ↔ Antivary f gantivaryOn_univ : AntivaryOn: {ι : Type ?u.1701} →
{α : Type ?u.1700} → {β : Type ?u.1699} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropAntivaryOn f: ι → αf g: ι → βg univ: {α : Type ?u.1713} → Set αuniv ↔ Antivary: {ι : Type ?u.1727} →
{α : Type ?u.1726} → {β : Type ?u.1725} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropAntivary f: ι → αf g: ι → βg :=
⟨fun h: ?m.1749h _: ?m.1752_ _: ?m.1755_ => h: ?m.1749h trivial: Truetrivial trivial: Truetrivial, fun h: ?m.1774h _: ?m.1777_ _: ?m.1780_ _: ?m.1783_ _: ?m.1786_ hij: ?m.1789hij => h: ?m.1774h hij: ?m.1789hij⟩
#align antivary_on_univ antivaryOn_univ: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
AntivaryOn f g univ ↔ Antivary f gantivaryOn_univ

protected theorem MonovaryOn.subset: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
{s t : Set ι}, s ⊆ t → MonovaryOn f g t → MonovaryOn f g sMonovaryOn.subset (hst: s ⊆ thst : s: Set ιs ⊆ t: Set ιt) (h: MonovaryOn f g th : MonovaryOn: {ι : Type ?u.1928} →
{α : Type ?u.1927} → {β : Type ?u.1926} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropMonovaryOn f: ι → αf g: ι → βg t: Set ιt) : MonovaryOn: {ι : Type ?u.1975} →
{α : Type ?u.1974} → {β : Type ?u.1973} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropMonovaryOn f: ι → αf g: ι → βg s: Set ιs :=
fun _: ?m.2016_ hi: ?m.2019hi _: ?m.2022_ hj: ?m.2025hj => h: MonovaryOn f g th (hst: s ⊆ thst hi: ?m.2019hi) (hst: s ⊆ thst hj: ?m.2025hj)
#align monovary_on.subset MonovaryOn.subset: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
{s t : Set ι}, s ⊆ t → MonovaryOn f g t → MonovaryOn f g sMonovaryOn.subset

protected theorem AntivaryOn.subset: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
{s t : Set ι}, s ⊆ t → AntivaryOn f g t → AntivaryOn f g sAntivaryOn.subset (hst: s ⊆ thst : s: Set ιs ⊆ t: Set ιt) (h: AntivaryOn f g th : AntivaryOn: {ι : Type ?u.2135} →
{α : Type ?u.2134} → {β : Type ?u.2133} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropAntivaryOn f: ι → αf g: ι → βg t: Set ιt) : AntivaryOn: {ι : Type ?u.2182} →
{α : Type ?u.2181} → {β : Type ?u.2180} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropAntivaryOn f: ι → αf g: ι → βg s: Set ιs :=
fun _: ?m.2223_ hi: ?m.2226hi _: ?m.2229_ hj: ?m.2232hj => h: AntivaryOn f g th (hst: s ⊆ thst hi: ?m.2226hi) (hst: s ⊆ thst hj: ?m.2232hj)
#align antivary_on.subset AntivaryOn.subset: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
{s t : Set ι}, s ⊆ t → AntivaryOn f g t → AntivaryOn f g sAntivaryOn.subset

theorem monovary_const_left: ∀ (g : ι → β) (a : α), Monovary (const ι a) gmonovary_const_left (g: ι → βg : ι: Type ?u.2275ι → β: Type ?u.2284β) (a: αa : α: Type ?u.2281α) : Monovary: {ι : Type ?u.2329} →
{α : Type ?u.2328} → {β : Type ?u.2327} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropMonovary (const: {α : Sort ?u.2358} → (β : Sort ?u.2357) → α → β → αconst ι: Type ?u.2275ι a: αa) g: ι → βg := fun _: ?m.2382_ _: ?m.2385_ _: ?m.2388_ => le_rfl: ∀ {α : Type ?u.2390} [inst : Preorder α] {a : α}, a ≤ ale_rfl
#align monovary_const_left monovary_const_left: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (g : ι → β) (a : α),
Monovary (const ι a) gmonovary_const_left

theorem antivary_const_left: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (g : ι → β) (a : α),
Antivary (const ι a) gantivary_const_left (g: ι → βg : ι: Type ?u.2437ι → β: Type ?u.2446β) (a: αa : α: Type ?u.2443α) : Antivary: {ι : Type ?u.2491} →
{α : Type ?u.2490} → {β : Type ?u.2489} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropAntivary (const: {α : Sort ?u.2520} → (β : Sort ?u.2519) → α → β → αconst ι: Type ?u.2437ι a: αa) g: ι → βg := fun _: ?m.2544_ _: ?m.2547_ _: ?m.2550_ => le_rfl: ∀ {α : Type ?u.2552} [inst : Preorder α] {a : α}, a ≤ ale_rfl
#align antivary_const_left antivary_const_left: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (g : ι → β) (a : α),
Antivary (const ι a) gantivary_const_left

theorem monovary_const_right: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : ι → α) (b : β),
Monovary f (const ι b)monovary_const_right (f: ι → αf : ι: Type ?u.2599ι → α: Type ?u.2605α) (b: βb : β: Type ?u.2608β) : Monovary: {ι : Type ?u.2653} →
{α : Type ?u.2652} → {β : Type ?u.2651} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropMonovary f: ι → αf (const: {α : Sort ?u.2685} → (β : Sort ?u.2684) → α → β → αconst ι: Type ?u.2599ι b: βb) := fun _: ?m.2706_ _: ?m.2709_ h: ?m.2712h =>
(h: ?m.2712h.ne: ∀ {α : Type ?u.2714} [inst : Preorder α] {a b : α}, a < b → a ≠ bne rfl: ∀ {α : Sort ?u.2733} {a : α}, a = arfl).elim: ∀ {C : Sort ?u.2743}, False → Celim
#align monovary_const_right monovary_const_right: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : ι → α) (b : β),
Monovary f (const ι b)monovary_const_right

theorem antivary_const_right: ∀ (f : ι → α) (b : β), Antivary f (const ι b)antivary_const_right (f: ι → αf : ι: Type ?u.2762ι → α: Type ?u.2768α) (b: βb : β: Type ?u.2771β) : Antivary: {ι : Type ?u.2816} →
{α : Type ?u.2815} → {β : Type ?u.2814} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropAntivary f: ι → αf (const: {α : Sort ?u.2848} → (β : Sort ?u.2847) → α → β → αconst ι: Type ?u.2762ι b: βb) := fun _: ?m.2869_ _: ?m.2872_ h: ?m.2875h =>
(h: ?m.2875h.ne: ∀ {α : Type ?u.2877} [inst : Preorder α] {a b : α}, a < b → a ≠ bne rfl: ∀ {α : Sort ?u.2896} {a : α}, a = arfl).elim: ∀ {C : Sort ?u.2906}, False → Celim
#align antivary_const_right antivary_const_right: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : ι → α) (b : β),
Antivary f (const ι b)antivary_const_right

theorem monovary_self: ∀ {ι : Type u_1} {α : Type u_2} [inst : Preorder α] (f : ι → α), Monovary f fmonovary_self (f: ι → αf : ι: Type ?u.2925ι → α: Type ?u.2931α) : Monovary: {ι : Type ?u.2977} →
{α : Type ?u.2976} → {β : Type ?u.2975} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropMonovary f: ι → αf f: ι → αf := fun _: ?m.3019_ _: ?m.3022_ => le_of_lt: ∀ {α : Type ?u.3024} [inst : Preorder α] {a b : α}, a < b → a ≤ ble_of_lt
#align monovary_self monovary_self: ∀ {ι : Type u_1} {α : Type u_2} [inst : Preorder α] (f : ι → α), Monovary f fmonovary_self

theorem monovaryOn_self: ∀ (f : ι → α) (s : Set ι), MonovaryOn f f smonovaryOn_self (f: ι → αf : ι: Type ?u.3061ι → α: Type ?u.3067α) (s: Set ιs : Set: Type ?u.3111 → Type ?u.3111Set ι: Type ?u.3061ι) : MonovaryOn: {ι : Type ?u.3116} →
{α : Type ?u.3115} → {β : Type ?u.3114} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropMonovaryOn f: ι → αf f: ι → αf s: Set ιs := fun _: ?m.3162_ _: ?m.3165_ _: ?m.3168_ _: ?m.3171_ => le_of_lt: ∀ {α : Type ?u.3173} [inst : Preorder α] {a b : α}, a < b → a ≤ ble_of_lt
#align monovary_on_self monovaryOn_self: ∀ {ι : Type u_1} {α : Type u_2} [inst : Preorder α] (f : ι → α) (s : Set ι), MonovaryOn f f smonovaryOn_self

protected theorem Subsingleton.monovary: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Subsingleton ι]
(f : ι → α) (g : ι → β), Monovary f gSubsingleton.monovary [Subsingleton: Sort ?u.3261 → PropSubsingleton ι: Type ?u.3215ι] (f: ι → αf : ι: Type ?u.3215ι → α: Type ?u.3221α) (g: ι → βg : ι: Type ?u.3215ι → β: Type ?u.3224β) : Monovary: {ι : Type ?u.3274} →
{α : Type ?u.3273} → {β : Type ?u.3272} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropMonovary f: ι → αf g: ι → βg :=
fun _: ?m.3324_ _: ?m.3327_ h: ?m.3330h => (ne_of_apply_ne: ∀ {α : Sort ?u.3332} {β : Sort ?u.3333} (f : α → β) {x y : α}, f x ≠ f y → x ≠ yne_of_apply_ne _: ?m.3334 → ?m.3335_ h: ?m.3330h.ne: ∀ {α : Type ?u.3339} [inst : Preorder α] {a b : α}, a < b → a ≠ bne <| Subsingleton.elim: ∀ {α : Sort ?u.3367} [h : Subsingleton α] (a b : α), a = bSubsingleton.elim _: ?m.3368_ _: ?m.3368_).elim: ∀ {C : Sort ?u.3402}, False → Celim
#align subsingleton.monovary Subsingleton.monovary: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Subsingleton ι]
(f : ι → α) (g : ι → β), Monovary f gSubsingleton.monovary

protected theorem Subsingleton.antivary: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Subsingleton ι]
(f : ι → α) (g : ι → β), Antivary f gSubsingleton.antivary [Subsingleton: Sort ?u.3469 → PropSubsingleton ι: Type ?u.3423ι] (f: ι → αf : ι: Type ?u.3423ι → α: Type ?u.3429α) (g: ι → βg : ι: Type ?u.3423ι → β: Type ?u.3432β) : Antivary: {ι : Type ?u.3482} →
{α : Type ?u.3481} → {β : Type ?u.3480} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropAntivary f: ι → αf g: ι → βg :=
fun _: ?m.3532_ _: ?m.3535_ h: ?m.3538h => (ne_of_apply_ne: ∀ {α : Sort ?u.3540} {β : Sort ?u.3541} (f : α → β) {x y : α}, f x ≠ f y → x ≠ yne_of_apply_ne _: ?m.3542 → ?m.3543_ h: ?m.3538h.ne: ∀ {α : Type ?u.3547} [inst : Preorder α] {a b : α}, a < b → a ≠ bne <| Subsingleton.elim: ∀ {α : Sort ?u.3575} [h : Subsingleton α] (a b : α), a = bSubsingleton.elim _: ?m.3576_ _: ?m.3576_).elim: ∀ {C : Sort ?u.3610}, False → Celim
#align subsingleton.antivary Subsingleton.antivary: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Subsingleton ι]
(f : ι → α) (g : ι → β), Antivary f gSubsingleton.antivary

protected theorem Subsingleton.monovaryOn: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Subsingleton ι]
(f : ι → α) (g : ι → β) (s : Set ι), MonovaryOn f g sSubsingleton.monovaryOn [Subsingleton: Sort ?u.3677 → PropSubsingleton ι: Type ?u.3631ι] (f: ι → αf : ι: Type ?u.3631ι → α: Type ?u.3637α) (g: ι → βg : ι: Type ?u.3631ι → β: Type ?u.3640β) (s: Set ιs : Set: Type ?u.3688 → Type ?u.3688Set ι: Type ?u.3631ι) :
MonovaryOn: {ι : Type ?u.3693} →
{α : Type ?u.3692} → {β : Type ?u.3691} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropMonovaryOn f: ι → αf g: ι → βg s: Set ιs := fun _: ?m.3747_ _: ?m.3750_ _: ?m.3753_ _: ?m.3756_ h: ?m.3759h => (ne_of_apply_ne: ∀ {α : Sort ?u.3761} {β : Sort ?u.3762} (f : α → β) {x y : α}, f x ≠ f y → x ≠ yne_of_apply_ne _: ?m.3763 → ?m.3764_ h: ?m.3759h.ne: ∀ {α : Type ?u.3768} [inst : Preorder α] {a b : α}, a < b → a ≠ bne <| Subsingleton.elim: ∀ {α : Sort ?u.3796} [h : Subsingleton α] (a b : α), a = bSubsingleton.elim _: ?m.3797_ _: ?m.3797_).elim: ∀ {C : Sort ?u.3831}, False → Celim
#align subsingleton.monovary_on Subsingleton.monovaryOn: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Subsingleton ι]
(f : ι → α) (g : ι → β) (s : Set ι), MonovaryOn f g sSubsingleton.monovaryOn

protected theorem Subsingleton.antivaryOn: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Subsingleton ι]
(f : ι → α) (g : ι → β) (s : Set ι), AntivaryOn f g sSubsingleton.antivaryOn [Subsingleton: Sort ?u.3903 → PropSubsingleton ι: Type ?u.3857ι] (f: ι → αf : ι: Type ?u.3857ι → α: Type ?u.3863α) (g: ι → βg : ι: Type ?u.3857ι → β: Type ?u.3866β) (s: Set ιs : Set: Type ?u.3914 → Type ?u.3914Set ι: Type ?u.3857ι) :
AntivaryOn: {ι : Type ?u.3919} →
{α : Type ?u.3918} → {β : Type ?u.3917} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropAntivaryOn f: ι → αf g: ι → βg s: Set ιs := fun _: ?m.3973_ _: ?m.3976_ _: ?m.3979_ _: ?m.3982_ h: ?m.3985h => (ne_of_apply_ne: ∀ {α : Sort ?u.3987} {β : Sort ?u.3988} (f : α → β) {x y : α}, f x ≠ f y → x ≠ yne_of_apply_ne _: ?m.3989 → ?m.3990_ h: ?m.3985h.ne: ∀ {α : Type ?u.3994} [inst : Preorder α] {a b : α}, a < b → a ≠ bne <| Subsingleton.elim: ∀ {α : Sort ?u.4022} [h : Subsingleton α] (a b : α), a = bSubsingleton.elim _: ?m.4023_ _: ?m.4023_).elim: ∀ {C : Sort ?u.4057}, False → Celim
#align subsingleton.antivary_on Subsingleton.antivaryOn: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Subsingleton ι]
(f : ι → α) (g : ι → β) (s : Set ι), AntivaryOn f g sSubsingleton.antivaryOn

theorem monovaryOn_const_left: ∀ (g : ι → β) (a : α) (s : Set ι), MonovaryOn (const ι a) g smonovaryOn_const_left (g: ι → βg : ι: Type ?u.4083ι → β: Type ?u.4092β) (a: αa : α: Type ?u.4089α) (s: Set ιs : Set: Type ?u.4135 → Type ?u.4135Set ι: Type ?u.4083ι) : MonovaryOn: {ι : Type ?u.4140} →
{α : Type ?u.4139} → {β : Type ?u.4138} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropMonovaryOn (const: {α : Sort ?u.4169} → (β : Sort ?u.4168) → α → β → αconst ι: Type ?u.4083ι a: αa) g: ι → βg s: Set ιs :=
fun _: ?m.4197_ _: ?m.4200_ _: ?m.4203_ _: ?m.4206_ _: ?m.4209_ => le_rfl: ∀ {α : Type ?u.4211} [inst : Preorder α] {a : α}, a ≤ ale_rfl
#align monovary_on_const_left monovaryOn_const_left: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (g : ι → β) (a : α)
(s : Set ι), MonovaryOn (const ι a) g smonovaryOn_const_left

theorem antivaryOn_const_left: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (g : ι → β) (a : α)
(s : Set ι), AntivaryOn (const ι a) g santivaryOn_const_left (g: ι → βg : ι: Type ?u.4265ι → β: Type ?u.4274β) (a: αa : α: Type ?u.4271α) (s: Set ιs : Set: Type ?u.4317 → Type ?u.4317Set ι: Type ?u.4265ι) : AntivaryOn: {ι : Type ?u.4322} →
{α : Type ?u.4321} → {β : Type ?u.4320} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropAntivaryOn (const: {α : Sort ?u.4351} → (β : Sort ?u.4350) → α → β → αconst ι: Type ?u.4265ι a: αa) g: ι → βg s: Set ιs :=
fun _: ?m.4379_ _: ?m.4382_ _: ?m.4385_ _: ?m.4388_ _: ?m.4391_ => le_rfl: ∀ {α : Type ?u.4393} [inst : Preorder α] {a : α}, a ≤ ale_rfl
#align antivary_on_const_left antivaryOn_const_left: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (g : ι → β) (a : α)
(s : Set ι), AntivaryOn (const ι a) g santivaryOn_const_left

theorem monovaryOn_const_right: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : ι → α) (b : β)
(s : Set ι), MonovaryOn f (const ι b) smonovaryOn_const_right (f: ι → αf : ι: Type ?u.4447ι → α: Type ?u.4453α) (b: βb : β: Type ?u.4456β) (s: Set ιs : Set: Type ?u.4499 → Type ?u.4499Set ι: Type ?u.4447ι) : MonovaryOn: {ι : Type ?u.4504} →
{α : Type ?u.4503} → {β : Type ?u.4502} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropMonovaryOn f: ι → αf (const: {α : Sort ?u.4536} → (β : Sort ?u.4535) → α → β → αconst ι: Type ?u.4447ι b: βb) s: Set ιs :=
fun _: ?m.4561_ _: ?m.4564_ _: ?m.4567_ _: ?m.4570_ h: ?m.4573h => (h: ?m.4573h.ne: ∀ {α : Type ?u.4575} [inst : Preorder α] {a b : α}, a < b → a ≠ bne rfl: ∀ {α : Sort ?u.4594} {a : α}, a = arfl).elim: ∀ {C : Sort ?u.4604}, False → Celim
#align monovary_on_const_right monovaryOn_const_right: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : ι → α) (b : β)
(s : Set ι), MonovaryOn f (const ι b) smonovaryOn_const_right

theorem antivaryOn_const_right: ∀ (f : ι → α) (b : β) (s : Set ι), AntivaryOn f (const ι b) santivaryOn_const_right (f: ι → αf : ι: Type ?u.4628ι → α: Type ?u.4634α) (b: βb : β: Type ?u.4637β) (s: Set ιs : Set: Type ?u.4680 → Type ?u.4680Set ι: Type ?u.4628ι) : AntivaryOn: {ι : Type ?u.4685} →
{α : Type ?u.4684} → {β : Type ?u.4683} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropAntivaryOn f: ι → αf (const: {α : Sort ?u.4717} → (β : Sort ?u.4716) → α → β → αconst ι: Type ?u.4628ι b: βb) s: Set ιs :=
fun _: ?m.4742_ _: ?m.4745_ _: ?m.4748_ _: ?m.4751_ h: ?m.4754h => (h: ?m.4754h.ne: ∀ {α : Type ?u.4756} [inst : Preorder α] {a b : α}, a < b → a ≠ bne rfl: ∀ {α : Sort ?u.4775} {a : α}, a = arfl).elim: ∀ {C : Sort ?u.4785}, False → Celim
#align antivary_on_const_right antivaryOn_const_right: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : ι → α) (b : β)
(s : Set ι), AntivaryOn f (const ι b) santivaryOn_const_right

theorem Monovary.comp_right: Monovary f g → ∀ (k : ι' → ι), Monovary (f ∘ k) (g ∘ k)Monovary.comp_right (h: Monovary f gh : Monovary: {ι : Type ?u.4857} →
{α : Type ?u.4856} → {β : Type ?u.4855} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropMonovary f: ι → αf g: ι → βg) (k: ι' → ιk : ι': Type ?u.4812ι' → ι: Type ?u.4809ι) : Monovary: {ι : Type ?u.4907} →
{α : Type ?u.4906} → {β : Type ?u.4905} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropMonovary (f: ι → αf ∘ k: ι' → ιk) (g: ι → βg ∘ k: ι' → ιk) :=
fun _: ?m.4975_ _: ?m.4978_ hij: ?m.4981hij => h: Monovary f gh hij: ?m.4981hij
#align monovary.comp_right Monovary.comp_right: ∀ {ι : Type u_1} {ι' : Type u_4} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α}
{g : ι → β}, Monovary f g → ∀ (k : ι' → ι), Monovary (f ∘ k) (g ∘ k)Monovary.comp_right

theorem Antivary.comp_right: ∀ {ι : Type u_1} {ι' : Type u_4} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α}
{g : ι → β}, Antivary f g → ∀ (k : ι' → ι), Antivary (f ∘ k) (g ∘ k)Antivary.comp_right (h: Antivary f gh : Antivary: {ι : Type ?u.5065} →
{α : Type ?u.5064} → {β : Type ?u.5063} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropAntivary f: ι → αf g: ι → βg) (k: ι' → ιk : ι': Type ?u.5020ι' → ι: Type ?u.5017ι) : Antivary: {ι : Type ?u.5115} →
{α : Type ?u.5114} → {β : Type ?u.5113} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropAntivary (f: ι → αf ∘ k: ι' → ιk) (g: ι → βg ∘ k: ι' → ιk) :=
fun _: ?m.5183_ _: ?m.5186_ hij: ?m.5189hij => h: Antivary f gh hij: ?m.5189hij
#align antivary.comp_right Antivary.comp_right: ∀ {ι : Type u_1} {ι' : Type u_4} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α}
{g : ι → β}, Antivary f g → ∀ (k : ι' → ι), Antivary (f ∘ k) (g ∘ k)Antivary.comp_right

theorem MonovaryOn.comp_right: MonovaryOn f g s → ∀ (k : ι' → ι), MonovaryOn (f ∘ k) (g ∘ k) (k ⁻¹' s)MonovaryOn.comp_right (h: MonovaryOn f g sh : MonovaryOn: {ι : Type ?u.5273} →
{α : Type ?u.5272} → {β : Type ?u.5271} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropMonovaryOn f: ι → αf g: ι → βg s: Set ιs) (k: ι' → ιk : ι': Type ?u.5228ι' → ι: Type ?u.5225ι) :
MonovaryOn: {ι : Type ?u.5325} →
{α : Type ?u.5324} → {β : Type ?u.5323} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropMonovaryOn (f: ι → αf ∘ k: ι' → ιk) (g: ι → βg ∘ k: ι' → ιk) (k: ι' → ιk ⁻¹' s: Set ιs) := fun _: ?m.5404_ hi: ?m.5407hi _: ?m.5410_ hj: ?m.5413hj => h: MonovaryOn f g sh hi: ?m.5407hi hj: ?m.5413hj
#align monovary_on.comp_right MonovaryOn.comp_right: ∀ {ι : Type u_1} {ι' : Type u_4} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α}
{g : ι → β} {s : Set ι}, MonovaryOn f g s → ∀ (k : ι' → ι), MonovaryOn (f ∘ k) (g ∘ k) (k ⁻¹' s)MonovaryOn.comp_right

theorem AntivaryOn.comp_right: AntivaryOn f g s → ∀ (k : ι' → ι), AntivaryOn (f ∘ k) (g ∘ k) (k ⁻¹' s)AntivaryOn.comp_right (h: AntivaryOn f g sh : AntivaryOn: {ι : Type ?u.5521} →
{α : Type ?u.5520} → {β : Type ?u.5519} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropAntivaryOn f: ι → αf g: ι → βg s: Set ιs) (k: ι' → ιk : ι': Type ?u.5476ι' → ι: Type ?u.5473ι) :
AntivaryOn: {ι : Type ?u.5573} →
{α : Type ?u.5572} → {β : Type ?u.5571} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropAntivaryOn (f: ι → αf ∘ k: ι' → ιk) (g: ι → βg ∘ k: ι' → ιk) (k: ι' → ιk ⁻¹' s: Set ιs) := fun _: ?m.5652_ hi: ?m.5655hi _: ?m.5658_ hj: ?m.5661hj => h: AntivaryOn f g sh hi: ?m.5655hi hj: ?m.5661hj
#align antivary_on.comp_right AntivaryOn.comp_right: ∀ {ι : Type u_1} {ι' : Type u_4} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α}
{g : ι → β} {s : Set ι}, AntivaryOn f g s → ∀ (k : ι' → ι), AntivaryOn (f ∘ k) (g ∘ k) (k ⁻¹' s)AntivaryOn.comp_right

theorem Monovary.comp_monotone_left: Monovary f g → Monotone f' → Monovary (f' ∘ f) gMonovary.comp_monotone_left (h: Monovary f gh : Monovary: {ι : Type ?u.5769} →
{α : Type ?u.5768} → {β : Type ?u.5767} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropMonovary f: ι → αf g: ι → βg) (hf: Monotone f'hf : Monotone: {α : Type ?u.5814} → {β : Type ?u.5813} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropMonotone f': α → γf') : Monovary: {ι : Type ?u.5852} →
{α : Type ?u.5851} → {β : Type ?u.5850} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropMonovary (f': α → γf' ∘ f: ι → αf) g: ι → βg :=
fun _: ?m.5906_ _: ?m.5909_ hij: ?m.5912hij => hf: Monotone f'hf <| h: Monovary f gh hij: ?m.5912hij
#align monovary.comp_monotone_left Monovary.comp_monotone_left: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β]
[inst_2 : Preorder γ] {f : ι → α} {f' : α → γ} {g : ι → β}, Monovary f g → Monotone f' → Monovary (f' ∘ f) gMonovary.comp_monotone_left

theorem Monovary.comp_antitone_left: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β]
[inst_2 : Preorder γ] {f : ι → α} {f' : α → γ} {g : ι → β}, Monovary f g → Antitone f' → Antivary (f' ∘ f) gMonovary.comp_antitone_left (h: Monovary f gh : Monovary: {ι : Type ?u.6003} →
{α : Type ?u.6002} → {β : Type ?u.6001} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropMonovary f: ι → αf g: ι → βg) (hf: Antitone f'hf : Antitone: {α : Type ?u.6048} → {β : Type ?u.6047} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropAntitone f': α → γf') : Antivary: {ι : Type ?u.6086} →
{α : Type ?u.6085} → {β : Type ?u.6084} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropAntivary (f': α → γf' ∘ f: ι → αf) g: ι → βg :=
fun _: ?m.6140_ _: ?m.6143_ hij: ?m.6146hij => hf: Antitone f'hf <| h: Monovary f gh hij: ?m.6146hij
#align monovary.comp_antitone_left Monovary.comp_antitone_left: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β]
[inst_2 : Preorder γ] {f : ι → α} {f' : α → γ} {g : ι → β}, Monovary f g → Antitone f' → Antivary (f' ∘ f) gMonovary.comp_antitone_left

theorem Antivary.comp_monotone_left: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β]
[inst_2 : Preorder γ] {f : ι → α} {f' : α → γ} {g : ι → β}, Antivary f g → Monotone f' → Antivary (f' ∘ f) gAntivary.comp_monotone_left (h: Antivary f gh : Antivary: {ι : Type ?u.6237} →
{α : Type ?u.6236} → {β : Type ?u.6235} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropAntivary f: ι → αf g: ι → βg) (hf: Monotone f'hf : Monotone: {α : Type ?u.6282} → {β : Type ?u.6281} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropMonotone f': α → γf') : Antivary: {ι : Type ?u.6320} →
{α : Type ?u.6319} → {β : Type ?u.6318} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropAntivary (f': α → γf' ∘ f: ι → αf) g: ι → βg :=
fun _: ?m.6374_ _: ?m.6377_ hij: ?m.6380hij => hf: Monotone f'hf <| h: Antivary f gh hij: ?m.6380hij
#align antivary.comp_monotone_left Antivary.comp_monotone_left: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β]
[inst_2 : Preorder γ] {f : ι → α} {f' : α → γ} {g : ι → β}, Antivary f g → Monotone f' → Antivary (f' ∘ f) gAntivary.comp_monotone_left

theorem Antivary.comp_antitone_left: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β]
[inst_2 : Preorder γ] {f : ι → α} {f' : α → γ} {g : ι → β}, Antivary f g → Antitone f' → Monovary (f' ∘ f) gAntivary.comp_antitone_left (h: Antivary f gh : Antivary: {ι : Type ?u.6471} →
{α : Type ?u.6470} → {β : Type ?u.6469} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropAntivary f: ι → αf g: ι → βg) (hf: Antitone f'hf : Antitone: {α : Type ?u.6516} → {β : Type ?u.6515} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropAntitone f': α → γf') : Monovary: {ι : Type ?u.6554} →
{α : Type ?u.6553} → {β : Type ?u.6552} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropMonovary (f': α → γf' ∘ f: ι → αf) g: ι → βg :=
fun _: ?m.6608_ _: ?m.6611_ hij: ?m.6614hij => hf: Antitone f'hf <| h: Antivary f gh hij: ?m.6614hij
#align antivary.comp_antitone_left Antivary.comp_antitone_left: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β]
[inst_2 : Preorder γ] {f : ι → α} {f' : α → γ} {g : ι → β}, Antivary f g → Antitone f' → Monovary (f' ∘ f) gAntivary.comp_antitone_left

theorem MonovaryOn.comp_monotone_on_left: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β]
[inst_2 : Preorder γ] {f : ι → α} {f' : α → γ} {g : ι → β} {s : Set ι},
MonovaryOn f g s → Monotone f' → MonovaryOn (f' ∘ f) g sMonovaryOn.comp_monotone_on_left (h: MonovaryOn f g sh : MonovaryOn: {ι : Type ?u.6705} →
{α : Type ?u.6704} → {β : Type ?u.6703} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropMonovaryOn f: ι → αf g: ι → βg s: Set ιs) (hf: Monotone f'hf : Monotone: {α : Type ?u.6752} → {β : Type ?u.6751} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropMonotone f': α → γf') :
MonovaryOn: {ι : Type ?u.6790} →
{α : Type ?u.6789} → {β : Type ?u.6788} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropMonovaryOn (f': α → γf' ∘ f: ι → αf) g: ι → βg s: Set ιs := fun _: ?m.6845_ hi: ?m.6848hi _: ?m.6851_ hj: ?m.6854hj hij: ?m.6857hij => hf: Monotone f'hf <| h: MonovaryOn f g sh hi: ?m.6848hi hj: ?m.6854hj hij: ?m.6857hij
#align monovary_on.comp_monotone_on_left MonovaryOn.comp_monotone_on_left: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β]
[inst_2 : Preorder γ] {f : ι → α} {f' : α → γ} {g : ι → β} {s : Set ι},
MonovaryOn f g s → Monotone f' → MonovaryOn (f' ∘ f) g sMonovaryOn.comp_monotone_on_left

theorem MonovaryOn.comp_antitone_on_left: MonovaryOn f g s → Antitone f' → AntivaryOn (f' ∘ f) g sMonovaryOn.comp_antitone_on_left (h: MonovaryOn f g sh : MonovaryOn: {ι : Type ?u.6960} →
{α : Type ?u.6959} → {β : Type ?u.6958} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropMonovaryOn f: ι → αf g: ι → βg s: Set ιs) (hf: Antitone f'hf : Antitone: {α : Type ?u.7007} → {β : Type ?u.7006} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropAntitone f': α → γf') :
AntivaryOn: {ι : Type ?u.7045} →
{α : Type ?u.7044} → {β : Type ?u.7043} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropAntivaryOn (f': α → γf' ∘ f: ι → αf) g: ι → βg s: Set ιs := fun _: ?m.7100_ hi: ?m.7103hi _: ?m.7106_ hj: ?m.7109hj hij: ?m.7112hij => hf: Antitone f'hf <| h: MonovaryOn f g sh hi: ?m.7103hi hj: ?m.7109hj hij: ?m.7112hij
#align monovary_on.comp_antitone_on_left MonovaryOn.comp_antitone_on_left: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β]
[inst_2 : Preorder γ] {f : ι → α} {f' : α → γ} {g : ι → β} {s : Set ι},
MonovaryOn f g s → Antitone f' → AntivaryOn (f' ∘ f) g sMonovaryOn.comp_antitone_on_left

theorem AntivaryOn.comp_monotone_on_left: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β]
[inst_2 : Preorder γ] {f : ι → α} {f' : α → γ} {g : ι → β} {s : Set ι},
AntivaryOn f g s → Monotone f' → AntivaryOn (f' ∘ f) g sAntivaryOn.comp_monotone_on_left (h: AntivaryOn f g sh : AntivaryOn: {ι : Type ?u.7215} →
{α : Type ?u.7214} → {β : Type ?u.7213} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropAntivaryOn f: ι → αf g: ι → βg s: Set ιs) (hf: Monotone f'hf : Monotone: {α : Type ?u.7262} → {β : Type ?u.7261} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropMonotone f': α → γf') :
AntivaryOn: {ι : Type ?u.7300} →
{α : Type ?u.7299} → {β : Type ?u.7298} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropAntivaryOn (f': α → γf' ∘ f: ι → αf) g: ι → βg s: Set ιs := fun _: ?m.7355_ hi: ?m.7358hi _: ?m.7361_ hj: ?m.7364hj hij: ?m.7367hij => hf: Monotone f'hf <| h: AntivaryOn f g sh hi: ?m.7358hi hj: ?m.7364hj hij: ?m.7367hij
#align antivary_on.comp_monotone_on_left AntivaryOn.comp_monotone_on_left: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β]
[inst_2 : Preorder γ] {f : ι → α} {f' : α → γ} {g : ι → β} {s : Set ι},
AntivaryOn f g s → Monotone f' → AntivaryOn (f' ∘ f) g sAntivaryOn.comp_monotone_on_left

theorem AntivaryOn.comp_antitone_on_left: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β]
[inst_2 : Preorder γ] {f : ι → α} {f' : α → γ} {g : ι → β} {s : Set ι},
AntivaryOn f g s → Antitone f' → MonovaryOn (f' ∘ f) g sAntivaryOn.comp_antitone_on_left (h: AntivaryOn f g sh : AntivaryOn: {ι : Type ?u.7470} →
{α : Type ?u.7469} → {β : Type ?u.7468} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropAntivaryOn f: ι → αf g: ι → βg s: Set ιs) (hf: Antitone f'hf : Antitone: {α : Type ?u.7517} → {β : Type ?u.7516} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropAntitone f': α → γf') :
MonovaryOn: {ι : Type ?u.7555} →
{α : Type ?u.7554} → {β : Type ?u.7553} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropMonovaryOn (f': α → γf' ∘ f: ι → αf) g: ι → βg s: Set ιs := fun _: ?m.7610_ hi: ?m.7613hi _: ?m.7616_ hj: ?m.7619hj hij: ?m.7622hij => hf: Antitone f'hf <| h: AntivaryOn f g sh hi: ?m.7613hi hj: ?m.7619hj hij: ?m.7622hij
#align antivary_on.comp_antitone_on_left AntivaryOn.comp_antitone_on_left: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β]
[inst_2 : Preorder γ] {f : ι → α} {f' : α → γ} {g : ι → β} {s : Set ι},
AntivaryOn f g s → Antitone f' → MonovaryOn (f' ∘ f) g sAntivaryOn.comp_antitone_on_left

section OrderDual

open OrderDual

theorem Monovary.dual: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
Monovary f g → Monovary (↑toDual ∘ f) (↑toDual ∘ g)Monovary.dual : Monovary: {ι : Type ?u.7726} →
{α : Type ?u.7725} → {β : Type ?u.7724} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropMonovary f: ι → αf g: ι → βg → Monovary: {ι : Type ?u.7771} →
{α : Type ?u.7770} → {β : Type ?u.7769} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropMonovary (toDual: {α : Type ?u.7807} → α ≃ αᵒᵈtoDual ∘ f: ι → αf) (toDual: {α : Type ?u.7886} → α ≃ αᵒᵈtoDual ∘ g: ι → βg) :=
swap: ∀ {α : Sort ?u.7977} {β : Sort ?u.7976} {φ : α → β → Sort ?u.7975},
(∀ (x : α) (y : β), φ x y) → ∀ (y : β) (x : α), φ x yswap
#align monovary.dual Monovary.dual: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
Monovary f g → Monovary (↑toDual ∘ f) (↑toDual ∘ g)Monovary.dual

theorem Antivary.dual: Antivary f g → Antivary (↑toDual ∘ f) (↑toDual ∘ g)Antivary.dual : Antivary: {ι : Type ?u.8065} →
{α : Type ?u.8064} → {β : Type ?u.8063} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropAntivary f: ι → αf g: ι → βg → Antivary: {ι : Type ?u.8110} →
{α : Type ?u.8109} → {β : Type ?u.8108} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropAntivary (toDual: {α : Type ?u.8146} → α ≃ αᵒᵈtoDual ∘ f: ι → αf) (toDual: {α : Type ?u.8225} → α ≃ αᵒᵈtoDual ∘ g: ι → βg) :=
swap: ∀ {α : Sort ?u.8316} {β : Sort ?u.8315} {φ : α → β → Sort ?u.8314},
(∀ (x : α) (y : β), φ x y) → ∀ (y : β) (x : α), φ x yswap
#align antivary.dual Antivary.dual: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
Antivary f g → Antivary (↑toDual ∘ f) (↑toDual ∘ g)Antivary.dual

theorem Monovary.dual_left: Monovary f g → Antivary (↑toDual ∘ f) gMonovary.dual_left : Monovary: {ι : Type ?u.8404} →
{α : Type ?u.8403} → {β : Type ?u.8402} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropMonovary f: ι → αf g: ι → βg → Antivary: {ι : Type ?u.8449} →
{α : Type ?u.8448} → {β : Type ?u.8447} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropAntivary (toDual: {α : Type ?u.8485} → α ≃ αᵒᵈtoDual ∘ f: ι → αf) g: ι → βg :=
id: ∀ {α : Sort ?u.8569}, α → αid
#align monovary.dual_left Monovary.dual_left: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
Monovary f g → Antivary (↑toDual ∘ f) gMonovary.dual_left

theorem Antivary.dual_left: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
Antivary f g → Monovary (↑toDual ∘ f) gAntivary.dual_left : Antivary: {ι : Type ?u.8641} →
{α : Type ?u.8640} → {β : Type ?u.8639} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropAntivary f: ι → αf g: ι → βg → Monovary: {ι : Type ?u.8686} →
{α : Type ?u.8685} → {β : Type ?u.8684} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropMonovary (toDual: {α : Type ?u.8722} → α ≃ αᵒᵈtoDual ∘ f: ι → αf) g: ι → βg :=
id: ∀ {α : Sort ?u.8806}, α → αid
#align antivary.dual_left Antivary.dual_left: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
Antivary f g → Monovary (↑toDual ∘ f) gAntivary.dual_left

theorem Monovary.dual_right: Monovary f g → Antivary f (↑toDual ∘ g)Monovary.dual_right : Monovary: {ι : Type ?u.8878} →
{α : Type ?u.8877} → {β : Type ?u.8876} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropMonovary f: ι → αf g: ι → βg → Antivary: {ι : Type ?u.8923} →
{α : Type ?u.8922} → {β : Type ?u.8921} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropAntivary f: ι → αf (toDual: {α : Type ?u.8962} → α ≃ αᵒᵈtoDual ∘ g: ι → βg) :=
swap: ∀ {α : Sort ?u.9045} {β : Sort ?u.9044} {φ : α → β → Sort ?u.9043},
(∀ (x : α) (y : β), φ x y) → ∀ (y : β) (x : α), φ x yswap
#align monovary.dual_right Monovary.dual_right: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
Monovary f g → Antivary f (↑toDual ∘ g)Monovary.dual_right

theorem Antivary.dual_right: Antivary f g → Monovary f (↑toDual ∘ g)Antivary.dual_right : Antivary: {ι : Type ?u.9131} →
{α : Type ?u.9130} → {β : Type ?u.9129} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropAntivary f: ι → αf g: ι → βg → Monovary: {ι : Type ?u.9176} →
{α : Type ?u.9175} → {β : Type ?u.9174} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropMonovary f: ι → αf (toDual: {α : Type ?u.9215} → α ≃ αᵒᵈtoDual ∘ g: ι → βg) :=
swap: ∀ {α : Sort ?u.9298} {β : Sort ?u.9297} {φ : α → β → Sort ?u.9296},
(∀ (x : α) (y : β), φ x y) → ∀ (y : β) (x : α), φ x yswap
#align antivary.dual_right Antivary.dual_right: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
Antivary f g → Monovary f (↑toDual ∘ g)Antivary.dual_right

theorem MonovaryOn.dual: MonovaryOn f g s → MonovaryOn (↑toDual ∘ f) (↑toDual ∘ g) sMonovaryOn.dual : MonovaryOn: {ι : Type ?u.9384} →
{α : Type ?u.9383} → {β : Type ?u.9382} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropMonovaryOn f: ι → αf g: ι → βg s: Set ιs → MonovaryOn: {ι : Type ?u.9431} →
{α : Type ?u.9430} → {β : Type ?u.9429} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropMonovaryOn (toDual: {α : Type ?u.9467} → α ≃ αᵒᵈtoDual ∘ f: ι → αf) (toDual: {α : Type ?u.9546} → α ≃ αᵒᵈtoDual ∘ g: ι → βg) s: Set ιs :=
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₂swap₂
#align monovary_on.dual MonovaryOn.dual: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
{s : Set ι}, MonovaryOn f g s → MonovaryOn (↑toDual ∘ f) (↑toDual ∘ g) sMonovaryOn.dual

theorem AntivaryOn.dual: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
{s : Set ι}, AntivaryOn f g s → AntivaryOn (↑toDual ∘ f) (↑toDual ∘ g) sAntivaryOn.dual : AntivaryOn: {ι : Type ?u.9751} →
{α : Type ?u.9750} → {β : Type ?u.9749} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropAntivaryOn f: ι → αf g: ι → βg s: Set ιs → AntivaryOn: {ι : Type ?u.9798} →
{α : Type ?u.9797} → {β : Type ?u.9796} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropAntivaryOn (toDual: {α : Type ?u.9834} → α ≃ αᵒᵈtoDual ∘ f: ι → αf) (toDual: {α : Type ?u.9913} → α ≃ αᵒᵈtoDual ∘ g: ι → βg) s: Set ιs :=
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₂swap₂
#align antivary_on.dual AntivaryOn.dual: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
{s : Set ι}, AntivaryOn f g s → AntivaryOn (↑toDual ∘ f) (↑toDual ∘ g) sAntivaryOn.dual

theorem MonovaryOn.dual_left: MonovaryOn f g s → AntivaryOn (↑toDual ∘ f) g sMonovaryOn.dual_left : MonovaryOn: {ι : Type ?u.10118} →
{α : Type ?u.10117} →
{β : Type ?u.10116} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropMonovaryOn f: ι → αf g: ι → βg s: Set ιs → AntivaryOn: {ι : Type ?u.10165} →
{α : Type ?u.10164} →
{β : Type ?u.10163} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropAntivaryOn (toDual: {α : Type ?u.10201} → α ≃ αᵒᵈtoDual ∘ f: ι → αf) g: ι → βg s: Set ιs :=
id: ∀ {α : Sort ?u.10286}, α → αid
#align monovary_on.dual_left MonovaryOn.dual_left: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
{s : Set ι}, MonovaryOn f g s → AntivaryOn (↑toDual ∘ f) g sMonovaryOn.dual_left

theorem AntivaryOn.dual_left: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
{s : Set ι}, AntivaryOn f g s → MonovaryOn (↑toDual ∘ f) g sAntivaryOn.dual_left : AntivaryOn: {ι : Type ?u.10363} →
{α : Type ?u.10362} →
{β : Type ?u.10361} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropAntivaryOn f: ι → αf g: ι → βg s: Set ιs → MonovaryOn: {ι : Type ?u.10410} →
{α : Type ?u.10409} →
{β : Type ?u.10408} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropMonovaryOn (toDual: {α : Type ?u.10446} → α ≃ αᵒᵈtoDual ∘ f: ι → αf) g: ι → βg s: Set ιs :=
id: ∀ {α : Sort ?u.10531}, α → αid
#align antivary_on.dual_left AntivaryOn.dual_left: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
{s : Set ι}, AntivaryOn f g s → MonovaryOn (↑toDual ∘ f) g sAntivaryOn.dual_left

theorem MonovaryOn.dual_right: MonovaryOn f g s → AntivaryOn f (↑toDual ∘ g) sMonovaryOn.dual_right : MonovaryOn: {ι : Type ?u.10608} →
{α : Type ?u.10607} →
{β : Type ?u.10606} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropMonovaryOn f: ι → αf g: ι → βg s: Set ιs → AntivaryOn: {ι : Type ?u.10655} →
{α : Type ?u.10654} →
{β : Type ?u.10653} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropAntivaryOn f: ι → αf (toDual: {α : Type ?u.10694} → α ≃ αᵒᵈtoDual ∘ g: ι → βg) s: Set ιs :=
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₂swap₂
#align monovary_on.dual_right MonovaryOn.dual_right: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
{s : Set ι}, MonovaryOn f g s → AntivaryOn f (↑toDual ∘ g) sMonovaryOn.dual_right

theorem AntivaryOn.dual_right: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
{s : Set ι}, AntivaryOn f g s → MonovaryOn f (↑toDual ∘ g) sAntivaryOn.dual_right : AntivaryOn: {ι : Type ?u.10889} →
{α : Type ?u.10888} →
{β : Type ?u.10887} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropAntivaryOn f: ι → αf g: ι → βg s: Set ιs → MonovaryOn: {ι : Type ?u.10936} →
{α : Type ?u.10935} →
{β : Type ?u.10934} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropMonovaryOn f: ι → αf (toDual: {α : Type ?u.10975} → α ≃ αᵒᵈtoDual ∘ g: ι → βg) s: Set ιs :=
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₂swap₂
#align antivary_on.dual_right AntivaryOn.dual_right: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
{s : Set ι}, AntivaryOn f g s → MonovaryOn f (↑toDual ∘ g) sAntivaryOn.dual_right

@[simp]
theorem monovary_toDual_left: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
Monovary (↑toDual ∘ f) g ↔ Antivary f gmonovary_toDual_left : Monovary: {ι : Type ?u.11169} →
{α : Type ?u.11168} → {β : Type ?u.11167} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropMonovary (toDual: {α : Type ?u.11183} → α ≃ αᵒᵈtoDual ∘ f: ι → αf) g: ι → βg ↔ Antivary: {ι : Type ?u.11273} →
{α : Type ?u.11272} → {β : Type ?u.11271} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropAntivary f: ι → αf g: ι → βg :=
Iff.rfl: ∀ {a : Prop}, a ↔ aIff.rfl
#align monovary_to_dual_left monovary_toDual_left: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
Monovary (↑toDual ∘ f) g ↔ Antivary f gmonovary_toDual_left

@[simp]
theorem monovary_toDual_right: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
Monovary f (↑toDual ∘ g) ↔ Antivary f gmonovary_toDual_right : Monovary: {ι : Type ?u.11411} →
{α : Type ?u.11410} → {β : Type ?u.11409} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropMonovary f: ι → αf (toDual: {α : Type ?u.11428} → α ≃ αᵒᵈtoDual ∘ g: ι → βg) ↔ Antivary: {ι : Type ?u.11515} →
{α : Type ?u.11514} → {β : Type ?u.11513} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropAntivary f: ι → αf g: ι → βg :=
forall_swap: ∀ {α : Sort ?u.11530} {β : Sort ?u.11531} {p : α → β → Prop}, (∀ (x : α) (y : β), p x y) ↔ ∀ (y : β) (x : α), p x yforall_swap
#align monovary_to_dual_right monovary_toDual_right: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
Monovary f (↑toDual ∘ g) ↔ Antivary f gmonovary_toDual_right

@[simp]
theorem antivary_toDual_left: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
Antivary (↑toDual ∘ f) g ↔ Monovary f gantivary_toDual_left : Antivary: {ι : Type ?u.11667} →
{α : Type ?u.11666} → {β : Type ?u.11665} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropAntivary (toDual: {α : Type ?u.11681} → α ≃ αᵒᵈtoDual ∘ f: ι → αf) g: ι → βg ↔ Monovary: {ι : Type ?u.11771} →
{α : Type ?u.11770} → {β : Type ?u.11769} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropMonovary f: ι → αf g: ι → βg :=
Iff.rfl: ∀ {a : Prop}, a ↔ aIff.rfl
#align antivary_to_dual_left antivary_toDual_left: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
Antivary (↑toDual ∘ f) g ↔ Monovary f gantivary_toDual_left

@[simp]
theorem antivary_toDual_right: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
Antivary f (↑toDual ∘ g) ↔ Monovary f gantivary_toDual_right : Antivary: {ι : Type ?u.11909} →
{α : Type ?u.11908} → {β : Type ?u.11907} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropAntivary f: ι → αf (toDual: {α : Type ?u.11926} → α ≃ αᵒᵈtoDual ∘ g: ι → βg) ↔ Monovary: {ι : Type ?u.12013} →
{α : Type ?u.12012} → {β : Type ?u.12011} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropMonovary f: ι → αf g: ι → βg :=
forall_swap: ∀ {α : Sort ?u.12028} {β : Sort ?u.12029} {p : α → β → Prop}, (∀ (x : α) (y : β), p x y) ↔ ∀ (y : β) (x : α), p x yforall_swap
#align antivary_to_dual_right antivary_toDual_right: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
Antivary f (↑toDual ∘ g) ↔ Monovary f gantivary_toDual_right

@[simp]
theorem monovaryOn_toDual_left: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
{s : Set ι}, MonovaryOn (↑toDual ∘ f) g s ↔ AntivaryOn f g smonovaryOn_toDual_left : MonovaryOn: {ι : Type ?u.12165} →
{α : Type ?u.12164} →
{β : Type ?u.12163} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropMonovaryOn (toDual: {α : Type ?u.12179} → α ≃ αᵒᵈtoDual ∘ f: ι → αf) g: ι → βg s: Set ιs ↔ AntivaryOn: {ι : Type ?u.12271} →
{α : Type ?u.12270} →
{β : Type ?u.12269} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropAntivaryOn f: ι → αf g: ι → βg s: Set ιs :=
Iff.rfl: ∀ {a : Prop}, a ↔ aIff.rfl
#align monovary_on_to_dual_left monovaryOn_toDual_left: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
{s : Set ι}, MonovaryOn (↑toDual ∘ f) g s ↔ AntivaryOn f g smonovaryOn_toDual_left

@[simp]
theorem monovaryOn_toDual_right: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
{s : Set ι}, MonovaryOn f (↑toDual ∘ g) s ↔ AntivaryOn f g smonovaryOn_toDual_right : MonovaryOn: {ι : Type ?u.12420} →
{α : Type ?u.12419} →
{β : Type ?u.12418} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropMonovaryOn f: ι → αf (toDual: {α : Type ?u.12437} → α ≃ αᵒᵈtoDual ∘ g: ι → βg) s: Set ιs ↔ AntivaryOn: {ι : Type ?u.12526} →
{α : Type ?u.12525} →
{β : Type ?u.12524} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropAntivaryOn f: ι → αf g: ι → βg s: Set ιs :=
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₂forall₂_swap
#align monovary_on_to_dual_right monovaryOn_toDual_right: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
{s : Set ι}, MonovaryOn f (↑toDual ∘ g) s ↔ AntivaryOn f g smonovaryOn_toDual_right

@[simp]
theorem antivaryOn_toDual_left: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
{s : Set ι}, AntivaryOn (↑toDual ∘ f) g s ↔ MonovaryOn f g santivaryOn_toDual_left : AntivaryOn: {ι : Type ?u.12707} →
{α : Type ?u.12706} →
{β : Type ?u.12705} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropAntivaryOn (toDual: {α : Type ?u.12721} → α ≃ αᵒᵈtoDual ∘ f: ι → αf) g: ι → βg s: Set ιs ↔ MonovaryOn: {ι : Type ?u.12813} →
{α : Type ?u.12812} →
{β : Type ?u.12811} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropMonovaryOn f: ι → αf g: ι → βg s: Set ιs :=
Iff.rfl: ∀ {a : Prop}, a ↔ aIff.rfl
#align antivary_on_to_dual_left antivaryOn_toDual_left: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
{s : Set ι}, AntivaryOn (↑toDual ∘ f) g s ↔ MonovaryOn f g santivaryOn_toDual_left

@[simp]
theorem antivaryOn_toDual_right: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
{s : Set ι}, AntivaryOn f (↑toDual ∘ g) s ↔ MonovaryOn f g santivaryOn_toDual_right : AntivaryOn: {ι : Type ?u.12962} →
{α : Type ?u.12961} →
{β : Type ?u.12960} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropAntivaryOn f: ι → αf (toDual: {α : Type ?u.12979} → α ≃ αᵒᵈtoDual ∘ g: ι → βg) s: Set ιs ↔ MonovaryOn: {ι : Type ?u.13068} →
{α : Type ?u.13067} →
{β : Type ?u.13066} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropMonovaryOn f: ι → αf g: ι → βg s: Set ιs :=
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₂forall₂_swap
#align antivary_on_to_dual_right antivaryOn_toDual_right: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
{s : Set ι}, AntivaryOn f (↑toDual ∘ g) s ↔ MonovaryOn f g santivaryOn_toDual_right

end OrderDual

section PartialOrder

variable [PartialOrder: Type ?u.13502 → Type ?u.13502PartialOrder ι: Type ?u.13201ι]

@[simp]
theorem monovary_id_iff: ∀ {ι : Type u_1} {α : Type u_2} [inst : Preorder α] {f : ι → α} [inst_1 : PartialOrder ι], Monovary f id ↔ Monotone fmonovary_id_iff : Monovary: {ι : Type ?u.13301} →
{α : Type ?u.13300} → {β : Type ?u.13299} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropMonovary f: ι → αf id: {α : Sort ?u.13310} → α → αid ↔ Monotone: {α : Type ?u.13332} → {β : Type ?u.13331} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropMonotone f: ι → αf :=
monotone_iff_forall_lt: ∀ {α : Type ?u.13342} {β : Type ?u.13341} [inst : PartialOrder α] [inst_1 : Preorder β] {f : α → β},
Monotone f ↔ ∀ ⦃a b : α⦄, a < b → f a ≤ f bmonotone_iff_forall_lt.symm: ∀ {a b : Prop}, (a ↔ b) → (b ↔ a)symm
#align monovary_id_iff monovary_id_iff: ∀ {ι : Type u_1} {α : Type u_2} [inst : Preorder α] {f : ι → α} [inst_1 : PartialOrder ι], Monovary f id ↔ Monotone fmonovary_id_iff

@[simp]
theorem antivary_id_iff: ∀ {ι : Type u_1} {α : Type u_2} [inst : Preorder α] {f : ι → α} [inst_1 : PartialOrder ι], Antivary f id ↔ Antitone fantivary_id_iff : Antivary: {ι : Type ?u.13507} →
{α : Type ?u.13506} → {β : Type ?u.13505} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropAntivary f: ι → αf id: {α : Sort ?u.13516} → α → αid ↔ Antitone: {α : Type ?u.13538} → {β : Type ?u.13537} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropAntitone f: ι → αf :=
antitone_iff_forall_lt: ∀ {α : Type ?u.13548} {β : Type ?u.13547} [inst : PartialOrder α] [inst_1 : Preorder β] {f : α → β},
Antitone f ↔ ∀ ⦃a b : α⦄, a < b → f b ≤ f aantitone_iff_forall_lt.symm: ∀ {a b : Prop}, (a ↔ b) → (b ↔ a)symm
#align antivary_id_iff antivary_id_iff: ∀ {ι : Type u_1} {α : Type u_2} [inst : Preorder α] {f : ι → α} [inst_1 : PartialOrder ι], Antivary f id ↔ Antitone fantivary_id_iff

@[simp]
theorem monovaryOn_id_iff: ∀ {ι : Type u_1} {α : Type u_2} [inst : Preorder α] {f : ι → α} {s : Set ι} [inst_1 : PartialOrder ι],
MonovaryOn f id s ↔ MonotoneOn f smonovaryOn_id_iff : MonovaryOn: {ι : Type ?u.13713} →
{α : Type ?u.13712} →
{β : Type ?u.13711} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropMonovaryOn f: ι → αf id: {α : Sort ?u.13722} → α → αid s: Set ιs ↔ MonotoneOn: {α : Type ?u.13746} → {β : Type ?u.13745} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Set α → PropMonotoneOn f: ι → αf s: Set ιs :=
monotoneOn_iff_forall_lt: ∀ {α : Type ?u.13757} {β : Type ?u.13756} [inst : PartialOrder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
MonotoneOn f s ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a < b → f a ≤ f bmonotoneOn_iff_forall_lt.symm: ∀ {a b : Prop}, (a ↔ b) → (b ↔ a)symm
#align monovary_on_id_iff monovaryOn_id_iff: ∀ {ι : Type u_1} {α : Type u_2} [inst : Preorder α] {f : ι → α} {s : Set ι} [inst_1 : PartialOrder ι],
MonovaryOn f id s ↔ MonotoneOn f smonovaryOn_id_iff

@[simp]
theorem antivaryOn_id_iff: ∀ {ι : Type u_1} {α : Type u_2} [inst : Preorder α] {f : ι → α} {s : Set ι} [inst_1 : PartialOrder ι],
AntivaryOn f id s ↔ AntitoneOn f santivaryOn_id_iff : AntivaryOn: {ι : Type ?u.13945} →
{α : Type ?u.13944} →
{β : Type ?u.13943} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropAntivaryOn f: ι → αf id: {α : Sort ?u.13954} → α → αid s: Set ιs ↔ AntitoneOn: {α : Type ?u.13978} → {β : Type ?u.13977} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Set α → PropAntitoneOn f: ι → αf s: Set ιs :=
antitoneOn_iff_forall_lt: ∀ {α : Type ?u.13989} {β : Type ?u.13988} [inst : PartialOrder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
AntitoneOn f s ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a < b → f b ≤ f aantitoneOn_iff_forall_lt.symm: ∀ {a b : Prop}, (a ↔ b) → (b ↔ a)symm
#align antivary_on_id_iff antivaryOn_id_iff: ∀ {ι : Type u_1} {α : Type u_2} [inst : Preorder α] {f : ι → α} {s : Set ι} [inst_1 : PartialOrder ι],
AntivaryOn f id s ↔ AntitoneOn f santivaryOn_id_iff

end PartialOrder

variable [LinearOrder: Type ?u.16213 → Type ?u.16213LinearOrder ι: Type ?u.14126ι]

/-Porting note: Due to a bug in `alias`, many of the below lemmas have dot notation removed in the
proof-/

protected theorem Monotone.monovary: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
[inst_2 : LinearOrder ι], Monotone f → Monotone g → Monovary f gMonotone.monovary (hf: Monotone fhf : Monotone: {α : Type ?u.14225} → {β : Type ?u.14224} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropMonotone f: ι → αf) (hg: Monotone ghg : Monotone: {α : Type ?u.14348} → {β : Type ?u.14347} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropMonotone g: ι → βg) : Monovary: {ι : Type ?u.14386} →
{α : Type ?u.14385} → {β : Type ?u.14384} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropMonovary f: ι → αf g: ι → βg :=
fun _: ?m.14426_ _: ?m.14429_ hij: ?m.14432hij => hf: Monotone fhf (hg: Monotone ghg.reflect_lt: ∀ {α : Type ?u.14442} {β : Type ?u.14441} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β},
Monotone f → ∀ {a b : α}, f a < f b → a < breflect_lt hij: ?m.14432hij).le: ∀ {α : Type ?u.14478} [inst : Preorder α] {a b : α}, a < b → a ≤ ble
#align monotone.monovary Monotone.monovary: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
[inst_2 : LinearOrder ι], Monotone f → Monotone g → Monovary f gMonotone.monovary

protected theorem Monotone.antivary: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
[inst_2 : LinearOrder ι], Monotone f → Antitone g → Antivary f gMonotone.antivary (hf: Monotone fhf : Monotone: {α : Type ?u.14644} → {β : Type ?u.14643} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropMonotone f: ι → αf) (hg: Antitone ghg : Antitone: {α : Type ?u.14767} → {β : Type ?u.14766} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropAntitone g: ι → βg) : Antivary: {ι : Type ?u.14805} →
{α : Type ?u.14804} → {β : Type ?u.14803} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropAntivary f: ι → αf g: ι → βg :=
(hf: Monotone fhf.monovary: ∀ {ι : Type ?u.14844} {α : Type ?u.14845} {β : Type ?u.14846} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α}
{g : ι → β} [inst_2 : LinearOrder ι], Monotone f → Monotone g → Monovary f gmonovary (Antitone.dual_right: ∀ {α : Type ?u.14896} {β : Type ?u.14895} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
Antitone f → Monotone (↑OrderDual.toDual ∘ f)Antitone.dual_right hg: Antitone ghg)).dual_right: ∀ {ι : Type ?u.15055} {α : Type ?u.15056} {β : Type ?u.15057} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α}
{g : ι → β}, Monovary f g → Antivary f (↑OrderDual.toDual ∘ g)dual_right
#align monotone.antivary Monotone.antivary: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
[inst_2 : LinearOrder ι], Monotone f → Antitone g → Antivary f gMonotone.antivary

protected theorem Antitone.monovary: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
[inst_2 : LinearOrder ι], Antitone f → Antitone g → Monovary f gAntitone.monovary (hf: Antitone fhf : Antitone: {α : Type ?u.15179} → {β : Type ?u.15178} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropAntitone f: ι → αf) (hg: Antitone ghg : Antitone: {α : Type ?u.15302} → {β : Type ?u.15301} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropAntitone g: ι → βg) : Monovary: {ι : Type ?u.15340} →
{α : Type ?u.15339} → {β : Type ?u.15338} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropMonovary f: ι → αf g: ι → βg :=
(hf: Antitone fhf.dual_right: ∀ {α : Type ?u.15380} {β : Type ?u.15379} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
Antitone f → Monotone (↑OrderDual.toDual ∘ f)dual_right.antivary: ∀ {ι : Type ?u.15483} {α : Type ?u.15484} {β : Type ?u.15485} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α}
{g : ι → β} [inst_2 : LinearOrder ι], Monotone f → Antitone g → Antivary f gantivary hg: Antitone ghg).dual_left: ∀ {ι : Type ?u.15558} {α : Type ?u.15559} {β : Type ?u.15560} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α}
{g : ι → β}, Antivary f g → Monovary (↑OrderDual.toDual ∘ f) gdual_left
#align antitone.monovary Antitone.monovary: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
[inst_2 : LinearOrder ι], Antitone f → Antitone g → Monovary f gAntitone.monovary

protected theorem Antitone.antivary: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
[inst_2 : LinearOrder ι], Antitone f → Monotone g → Antivary f gAntitone.antivary (hf: Antitone fhf : Antitone: {α : Type ?u.15682} → {β : Type ?u.15681} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropAntitone f: ι → αf) (hg: Monotone ghg : Monotone: {α : Type ?u.15805} → {β : Type ?u.15804} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropMonotone g: ι → βg) : Antivary: {ι : Type ?u.15843} →
{α : Type ?u.15842} → {β : Type ?u.15841} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → PropAntivary f: ι → αf g: ι → βg :=
(hf: Antitone fhf.monovary: ∀ {ι : Type ?u.15882} {α : Type ?u.15883} {β : Type ?u.15884} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α}
{g : ι → β} [inst_2 : LinearOrder ι], Antitone f → Antitone g → Monovary f gmonovary (Monotone.dual_right: ∀ {α : Type ?u.15934} {β : Type ?u.15933} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
Monotone f → Antitone (↑OrderDual.toDual ∘ f)Monotone.dual_right hg: Monotone ghg)).dual_right: ∀ {ι : Type ?u.16093} {α : Type ?u.16094} {β : Type ?u.16095} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α}
{g : ι → β}, Monovary f g → Antivary f (↑OrderDual.toDual ∘ g)dual_right
#align antitone.antivary Antitone.antivary: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
[inst_2 : LinearOrder ι], Antitone f → Monotone g → Antivary f gAntitone.antivary

protected theorem MonotoneOn.monovaryOn: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
{s : Set ι} [inst_2 : LinearOrder ι], MonotoneOn f s → MonotoneOn g s → MonovaryOn f g sMonotoneOn.monovaryOn (hf: MonotoneOn f shf : MonotoneOn: {α : Type ?u.16217} → {β : Type ?u.16216} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Set α → PropMonotoneOn f: ι → αf s: Set ιs) (hg: MonotoneOn g shg : MonotoneOn: {α : Type ?u.16342} → {β : Type ?u.16341} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Set α → PropMonotoneOn g: ι → βg s: Set ιs) :
MonovaryOn: {ι : Type ?u.16381} →
{α : Type ?u.16380} →
{β : Type ?u.16379} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropMonovaryOn f: ι → αf g: ι → βg s: Set ιs := fun _: ?m.16422_ hi: ?m.16425hi _: ?m.16428_ hj: ?m.16431hj hij: ?m.16434hij => hf: MonotoneOn f shf hi: ?m.16425hi hj: ?m.16431hj (hg: MonotoneOn g shg.reflect_lt: ∀ {α : Type ?u.16449} {β : Type ?u.16448} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
MonotoneOn f s → ∀ {a b : α}, a ∈ s → b ∈ s → f a < f b → a < breflect_lt hi: ?m.16425hi hj: ?m.16431hj hij: ?m.16434hij).le: ∀ {α : Type ?u.16487} [inst : Preorder α] {a b : α}, a < b → a ≤ ble
#align monotone_on.monovary_on MonotoneOn.monovaryOn: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
{s : Set ι} [inst_2 : LinearOrder ι], MonotoneOn f s → MonotoneOn g s → MonovaryOn f g sMonotoneOn.monovaryOn

protected theorem MonotoneOn.antivaryOn: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
{s : Set ι} [inst_2 : LinearOrder ι], MonotoneOn f s → AntitoneOn g s → AntivaryOn f g sMonotoneOn.antivaryOn (hf: MonotoneOn f shf : MonotoneOn: {α : Type ?u.16658} → {β : Type ?u.16657} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Set α → PropMonotoneOn f: ι → αf s: Set ιs) (hg: AntitoneOn g shg : AntitoneOn: {α : Type ?u.16783} → {β : Type ?u.16782} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Set α → PropAntitoneOn g: ι → βg s: Set ιs) :
AntivaryOn: {ι : Type ?u.16822} →
{α : Type ?u.16821} →
{β : Type ?u.16820} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropAntivaryOn f: ι → αf g: ι → βg s: Set ιs :=
(hf: MonotoneOn f shf.monovaryOn: ∀ {ι : Type ?u.16862} {α : Type ?u.16863} {β : Type ?u.16864} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α}
{g : ι → β} {s : Set ι} [inst_2 : LinearOrder ι], MonotoneOn f s → MonotoneOn g s → MonovaryOn f g smonovaryOn (AntitoneOn.dual_right: ∀ {α : Type ?u.16921} {β : Type ?u.16920} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
AntitoneOn f s → MonotoneOn (↑OrderDual.toDual ∘ f) sAntitoneOn.dual_right hg: AntitoneOn g shg)).dual_right: ∀ {ι : Type ?u.17091} {α : Type ?u.17092} {β : Type ?u.17093} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α}
{g : ι → β} {s : Set ι}, MonovaryOn f g s → AntivaryOn f (↑OrderDual.toDual ∘ g) sdual_right
#align monotone_on.antivary_on MonotoneOn.antivaryOn: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
{s : Set ι} [inst_2 : LinearOrder ι], MonotoneOn f s → AntitoneOn g s → AntivaryOn f g sMonotoneOn.antivaryOn

protected theorem AntitoneOn.monovaryOn: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
{s : Set ι} [inst_2 : LinearOrder ι], AntitoneOn f s → AntitoneOn g s → MonovaryOn f g sAntitoneOn.monovaryOn (hf: AntitoneOn f shf : AntitoneOn: {α : Type ?u.17224} → {β : Type ?u.17223} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Set α → PropAntitoneOn f: ι → αf s: Set ιs) (hg: AntitoneOn g shg : AntitoneOn: {α : Type ?u.17349} → {β : Type ?u.17348} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Set α → PropAntitoneOn g: ι → βg s: Set ιs) :
MonovaryOn: {ι : Type ?u.17388} →
{α : Type ?u.17387} →
{β : Type ?u.17386} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropMonovaryOn f: ι → αf g: ι → βg s: Set ιs :=
(hf: AntitoneOn f shf.dual_right: ∀ {α : Type ?u.17429} {β : Type ?u.17428} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
AntitoneOn f s → MonotoneOn (↑OrderDual.toDual ∘ f) sdual_right.antivaryOn: ∀ {ι : Type ?u.17536} {α : Type ?u.17537} {β : Type ?u.17538} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α}
{g : ι → β} {s : Set ι} [inst_2 : LinearOrder ι], MonotoneOn f s → AntitoneOn g s → AntivaryOn f g santivaryOn hg: AntitoneOn g shg).dual_left: ∀ {ι : Type ?u.17621} {α : Type ?u.17622} {β : Type ?u.17623} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α}
{g : ι → β} {s : Set ι}, AntivaryOn f g s → MonovaryOn (↑OrderDual.toDual ∘ f) g sdual_left
#align antitone_on.monovary_on AntitoneOn.monovaryOn: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
{s : Set ι} [inst_2 : LinearOrder ι], AntitoneOn f s → AntitoneOn g s → MonovaryOn f g sAntitoneOn.monovaryOn

protected theorem AntitoneOn.antivaryOn: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
{s : Set ι} [inst_2 : LinearOrder ι], AntitoneOn f s → MonotoneOn g s → AntivaryOn f g sAntitoneOn.antivaryOn (hf: AntitoneOn f shf : AntitoneOn: {α : Type ?u.17754} → {β : Type ?u.17753} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Set α → PropAntitoneOn f: ι → αf s: Set ιs) (hg: MonotoneOn g shg : MonotoneOn: {α : Type ?u.17879} → {β : Type ?u.17878} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Set α → PropMonotoneOn g: ι → βg s: Set ιs) :
AntivaryOn: {ι : Type ?u.17918} →
{α : Type ?u.17917} →
{β : Type ?u.17916} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropAntivaryOn f: ι → αf g: ι → βg s: Set ιs :=
(hf: AntitoneOn f shf.monovaryOn: ∀ {ι : Type ?u.17958} {α : Type ?u.17959} {β : Type ?u.17960} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α}
{g : ι → β} {s : Set ι} [inst_2 : LinearOrder ι], AntitoneOn f s → AntitoneOn g s → MonovaryOn f g smonovaryOn (MonotoneOn.dual_right: ∀ {α : Type ?u.18017} {β : Type ?u.18016} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
MonotoneOn f s → AntitoneOn (↑OrderDual.toDual ∘ f) sMonotoneOn.dual_right hg: MonotoneOn g shg)).dual_right: ∀ {ι : Type ?u.18187} {α : Type ?u.18188} {β : Type ?u.18189} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α}
{g : ι → β} {s : Set ι}, MonovaryOn f g s → AntivaryOn f (↑OrderDual.toDual ∘ g) sdual_right
#align antitone_on.antivary_on AntitoneOn.antivaryOn: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
{s : Set ι} [inst_2 : LinearOrder ι], AntitoneOn f s → MonotoneOn g s → AntivaryOn f g sAntitoneOn.antivaryOn

end Preorder

section LinearOrder

variable [Preorder: Type ?u.18737 → Type ?u.18737Preorder α: Type ?u.18276α] [LinearOrder: Type ?u.18288 → Type ?u.18288LinearOrder β: Type ?u.18279β] [Preorder: Type ?u.19970 → Type ?u.19970Preorder γ: Type ?u.18282γ] {f: ι → αf : ι: Type ?u.18722ι → α: Type ?u.18319α} {f': α → γf' : α: Type ?u.18276α → γ: Type ?u.20876γ} {g: ι → βg : ι: Type ?u.18313ι → β: Type ?u.19140β} {g': β → γg' : β: Type ?u.18279β → γ: Type ?u.18282γ}
{s: Set ιs : Set: Type ?u.18310 → Type ?u.18310Set ι: Type ?u.18270ι}

theorem MonovaryOn.comp_monotoneOn_right: MonovaryOn f g s → MonotoneOn g' (g '' s) → MonovaryOn f (g' ∘ g) sMonovaryOn.comp_monotoneOn_right (h: MonovaryOn f g sh : MonovaryOn: {ι : Type ?u.18358} →
{α : Type ?u.18357} →
{β : Type ?u.18356} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropMonovaryOn f: ι → αf g: ι → βg s: Set ιs) (hg: MonotoneOn g' (g '' s)hg : MonotoneOn: {α : Type ?u.18487} → {β : Type ?u.18486} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Set α → PropMonotoneOn g': β → γg' (g: ι → βg '' s: Set ιs)) :
MonovaryOn: {ι : Type ?u.18536} →
{α : Type ?u.18535} →
{β : Type ?u.18534} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropMonovaryOn f: ι → αf (g': β → γg' ∘ g: ι → βg) s: Set ιs := fun _: ?m.18591_ hi: ?m.18594hi _: ?m.18597_ hj: ?m.18600hj hij: ?m.18603hij =>
h: MonovaryOn f g sh hi: ?m.18594hi hj: ?m.18600hj <| hg: MonotoneOn g' (g '' s)hg.reflect_lt: ∀ {α : Type ?u.18618} {β : Type ?u.18617} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
MonotoneOn f s → ∀ {a b : α}, a ∈ s → b ∈ s → f a < f b → a < breflect_lt (mem_image_of_mem: ∀ {α : Type ?u.18660} {β : Type ?u.18661} (f : α → β) {x : α} {a : Set α}, x ∈ a → f x ∈ f '' amem_image_of_mem _: ?m.18662 → ?m.18663_ hi: ?m.18594hi) (mem_image_of_mem: ∀ {α : Type ?u.18681} {β : Type ?u.18682} (f : α → β) {x : α} {a : Set α}, x ∈ a → f x ∈ f '' amem_image_of_mem _: ?m.18683 → ?m.18684_ hj: ?m.18600hj) hij: ?m.18603hij
#align monovary_on.comp_monotone_on_right MonovaryOn.comp_monotoneOn_right: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : LinearOrder β]
[inst_2 : Preorder γ] {f : ι → α} {g : ι → β} {g' : β → γ} {s : Set ι},
MonovaryOn f g s → MonotoneOn g' (g '' s) → MonovaryOn f (g' ∘ g) sMonovaryOn.comp_monotoneOn_right

theorem MonovaryOn.comp_antitoneOn_right: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : LinearOrder β]
[inst_2 : Preorder γ] {f : ι → α} {g : ι → β} {g' : β → γ} {s : Set ι},
MonovaryOn f g s → AntitoneOn g' (g '' s) → AntivaryOn f (g' ∘ g) sMonovaryOn.comp_antitoneOn_right (h: MonovaryOn f g sh : MonovaryOn: {ι : Type ?u.18767} →
{α : Type ?u.18766} →
{β : Type ?u.18765} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropMonovaryOn f: ι → αf g: ι → βg s: Set ιs) (hg: AntitoneOn g' (g '' s)hg : AntitoneOn: {α : Type ?u.18896} → {β : Type ?u.18895} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Set α → PropAntitoneOn g': β → γg' (g: ι → βg '' s: Set ιs)) :
AntivaryOn: {ι : Type ?u.18945} →
{α : Type ?u.18944} →
{β : Type ?u.18943} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropAntivaryOn f: ι → αf (g': β → γg' ∘ g: ι → βg) s: Set ιs := fun _: ?m.19000_ hi: ?m.19003hi _: ?m.19006_ hj: ?m.19009hj hij: ?m.19012hij =>
h: MonovaryOn f g sh hj: ?m.19009hj hi: ?m.19003hi <| hg: AntitoneOn g' (g '' s)hg.reflect_lt: ∀ {α : Type ?u.19027} {β : Type ?u.19026} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
AntitoneOn f s → ∀ {a b : α}, a ∈ s → b ∈ s → f a < f b → b < areflect_lt (mem_image_of_mem: ∀ {α : Type ?u.19069} {β : Type ?u.19070} (f : α → β) {x : α} {a : Set α}, x ∈ a → f x ∈ f '' amem_image_of_mem _: ?m.19071 → ?m.19072_ hi: ?m.19003hi) (mem_image_of_mem: ∀ {α : Type ?u.19090} {β : Type ?u.19091} (f : α → β) {x : α} {a : Set α}, x ∈ a → f x ∈ f '' amem_image_of_mem _: ?m.19092 → ?m.19093_ hj: ?m.19009hj) hij: ?m.19012hij
#align monovary_on.comp_antitone_on_right MonovaryOn.comp_antitoneOn_right: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : LinearOrder β]
[inst_2 : Preorder γ] {f : ι → α} {g : ι → β} {g' : β → γ} {s : Set ι},
MonovaryOn f g s → AntitoneOn g' (g '' s) → AntivaryOn f (g' ∘ g) sMonovaryOn.comp_antitoneOn_right

theorem AntivaryOn.comp_monotoneOn_right: ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : LinearOrder β]
[inst_2 : Preorder γ] {f : ι → α} {g : ι → β} {g' : β → γ} {s : Set ι},
AntivaryOn f g s → MonotoneOn g' (g '' s) → AntivaryOn f (g' ∘ g) sAntivaryOn.comp_monotoneOn_right (h: AntivaryOn f g sh : AntivaryOn: {ι : Type ?u.19176} →
{α : Type ?u.19175} →
{β : Type ?u.19174} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropAntivaryOn f: ι → αf g: ι → βg s: Set ιs) (hg: MonotoneOn g' (g '' s)hg : MonotoneOn: {α : Type ?u.19305} → {β : Type ?u.19304} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Set α → PropMonotoneOn g': β → γg' (g: ι → βg '' s: Set ιs)) :
AntivaryOn: {ι : Type ?u.19354} →
{α : Type ?u.19353} →
{β : Type ?u.19352} → [inst : Preorder α] → [inst : Preorder β] → (ι → α) → (ι → β) → Set ι → PropAntivaryOn f: ι → αf (g': β → γg' ∘ g: ι → βg) s: Set ιs := fun _: ?m.19409_ hi: ?m.19412hi _: ?m.19415_ hj: ?m.19418hj hij: ?m.19421hij =>
h: AntivaryOn f g sh hi: ?m.19412hi hj: ?m.19418hj <| hg: MonotoneOn g' (g '' s)hg.reflect_lt: ∀ {α : Type ?u.19436} {β : Type ?u.19435} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
MonotoneOn f s → ∀ {a b : α}, a ∈ s → b ∈ s → f a < f b → a < breflect_lt (mem_image_of_mem: ∀ {α : Type ?u.19478} {β : Type ?u.19479} (f : α → β) {x : α} {a : Set α}, x ∈ a → f x ∈ f '' amem_image_of_mem _: ?m.19480 → ?m.19481_ hi: ?m.19412hi) (mem_image_of_mem: ∀ {α : Type ?u.19499} {β : Type ?u.19500} (f : α → β) {x : α} {a : Set α}, x ∈ a → f x ∈ f '' amem_image_of_mem _: ?m.19501 → ?m.19502_ hj: ?m.19418hj) hij: ?m.19421hij
#align antivary_```