Loogle!

Result

Found 416 declarations mentioning OrderDual.toDual. Of these, only the first 200 are shown.

• OrderDual.toDual 📋 Mathlib.Order.OrderDual
  {α : Type u_1} : α ≃ αᵒᵈ
• OrderDual.ofDual_symm_eq 📋 Mathlib.Order.OrderDual
  {α : Type u_1} : OrderDual.ofDual.symm = OrderDual.toDual
• OrderDual.toDual_symm_eq 📋 Mathlib.Order.OrderDual
  {α : Type u_1} : OrderDual.toDual.symm = OrderDual.ofDual
• OrderDual.toDual_trans_ofDual 📋 Mathlib.Order.OrderDual
  {α : Type u_1} : OrderDual.toDual.trans OrderDual.ofDual = Equiv.refl α
• OrderDual.ofDual_trans_toDual 📋 Mathlib.Order.OrderDual
  {α : Type u_1} : OrderDual.ofDual.trans OrderDual.toDual = Equiv.refl αᵒᵈ
• OrderDual.rec 📋 Mathlib.Order.OrderDual
  {α : Type u_1} {motive : αᵒᵈ → Sort u_2} (toDual : (a : α) → motive (OrderDual.toDual a)) (a : αᵒᵈ) : motive a
• OrderDual.forall 📋 Mathlib.Order.OrderDual
  {α : Type u_1} {p : αᵒᵈ → Prop} : (∀ (a : αᵒᵈ), p a) ↔ ∀ (a : α), p (OrderDual.toDual a)
• OrderDual.exists 📋 Mathlib.Order.OrderDual
  {α : Type u_1} {p : αᵒᵈ → Prop} : (∃ a, p a) ↔ ∃ a, p (OrderDual.toDual a)
• OrderDual.ofDual_toDual 📋 Mathlib.Order.OrderDual
  {α : Type u_1} (a : α) : OrderDual.ofDual (OrderDual.toDual a) = a
• OrderDual.toDual_ofDual 📋 Mathlib.Order.OrderDual
  {α : Type u_1} (a : αᵒᵈ) : OrderDual.toDual (OrderDual.ofDual a) = a
• OrderDual.ofDual_comp_toDual 📋 Mathlib.Order.OrderDual
  {α : Type u_1} : ⇑OrderDual.ofDual ∘ ⇑OrderDual.toDual = id
• OrderDual.toDual_inj 📋 Mathlib.Order.OrderDual
  {α : Type u_1} {a b : α} : OrderDual.toDual a = OrderDual.toDual b ↔ a = b
• OrderDual.toDual_comp_ofDual 📋 Mathlib.Order.OrderDual
  {α : Type u_1} : ⇑OrderDual.toDual ∘ ⇑OrderDual.ofDual = id
• LE.le.dual 📋 Mathlib.Order.OrderDual
  {α : Type u_1} [LE α] {a b : α} : b ≤ a → OrderDual.toDual a ≤ OrderDual.toDual b
• LT.lt.dual 📋 Mathlib.Order.OrderDual
  {α : Type u_1} [LT α] {a b : α} : b < a → OrderDual.toDual a < OrderDual.toDual b
• OrderDual.toDual_le_toDual 📋 Mathlib.Order.OrderDual
  {α : Type u_1} [LE α] {a b : α} : OrderDual.toDual a ≤ OrderDual.toDual b ↔ b ≤ a
• OrderDual.toDual_lt_toDual 📋 Mathlib.Order.OrderDual
  {α : Type u_1} [LT α] {a b : α} : OrderDual.toDual a < OrderDual.toDual b ↔ b < a
• OrderDual.le_toDual 📋 Mathlib.Order.OrderDual
  {α : Type u_1} [LE α] {a : αᵒᵈ} {b : α} : a ≤ OrderDual.toDual b ↔ b ≤ OrderDual.ofDual a
• OrderDual.lt_toDual 📋 Mathlib.Order.OrderDual
  {α : Type u_1} [LT α] {a : αᵒᵈ} {b : α} : a < OrderDual.toDual b ↔ b < OrderDual.ofDual a
• OrderDual.toDual_le 📋 Mathlib.Order.OrderDual
  {α : Type u_1} [LE α] {a : αᵒᵈ} {b : α} : OrderDual.toDual b ≤ a ↔ OrderDual.ofDual a ≤ b
• OrderDual.toDual_lt 📋 Mathlib.Order.OrderDual
  {α : Type u_1} [LT α] {a : αᵒᵈ} {b : α} : OrderDual.toDual b < a ↔ OrderDual.ofDual a < b
• IsBot.toDual 📋 Mathlib.Order.Max
  {α : Type u_1} [LE α] {a : α} : IsBot a → IsTop (OrderDual.toDual a)
• IsMax.toDual 📋 Mathlib.Order.Max
  {α : Type u_1} [LE α] {a : α} : IsMax a → IsMin (OrderDual.toDual a)
• IsMin.toDual 📋 Mathlib.Order.Max
  {α : Type u_1} [LE α] {a : α} : IsMin a → IsMax (OrderDual.toDual a)
• IsTop.toDual 📋 Mathlib.Order.Max
  {α : Type u_1} [LE α] {a : α} : IsTop a → IsBot (OrderDual.toDual a)
• isBot_toDual_iff 📋 Mathlib.Order.Max
  {α : Type u_1} [LE α] {a : α} : IsBot (OrderDual.toDual a) ↔ IsTop a
• isMax_toDual_iff 📋 Mathlib.Order.Max
  {α : Type u_1} [LE α] {a : α} : IsMax (OrderDual.toDual a) ↔ IsMin a
