Loogle!

Result

Found 165 declarations mentioning Function.swap.

• Function.swap 📋 Mathlib.Logic.Function.Defs
  {α : Sort u₁} {β : Sort u₂} {φ : α → β → Sort u₃} (f : (x : α) → (y : β) → φ x y) (y : β) (x : α) : φ x y
• Function.swap_def 📋 Mathlib.Logic.Function.Defs
  {α : Sort u₁} {β : Sort u₂} {φ : α → β → Sort u₃} (f : (x : α) → (y : β) → φ x y) : Function.swap f = fun y x => f x y
• Function.swap_ge 📋 Mathlib.Logic.Function.Basic
  {α : Type u_4} [LE α] : (Function.swap fun x1 x2 => x1 ≥ x2) = fun x1 x2 => x1 ≤ x2
• Function.swap_gt 📋 Mathlib.Logic.Function.Basic
  {α : Type u_4} [LT α] : (Function.swap fun x1 x2 => x1 > x2) = fun x1 x2 => x1 < x2
• Function.swap_le 📋 Mathlib.Logic.Function.Basic
  {α : Type u_4} [LE α] : (Function.swap fun x1 x2 => x1 ≤ x2) = fun x1 x2 => x1 ≥ x2
• Function.swap_lt 📋 Mathlib.Logic.Function.Basic
  {α : Type u_4} [LT α] : (Function.swap fun x1 x2 => x1 < x2) = fun x1 x2 => x1 > x2
• Symmetric.swap_eq 📋 Mathlib.Logic.Relation
  {α : Sort u_1} {r : α → α → Prop} : Symmetric r → Function.swap r = r
• swap_eq_iff 📋 Mathlib.Logic.Relation
  {α : Sort u_1} {r : α → α → Prop} : Function.swap r = r ↔ Symmetric r
• Relation.symmGen_swap 📋 Mathlib.Logic.Relation
  {α : Sort u_1} (r : α → α → Prop) : Relation.SymmGen (Function.swap r) = Relation.SymmGen r
• Relation.ReflTransGen.swap 📋 Mathlib.Logic.Relation
  {α : Sort u_1} {r : α → α → Prop} {a b : α} (h : Relation.ReflTransGen r b a) : Relation.ReflTransGen (Function.swap r) a b
• Relation.SymmGen.swap 📋 Mathlib.Logic.Relation
  {α : Sort u_1} {r : α → α → Prop} {a b : α} (h : Relation.SymmGen r b a) : Relation.SymmGen (Function.swap r) a b
• Relation.TransGen.swap 📋 Mathlib.Logic.Relation
  {α : Sort u_1} {r : α → α → Prop} {a b : α} (h : Relation.TransGen r b a) : Relation.TransGen (Function.swap r) a b
• Relation.reflTransGen_swap 📋 Mathlib.Logic.Relation
  {α : Sort u_1} {r : α → α → Prop} {a b : α} : Relation.ReflTransGen (Function.swap r) a b ↔ Relation.ReflTransGen r b a
• Relation.symmGen_swap_apply 📋 Mathlib.Logic.Relation
  {α : Sort u_1} {a b : α} (r : α → α → Prop) : Relation.SymmGen (Function.swap r) a b ↔ Relation.SymmGen r a b
• Relation.transGen_swap 📋 Mathlib.Logic.Relation
  {α : Sort u_1} {r : α → α → Prop} {a b : α} : Relation.TransGen (Function.swap r) a b ↔ Relation.TransGen r b a
• Function.swap_bijective 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u_1} {β : Sort u_2} {γ : α → β → Sort u_3} : Function.Bijective Function.swap
• Equiv.functionSwap_apply 📋 Mathlib.Logic.Equiv.Defs
  (α : Sort u_1) (β : Sort u_2) (γ : α → β → Sort u_3) : ⇑(Equiv.functionSwap α β γ) = Function.swap
• Equiv.functionSwap_symm_apply 📋 Mathlib.Logic.Equiv.Defs
  (α : Sort u_1) (β : Sort u_2) (γ : α → β → Sort u_3) : ⇑(Equiv.functionSwap α β γ).symm = Function.swap
• IsAsymm.swap 📋 Mathlib.Order.RelClasses
  {α : Type u} (r : α → α → Prop) [Std.Asymm r] : Std.Asymm (Function.swap r)
