Loogle!

Result

Found 29 declarations whose name contains "eq_symm_apply".

• Equiv.apply_eq_iff_eq_symm_apply 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {x : α} {y : β} (f : α ≃ β) : f x = y ↔ x = f.symm y
• Equiv.eq_symm_apply 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u_1} {β : Sort u_2} (e : α ≃ β) {x : β} {y : α} : y = e.symm x ↔ e y = x
• Equiv.sigmaSigmaSubtypeEq_symm_apply 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_9} {β : Type u_10} {γ : α → β → Type u_11} {a : α} {b : β} (c : γ a b) : (Equiv.sigmaSigmaSubtypeEq a b).symm c = ⟨⟨a, ⟨b, c⟩⟩, ⋯⟩
• AddEquiv.eq_symm_apply 📋 Mathlib.Algebra.Group.Equiv.Defs
  {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) {x : N} {y : M} : y = e.symm x ↔ e y = x
• MulEquiv.eq_symm_apply 📋 Mathlib.Algebra.Group.Equiv.Defs
  {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) {x : N} {y : M} : y = e.symm x ↔ e y = x
• RelIso.apply_eq_iff_eq_symm_apply 📋 Mathlib.Order.RelIso.Basic
  {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {x : α} {y : β} (f : r ≃r s) : f x = y ↔ x = f.symm y
• RelIso.eq_symm_apply 📋 Mathlib.Order.RelIso.Basic
  {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) {x : β} {y : α} : y = e.symm x ↔ e y = x
• OrderIso.apply_eq_iff_eq_symm_apply 📋 Mathlib.Order.Hom.Basic
  {α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) (x : α) (y : β) : e x = y ↔ x = e.symm y
• RingEquiv.eq_symm_apply 📋 Mathlib.Algebra.Ring.Equiv
  {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] (e : R ≃+* S) {x : S} {y : R} : y = e.symm x ↔ e y = x
• LinearEquiv.eq_symm_apply 📋 Mathlib.Algebra.Module.Equiv.Defs
  {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) {x : M₂} {y : M} : y = e.symm x ↔ e y = x
• AlgEquiv.eq_symm_apply 📋 Mathlib.Algebra.Algebra.Equiv
  {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) {x : A₂} {y : A₁} : y = e.symm x ↔ e y = x
• OrderAddMonoidIso.eq_symm_apply 📋 Mathlib.Algebra.Order.Hom.Monoid
  {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Add α] [Add β] (e : α ≃+o β) {x : β} {y : α} : y = e.symm x ↔ e y = x
• OrderMonoidIso.eq_symm_apply 📋 Mathlib.Algebra.Order.Hom.Monoid
  {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [Mul α] [Mul β] (e : α ≃*o β) {x : β} {y : α} : y = e.symm x ↔ e y = x
• ContinuousAddEquiv.eq_symm_apply 📋 Mathlib.Topology.Algebra.ContinuousMonoidHom
  {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M] [Add N] (e : M ≃ₜ+ N) {x : N} {y : M} : y = e.symm x ↔ e y = x
• ContinuousMulEquiv.eq_symm_apply 📋 Mathlib.Topology.Algebra.ContinuousMonoidHom
  {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Mul M] [Mul N] (e : M ≃ₜ* N) {x : N} {y : M} : y = e.symm x ↔ e y = x
• IsometryEquiv.eq_symm_apply 📋 Mathlib.Topology.MetricSpace.Isometry
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (h : α ≃ᵢ β) {x : α} {y : β} : x = h.symm y ↔ h x = y
• Fin.appendIsometryOfEq_symm_apply 📋 Mathlib.Topology.MetricSpace.Isometry
  {α : Type u} [PseudoEMetricSpace α] {n m l : ℕ} (hmln : m + l = n) (a✝ : Fin n → α) : (Fin.appendIsometryOfEq hmln).symm a✝ = (fun i => a✝ (Fin.cast ⋯ (Fin.castAdd l i)), fun i => a✝ (Fin.cast ⋯ (Fin.natAdd m i)))
• ContinuousLinearEquiv.eq_symm_apply 📋 Mathlib.Topology.Algebra.Module.Equiv
  {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_5} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) {x : M₂} {y : M₁} : y = e.symm x ↔ e y = x
• PartialEquiv.eq_symm_apply 📋 Mathlib.Logic.Equiv.PartialEquiv
  {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {x : α} {y : β} (hx : x ∈ e.source) (hy : y ∈ e.target) : x = ↑e.symm y ↔ ↑e x = y
• Equiv.toPartialEquivOfImageEq_symm_apply 📋 Mathlib.Logic.Equiv.PartialEquiv
  {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Set α) (t : Set β) (h : ⇑e '' s = t) : ↑(e.toPartialEquivOfImageEq s t h).symm = ⇑e.symm
• OpenPartialHomeomorph.eq_symm_apply 📋 Mathlib.Topology.OpenPartialHomeomorph.Defs
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} {y : Y} (hx : x ∈ e.source) (hy : y ∈ e.target) : x = ↑e.symm y ↔ ↑e x = y
• Homeomorph.toOpenPartialHomeomorphOfImageEq_symm_apply 📋 Mathlib.Topology.OpenPartialHomeomorph.Defs
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) (s : Set X) (hs : IsOpen s) (t : Set Y) (h : ⇑e '' s = t) : ↑(e.toOpenPartialHomeomorphOfImageEq s hs t h).symm = ⇑e.symm
• addEquivOfAddOrderOfEq_symm_apply_gen 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic
  {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] {g : G} (hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g) {g' : G'} (hg' : ∀ (x : G'), x ∈ AddSubgroup.zmultiples g') (h : addOrderOf g = addOrderOf g') : (addEquivOfAddOrderOfEq hg hg' h).symm g' = g
• mulEquivOfOrderOfEq_symm_apply_gen 📋 Mathlib.GroupTheory.SpecificGroups.Cyclic
  {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {g' : G'} (hg' : ∀ (x : G'), x ∈ Subgroup.zpowers g') (h : orderOf g = orderOf g') : (mulEquivOfOrderOfEq hg hg' h).symm g' = g
• LieModuleEquiv.apply_eq_iff_eq_symm_apply 📋 Mathlib.Algebra.Lie.Basic
  {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] {m : M} {n : N} (e : M ≃ₗ⁅R,L⁆ N) : e m = n ↔ m = e.symm n
• AffineEquiv.apply_eq_iff_eq_symm_apply 📋 Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
  {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) {p₁ : P₁} {p₂ : P₂} : e p₁ = p₂ ↔ p₁ = e.symm p₂
• ContinuousAlgEquiv.eq_symm_apply 📋 Mathlib.Topology.Algebra.Algebra.Equiv
  {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) {a : A} {b : B} : a = e.symm b ↔ e a = b
• ContinuousAffineEquiv.apply_eq_iff_eq_symm_apply 📋 Mathlib.Topology.Algebra.ContinuousAffineEquiv
  {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[k] P₂) {p₁ : P₁} {p₂ : P₂} : e p₁ = p₂ ↔ p₁ = e.symm p₂
• ContinuousAffineEquiv.eq_symm_apply 📋 Mathlib.Topology.Algebra.ContinuousAffineEquiv
  {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (e : P₁ ≃ᴬ[k] P₂) {x : P₂} {y : P₁} : y = e.symm x ↔ e y = x

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 6ff4759 serving mathlib revision 519f454