• isMin_toDual_iff 📋 Mathlib.Order.Max
  {α : Type u_1} [LE α] {a : α} : IsMin (OrderDual.toDual a) ↔ IsMax a
• isTop_toDual_iff 📋 Mathlib.Order.Max
  {α : Type u_1} [LE α] {a : α} : IsTop (OrderDual.toDual a) ↔ IsBot a
• OrderDual.toDual_bot 📋 Mathlib.Order.BoundedOrder.Basic
  (α : Type u) [Bot α] : OrderDual.toDual ⊥ = ⊤
• OrderDual.toDual_top 📋 Mathlib.Order.BoundedOrder.Basic
  (α : Type u) [Top α] : OrderDual.toDual ⊤ = ⊥
• OrderDual.toDual_eq_bot 📋 Mathlib.Order.BoundedOrder.Basic
  (α : Type u) [Top α] {a : α} : OrderDual.toDual a = ⊥ ↔ a = ⊤
• OrderDual.toDual_eq_top 📋 Mathlib.Order.BoundedOrder.Basic
  (α : Type u) [Bot α] {a : α} : OrderDual.toDual a = ⊤ ↔ a = ⊥
• toDual_compares_toDual 📋 Mathlib.Order.Compare
  {α : Type u_1} [LT α] {a b : α} {o : Ordering} : o.Compares (OrderDual.toDual a) (OrderDual.toDual b) ↔ o.Compares b a
• cmpLE_toDual 📋 Mathlib.Order.Compare
  {α : Type u_1} [LE α] [DecidableLE α] (x y : α) : cmpLE (OrderDual.toDual x) (OrderDual.toDual y) = cmpLE y x
• cmp_toDual 📋 Mathlib.Order.Compare
  {α : Type u_1} [LT α] [DecidableLT α] (x y : α) : cmp (OrderDual.toDual x) (OrderDual.toDual y) = cmp y x
• Antitone.dual_right 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} : Antitone f → Monotone (⇑OrderDual.toDual ∘ f)
• Monotone.dual_right 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} : Monotone f → Antitone (⇑OrderDual.toDual ∘ f)
• StrictAnti.dual_right 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} : StrictAnti f → StrictMono (⇑OrderDual.toDual ∘ f)
• StrictMono.dual_right 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} : StrictMono f → StrictAnti (⇑OrderDual.toDual ∘ f)
• antitone_toDual_comp_iff 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} : Antitone (⇑OrderDual.toDual ∘ f) ↔ Monotone f
• monotone_toDual_comp_iff 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} : Monotone (⇑OrderDual.toDual ∘ f) ↔ Antitone f
• strictAnti_toDual_comp_iff 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} : StrictAnti (⇑OrderDual.toDual ∘ f) ↔ StrictMono f
• strictMono_toDual_comp_iff 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} : StrictMono (⇑OrderDual.toDual ∘ f) ↔ StrictAnti f
• AntitoneOn.dual_right 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : AntitoneOn f s → MonotoneOn (⇑OrderDual.toDual ∘ f) s
• MonotoneOn.dual_right 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : MonotoneOn f s → AntitoneOn (⇑OrderDual.toDual ∘ f) s
• StrictAntiOn.dual_right 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : StrictAntiOn f s → StrictMonoOn (⇑OrderDual.toDual ∘ f) s
• StrictMonoOn.dual_right 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : StrictMonoOn f s → StrictAntiOn (⇑OrderDual.toDual ∘ f) s
• antitoneOn_toDual_comp_iff 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : AntitoneOn (⇑OrderDual.toDual ∘ f) s ↔ MonotoneOn f s
• monotoneOn_toDual_comp_iff 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : MonotoneOn (⇑OrderDual.toDual ∘ f) s ↔ AntitoneOn f s
• strictAntiOn_toDual_comp_iff 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : StrictAntiOn (⇑OrderDual.toDual ∘ f) s ↔ StrictMonoOn f s
• strictMonoOn_toDual_comp_iff 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : StrictMonoOn (⇑OrderDual.toDual ∘ f) s ↔ StrictAntiOn f s
• Antitone.dual 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} : Antitone f → Antitone (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual)
• Monotone.dual 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} : Monotone f → Monotone (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual)
• StrictAnti.dual 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} : StrictAnti f → StrictAnti (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual)
• StrictMono.dual 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} : StrictMono f → StrictMono (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual)
• antitone_dual_iff 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} : Antitone (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) ↔ Antitone f
• monotone_dual_iff 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} : Monotone (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) ↔ Monotone f
• strictAnti_dual_iff 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} : StrictAnti (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) ↔ StrictAnti f
• strictMono_dual_iff 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} : StrictMono (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) ↔ StrictMono f
• AntitoneOn.dual 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : AntitoneOn f s → AntitoneOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s
• MonotoneOn.dual 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : MonotoneOn f s → MonotoneOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s
• StrictAntiOn.dual 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : StrictAntiOn f s → StrictAntiOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s
• StrictMonoOn.dual 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : StrictMonoOn f s → StrictMonoOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s
• antitoneOn_dual_iff 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : AntitoneOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s ↔ AntitoneOn f s
• monotoneOn_dual_iff 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : MonotoneOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s ↔ MonotoneOn f s
• strictAntiOn_dual_iff 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : StrictAntiOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s ↔ StrictAntiOn f s
• strictMonoOn_dual_iff 📋 Mathlib.Order.Monotone.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : StrictMonoOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s ↔ StrictMonoOn f s
• toDual_inf 📋 Mathlib.Order.Lattice
  {α : Type u} [Min α] (a b : α) : OrderDual.toDual (a ⊓ b) = OrderDual.toDual a ⊔ OrderDual.toDual b