• IsPartialOrder.swap 📋 Mathlib.Order.RelClasses
  {α : Type u} (r : α → α → Prop) [IsPartialOrder α r] : IsPartialOrder α (Function.swap r)
• IsPreorder.swap 📋 Mathlib.Order.RelClasses
  {α : Type u} (r : α → α → Prop) [IsPreorder α r] : IsPreorder α (Function.swap r)
• IsRefl.swap 📋 Mathlib.Order.RelClasses
  {α : Type u} (r : α → α → Prop) [Std.Refl r] : Std.Refl (Function.swap r)
• IsStrictOrder.swap 📋 Mathlib.Order.RelClasses
  {α : Type u} (r : α → α → Prop) [IsStrictOrder α r] : IsStrictOrder α (Function.swap r)
• IsStrictTotalOrder.swap 📋 Mathlib.Order.RelClasses
  {α : Type u} (r : α → α → Prop) [IsStrictTotalOrder α r] : IsStrictTotalOrder α (Function.swap r)
• IsTrans.swap 📋 Mathlib.Order.RelClasses
  {α : Type u} (r : α → α → Prop) [IsTrans α r] : IsTrans α (Function.swap r)
• IsTrichotomous.swap 📋 Mathlib.Order.RelClasses
  {α : Type u} (r : α → α → Prop) [Std.Trichotomous r] : Std.Trichotomous (Function.swap r)
• Std.Antisymm.swap 📋 Mathlib.Order.RelClasses
  {α : Type u} (r : α → α → Prop) [Std.Antisymm r] : Std.Antisymm (Function.swap r)
• Std.Asymm.swap 📋 Mathlib.Order.RelClasses
  {α : Type u} (r : α → α → Prop) [Std.Asymm r] : Std.Asymm (Function.swap r)
• Std.Irrefl.swap 📋 Mathlib.Order.RelClasses
  {α : Type u} (r : α → α → Prop) [Std.Irrefl r] : Std.Irrefl (Function.swap r)
• Std.Refl.swap 📋 Mathlib.Order.RelClasses
  {α : Type u} (r : α → α → Prop) [Std.Refl r] : Std.Refl (Function.swap r)
• Std.Total.swap 📋 Mathlib.Order.RelClasses
  {α : Type u} (r : α → α → Prop) [Std.Total r] : Std.Total (Function.swap r)
• Std.Trichotomous.swap 📋 Mathlib.Order.RelClasses
  {α : Type u} (r : α → α → Prop) [Std.Trichotomous r] : Std.Trichotomous (Function.swap r)
• Equiv.piComm_symm 📋 Mathlib.Logic.Equiv.Basic
  {α : Sort u_1} {β : Sort u_4} {φ : α → β → Sort u_9} : (Equiv.piComm φ).symm = Equiv.piComm (Function.swap φ)
• Equiv.piComm_apply 📋 Mathlib.Logic.Equiv.Basic
  {α : Sort u_1} {β : Sort u_4} (φ : α → β → Sort u_9) (f : (x : α) → (y : β) → φ x y) (y : β) (x : α) : (Equiv.piComm φ) f y x = Function.swap f y x
