MonovaryOn on singleton, union, insert, and image

[UPSTREAM] mathlib's MonovaryOn API (Mathlib/Order/Monotone/Monovary.lean) has empty / subset / comp_right / comp_monotone_left, but lacks the structural set-building lemmas that Set.Pairwise enjoys (Set.pairwise_singleton / pairwise_union / pairwise_insert). This file fills the gap, modelled on the Set.Pairwise family lemma-for-lemma, plus the image companion of MonovaryOn.comp_right (which is the preimage form). Each pairs with its AntivaryOn twin, as every lemma in the mathlib file does.

Upstream home: section Preorder of Mathlib/Order/Monotone/Monovary.lean, beside MonovaryOn.empty and MonovaryOn.comp_right.

Main results

• monovaryOn_singleton / monovaryOn_union / monovaryOn_insert — the Set.pairwise_* analogues (and antivaryOn_* twins).
• monovaryOn_image — MonovaryOn f g (k '' u) ↔ MonovaryOn (f ∘ k) (g ∘ k) u, the image companion of MonovaryOn.comp_right (and antivaryOn_image twin).
• MonovaryOn and AntivaryOn on a finset are decidable, so decide checks them on finite data.

Monovary

@[simp]

theorem monovaryOn_singleton {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} (a : ι) : MonovaryOn f g {a}

MonovaryOn holds vacuously on a singleton: there is only one index.

theorem monovaryOn_union {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} {s t : Set ι} : MonovaryOn f g (s ∪ t) ↔ MonovaryOn f g s ∧ MonovaryOn f g t ∧ ∀ (a : ι), a ∈ s → ∀ (b : ι), b ∈ t → (g a < g b → f a ≤ f b) ∧ (g b < g a → f b ≤ f a)

MonovaryOn on a union: monovary on each part, plus neither part inverts the order against the other. The Monovary analogue of Set.pairwise_union.

theorem monovaryOn_insert {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} {s : Set ι} {a : ι} : MonovaryOn f g (insert a s) ↔ MonovaryOn f g s ∧ ∀ (b : ι), b ∈ s → (g a < g b → f a ≤ f b) ∧ (g b < g a → f b ≤ f a)

MonovaryOn on insert a s. The Monovary analogue of Set.pairwise_insert.

theorem monovaryOn_image {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} (k : ι' → ι) (u : Set ι') : MonovaryOn f g (k '' u) ↔ MonovaryOn (f ∘ k) (g ∘ k) u

MonovaryOn transports across an image: f, g monovary on k '' u iff f ∘ k, g ∘ k monovary on u. The image companion of MonovaryOn.comp_right (the preimage form).

Antivary

@[simp]

theorem antivaryOn_singleton {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} (a : ι) : AntivaryOn f g {a}

AntivaryOn holds vacuously on a singleton: there is only one index.

theorem antivaryOn_union {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} {s t : Set ι} : AntivaryOn f g (s ∪ t) ↔ AntivaryOn f g s ∧ AntivaryOn f g t ∧ ∀ (a : ι), a ∈ s → ∀ (b : ι), b ∈ t → (g a < g b → f b ≤ f a) ∧ (g b < g a → f a ≤ f b)

AntivaryOn on a union. The Antivary analogue of Set.pairwise_union.

theorem antivaryOn_insert {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} {s : Set ι} {a : ι} : AntivaryOn f g (insert a s) ↔ AntivaryOn f g s ∧ ∀ (b : ι), b ∈ s → (g a < g b → f b ≤ f a) ∧ (g b < g a → f a ≤ f b)

AntivaryOn on insert a s. The Antivary analogue of Set.pairwise_insert.

theorem antivaryOn_image {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} (k : ι' → ι) (u : Set ι') : AntivaryOn f g (k '' u) ↔ AntivaryOn (f ∘ k) (g ∘ k) u

AntivaryOn transports across an image. The image companion of AntivaryOn.comp_right.

Decidability

@[instance_reducible]

instance instDecidableMonovaryOnCoeFinsetOfDecidableLTOfDecidableLE_linglib {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} [DecidableLT β] [DecidableLE α] {t : Finset ι} : Decidable (MonovaryOn f g ↑t)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance instDecidableAntivaryOnCoeFinsetOfDecidableLTOfDecidableLE_linglib {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} [DecidableLT β] [DecidableLE α] {t : Finset ι} : Decidable (AntivaryOn f g ↑t)

Equations

• One or more equations did not get rendered due to their size.