• toDual_sup 📋 Mathlib.Order.Lattice
  {α : Type u} [Max α] (a b : α) : OrderDual.toDual (a ⊔ b) = OrderDual.toDual a ⊓ OrderDual.toDual b
• toDual_max 📋 Mathlib.Order.Lattice
  {α : Type u} [LinearOrder α] (a b : α) : OrderDual.toDual (max a b) = min (OrderDual.toDual a) (OrderDual.toDual b)
• toDual_min 📋 Mathlib.Order.Lattice
  {α : Type u} [LinearOrder α] (a b : α) : OrderDual.toDual (min a b) = max (OrderDual.toDual a) (OrderDual.toDual b)
• Codisjoint.dual 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [PartialOrder α] [OrderTop α] {a b : α} : Codisjoint a b → Disjoint (OrderDual.toDual a) (OrderDual.toDual b)
• Disjoint.dual 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [PartialOrder α] [OrderBot α] {a b : α} : Disjoint a b → Codisjoint (OrderDual.toDual a) (OrderDual.toDual b)
• IsCompl.dual 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [PartialOrder α] [BoundedOrder α] {x y : α} (h : IsCompl x y) : IsCompl (OrderDual.toDual x) (OrderDual.toDual y)
• codisjoint_toDual_iff 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [PartialOrder α] [OrderBot α] {a b : α} : Codisjoint (OrderDual.toDual a) (OrderDual.toDual b) ↔ Disjoint a b
• disjoint_toDual_iff 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [PartialOrder α] [OrderTop α] {a b : α} : Disjoint (OrderDual.toDual a) (OrderDual.toDual b) ↔ Codisjoint a b
• isCompl_toDual_iff 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [Lattice α] [BoundedOrder α] {a b : α} : IsCompl (OrderDual.toDual a) (OrderDual.toDual b) ↔ IsCompl a b
• GaloisCoinsertion.dual 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} : GaloisCoinsertion l u → GaloisInsertion (⇑OrderDual.toDual ∘ u ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ l ∘ ⇑OrderDual.ofDual)
• GaloisConnection.dual 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : GaloisConnection (⇑OrderDual.toDual ∘ u ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ l ∘ ⇑OrderDual.ofDual)
• GaloisInsertion.dual 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {u : α → β} {l : β → α} : GaloisInsertion l u → GaloisCoinsertion (⇑OrderDual.toDual ∘ u ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ l ∘ ⇑OrderDual.ofDual)
• GaloisCoinsertion.ofDual 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : αᵒᵈ → βᵒᵈ} {u : βᵒᵈ → αᵒᵈ} : GaloisCoinsertion l u → GaloisInsertion (⇑OrderDual.ofDual ∘ u ∘ ⇑OrderDual.toDual) (⇑OrderDual.ofDual ∘ l ∘ ⇑OrderDual.toDual)
• GaloisInsertion.ofDual 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {u : αᵒᵈ → βᵒᵈ} {l : βᵒᵈ → αᵒᵈ} : GaloisInsertion l u → GaloisCoinsertion (⇑OrderDual.ofDual ∘ u ∘ ⇑OrderDual.toDual) (⇑OrderDual.ofDual ∘ l ∘ ⇑OrderDual.toDual)
• toDual_compl 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [HeytingAlgebra α] (a : α) : OrderDual.toDual aᶜ = ￢OrderDual.toDual a
• toDual_hnot 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [CoheytingAlgebra α] (a : α) : OrderDual.toDual (￢a) = (OrderDual.toDual a)ᶜ
• toDual_himp 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [HeytingAlgebra α] (a b : α) : OrderDual.toDual (a ⇨ b) = OrderDual.toDual b \ OrderDual.toDual a
• toDual_sdiff 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [CoheytingAlgebra α] (a b : α) : OrderDual.toDual (b \ a) = OrderDual.toDual a ⇨ OrderDual.toDual b
• toDual_bihimp 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b : α) : OrderDual.toDual (bihimp a b) = symmDiff (OrderDual.toDual a) (OrderDual.toDual b)
• toDual_symmDiff 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a b : α) : OrderDual.toDual (symmDiff a b) = bihimp (OrderDual.toDual a) (OrderDual.toDual b)
• OrderIso.dualDual_apply 📋 Mathlib.Order.Hom.Basic
  {α : Type u_2} [LE α] (a : α) : (OrderIso.dualDual α) a = OrderDual.toDual (OrderDual.toDual a)
• OrderIso.coe_dualDual 📋 Mathlib.Order.Hom.Basic
  (α : Type u_2) [LE α] : ⇑(OrderIso.dualDual α) = ⇑OrderDual.toDual ∘ ⇑OrderDual.toDual
• OrderIso.dual_apply 📋 Mathlib.Order.Hom.Basic
  {α : Type u_2} {β : Type u_3} [LE α] [LE β] (f : α ≃o β) (x : αᵒᵈ) : f.dual x = OrderDual.toDual (f (OrderDual.ofDual x))
• OrderIso.dual_symm_apply 📋 Mathlib.Order.Hom.Basic
  {α : Type u_2} {β : Type u_3} [LE α] [LE β] (f : α ≃o β) (x : βᵒᵈ) : f.dual.symm x = OrderDual.toDual (f.symm (OrderDual.ofDual x))