• act_rel_act_of_rel_of_rel 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  {N : Type u_2} {r : N → N → Prop} {mu : N → N → N} [IsTrans N r] [i : CovariantClass N N mu r] [i' : CovariantClass N N (Function.swap mu) r] {a b c d : N} (ab : r a b) (cd : r c d) : r (mu a c) (mu b d)
• Antitone.covariant_of_const' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  {N : Type u_2} {α : Type u_3} [Preorder α] [Preorder N] {f : N → α} {μ : N → N → N} [CovariantClass N N (Function.swap μ) fun x1 x2 => x1 ≤ x2] (hf : Antitone f) (m : N) : Antitone fun x => f (μ x m)
• Monotone.covariant_of_const' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  {N : Type u_2} {α : Type u_3} [Preorder α] [Preorder N] {f : N → α} {μ : N → N → N} [CovariantClass N N (Function.swap μ) fun x1 x2 => x1 ≤ x2] (hf : Monotone f) (m : N) : Monotone fun x => f (μ x m)
• contravariant_swap_add_of_contravariant_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  (N : Type u_2) (r : N → N → Prop) [AddCommSemigroup N] [ContravariantClass N N (fun x1 x2 => x1 + x2) r] : ContravariantClass N N (Function.swap fun x1 x2 => x1 + x2) r
• contravariant_swap_mul_of_contravariant_mul 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  (N : Type u_2) (r : N → N → Prop) [CommSemigroup N] [ContravariantClass N N (fun x1 x2 => x1 * x2) r] : ContravariantClass N N (Function.swap fun x1 x2 => x1 * x2) r
• covariant_swap_add_of_covariant_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  (N : Type u_2) (r : N → N → Prop) [AddCommSemigroup N] [CovariantClass N N (fun x1 x2 => x1 + x2) r] : CovariantClass N N (Function.swap fun x1 x2 => x1 + x2) r
• covariant_swap_mul_of_covariant_mul 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  (N : Type u_2) (r : N → N → Prop) [CommSemigroup N] [CovariantClass N N (fun x1 x2 => x1 * x2) r] : CovariantClass N N (Function.swap fun x1 x2 => x1 * x2) r
• AddGroup.covconv_swap 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  {N : Type u_2} {r : N → N → Prop} [AddGroup N] [CovariantClass N N (Function.swap fun x1 x2 => x1 + x2) r] : ContravariantClass N N (Function.swap fun x1 x2 => x1 + x2) r
• Group.covconv_swap 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  {N : Type u_2} {r : N → N → Prop} [Group N] [CovariantClass N N (Function.swap fun x1 x2 => x1 * x2) r] : ContravariantClass N N (Function.swap fun x1 x2 => x1 * x2) r
• AddGroup.covariant_swap_iff_contravariant_swap 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  {N : Type u_2} {r : N → N → Prop} [AddGroup N] : Covariant N N (Function.swap fun x1 x2 => x1 + x2) r ↔ Contravariant N N (Function.swap fun x1 x2 => x1 + x2) r
• Group.covariant_swap_iff_contravariant_swap 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  {N : Type u_2} {r : N → N → Prop} [Group N] : Covariant N N (Function.swap fun x1 x2 => x1 * x2) r ↔ Contravariant N N (Function.swap fun x1 x2 => x1 * x2) r
• RelEmbedding.swap 📋 Mathlib.Order.RelIso.Basic
  {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) : Function.swap r ↪r Function.swap s
• RelHom.swap 📋 Mathlib.Order.RelIso.Basic
  {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r →r s) : Function.swap r →r Function.swap s
• RelIso.swap 📋 Mathlib.Order.RelIso.Basic
  {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) : Function.swap r ≃r Function.swap s
• RelEmbedding.swap_apply 📋 Mathlib.Order.RelIso.Basic
  {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) (a : α) : f.swap a = f a
• RelHom.swap_apply 📋 Mathlib.Order.RelIso.Basic
  {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r →r s) (a : α) : f.swap a = f a
• BddAbove.bddAbove_image2_of_bddBelow 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) : BddAbove s → BddBelow t → BddAbove (Set.image2 f s t)
• BddAbove.bddBelow_image2_of_bddBelow 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) : BddAbove s → BddBelow t → BddBelow (Set.image2 f s t)
• BddAbove.image2 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) : BddAbove s → BddAbove t → BddAbove (Set.image2 f s t)
• BddAbove.image2_bddBelow 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) : BddAbove s → BddAbove t → BddBelow (Set.image2 f s t)
• BddBelow.bddAbove_image2_of_bddAbove 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) : BddBelow s → BddAbove t → BddAbove (Set.image2 f s t)
• BddBelow.bddBelow_image2_of_bddAbove 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) : BddBelow s → BddAbove t → BddBelow (Set.image2 f s t)
• BddBelow.image2 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) : BddBelow s → BddBelow t → BddBelow (Set.image2 f s t)
• BddBelow.image2_bddAbove 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) : BddBelow s → BddBelow t → BddAbove (Set.image2 f s t)
• IsGreatest.image2 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) (ha : IsGreatest s a) (hb : IsGreatest t b) : IsGreatest (Set.image2 f s t) (f a b)
• IsGreatest.isGreatest_image2_of_isLeast 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : IsGreatest s a) (hb : IsLeast t b) : IsGreatest (Set.image2 f s t) (f a b)
• IsGreatest.isLeast_image2 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : IsGreatest s a) (hb : IsGreatest t b) : IsLeast (Set.image2 f s t) (f a b)
• IsGreatest.isLeast_image2_of_isLeast 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) (ha : IsGreatest s a) (hb : IsLeast t b) : IsLeast (Set.image2 f s t) (f a b)
• IsLeast.image2 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) (ha : IsLeast s a) (hb : IsLeast t b) : IsLeast (Set.image2 f s t) (f a b)
• IsLeast.isGreatest_image2 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : IsLeast s a) (hb : IsLeast t b) : IsGreatest (Set.image2 f s t) (f a b)
• IsLeast.isGreatest_image2_of_isGreatest 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) (ha : IsLeast s a) (hb : IsGreatest t b) : IsGreatest (Set.image2 f s t) (f a b)
• IsLeast.isLeast_image2_of_isGreatest 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : IsLeast s a) (hb : IsGreatest t b) : IsLeast (Set.image2 f s t) (f a b)
• image2_lowerBounds_lowerBounds_subset 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) : Set.image2 f (lowerBounds s) (lowerBounds t) ⊆ lowerBounds (Set.image2 f s t)
• image2_lowerBounds_lowerBounds_subset_lowerBounds_image2 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) : Set.image2 f (upperBounds s) (upperBounds t) ⊆ lowerBounds (Set.image2 f s t)
• image2_lowerBounds_upperBounds_subset_lowerBounds_image2 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) : Set.image2 f (lowerBounds s) (upperBounds t) ⊆ lowerBounds (Set.image2 f s t)
• image2_lowerBounds_upperBounds_subset_upperBounds_image2 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) : Set.image2 f (lowerBounds s) (upperBounds t) ⊆ upperBounds (Set.image2 f s t)
• image2_upperBounds_lowerBounds_subset_lowerBounds_image2 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) : Set.image2 f (upperBounds s) (lowerBounds t) ⊆ lowerBounds (Set.image2 f s t)
• image2_upperBounds_lowerBounds_subset_upperBounds_image2 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) : Set.image2 f (upperBounds s) (lowerBounds t) ⊆ upperBounds (Set.image2 f s t)
• image2_upperBounds_upperBounds_subset 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) : Set.image2 f (upperBounds s) (upperBounds t) ⊆ upperBounds (Set.image2 f s t)
• image2_upperBounds_upperBounds_subset_upperBounds_image2 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) : Set.image2 f (lowerBounds s) (lowerBounds t) ⊆ upperBounds (Set.image2 f s t)
• mem_lowerBounds_image2 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) (ha : a ∈ lowerBounds s) (hb : b ∈ lowerBounds t) : f a b ∈ lowerBounds (Set.image2 f s t)
• mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) (ha : a ∈ upperBounds s) (hb : b ∈ lowerBounds t) : f a b ∈ lowerBounds (Set.image2 f s t)
• mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : a ∈ lowerBounds s) (hb : b ∈ upperBounds t) : f a b ∈ lowerBounds (Set.image2 f s t)
• mem_lowerBounds_image2_of_mem_upperBounds 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : a ∈ upperBounds s) (hb : b ∈ upperBounds t) : f a b ∈ lowerBounds (Set.image2 f s t)
• mem_upperBounds_image2 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) (ha : a ∈ upperBounds s) (hb : b ∈ upperBounds t) : f a b ∈ upperBounds (Set.image2 f s t)
• mem_upperBounds_image2_of_mem_lowerBounds 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : a ∈ lowerBounds s) (hb : b ∈ lowerBounds t) : f a b ∈ upperBounds (Set.image2 f s t)
• mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : a ∈ upperBounds s) (hb : b ∈ lowerBounds t) : f a b ∈ upperBounds (Set.image2 f s t)
• mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) (ha : a ∈ lowerBounds s) (hb : b ∈ upperBounds t) : f a b ∈ upperBounds (Set.image2 f s t)
• List.rel_flatMap 📋 Mathlib.Data.List.Forall2
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {R : α → β → Prop} {P : γ → δ → Prop} : Relator.LiftFun (List.Forall₂ R) (Relator.LiftFun (Relator.LiftFun R (List.Forall₂ P)) (List.Forall₂ P)) (Function.swap List.flatMap) (Function.swap List.flatMap)
• isGLB_image2_of_isGLB_isGLB 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {s : Set α} {t : Set β} {u : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β} {a₀ : α} {b₀ : β} (h₁ : ∀ (b : β), GaloisConnection (l₁ b) (Function.swap u b)) (h₂ : ∀ (a : α), GaloisConnection (l₂ a) (u a)) (ha₀ : IsGLB s a₀) (hb₀ : IsGLB t b₀) : IsGLB (Set.image2 u s t) (u a₀ b₀)
• isLUB_image2_of_isLUB_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) (u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)) (ha₀ : IsLUB s a₀) (hb₀ : IsLUB t b₀) : IsLUB (Set.image2 l s t) (l a₀ b₀)
• sInf_image2_eq_sInf_sInf 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] {s : Set α} {t : Set β} {u : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (l₁ b) (Function.swap u b)) (h₂ : ∀ (a : α), GaloisConnection (l₂ a) (u a)) : sInf (Set.image2 u s t) = u (sInf s) (sInf t)
• sSup_image2_eq_sSup_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) (u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)) : sSup (Set.image2 l s t) = l (sSup s) (sSup t)
• isGLB_image2_of_isGLB_isLUB 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {s : Set α} {t : Set β} {u : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β} {a₀ : α} {b₀ : β} (h₁ : ∀ (b : β), GaloisConnection (l₁ b) (Function.swap u b)) (h₂ : ∀ (a : α), GaloisConnection (⇑OrderDual.toDual ∘ l₂ 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 : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β} {a₀ : α} {b₀ : β} (h₁ : ∀ (b : β), GaloisConnection (⇑OrderDual.toDual ∘ l₁ b) (Function.swap u b ∘ ⇑OrderDual.ofDual)) (h₂ : ∀ (a : α), GaloisConnection (l₂ 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 : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (l₁ b) (Function.swap u b)) (h₂ : ∀ (a : α), GaloisConnection (⇑OrderDual.toDual ∘ l₂ 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 : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (⇑OrderDual.toDual ∘ l₁ b) (Function.swap u b ∘ ⇑OrderDual.ofDual)) (h₂ : ∀ (a : α), GaloisConnection (l₂ 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 : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β} {a₀ : α} {b₀ : β} (h₁ : ∀ (b : β), GaloisConnection (⇑OrderDual.toDual ∘ l₁ b) (Function.swap u b ∘ ⇑OrderDual.ofDual)) (h₂ : ∀ (a : α), GaloisConnection (⇑OrderDual.toDual ∘ l₂ 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 : α → β → γ} {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)) : 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_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 (l₁ b) (Function.swap u b)) (h₂ : ∀ (a : α), GaloisConnection (l₂ a) (u a)) (hs₀ : s.Nonempty) (hs₁ : BddBelow s) (ht₀ : t.Nonempty) (ht₁ : BddBelow t) : sInf (Set.image2 u s t) = u (sInf s) (sInf t)
• csSup_image2_eq_csSup_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) (u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)) (hs₀ : s.Nonempty) (hs₁ : BddAbove s) (ht₀ : t.Nonempty) (ht₁ : BddAbove t) : sSup (Set.image2 l s t) = l (sSup s) (sSup 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)
• IsAntichain.swap 📋 Mathlib.Order.Antichain
  {α : Type u_1} {r : α → α → Prop} {s : Set α} (hs : IsAntichain r s) : IsAntichain (Function.swap r) s
• IsStrongAntichain.swap 📋 Mathlib.Order.Antichain
  {α : Type u_1} {r : α → α → Prop} {s : Set α} [Std.Symm r] (hs : IsStrongAntichain r s) : IsStrongAntichain (Function.swap r) s
• RelEmbedding.pairwise_swap_listMap 📋 Mathlib.Data.List.Sort
  {α : Type u_1} {β : Type u_2} {ra : α → α → Prop} {rb : β → β → Prop} (e : ra ↪r rb) {l : List α} : List.Pairwise (Function.swap rb) (List.map (⇑e) l) ↔ List.Pairwise (Function.swap ra) l
• RelEmbedding.sorted_swap_listMap 📋 Mathlib.Data.List.Sort
  {α : Type u_1} {β : Type u_2} {ra : α → α → Prop} {rb : β → β → Prop} (e : ra ↪r rb) {l : List α} : List.Pairwise (Function.swap rb) (List.map (⇑e) l) ↔ List.Pairwise (Function.swap ra) l
• RelIso.pairwise_swap_listMap 📋 Mathlib.Data.List.Sort
  {α : Type u_1} {β : Type u_2} {ra : α → α → Prop} {rb : β → β → Prop} (e : ra ≃r rb) {l : List α} : List.Pairwise (Function.swap rb) (List.map (⇑e) l) ↔ List.Pairwise (Function.swap ra) l
• Sigma.lex_swap 📋 Mathlib.Data.Sigma.Lex
  {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} {a b : (i : ι) × α i} : Sigma.Lex (Function.swap r) s a b ↔ Sigma.Lex r (fun i => Function.swap (s i)) b a
• List.Pairwise.sublists' 📋 Mathlib.Data.List.Sublists
  {α : Type u} {R : α → α → Prop} {l : List α} : List.Pairwise R l → List.Pairwise (List.Lex (Function.swap R)) l.sublists'
• antisymmRel_swap 📋 Mathlib.Order.Antisymmetrization
  {α : Type u_1} (r : α → α → Prop) : AntisymmRel (Function.swap r) = AntisymmRel r
• antisymmRel_swap_apply 📋 Mathlib.Order.Antisymmetrization
  {α : Type u_1} {a b : α} (r : α → α → Prop) : AntisymmRel (Function.swap r) a b ↔ AntisymmRel r a b
• Filter.covariant_swap_div 📋 Mathlib.Order.Filter.Pointwise
  {α : Type u_2} [Div α] : CovariantClass (Filter α) (Filter α) (Function.swap fun x1 x2 => x1 / x2) fun x1 x2 => x1 ≤ x2
• Filter.covariant_swap_sub 📋 Mathlib.Order.Filter.Pointwise
  {α : Type u_2} [Sub α] : CovariantClass (Filter α) (Filter α) (Function.swap fun x1 x2 => x1 - x2) fun x1 x2 => x1 ≤ x2
• swap_dist 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] : Function.swap dist = dist
• equicontinuous_iff_continuous 📋 Mathlib.Topology.UniformSpace.Equicontinuity
  {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {F : ι → X → α} : Equicontinuous F ↔ Continuous (⇑UniformFun.ofFun ∘ Function.swap F)
• uniformEquicontinuous_iff_uniformContinuous 📋 Mathlib.Topology.UniformSpace.Equicontinuity
  {ι : Type u_1} {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] {F : ι → β → α} : UniformEquicontinuous F ↔ UniformContinuous (⇑UniformFun.ofFun ∘ Function.swap F)
• equicontinuousAt_iff_continuousAt 📋 Mathlib.Topology.UniformSpace.Equicontinuity
  {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {F : ι → X → α} {x₀ : X} : EquicontinuousAt F x₀ ↔ ContinuousAt (⇑UniformFun.ofFun ∘ Function.swap F) x₀
• equicontinuousOn_iff_continuousOn 📋 Mathlib.Topology.UniformSpace.Equicontinuity
  {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {F : ι → X → α} {S : Set X} : EquicontinuousOn F S ↔ ContinuousOn (⇑UniformFun.ofFun ∘ Function.swap F) S
• uniformEquicontinuousOn_iff_uniformContinuousOn 📋 Mathlib.Topology.UniformSpace.Equicontinuity
  {ι : Type u_1} {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] {F : ι → β → α} {S : Set β} : UniformEquicontinuousOn F S ↔ UniformContinuousOn (⇑UniformFun.ofFun ∘ Function.swap F) S
• equicontinuousWithinAt_iff_continuousWithinAt 📋 Mathlib.Topology.UniformSpace.Equicontinuity
  {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {F : ι → X → α} {S : Set X} {x₀ : X} : EquicontinuousWithinAt F S x₀ ↔ ContinuousWithinAt (⇑UniformFun.ofFun ∘ Function.swap F) S x₀
• Computation.LiftRel.swap 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} (R : α → β → Prop) (ca : Computation α) (cb : Computation β) : Computation.LiftRel (Function.swap R) cb ca ↔ Computation.LiftRel R ca cb
• Computation.LiftRelAux.swap 📋 Mathlib.Data.Seq.Computation
  {α : Type u} {β : Type v} (R : α → β → Prop) (C : Computation α → Computation β → Prop) (a : α ⊕ Computation α) (b : β ⊕ Computation β) : Computation.LiftRelAux (Function.swap R) (Function.swap C) b a = Computation.LiftRelAux R C a b
• DFinsupp.Lex.wellFounded' 📋 Mathlib.Data.DFinsupp.WellFounded
  {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} (hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0) (hs : ∀ (i : ι), WellFounded (s i)) [Std.Trichotomous r] (hr : WellFounded (Function.swap r)) : WellFounded (DFinsupp.Lex r s)
• Finsupp.Lex.wellFounded' 📋 Mathlib.Data.Finsupp.WellFounded
  {α : Type u_1} {N : Type u_2} [Zero N] {r : α → α → Prop} {s : N → N → Prop} (hbot : ∀ ⦃n : N⦄, ¬s n 0) (hs : WellFounded s) [Std.Trichotomous r] (hr : WellFounded (Function.swap r)) : WellFounded (Finsupp.Lex r s)
• Finsupp.DegLex.wellFounded 📋 Mathlib.Data.Finsupp.MonomialOrder.DegLex
  {α : Type u_1} {r : α → α → Prop} [Std.Trichotomous r] (hr : WellFounded (Function.swap r)) {s : ℕ → ℕ → Prop} (hs : WellFounded s) (hs0 : ∀ ⦃n : ℕ⦄, ¬s n 0) : WellFounded (Finsupp.DegLex r s)
• HasFPowerSeriesAt.has_fpower_series_iterate_dslope_fslope 📋 Mathlib.Analysis.Analytic.IsolatedZeros
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {p : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E} {z₀ : 𝕜} (n : ℕ) (hp : HasFPowerSeriesAt f p z₀) : HasFPowerSeriesAt ((Function.swap dslope z₀)^[n] f) (FormalMultilinearSeries.fslope^[n] p) z₀
• HasFPowerSeriesAt.eq_pow_order_mul_iterate_dslope 📋 Mathlib.Analysis.Analytic.IsolatedZeros
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {p : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E} {z₀ : 𝕜} (hp : HasFPowerSeriesAt f p z₀) : ∀ᶠ (z : 𝕜) in nhds z₀, f z = (z - z₀) ^ p.order • (Function.swap dslope z₀)^[p.order] f z
• HasFPowerSeriesAt.iterate_dslope_fslope_ne_zero 📋 Mathlib.Analysis.Analytic.IsolatedZeros
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {p : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E} {z₀ : 𝕜} (hp : HasFPowerSeriesAt f p z₀) (h : p ≠ 0) : (Function.swap dslope z₀)^[p.order] f z₀ ≠ 0
• Finset.bipartiteBelow_swap 📋 Mathlib.Combinatorics.Enumerative.DoubleCounting
  {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : Finset β) (a : α) [DecidablePred (r a)] : Finset.bipartiteBelow (Function.swap r) t a = Finset.bipartiteAbove r t a
• Finset.bipartiteAbove_swap 📋 Mathlib.Combinatorics.Enumerative.DoubleCounting
  {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : Finset α) (b : β) [(a : α) → Decidable (r a b)] : Finset.bipartiteAbove (Function.swap r) s b = Finset.bipartiteBelow r s b
• Nat.Primrec.swap 📋 Mathlib.Computability.Primrec.Basic
  : Nat.Primrec (Nat.unpaired (Function.swap Nat.pair))
• Nat.Primrec.swap' 📋 Mathlib.Computability.Primrec.Basic
  {f : ℕ → ℕ → ℕ} (hf : Nat.Primrec (Nat.unpaired f)) : Nat.Primrec (Nat.unpaired (Function.swap f))
• PrimrecRel.swap 📋 Mathlib.Computability.Primrec.Basic
  {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {r : α → β → Prop} (h : PrimrecRel r) : PrimrecRel (Function.swap r)
• Primrec₂.swap 📋 Mathlib.Computability.Primrec.Basic
  {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α → β → σ} (h : Primrec₂ f) : Primrec₂ (Function.swap f)
• Nat.bitwise_swap 📋 Mathlib.Data.Nat.Bitwise
  {f : Bool → Bool → Bool} : Nat.bitwise (Function.swap f) = Function.swap (Nat.bitwise f)
• Stream'.WSeq.LiftRel.swap_lem 📋 Mathlib.Data.WSeq.Relation
  {α : Type u} {β : Type v} {R : α → β → Prop} {s1 : Stream'.WSeq α} {s2 : Stream'.WSeq β} (h : Stream'.WSeq.LiftRel R s1 s2) : Stream'.WSeq.LiftRel (Function.swap R) s2 s1
• Stream'.WSeq.LiftRel.swap 📋 Mathlib.Data.WSeq.Relation
  {α : Type u} {β : Type v} (R : α → β → Prop) : Function.swap (Stream'.WSeq.LiftRel R) = Stream'.WSeq.LiftRel (Function.swap R)
• Stream'.WSeq.LiftRelO.swap 📋 Mathlib.Data.WSeq.Relation
  {α : Type u} {β : Type v} (R : α → β → Prop) (C : Stream'.WSeq α → Stream'.WSeq β → Prop) : Function.swap (Stream'.WSeq.LiftRelO R C) = Stream'.WSeq.LiftRelO (Function.swap R) (Function.swap C)
• swap_hammingDist 📋 Mathlib.InformationTheory.Hamming
  {ι : Type u_2} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] : Function.swap hammingDist = hammingDist
• Ordinal.isPrincipal_swap_iff 📋 Mathlib.SetTheory.Ordinal.Principal
  {o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}} : Ordinal.IsPrincipal (Function.swap op) o ↔ Ordinal.IsPrincipal op o
• Ordinal.principal_swap_iff 📋 Mathlib.SetTheory.Ordinal.Principal
  {o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}} : Ordinal.IsPrincipal (Function.swap op) o ↔ Ordinal.IsPrincipal op o
• Ordinal.isPrincipal_iff_of_monotone 📋 Mathlib.SetTheory.Ordinal.Principal
  {o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}} (h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)) (h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)) : Ordinal.IsPrincipal op o ↔ ∀ a < o, op a a < o
• Ordinal.principal_iff_of_monotone 📋 Mathlib.SetTheory.Ordinal.Principal
  {o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}} (h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)) (h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)) : Ordinal.IsPrincipal op o ↔ ∀ a < o, op a a < o
