Theorems · Theorem · order theory

AntivaryOn.dual_right

∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
  {s : Set ι}, AntivaryOn f g s → MonovaryOn f (⇑OrderDual.toDual ∘ g) s

Defined in

Mathlib.Order.Monotone.Monovary

Cited by

5 results in Mathlib

Foundations

Depth 14 from the axioms · uses Quot.sound

Assumes

PreorderPreorder