• OrderHom.dual_apply_coe 📋 Mathlib.Order.Hom.Basic
  {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) (a✝ : αᵒᵈ) : (OrderHom.dual f) a✝ = (⇑OrderDual.toDual ∘ ⇑f ∘ ⇑OrderDual.ofDual) a✝
• OrderHom.dual_symm_apply_coe 📋 Mathlib.Order.Hom.Basic
  {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : αᵒᵈ →o βᵒᵈ) (a✝ : α) : (OrderHom.dual.symm f) a✝ = (⇑OrderDual.ofDual ∘ ⇑f ∘ ⇑OrderDual.toDual) a✝
• OrderIso.inv_apply 📋 Mathlib.Algebra.Order.Group.OrderIso
  (α : Type u) [Group α] [LE α] [MulLeftMono α] [MulRightMono α] (a✝ : α) : (OrderIso.inv α) a✝ = OrderDual.toDual a✝⁻¹
• OrderIso.neg_apply 📋 Mathlib.Algebra.Order.Group.OrderIso
  (α : Type u) [AddGroup α] [LE α] [AddLeftMono α] [AddRightMono α] (a✝ : α) : (OrderIso.neg α) a✝ = OrderDual.toDual (-a✝)
• OrderIso.divLeft_apply 📋 Mathlib.Algebra.Order.Group.OrderIso
  {α : Type u} [Group α] [LE α] [MulLeftMono α] [MulRightMono α] (a a✝ : α) : (OrderIso.divLeft a) a✝ = OrderDual.toDual (a / a✝)
• OrderIso.subLeft_apply 📋 Mathlib.Algebra.Order.Group.OrderIso
  {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] [AddRightMono α] (a a✝ : α) : (OrderIso.subLeft a) a✝ = OrderDual.toDual (a - a✝)
• toDual_one 📋 Mathlib.Algebra.Order.Group.Synonym
  {α : Type u_1} [One α] : OrderDual.toDual 1 = 1
• toDual_zero 📋 Mathlib.Algebra.Order.Group.Synonym
  {α : Type u_1} [Zero α] : OrderDual.toDual 0 = 0
• isAddLeftRegular_toDual 📋 Mathlib.Algebra.Order.Group.Synonym
  {α : Type u_1} [AddMonoid α] {a : α} : IsAddLeftRegular (OrderDual.toDual a) ↔ IsAddLeftRegular a
• isAddRegular_toDual 📋 Mathlib.Algebra.Order.Group.Synonym
  {α : Type u_1} [AddMonoid α] {a : α} : IsAddRegular (OrderDual.toDual a) ↔ IsAddRegular a
• isAddRightRegular_toDual 📋 Mathlib.Algebra.Order.Group.Synonym
  {α : Type u_1} [AddMonoid α] {a : α} : IsAddRightRegular (OrderDual.toDual a) ↔ IsAddRightRegular a
• isLeftRegular_toDual 📋 Mathlib.Algebra.Order.Group.Synonym
  {α : Type u_1} [Monoid α] {a : α} : IsLeftRegular (OrderDual.toDual a) ↔ IsLeftRegular a
• isRegular_toDual 📋 Mathlib.Algebra.Order.Group.Synonym
  {α : Type u_1} [Monoid α] {a : α} : IsRegular (OrderDual.toDual a) ↔ IsRegular a
• isRightRegular_toDual 📋 Mathlib.Algebra.Order.Group.Synonym
  {α : Type u_1} [Monoid α] {a : α} : IsRightRegular (OrderDual.toDual a) ↔ IsRightRegular a
• toDual_eq_one 📋 Mathlib.Algebra.Order.Group.Synonym
  {α : Type u_1} [One α] {a : α} : OrderDual.toDual a = 1 ↔ a = 1
• toDual_eq_zero 📋 Mathlib.Algebra.Order.Group.Synonym
  {α : Type u_1} [Zero α] {a : α} : OrderDual.toDual a = 0 ↔ a = 0
• pow_toDual 📋 Mathlib.Algebra.Order.Group.Synonym
  {α : Type u_1} {β : Type u_2} [Pow α β] (a : α) (b : β) : a ^ OrderDual.toDual b = a ^ b
• toDual_smul' 📋 Mathlib.Algebra.Order.Group.Synonym
  {β : Type u_2} {α : Type u_1} [SMul β α] (b : β) (a : α) : OrderDual.toDual b • a = b • a
• toDual_vadd' 📋 Mathlib.Algebra.Order.Group.Synonym
  {β : Type u_2} {α : Type u_1} [VAdd β α] (b : β) (a : α) : OrderDual.toDual b +ᵥ a = b +ᵥ a
• toDual_inv 📋 Mathlib.Algebra.Order.Group.Synonym
  {α : Type u_1} [Inv α] (a : α) : OrderDual.toDual a⁻¹ = (OrderDual.toDual a)⁻¹
• toDual_neg 📋 Mathlib.Algebra.Order.Group.Synonym
  {α : Type u_1} [Neg α] (a : α) : OrderDual.toDual (-a) = -OrderDual.toDual a
• toDual_pow 📋 Mathlib.Algebra.Order.Group.Synonym
  {α : Type u_1} {β : Type u_2} [Pow α β] (a : α) (b : β) : OrderDual.toDual (a ^ b) = OrderDual.toDual a ^ b
• toDual_smul 📋 Mathlib.Algebra.Order.Group.Synonym
  {β : Type u_2} {α : Type u_1} [SMul β α] (b : β) (a : α) : OrderDual.toDual (b • a) = b • OrderDual.toDual a