• Ordinal.not_isPrincipal_iff_of_monotone 📋 Mathlib.SetTheory.Ordinal.Principal
  {o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}} (h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)) (h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)) : ¬Ordinal.IsPrincipal op o ↔ ∃ a < o, o ≤ op a a
• Ordinal.not_principal_iff_of_monotone 📋 Mathlib.SetTheory.Ordinal.Principal
  {o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}} (h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)) (h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)) : ¬Ordinal.IsPrincipal op o ↔ ∃ a < o, o ≤ op a a
• compRel_swap 📋 Mathlib.Order.Comparable
  {α : Type u_1} (r : α → α → Prop) : CompRel (Function.swap r) = CompRel r
• incompRel_swap 📋 Mathlib.Order.Comparable
  {α : Type u_1} (r : α → α → Prop) : IncompRel (Function.swap r) = IncompRel r
• compRel_swap_apply 📋 Mathlib.Order.Comparable
  {α : Type u_1} {a b : α} (r : α → α → Prop) : CompRel (Function.swap r) a b ↔ CompRel r a b
• incompRel_swap_apply 📋 Mathlib.Order.Comparable
  {α : Type u_1} {a b : α} (r : α → α → Prop) : IncompRel (Function.swap r) a b ↔ IncompRel r a b
• Concept.swap 📋 Mathlib.Order.Concept
  {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r) : Concept β α (Function.swap r)
