Loogle!

Result

Found 49 declarations whose name contains "contravariant".

• Contravariant 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  (M : Type u_1) (N : Type u_2) (μ : M → N → N) (r : N → N → Prop) : Prop
• ContravariantClass 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  (M : Type u_1) (N : Type u_2) (μ : M → N → N) (r : N → N → Prop) : Prop
• ContravariantClass.elim 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [self : ContravariantClass M N μ r] : Contravariant M N μ r
• ContravariantClass.mk 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} (elim : Contravariant M N μ r) : ContravariantClass M N μ r
• Contravariant.flip 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} (h : Contravariant M N μ r) : Contravariant M N μ (flip r)
• contravariant_flip_iff 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  (N : Type u_2) (r : N → N → Prop) (mu : N → N → N) [h : Std.Commutative mu] : Contravariant N N (flip mu) r ↔ Contravariant N N mu r
• contravariant_lt_of_contravariant_le 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  (M : Type u_1) (N : Type u_2) (μ : M → N → N) [PartialOrder N] : (Contravariant M N μ fun x1 x2 => x1 ≤ x2) → Contravariant M N μ fun x1 x2 => x1 < x2
• contravariant_lt_of_covariant_le 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  (N : Type u_2) (mu : N → N → N) [LinearOrder N] [CovariantClass N N mu fun x1 x2 => x1 ≤ x2] : ContravariantClass N N mu fun x1 x2 => x1 < x2
• covariant_lt_of_contravariant_le 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  (N : Type u_2) (mu : N → N → N) [LinearOrder N] [ContravariantClass N N mu fun x1 x2 => x1 ≤ x2] : CovariantClass N N mu fun x1 x2 => x1 < x2
• covariant_le_iff_contravariant_lt 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  (M : Type u_1) (N : Type u_2) (μ : M → N → N) [LinearOrder N] : (Covariant M N μ fun x1 x2 => x1 ≤ x2) ↔ Contravariant M N μ fun x1 x2 => x1 < x2
• covariant_lt_iff_contravariant_le 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  (M : Type u_1) (N : Type u_2) (μ : M → N → N) [LinearOrder N] : (Covariant M N μ fun x1 x2 => x1 < x2) ↔ Contravariant M N μ fun x1 x2 => x1 ≤ x2
• contravariant_le_of_contravariant_eq_and_lt 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  (M : Type u_1) (N : Type u_2) (μ : M → N → N) [PartialOrder N] [ContravariantClass M N μ fun x1 x2 => x1 = x2] [ContravariantClass M N μ fun x1 x2 => x1 < x2] : ContravariantClass M N μ fun x1 x2 => x1 ≤ x2
• covariant_lt_of_covariant_le_of_contravariant_eq 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  (M : Type u_1) (N : Type u_2) (μ : M → N → N) [ContravariantClass M N μ fun x1 x2 => x1 = x2] [PartialOrder N] [CovariantClass M N μ fun x1 x2 => x1 ≤ x2] : CovariantClass M N μ fun x1 x2 => x1 < x2
• contravariant_le_iff_contravariant_lt_and_eq 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  (M : Type u_1) (N : Type u_2) (μ : M → N → N) [PartialOrder N] : (Contravariant M N μ fun x1 x2 => x1 ≤ x2) ↔ (Contravariant M N μ fun x1 x2 => x1 < x2) ∧ Contravariant M N μ fun x1 x2 => x1 = x2
• 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
• AddGroup.covariant_iff_contravariant 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  {N : Type u_2} {r : N → N → Prop} [AddGroup N] : Covariant N N (fun x1 x2 => x1 + x2) r ↔ Contravariant N N (fun x1 x2 => x1 + x2) r
• Group.covariant_iff_contravariant 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  {N : Type u_2} {r : N → N → Prop} [Group N] : Covariant N N (fun x1 x2 => x1 * x2) r ↔ Contravariant N N (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
• Contravariant.AddLECancellable 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} [Add α] [LE α] [AddLeftReflectLE α] {a : α} : AddLECancellable a
• Contravariant.MulLECancellable 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} [Mul α] [LE α] [MulLeftReflectLE α] {a : α} : MulLECancellable a
• Contravariant.toAddLeftCancelSemigroup 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} [AddSemigroup α] [PartialOrder α] [AddLeftReflectLE α] : AddLeftCancelSemigroup α
• Contravariant.toAddRightCancelSemigroup 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} [AddSemigroup α] [PartialOrder α] [AddRightReflectLE α] : AddRightCancelSemigroup α
• Contravariant.toLeftCancelSemigroup 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} [Semigroup α] [PartialOrder α] [MulLeftReflectLE α] : LeftCancelSemigroup α
• Contravariant.toRightCancelSemigroup 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} [Semigroup α] [PartialOrder α] [MulRightReflectLE α] : RightCancelSemigroup α
• Contravariant.toAddLeftCancelSemigroup.eq_1 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} [AddSemigroup α] [PartialOrder α] [AddLeftReflectLE α] : Contravariant.toAddLeftCancelSemigroup = { toAddSemigroup := inst✝, add_left_cancel := ⋯ }
• Contravariant.toAddRightCancelSemigroup.eq_1 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} [AddSemigroup α] [PartialOrder α] [AddRightReflectLE α] : Contravariant.toAddRightCancelSemigroup = { toAddSemigroup := inst✝, add_right_cancel := ⋯ }
• Contravariant.toLeftCancelSemigroup.eq_1 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} [Semigroup α] [PartialOrder α] [MulLeftReflectLE α] : Contravariant.toLeftCancelSemigroup = { toSemigroup := inst✝, mul_left_cancel := ⋯ }
• Contravariant.toRightCancelSemigroup.eq_1 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} [Semigroup α] [PartialOrder α] [MulRightReflectLE α] : Contravariant.toRightCancelSemigroup = { toSemigroup := inst✝, mul_right_cancel := ⋯ }
• MulPosReflectLE.toContravariantClass 📋 Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
  {α : Type u_1} {inst✝ : Mul α} {inst✝¹ : Zero α} {inst✝² : Preorder α} [self : MulPosReflectLE α] : ContravariantClass { x // 0 < x } α (fun x y => y * ↑x) fun x1 x2 => x1 ≤ x2
• MulPosReflectLT.toContravariantClass 📋 Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
  {α : Type u_1} {inst✝ : Mul α} {inst✝¹ : Zero α} {inst✝² : Preorder α} [self : MulPosReflectLT α] : ContravariantClass { x // 0 ≤ x } α (fun x y => y * ↑x) fun x1 x2 => x1 < x2
• MulPosReflectLT.to_contravariantClass_pos_mul_lt 📋 Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
  {α : Type u_1} [Mul α] [Zero α] [Preorder α] [MulPosReflectLT α] : ContravariantClass { x // 0 < x } α (fun x y => y * ↑x) fun x1 x2 => x1 < x2
• PosMulReflectLE.toContravariantClass 📋 Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
  {α : Type u_1} {inst✝ : Mul α} {inst✝¹ : Zero α} {inst✝² : Preorder α} [self : PosMulReflectLE α] : ContravariantClass { x // 0 < x } α (fun x y => ↑x * y) fun x1 x2 => x1 ≤ x2
• PosMulReflectLT.toContravariantClass 📋 Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
  {α : Type u_1} {inst✝ : Mul α} {inst✝¹ : Zero α} {inst✝² : Preorder α} [self : PosMulReflectLT α] : ContravariantClass { x // 0 ≤ x } α (fun x y => ↑x * y) fun x1 x2 => x1 < x2
• PosMulReflectLT.to_contravariantClass_pos_mul_lt 📋 Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs
  {α : Type u_1} [Mul α] [Zero α] [Preorder α] [PosMulReflectLT α] : ContravariantClass { x // 0 < x } α (fun x y => ↑x * y) fun x1 x2 => x1 < x2
• mulPosReflectLT_iff_contravariant_pos 📋 Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
  {α : Type u_1} [MulZeroClass α] [PartialOrder α] : MulPosReflectLT α ↔ ContravariantClass { x // 0 < x } α (fun x y => y * ↑x) fun x1 x2 => x1 < x2
• posMulReflectLT_iff_contravariant_pos 📋 Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
  {α : Type u_1} [MulZeroClass α] [PartialOrder α] : PosMulReflectLT α ↔ ContravariantClass { x // 0 < x } α (fun x y => ↑x * y) fun x1 x2 => x1 < x2
• CategoryTheory.Abelian.Ext.contravariantSequence 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (Y : C) (n₀ n₁ : ℕ) (h : 1 + n₀ = n₁) : CategoryTheory.ComposableArrows AddCommGrp 5
• CategoryTheory.Abelian.Ext.contravariantSequence_exact 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (Y : C) (n₀ n₁ : ℕ) (h : 1 + n₀ = n₁) : (CategoryTheory.Abelian.Ext.contravariantSequence hS Y n₀ n₁ h).Exact
• CategoryTheory.Abelian.Ext.contravariant_sequence_exact₁ 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (Y : C) {n₀ : ℕ} (x₁ : CategoryTheory.Abelian.Ext S.X₁ Y n₀) {n₁ : ℕ} (hn₁ : 1 + n₀ = n₁) (hx₁ : hS.extClass.comp x₁ hn₁ = 0) : ∃ x₂, (CategoryTheory.Abelian.Ext.mk₀ S.f).comp x₂ ⋯ = x₁
• CategoryTheory.Abelian.Ext.contravariant_sequence_exact₃ 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (Y : C) {n₁ : ℕ} (x₃ : CategoryTheory.Abelian.Ext S.X₃ Y n₁) (hx₃ : (CategoryTheory.Abelian.Ext.mk₀ S.g).comp x₃ ⋯ = 0) {n₀ : ℕ} (hn₀ : 1 + n₀ = n₁) : ∃ x₁, hS.extClass.comp x₁ hn₀ = x₃
• CategoryTheory.Abelian.Ext.contravariant_sequence_exact₂ 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (Y : C) {n : ℕ} (x₂ : CategoryTheory.Abelian.Ext S.X₂ Y n) (hx₂ : (CategoryTheory.Abelian.Ext.mk₀ S.f).comp x₂ ⋯ = 0) : ∃ x₁, (CategoryTheory.Abelian.Ext.mk₀ S.g).comp x₁ ⋯ = x₂
• CategoryTheory.Abelian.Ext.contravariant_sequence_exact₁' 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (Y : C) (n₀ n₁ : ℕ) (h : 1 + n₀ = n₁) : { X₁ := AddCommGrp.of (CategoryTheory.Abelian.Ext S.X₂ Y n₀), X₂ := AddCommGrp.of (CategoryTheory.Abelian.Ext S.X₁ Y n₀), X₃ := AddCommGrp.of (CategoryTheory.Abelian.Ext S.X₃ Y n₁), f := AddCommGrp.ofHom ((CategoryTheory.Abelian.Ext.mk₀ S.f).precomp Y ⋯), g := AddCommGrp.ofHom (hS.extClass.precomp Y h), zero := ⋯ }.Exact
• CategoryTheory.Abelian.Ext.contravariant_sequence_exact₃' 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (Y : C) (n₀ n₁ : ℕ) (h : 1 + n₀ = n₁) : { X₁ := AddCommGrp.of (CategoryTheory.Abelian.Ext S.X₁ Y n₀), X₂ := AddCommGrp.of (CategoryTheory.Abelian.Ext S.X₃ Y n₁), X₃ := AddCommGrp.of (CategoryTheory.Abelian.Ext S.X₂ Y n₁), f := AddCommGrp.ofHom (hS.extClass.precomp Y h), g := AddCommGrp.ofHom ((CategoryTheory.Abelian.Ext.mk₀ S.g).precomp Y ⋯), zero := ⋯ }.Exact
• CategoryTheory.Abelian.Ext.contravariant_sequence_exact₂' 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (Y : C) (n : ℕ) : { X₁ := AddCommGrp.of (CategoryTheory.Abelian.Ext S.X₃ Y n), X₂ := AddCommGrp.of (CategoryTheory.Abelian.Ext S.X₂ Y n), X₃ := AddCommGrp.of (CategoryTheory.Abelian.Ext S.X₁ Y n), f := AddCommGrp.ofHom ((CategoryTheory.Abelian.Ext.mk₀ S.g).precomp Y ⋯), g := AddCommGrp.ofHom ((CategoryTheory.Abelian.Ext.mk₀ S.f).precomp Y ⋯), zero := ⋯ }.Exact
• instContravariantClassHSMulLeOfIsOrderedCancelSMul 📋 Mathlib.Algebra.Order.AddTorsor
  {G : Type u_1} {P : Type u_2} [LE G] [LE P] [SMul G P] [IsOrderedCancelSMul G P] : ContravariantClass G P (fun x1 x2 => x1 • x2) fun x1 x2 => x1 ≤ x2
• instContravariantClassHVAddLeOfIsOrderedCancelVAdd 📋 Mathlib.Algebra.Order.AddTorsor
  {G : Type u_1} {P : Type u_2} [LE G] [LE P] [VAdd G P] [IsOrderedCancelVAdd G P] : ContravariantClass G P (fun x1 x2 => x1 +ᵥ x2) fun x1 x2 => x1 ≤ x2
• InnerProductSpace.canonicalContravariantTensor 📋 Mathlib.Analysis.InnerProductSpace.CanonicalTensor
  (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] : TensorProduct ℝ E E →ₗ[ℝ] ℝ

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.

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.

This is Loogle revision 19971e9 serving mathlib revision f167e8d