• toDual_vadd 📋 Mathlib.Algebra.Order.Group.Synonym
  {β : Type u_2} {α : Type u_1} [VAdd β α] (b : β) (a : α) : OrderDual.toDual (b +ᵥ a) = b +ᵥ OrderDual.toDual a
• toDual_add 📋 Mathlib.Algebra.Order.Group.Synonym
  {α : Type u_1} [Add α] (a b : α) : OrderDual.toDual (a + b) = OrderDual.toDual a + OrderDual.toDual b
• toDual_div 📋 Mathlib.Algebra.Order.Group.Synonym
  {α : Type u_1} [Div α] (a b : α) : OrderDual.toDual (a / b) = OrderDual.toDual a / OrderDual.toDual b
• toDual_mul 📋 Mathlib.Algebra.Order.Group.Synonym
  {α : Type u_1} [Mul α] (a b : α) : OrderDual.toDual (a * b) = OrderDual.toDual a * OrderDual.toDual b
• toDual_sub 📋 Mathlib.Algebra.Order.Group.Synonym
  {α : Type u_1} [Sub α] (a b : α) : OrderDual.toDual (a - b) = OrderDual.toDual a - OrderDual.toDual b
• WithBot.toDual_apply_coe 📋 Mathlib.Order.WithBot
  {α : Type u_1} (a : α) : WithBot.toDual ↑a = ↑(OrderDual.toDual a)
• WithTop.toDual_apply_coe 📋 Mathlib.Order.WithBot
  {α : Type u_1} (a : α) : WithTop.toDual ↑a = ↑(OrderDual.toDual a)
• WithBot.map_toDual 📋 Mathlib.Order.WithBot
  {α : Type u_1} {β : Type u_2} (f : αᵒᵈ → βᵒᵈ) (a : WithBot α) : WithBot.map f (WithBot.toDual a) = WithBot.map (⇑OrderDual.toDual ∘ f) a
• WithTop.map_toDual 📋 Mathlib.Order.WithBot
  {α : Type u_1} {β : Type u_2} (f : αᵒᵈ → βᵒᵈ) (a : WithTop α) : WithTop.map f (WithTop.toDual a) = WithTop.map (⇑OrderDual.toDual ∘ f) a
• WithBot.toDual_map 📋 Mathlib.Order.WithBot
  {α : Type u_1} {β : Type u_2} (f : α → β) (a : WithBot α) : WithBot.toDual (WithBot.map f a) = WithTop.map (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) (WithBot.toDual a)
• WithTop.toDual_map 📋 Mathlib.Order.WithBot
  {α : Type u_1} {β : Type u_2} (f : α → β) (a : WithTop α) : WithTop.toDual (WithTop.map f a) = WithBot.map (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) (WithTop.toDual a)
• WithBot.ofDual_map 📋 Mathlib.Order.WithBot
  {α : Type u_1} {β : Type u_2} (f : αᵒᵈ → βᵒᵈ) (a : WithBot αᵒᵈ) : WithBot.ofDual (WithBot.map f a) = WithTop.map (⇑OrderDual.ofDual ∘ f ∘ ⇑OrderDual.toDual) (WithBot.ofDual a)
• WithTop.ofDual_map 📋 Mathlib.Order.WithBot
  {α : Type u_1} {β : Type u_2} (f : αᵒᵈ → βᵒᵈ) (a : WithTop αᵒᵈ) : WithTop.ofDual (WithTop.map f a) = WithBot.map (⇑OrderDual.ofDual ∘ f ∘ ⇑OrderDual.toDual) (WithTop.ofDual a)
• toDual_intCast 📋 Mathlib.Algebra.Order.Ring.Synonym
  {R : Type u_1} [IntCast R] (n : ℤ) : OrderDual.toDual ↑n = ↑n
• toDual_natCast 📋 Mathlib.Algebra.Order.Ring.Synonym
  {R : Type u_1} [NatCast R] (n : ℕ) : OrderDual.toDual ↑n = ↑n
• toDual_ofNat 📋 Mathlib.Algebra.Order.Ring.Synonym
  {R : Type u_1} [NatCast R] (n : ℕ) [n.AtLeastTwo] : OrderDual.toDual (OfNat.ofNat n) = OfNat.ofNat n
• toDual_ratCast 📋 Mathlib.Algebra.Field.Basic
  {K : Type u_1} [RatCast K] (n : ℚ) : OrderDual.toDual ↑n = ↑n
• OrderIso.dualAntisymmetrization_apply 📋 Mathlib.Order.Antisymmetrization
  (α : Type u_1) [Preorder α] (a : α) : (OrderIso.dualAntisymmetrization α) (OrderDual.toDual (toAntisymmetrization (fun x1 x2 => x1 ≤ x2) a)) = toAntisymmetrization (fun x1 x2 => x1 ≤ x2) (OrderDual.toDual a)
• OrderIso.dualAntisymmetrization_symm_apply 📋 Mathlib.Order.Antisymmetrization
  (α : Type u_1) [Preorder α] (a : α) : (OrderIso.dualAntisymmetrization α).symm (toAntisymmetrization (fun x1 x2 => x1 ≤ x2) (OrderDual.toDual a)) = OrderDual.toDual (toAntisymmetrization (fun x1 x2 => x1 ≤ x2) a)
• Set.Ici_ofDual 📋 Mathlib.Order.Interval.Set.Basic
  {α : Type u_1} [Preorder α] {x : αᵒᵈ} : Set.Ici (OrderDual.ofDual x) = ⇑OrderDual.toDual ⁻¹' Set.Iic x
