Theorems · Theorem · order theory

monovaryOn_toDual_right

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

Defined in

Mathlib.Order.Monotone.Monovary

Cited by

4 results in Mathlib

Foundations

Depth 14 from the axioms · uses Quot.sound

Assumes

PreorderPreorder