• lowerPolar_swap 📋 Mathlib.Order.Concept
  {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : Set α) : lowerPolar (Function.swap r) s = upperPolar r s
• upperPolar_swap 📋 Mathlib.Order.Concept
  {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : Set β) : upperPolar (Function.swap r) t = lowerPolar r t
• Concept.extent_swap 📋 Mathlib.Order.Concept
  {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r) : c.swap.extent = c.intent
• Concept.intent_swap 📋 Mathlib.Order.Concept
  {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r) : c.swap.intent = c.extent
• Concept.swap_swap 📋 Mathlib.Order.Concept
  {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r) : c.swap.swap = c
• Concept.swapEquiv 📋 Mathlib.Order.Concept
  {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : (Concept α β r)ᵒᵈ ≃o Concept β α (Function.swap r)
• Concept.swap_le_swap_iff 📋 Mathlib.Order.Concept
  {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : Concept α β r} : c.swap ≤ d.swap ↔ d ≤ c
• Concept.swap_lt_swap_iff 📋 Mathlib.Order.Concept
  {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : Concept α β r} : c.swap < d.swap ↔ d < c
• Concept.swapEquiv_apply 📋 Mathlib.Order.Concept
  {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (a✝ : (Concept α β r)ᵒᵈ) : Concept.swapEquiv a✝ = (Concept.swap ∘ ⇑OrderDual.ofDual) a✝
• Concept.swapEquiv_symm_apply 📋 Mathlib.Order.Concept
  {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (a✝ : Concept β α (Function.swap r)) : (RelIso.symm Concept.swapEquiv) a✝ = (⇑OrderDual.toDual ∘ Concept.swap) a✝

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. 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 8e80836 serving mathlib revision 6ef8cc2