• Set.Ici_toDual 📋 Mathlib.Order.Interval.Set.Basic
  {α : Type u_1} [Preorder α] {a : α} : Set.Ici (OrderDual.toDual a) = ⇑OrderDual.ofDual ⁻¹' Set.Iic a
• Set.Iic_ofDual 📋 Mathlib.Order.Interval.Set.Basic
  {α : Type u_1} [Preorder α] {x : αᵒᵈ} : Set.Iic (OrderDual.ofDual x) = ⇑OrderDual.toDual ⁻¹' Set.Ici x
• Set.Iic_toDual 📋 Mathlib.Order.Interval.Set.Basic
  {α : Type u_1} [Preorder α] {a : α} : Set.Iic (OrderDual.toDual a) = ⇑OrderDual.ofDual ⁻¹' Set.Ici a
• Set.Iio_ofDual 📋 Mathlib.Order.Interval.Set.Basic
  {α : Type u_1} [Preorder α] {x : αᵒᵈ} : Set.Iio (OrderDual.ofDual x) = ⇑OrderDual.toDual ⁻¹' Set.Ioi x
• Set.Iio_toDual 📋 Mathlib.Order.Interval.Set.Basic
  {α : Type u_1} [Preorder α] {a : α} : Set.Iio (OrderDual.toDual a) = ⇑OrderDual.ofDual ⁻¹' Set.Ioi a
• Set.Ioi_ofDual 📋 Mathlib.Order.Interval.Set.Basic
  {α : Type u_1} [Preorder α] {x : αᵒᵈ} : Set.Ioi (OrderDual.ofDual x) = ⇑OrderDual.toDual ⁻¹' Set.Iio x
• Set.Ioi_toDual 📋 Mathlib.Order.Interval.Set.Basic
  {α : Type u_1} [Preorder α] {a : α} : Set.Ioi (OrderDual.toDual a) = ⇑OrderDual.ofDual ⁻¹' Set.Iio a
• Set.Icc_toDual 📋 Mathlib.Order.Interval.Set.Basic
  {α : Type u_1} [Preorder α] {a b : α} : Set.Icc (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' Set.Icc b a
• Set.Ico_toDual 📋 Mathlib.Order.Interval.Set.Basic
  {α : Type u_1} [Preorder α] {a b : α} : Set.Ico (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' Set.Ioc b a
• Set.Ioc_toDual 📋 Mathlib.Order.Interval.Set.Basic
  {α : Type u_1} [Preorder α] {a b : α} : Set.Ioc (OrderDual.toDual b) (OrderDual.toDual a) = ⇑OrderDual.ofDual ⁻¹' Set.Ico a b
• Set.Ioo_toDual 📋 Mathlib.Order.Interval.Set.Basic
  {α : Type u_1} [Preorder α] {a b : α} : Set.Ioo (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' Set.Ioo b a
• Set.Icc_ofDual 📋 Mathlib.Order.Interval.Set.Basic
  {α : Type u_1} [Preorder α] {x y : αᵒᵈ} : Set.Icc (OrderDual.ofDual y) (OrderDual.ofDual x) = ⇑OrderDual.toDual ⁻¹' Set.Icc x y
• Set.Ico_ofDual 📋 Mathlib.Order.Interval.Set.Basic
  {α : Type u_1} [Preorder α] {x y : αᵒᵈ} : Set.Ico (OrderDual.ofDual y) (OrderDual.ofDual x) = ⇑OrderDual.toDual ⁻¹' Set.Ioc x y
• Set.Ioc_ofDual 📋 Mathlib.Order.Interval.Set.Basic
  {α : Type u_1} [Preorder α] {x y : αᵒᵈ} : Set.Ioc (OrderDual.ofDual x) (OrderDual.ofDual y) = ⇑OrderDual.toDual ⁻¹' Set.Ico y x
• Set.Ioo_ofDual 📋 Mathlib.Order.Interval.Set.Basic
  {α : Type u_1} [Preorder α] {x y : αᵒᵈ} : Set.Ioo (OrderDual.ofDual y) (OrderDual.ofDual x) = ⇑OrderDual.toDual ⁻¹' Set.Ioo x y
• bddAbove_preimage_toDual 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set αᵒᵈ} : BddAbove (⇑OrderDual.toDual ⁻¹' s) ↔ BddBelow s
• bddBelow_preimage_toDual 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set αᵒᵈ} : BddBelow (⇑OrderDual.toDual ⁻¹' s) ↔ BddAbove s
• IsGLB.dual 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : IsGLB s a) : IsLUB (⇑OrderDual.ofDual ⁻¹' s) (OrderDual.toDual a)
• IsGreatest.dual 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : IsGreatest s a) : IsLeast (⇑OrderDual.ofDual ⁻¹' s) (OrderDual.toDual a)
• IsLUB.dual 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : IsLUB s a) : IsGLB (⇑OrderDual.ofDual ⁻¹' s) (OrderDual.toDual a)
• IsLeast.dual 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : IsLeast s a) : IsGreatest (⇑OrderDual.ofDual ⁻¹' s) (OrderDual.toDual a)
• OrderIso.compl_apply 📋 Mathlib.Order.Hom.Set
  (α : Type u_1) [BooleanAlgebra α] (a✝ : α) : (OrderIso.compl α) a✝ = (OrderDual.toDual a✝)ᶜ
• ofDual_sInf 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_1} [SupSet α] (s : Set αᵒᵈ) : OrderDual.ofDual (sInf s) = sSup (⇑OrderDual.toDual ⁻¹' s)
• ofDual_sSup 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_1} [InfSet α] (s : Set αᵒᵈ) : OrderDual.ofDual (sSup s) = sInf (⇑OrderDual.toDual ⁻¹' s)
• toDual_sInf 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_1} [InfSet α] (s : Set α) : OrderDual.toDual (sInf s) = sSup (⇑OrderDual.ofDual ⁻¹' s)
• toDual_sSup 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_1} [SupSet α] (s : Set α) : OrderDual.toDual (sSup s) = sInf (⇑OrderDual.ofDual ⁻¹' s)
• toDual_iInf 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_1} {ι : Sort u_3} [InfSet α] (f : ι → α) : OrderDual.toDual (⨅ i, f i) = ⨆ i, OrderDual.toDual (f i)
• toDual_iSup 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_1} {ι : Sort u_3} [SupSet α] (f : ι → α) : OrderDual.toDual (⨆ i, f i) = ⨅ i, OrderDual.toDual (f i)
• gc_Ici_sInf 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} [CompleteSemilatticeInf α] : GaloisConnection (⇑OrderDual.toDual ∘ Set.Ici) (sInf ∘ ⇑OrderDual.ofDual)
• gciIciSInf 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} [CompleteSemilatticeInf α] : GaloisCoinsertion (⇑OrderDual.toDual ∘ Set.Ici) (sInf ∘ ⇑OrderDual.ofDual)
• gci_Ici_sInf 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} [CompleteSemilatticeInf α] : GaloisCoinsertion (⇑OrderDual.toDual ∘ Set.Ici) (sInf ∘ ⇑OrderDual.ofDual)
• isGLB_image2_of_isGLB_isLUB 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {s : Set α} {t : Set β} {u : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} {a₀ : α} {b₀ : β} (h₁ : ∀ (b : β), GaloisConnection (u₁ b) (Function.swap u b)) (h₂ : ∀ (a : α), GaloisConnection (⇑OrderDual.toDual ∘ u₂ a) (u a ∘ ⇑OrderDual.ofDual)) (ha₀ : IsGLB s a₀) (hb₀ : IsLUB t b₀) : IsGLB (Set.image2 u s t) (u a₀ b₀)
• isGLB_image2_of_isLUB_isGLB 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {s : Set α} {t : Set β} {u : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} {a₀ : α} {b₀ : β} (h₁ : ∀ (b : β), GaloisConnection (⇑OrderDual.toDual ∘ u₁ b) (Function.swap u b ∘ ⇑OrderDual.ofDual)) (h₂ : ∀ (a : α), GaloisConnection (u₂ a) (u a)) (ha₀ : IsLUB s a₀) (hb₀ : IsGLB t b₀) : IsGLB (Set.image2 u s t) (u a₀ b₀)
• isLUB_image2_of_isGLB_isLUB 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} {a₀ : α} {b₀ : β} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)) (ha₀ : IsGLB s a₀) (hb₀ : IsLUB t b₀) : IsLUB (Set.image2 l s t) (l a₀ b₀)
• isLUB_image2_of_isLUB_isGLB 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} {a₀ : α} {b₀ : β} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b) (u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₂ a)) (ha₀ : IsLUB s a₀) (hb₀ : IsGLB t b₀) : IsLUB (Set.image2 l s t) (l a₀ b₀)
• sInf_image2_eq_sInf_sSup 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] {s : Set α} {t : Set β} {u : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (u₁ b) (Function.swap u b)) (h₂ : ∀ (a : α), GaloisConnection (⇑OrderDual.toDual ∘ u₂ a) (u a ∘ ⇑OrderDual.ofDual)) : sInf (Set.image2 u s t) = u (sInf s) (sSup t)
• sInf_image2_eq_sSup_sInf 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] {s : Set α} {t : Set β} {u : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (⇑OrderDual.toDual ∘ u₁ b) (Function.swap u b ∘ ⇑OrderDual.ofDual)) (h₂ : ∀ (a : α), GaloisConnection (u₂ a) (u a)) : sInf (Set.image2 u s t) = u (sSup s) (sInf t)
• sSup_image2_eq_sInf_sSup 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)) : sSup (Set.image2 l s t) = l (sInf s) (sSup t)
• sSup_image2_eq_sSup_sInf 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b) (u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₂ a)) : sSup (Set.image2 l s t) = l (sSup s) (sInf t)
• isGLB_image2_of_isLUB_isLUB 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {s : Set α} {t : Set β} {u : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} {a₀ : α} {b₀ : β} (h₁ : ∀ (b : β), GaloisConnection (⇑OrderDual.toDual ∘ u₁ b) (Function.swap u b ∘ ⇑OrderDual.ofDual)) (h₂ : ∀ (a : α), GaloisConnection (⇑OrderDual.toDual ∘ u₂ a) (u a ∘ ⇑OrderDual.ofDual)) (ha₀ : IsLUB s a₀) (hb₀ : IsLUB t b₀) : IsGLB (Set.image2 u s t) (u a₀ b₀)
• isLUB_image2_of_isGLB_isGLB 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} {a₀ : α} {b₀ : β} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₂ a)) (ha₀ : IsGLB s a₀) (hb₀ : IsGLB t b₀) : IsLUB (Set.image2 l s t) (l a₀ b₀)
• sInf_image2_eq_sSup_sSup 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] {s : Set α} {t : Set β} {u : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (⇑OrderDual.toDual ∘ u₁ b) (Function.swap u b ∘ ⇑OrderDual.ofDual)) (h₂ : ∀ (a : α), GaloisConnection (⇑OrderDual.toDual ∘ u₂ a) (u a ∘ ⇑OrderDual.ofDual)) : sInf (Set.image2 u s t) = u (sSup s) (sSup t)
• sSup_image2_eq_sInf_sInf 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₂ a)) : sSup (Set.image2 l s t) = l (sInf s) (sInf t)
• csInf_image2_eq_csInf_csSup 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {s : Set α} {t : Set β} {u : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (l₁ b) (Function.swap u b)) (h₂ : ∀ (a : α), GaloisConnection (⇑OrderDual.toDual ∘ l₂ a) (u a ∘ ⇑OrderDual.ofDual)) : s.Nonempty → BddBelow s → t.Nonempty → BddAbove t → sInf (Set.image2 u s t) = u (sInf s) (sSup t)
• csInf_image2_eq_csSup_csInf 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {s : Set α} {t : Set β} {u : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (⇑OrderDual.toDual ∘ l₁ b) (Function.swap u b ∘ ⇑OrderDual.ofDual)) (h₂ : ∀ (a : α), GaloisConnection (l₂ a) (u a)) : s.Nonempty → BddAbove s → t.Nonempty → BddBelow t → sInf (Set.image2 u s t) = u (sSup s) (sInf t)
• csSup_image2_eq_csInf_csSup 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)) : s.Nonempty → BddBelow s → t.Nonempty → BddAbove t → sSup (Set.image2 l s t) = l (sInf s) (sSup t)
• csSup_image2_eq_csSup_csInf 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b) (u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₂ a)) : s.Nonempty → BddAbove s → t.Nonempty → BddBelow t → sSup (Set.image2 l s t) = l (sSup s) (sInf t)
• csInf_image2_eq_csSup_csSup 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {s : Set α} {t : Set β} {u : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (⇑OrderDual.toDual ∘ l₁ b) (Function.swap u b ∘ ⇑OrderDual.ofDual)) (h₂ : ∀ (a : α), GaloisConnection (⇑OrderDual.toDual ∘ l₂ a) (u a ∘ ⇑OrderDual.ofDual)) : s.Nonempty → BddAbove s → t.Nonempty → BddAbove t → sInf (Set.image2 u s t) = u (sSup s) (sSup t)
• csSup_image2_eq_csInf_csInf 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₂ a)) : s.Nonempty → BddBelow s → t.Nonempty → BddBelow t → sSup (Set.image2 l s t) = l (sInf s) (sInf t)
• Set.uIcc_toDual 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} [Lattice α] (a b : α) : Set.uIcc (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' Set.uIcc a b
• Set.uIoo_toDual 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} [LinearOrder α] (a b : α) : Set.uIoo (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' Set.uIoo a b
• Set.uIcc_ofDual 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} [Lattice α] (a b : αᵒᵈ) : Set.uIcc (OrderDual.ofDual a) (OrderDual.ofDual b) = ⇑OrderDual.toDual ⁻¹' Set.uIcc a b
• Set.uIoo_ofDual 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} [LinearOrder α] (a b : αᵒᵈ) : Set.uIoo (OrderDual.ofDual a) (OrderDual.ofDual b) = ⇑OrderDual.toDual ⁻¹' Set.uIoo a b
• Fin.revOrderIso_symm_apply 📋 Mathlib.Order.Fin.Basic
  {n : ℕ} (i : Fin n) : Fin.revOrderIso.symm i = OrderDual.toDual i.rev
• List.SortedGE.map_toDual 📋 Mathlib.Data.List.Sort
  {α : Type u_1} [Preorder α] {l : List α} : (List.map (⇑OrderDual.toDual) l).SortedGE → l.SortedLE
• List.SortedGE.of_map_toDual 📋 Mathlib.Data.List.Sort
  {α : Type u_1} [Preorder α] {l : List α} : l.SortedGE → (List.map (⇑OrderDual.toDual) l).SortedLE
• List.SortedGT.of_map_toDual 📋 Mathlib.Data.List.Sort
  {α : Type u_1} [Preorder α] {l : List α} : l.SortedGT → (List.map (⇑OrderDual.toDual) l).SortedLT
• List.SortedLE.map_toDual 📋 Mathlib.Data.List.Sort
  {α : Type u_1} [Preorder α] {l : List α} : (List.map (⇑OrderDual.toDual) l).SortedLE → l.SortedGE
• List.SortedLE.of_map_toDual 📋 Mathlib.Data.List.Sort
  {α : Type u_1} [Preorder α] {l : List α} : l.SortedLE → (List.map (⇑OrderDual.toDual) l).SortedGE
• List.SortedLT.map_toDual 📋 Mathlib.Data.List.Sort
  {α : Type u_1} [Preorder α] {l : List α} : (List.map (⇑OrderDual.toDual) l).SortedLT → l.SortedGT
• List.sortedGE_map_toDual 📋 Mathlib.Data.List.Sort
  {α : Type u_1} [Preorder α] {l : List α} : (List.map (⇑OrderDual.toDual) l).SortedGE ↔ l.SortedLE
• List.sortedLE_map_toDual 📋 Mathlib.Data.List.Sort
  {α : Type u_1} [Preorder α] {l : List α} : (List.map (⇑OrderDual.toDual) l).SortedLE ↔ l.SortedGE
• List.sortedLT_map_toDual 📋 Mathlib.Data.List.Sort
  {α : Type u_1} [Preorder α] {l : List α} : (List.map (⇑OrderDual.toDual) l).SortedLT ↔ l.SortedGT
• List.SortedGT.map_toDual 📋 Mathlib.Data.List.Sort
  {α : Type u_1} [Preorder α] {l : List αᵒᵈ} : (List.map (⇑OrderDual.toDual) l).SortedGT → l.SortedLT

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 69fae59