Loogle!

Result

Found 140 declarations mentioning InvolutiveInv.

InvolutiveInv 📋 Mathlib.Algebra.Group.DivInvMonoid
(G : Type u_2) : Type u_2
DivisionMonoid.toInvolutiveInv 📋 Mathlib.Algebra.Group.DivInvMonoid
{G : Type u_2} [self : DivisionMonoid G] : InvolutiveInv G
InvolutiveInv.toInv 📋 Mathlib.Algebra.Group.DivInvMonoid
{G : Type u_2} [self : InvolutiveInv G] : Inv G
InvolutiveInv.mk 📋 Mathlib.Algebra.Group.DivInvMonoid
{G : Type u_2} [toInv : Inv G] (inv_inv : ∀ (x : G), x⁻¹⁻¹ = x) : InvolutiveInv G
inv_inv 📋 Mathlib.Algebra.Group.DivInvMonoid
{G : Type u_1} [InvolutiveInv G] (a : G) : a⁻¹⁻¹ = a
InvolutiveInv.inv_inv 📋 Mathlib.Algebra.Group.DivInvMonoid
{G : Type u_2} [self : InvolutiveInv G] (x : G) : x⁻¹⁻¹ = x
AddOpposite.instInvolutiveInv 📋 Mathlib.Algebra.Opposites
{α : Type u_1} [InvolutiveInv α] : InvolutiveInv αᵃᵒᵖ
MulOpposite.instInvolutiveInv 📋 Mathlib.Algebra.Opposites
{α : Type u_1} [InvolutiveInv α] : InvolutiveInv αᵐᵒᵖ
Pi.involutiveInv 📋 Mathlib.Algebra.Group.Pi.Basic
{I : Type u} {f : I → Type v₁} [(i : I) → InvolutiveInv (f i)] : InvolutiveInv ((i : I) → f i)
inv_involutive 📋 Mathlib.Algebra.Group.Basic
{G : Type u_3} [InvolutiveInv G] : Function.Involutive Inv.inv
inv_bijective 📋 Mathlib.Algebra.Group.Basic
{G : Type u_3} [InvolutiveInv G] : Function.Bijective Inv.inv
inv_injective 📋 Mathlib.Algebra.Group.Basic
{G : Type u_3} [InvolutiveInv G] : Function.Injective Inv.inv
inv_surjective 📋 Mathlib.Algebra.Group.Basic
{G : Type u_3} [InvolutiveInv G] : Function.Surjective Inv.inv
leftInverse_inv 📋 Mathlib.Algebra.Group.Basic
(G : Type u_3) [InvolutiveInv G] : Function.LeftInverse (fun a => a⁻¹) fun a => a⁻¹
rightInverse_inv 📋 Mathlib.Algebra.Group.Basic
(G : Type u_3) [InvolutiveInv G] : Function.RightInverse (fun a => a⁻¹) fun a => a⁻¹
inv_comp_inv 📋 Mathlib.Algebra.Group.Basic
(G : Type u_3) [InvolutiveInv G] : Inv.inv ∘ Inv.inv = id
inv_eq_iff_eq_inv 📋 Mathlib.Algebra.Group.Basic
{G : Type u_3} [InvolutiveInv G] {a b : G} : a⁻¹ = b ↔ a = b⁻¹
inv_inj 📋 Mathlib.Algebra.Group.Basic
{G : Type u_3} [InvolutiveInv G] {a b : G} : a⁻¹ = b⁻¹ ↔ a = b
IsSelfInv.inv 📋 Mathlib.Algebra.Group.SelfInv
{α : Type u_1} [InvolutiveInv α] {a : α} : IsSelfInv a → IsSelfInv a⁻¹
isSelfInv_inv 📋 Mathlib.Algebra.Group.SelfInv
{α : Type u_1} [InvolutiveInv α] {a : α} : IsSelfInv a⁻¹ ↔ IsSelfInv a
Additive.involutiveNeg 📋 Mathlib.Algebra.Group.TypeTags.Basic
{α : Type u} [InvolutiveInv α] : InvolutiveNeg (Additive α)
Multiplicative.involutiveInv 📋 Mathlib.Algebra.Group.TypeTags.Basic
{α : Type u} [InvolutiveNeg α] : InvolutiveInv (Multiplicative α)
Function.Injective.involutiveInv 📋 Mathlib.Algebra.Group.InjSurj
{M₂ : Type u_2} {M₁ : Type u_3} [Inv M₁] [InvolutiveInv M₂] (f : M₁ → M₂) (hf : Function.Injective f) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) : InvolutiveInv M₁
Function.Surjective.involutiveInv 📋 Mathlib.Algebra.Group.InjSurj
{M₁ : Type u_1} {M₂ : Type u_3} [Inv M₂] [InvolutiveInv M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) : InvolutiveInv M₂
Prod.instInvolutiveInv 📋 Mathlib.Algebra.Group.Prod
{M : Type u_3} {N : Type u_4} [InvolutiveInv M] [InvolutiveInv N] : InvolutiveInv (M × N)
Equiv.inv 📋 Mathlib.Algebra.Group.Equiv.Basic
(G : Type u_14) [InvolutiveInv G] : Equiv.Perm G
Equiv.inv_symm 📋 Mathlib.Algebra.Group.Equiv.Basic
{G : Type u_14} [InvolutiveInv G] : Equiv.symm (Equiv.inv G) = Equiv.inv G
Equiv.inv_apply 📋 Mathlib.Algebra.Group.Equiv.Basic
(G : Type u_14) [InvolutiveInv G] : ⇑(Equiv.inv G) = Inv.inv
Colex.instInvolutiveInv 📋 Mathlib.Algebra.Order.Group.Synonym
{α : Type u_1} [InvolutiveInv α] : InvolutiveInv (Colex α)
Lex.instInvolutiveInv 📋 Mathlib.Algebra.Order.Group.Synonym
{α : Type u_1} [InvolutiveInv α] : InvolutiveInv (Lex α)
OrderDual.instInvolutiveInv 📋 Mathlib.Algebra.Order.Group.Synonym
{α : Type u_1} [InvolutiveInv α] : InvolutiveInv αᵒᵈ
WithZero.instInvolutiveInv 📋 Mathlib.Algebra.GroupWithZero.WithZero
{α : Type u_1} [InvolutiveInv α] : InvolutiveInv (WithZero α)
Set.involutiveInv 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
{α : Type u_2} [InvolutiveInv α] : InvolutiveInv (Set α)
Set.Nonempty.inv 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
{α : Type u_2} [InvolutiveInv α] {s : Set α} (h : s.Nonempty) : s⁻¹.Nonempty
Set.nonempty_inv 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
{α : Type u_2} [InvolutiveInv α] {s : Set α} : s⁻¹.Nonempty ↔ s.Nonempty
Set.image_inv_eq_inv 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
{α : Type u_2} [InvolutiveInv α] {s : Set α} : (fun x => x⁻¹) '' s = s⁻¹
Set.inv_eq_empty 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
{α : Type u_2} [InvolutiveInv α] {s : Set α} : s⁻¹ = ∅ ↔ s = ∅
Set.inv_range 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
{α : Type u_2} [InvolutiveInv α] {ι : Sort u_4} {f : ι → α} : (Set.range f)⁻¹ = Set.range fun i => (f i)⁻¹
Set.inv_eq_self_iff_inv_subset 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
{α : Type u_2} [InvolutiveInv α] {s : Set α} : s⁻¹ = s ↔ s⁻¹ ⊆ s
Set.inv_singleton 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
{α : Type u_2} [InvolutiveInv α] (a : α) : {a}⁻¹ = {a⁻¹}
Set.inv_mem_inv 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
{α : Type u_2} [InvolutiveInv α] {s : Set α} {a : α} : a⁻¹ ∈ s⁻¹ ↔ a ∈ s
Set.inv_range' 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
{α : Type u_2} [InvolutiveInv α] {ι : Type u_4} {f : ι → α} : (Set.range f)⁻¹ = Set.range f⁻¹
Set.inv_subset 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
{α : Type u_2} [InvolutiveInv α] {s t : Set α} : s⁻¹ ⊆ t ↔ s ⊆ t⁻¹
Set.inv_subset_inv 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
{α : Type u_2} [InvolutiveInv α] {s t : Set α} : s⁻¹ ⊆ t⁻¹ ↔ s ⊆ t
Set.forall_inv_mem 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
{α : Type u_2} [InvolutiveInv α] {s : Set α} {p : α → Prop} : (∀ (x : α), x⁻¹ ∈ s → p x) ↔ ∀ x ∈ s, p x⁻¹
Set.MapsTo.inv 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
{α : Type u_2} {β : Type u_3} [InvolutiveInv β] {A : Set α} {B : Set β} {f : α → β} (h : Set.MapsTo f A B) : Set.MapsTo f⁻¹ A B⁻¹
Set.image_op_inv 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
{α : Type u_2} [InvolutiveInv α] {s : Set α} : MulOpposite.op '' s⁻¹ = (MulOpposite.op '' s)⁻¹
Set.exists_inv_mem 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
{α : Type u_2} [InvolutiveInv α] {s : Set α} {p : α → Prop} : (∃ x, x⁻¹ ∈ s ∧ p x) ↔ ∃ x ∈ s, p x⁻¹
Set.inv_insert 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
{α : Type u_2} [InvolutiveInv α] (a : α) (s : Set α) : (insert a s)⁻¹ = insert a⁻¹ s⁻¹
Set.image_inv_of_apply_inv_eq 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
{α : Type u_2} {β : Type u_3} [InvolutiveInv α] {s : Set α} {f g : α → β} (H : ∀ x ∈ s, f x⁻¹ = g x) : f '' s⁻¹ = g '' s
Set.image_inv_of_apply_inv_eq_inv 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
{α : Type u_2} {β : Type u_3} [InvolutiveInv α] {s : Set α} [InvolutiveInv β] {f g : α → β} (H : ∀ x ∈ s, f x⁻¹ = (g x)⁻¹) : f '' s⁻¹ = (g '' s)⁻¹
Set.Finite.inv 📋 Mathlib.Algebra.Group.Pointwise.Set.Finite
{α : Type u_1} [InvolutiveInv α] {s : Set α} : s.Finite → s⁻¹.Finite
Set.Finite.of_inv 📋 Mathlib.Algebra.Group.Pointwise.Set.Finite
{α : Type u_1} [InvolutiveInv α] {s : Set α} : s⁻¹.Finite → s.Finite
Set.finite_inv 📋 Mathlib.Algebra.Group.Pointwise.Set.Finite
{α : Type u_1} [InvolutiveInv α] {s : Set α} : s⁻¹.Finite ↔ s.Finite
Set.infinite_inv 📋 Mathlib.Algebra.Group.Pointwise.Set.Finite
{α : Type u_1} [InvolutiveInv α] {s : Set α} : s⁻¹.Infinite ↔ s.Infinite
isSelfInv_singleton_iff 📋 Mathlib.Algebra.Group.Pointwise.Set.SelfInv
{α : Type u_1} [InvolutiveInv α] {a : α} : IsSelfInv {a} ↔ IsSelfInv a
IsSelfInv.inv_subset 📋 Mathlib.Algebra.Group.Pointwise.Set.SelfInv
{α : Type u_1} [InvolutiveInv α] {s : Set α} : IsSelfInv s → s⁻¹ ⊆ s
IsSelfInv.of_inv_subset 📋 Mathlib.Algebra.Group.Pointwise.Set.SelfInv
{α : Type u_1} [InvolutiveInv α] {s : Set α} : s⁻¹ ⊆ s → IsSelfInv s
IsSelfInv.of_subset_inv 📋 Mathlib.Algebra.Group.Pointwise.Set.SelfInv
{α : Type u_1} [InvolutiveInv α] {s : Set α} : s ⊆ s⁻¹ → IsSelfInv s
IsSelfInv.subset_inv 📋 Mathlib.Algebra.Group.Pointwise.Set.SelfInv
{α : Type u_1} [InvolutiveInv α] {s : Set α} : IsSelfInv s → s ⊆ s⁻¹
isSelfInv_iff_inv_subset 📋 Mathlib.Algebra.Group.Pointwise.Set.SelfInv
{α : Type u_1} [InvolutiveInv α] {s : Set α} : IsSelfInv s ↔ s⁻¹ ⊆ s
isSelfInv_iff_subset_inv 📋 Mathlib.Algebra.Group.Pointwise.Set.SelfInv
{α : Type u_1} [InvolutiveInv α] {s : Set α} : IsSelfInv s ↔ s ⊆ s⁻¹
IsSelfInv.inv_mem 📋 Mathlib.Algebra.Group.Pointwise.Set.SelfInv
{α : Type u_1} [InvolutiveInv α] {s : Set α} (h : IsSelfInv s) {x : α} (hx : x ∈ s) : x⁻¹ ∈ s
isSelfInv_iff_forall_inv_mem 📋 Mathlib.Algebra.Group.Pointwise.Set.SelfInv
{α : Type u_1} [InvolutiveInv α] {s : Set α} : IsSelfInv s ↔ ∀ ⦃x : α⦄, x ∈ s → x⁻¹ ∈ s
IsSelfInv.diff 📋 Mathlib.Algebra.Group.Pointwise.Set.SelfInv
{α : Type u_1} [InvolutiveInv α] {s t : Set α} (hs : IsSelfInv s) (ht : IsSelfInv t) : IsSelfInv (s \ t)
inv_mem_iff 📋 Mathlib.Algebra.Group.Subgroup.Defs
{S : Type u_3} {G : Type u_4} [InvolutiveInv G] {x✝ : SetLike S G} [InvMemClass S G] {H : S} {x : G} : x⁻¹ ∈ H ↔ x ∈ H
Submonoid.involutiveInv 📋 Mathlib.Algebra.Group.Submonoid.Pointwise
{G : Type u_2} [Group G] : InvolutiveInv (Submonoid G)
IsSelfInv.of_invMemClass 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
{G : Type u_2} {S : Type u_4} [InvolutiveInv G] [SetLike S G] [InvMemClass S G] (H : S) : IsSelfInv ↑H
inv_coe_set 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
{G : Type u_2} {S : Type u_4} [InvolutiveInv G] [SetLike S G] [InvMemClass S G] {H : S} : (↑H)⁻¹ = ↑H
DomMulAct.instInvolutiveInvOfMulOpposite 📋 Mathlib.GroupTheory.GroupAction.DomAct.Basic
{M : Type u_1} [InvolutiveInv Mᵐᵒᵖ] : InvolutiveInv Mᵈᵐᵃ
Finset.card_inv 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
{α : Type u_2} [DecidableEq α] [InvolutiveInv α] (s : Finset α) : s⁻¹.card = s.card
Finset.inv_univ 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
{α : Type u_2} [DecidableEq α] [InvolutiveInv α] [Fintype α] : Finset.univ⁻¹ = Finset.univ
Finset.coe_inv 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
{α : Type u_2} [DecidableEq α] [InvolutiveInv α] (s : Finset α) : ↑s⁻¹ = (↑s)⁻¹
Finset.mem_inv' 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
{α : Type u_2} [DecidableEq α] [InvolutiveInv α] {s : Finset α} {a : α} : a ∈ s⁻¹ ↔ a⁻¹ ∈ s
Finset.inv_filter_univ 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
{α : Type u_2} [DecidableEq α] [InvolutiveInv α] (p : α → Prop) [Fintype α] [DecidablePred p] : ↑{x | p x}⁻¹ = {x | p x⁻¹}
Finset.inv_inter 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
{α : Type u_2} [DecidableEq α] [InvolutiveInv α] (s t : Finset α) : (s ∩ t)⁻¹ = s⁻¹ ∩ t⁻¹
Finset.inv_filter 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
{α : Type u_2} [DecidableEq α] [InvolutiveInv α] (s : Finset α) (p : α → Prop) [DecidablePred p] : ({x ∈ s | p x})⁻¹ = {x ∈ s⁻¹ | p x⁻¹}
Finset.preimage_inv 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
{α : Type u_2} [DecidableEq α] [InvolutiveInv α] (s : Finset α) : s.preimage (fun x => x⁻¹) ⋯ = s⁻¹
Finset.inv_product 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
{α : Type u_2} {β : Type u_3} [DecidableEq α] [InvolutiveInv α] [DecidableEq β] [InvolutiveInv β] (s : Finset α) (t : Finset β) : (s ×ˢ t)⁻¹ = s⁻¹ ×ˢ t⁻¹
Finset.expect_inv_index 📋 Mathlib.Algebra.BigOperators.Expect
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [Module ℚ≥0 M] [DecidableEq ι] [InvolutiveInv ι] (s : Finset ι) (f : ι → M) : (s⁻¹.expect fun i => f i) = s.expect fun i => f i⁻¹
FunLike.involutiveInv 📋 Mathlib.Data.FunLike.Group
{F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Inv F] [InvolutiveInv β] [IsInvApply F α β] : InvolutiveInv F
Filter.instInvolutiveInv 📋 Mathlib.Order.Filter.Pointwise
{α : Type u_2} [InvolutiveInv α] : InvolutiveInv (Filter α)
Filter.comap_inv 📋 Mathlib.Order.Filter.Pointwise
{α : Type u_2} [InvolutiveInv α] {f : Filter α} : Filter.comap Inv.inv f = f⁻¹
Filter.inv_le_self 📋 Mathlib.Order.Filter.Pointwise
{α : Type u_2} [InvolutiveInv α] {f : Filter α} : f⁻¹ ≤ f ↔ f⁻¹ = f
Filter.inv_mem_inv 📋 Mathlib.Order.Filter.Pointwise
{α : Type u_2} [InvolutiveInv α] {f : Filter α} {s : Set α} (hs : s ∈ f) : s⁻¹ ∈ f⁻¹
Filter.HasBasis.inv 📋 Mathlib.Order.Filter.Pointwise
{α : Type u_2} [InvolutiveInv α] {f : Filter α} {ι : Sort u_5} {p : ι → Prop} {s : ι → Set α} (h : f.HasBasis p s) : f⁻¹.HasBasis p fun i => (s i)⁻¹
Filter.inv_le_iff_le_inv 📋 Mathlib.Order.Filter.Pointwise
{α : Type u_2} [InvolutiveInv α] {f g : Filter α} : f⁻¹ ≤ g ↔ f ≤ g⁻¹
Filter.inv_le_inv_iff 📋 Mathlib.Order.Filter.Pointwise
{α : Type u_2} [InvolutiveInv α] {f g : Filter α} : f⁻¹ ≤ g⁻¹ ↔ f ≤ g
Homeomorph.inv 📋 Mathlib.Topology.Algebra.Group.ContinuousInv
(G : Type u_4) [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] : G ≃ₜ G
isClosedMap_inv 📋 Mathlib.Topology.Algebra.Group.ContinuousInv
(G : Type u_1) [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] : IsClosedMap Inv.inv
isOpenMap_inv 📋 Mathlib.Topology.Algebra.Group.ContinuousInv
(G : Type u_1) [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] : IsOpenMap Inv.inv
IsClosed.inv 📋 Mathlib.Topology.Algebra.Group.ContinuousInv
{G : Type u_1} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] {s : Set G} (hs : IsClosed s) : IsClosed s⁻¹
IsCompact.inv 📋 Mathlib.Topology.Algebra.Group.ContinuousInv
{G : Type u_1} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] {s : Set G} (hs : IsCompact s) : IsCompact s⁻¹
IsOpen.inv 📋 Mathlib.Topology.Algebra.Group.ContinuousInv
{G : Type u_1} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] {s : Set G} (hs : IsOpen s) : IsOpen s⁻¹
Homeomorph.symm_inv 📋 Mathlib.Topology.Algebra.Group.ContinuousInv
{G : Type u_4} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] : (Homeomorph.inv G).symm = Homeomorph.inv G
nhds_inv 📋 Mathlib.Topology.Algebra.Group.ContinuousInv
(G : Type u_1) [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] (a : G) : nhds a⁻¹ = (nhds a)⁻¹
Continuous.of_inv 📋 Mathlib.Topology.Algebra.Group.ContinuousInv
{G : Type u_1} {α : Type u_3} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] [TopologicalSpace α] {f : α → G} : Continuous f⁻¹ → Continuous f
continuous_inv_iff 📋 Mathlib.Topology.Algebra.Group.ContinuousInv
{G : Type u_1} {α : Type u_3} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] [TopologicalSpace α] {f : α → G} : Continuous f⁻¹ ↔ Continuous f
inv_closure 📋 Mathlib.Topology.Algebra.Group.ContinuousInv
{G : Type u_1} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] (s : Set G) : (closure s)⁻¹ = closure s⁻¹
ContinuousAt.of_inv 📋 Mathlib.Topology.Algebra.Group.ContinuousInv
{G : Type u_1} {α : Type u_3} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] [TopologicalSpace α] {f : α → G} {x : α} : ContinuousAt f⁻¹ x → ContinuousAt f x
continuousAt_inv_iff 📋 Mathlib.Topology.Algebra.Group.ContinuousInv
{G : Type u_1} {α : Type u_3} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] [TopologicalSpace α] {f : α → G} {x : α} : ContinuousAt f⁻¹ x ↔ ContinuousAt f x
ContinuousOn.of_inv 📋 Mathlib.Topology.Algebra.Group.ContinuousInv
{G : Type u_1} {α : Type u_3} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] [TopologicalSpace α] {f : α → G} {s : Set α} : ContinuousOn f⁻¹ s → ContinuousOn f s
continuousOn_inv_iff 📋 Mathlib.Topology.Algebra.Group.ContinuousInv
{G : Type u_1} {α : Type u_3} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] [TopologicalSpace α] {f : α → G} {s : Set α} : ContinuousOn f⁻¹ s ↔ ContinuousOn f s
Homeomorph.coe_inv 📋 Mathlib.Topology.Algebra.Group.ContinuousInv
{G : Type u_4} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] : ⇑(Homeomorph.inv G) = Inv.inv
tendsto_inv_iff 📋 Mathlib.Topology.Algebra.Group.ContinuousInv
{G : Type u_1} {α : Type u_3} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] {l : Filter α} {m : α → G} {a : G} : Filter.Tendsto (fun x => (m x)⁻¹) l (nhds a⁻¹) ↔ Filter.Tendsto m l (nhds a)
Filter.inv_nhdsNE 📋 Mathlib.Topology.Algebra.Group.ContinuousInv
{G : Type u_1} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] {a : G} : (nhdsWithin a {a}ᶜ)⁻¹ = nhdsWithin a⁻¹ {a⁻¹}ᶜ
WithOne.instInvolutiveInv 📋 Mathlib.Algebra.Group.WithOne.Basic
{α : Type u} [InvolutiveInv α] : InvolutiveInv (WithOne α)
IsMulIndecomposable.pairwise_div_notMem_range 📋 Mathlib.Algebra.Group.Irreducible.Indecomposable
{ι : Type u_1} {G : Type u_3} [CommGroup G] [InvolutiveInv ι] (v : ι → G) (hv_one : ∀ (i : ι), v i ≠ 1) (hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹) (s t : Set ι) (hst : s ⊆ {i | IsMulIndecomposable v t i}) (hv_t : ∀ (i : ι), i ∈ t ∨ i⁻¹ ∈ t) : s.Pairwise fun i j => v i / v j ∉ Set.range v
Subgroup.closure_image_isMulIndecomposable_baseOf 📋 Mathlib.Algebra.Group.Irreducible.Indecomposable
{ι : Type u_1} {G : Type u_3} {S : Type u_4} [CommGroup G] [LinearOrder S] [Finite ι] [InvolutiveInv ι] [CommGroup S] [IsOrderedMonoid S] (v : ι → G) (hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹) (f : G →* S) (hf : ∀ (i : ι), f (v i) ≠ 1) : Subgroup.closure (v '' IsMulIndecomposable.baseOf v f) = Subgroup.closure (Set.range v)
IsMulIndecomposable.pairwise_baseOf_div_notMem 📋 Mathlib.Algebra.Group.Irreducible.Indecomposable
{ι : Type u_1} {G : Type u_3} {S : Type u_4} [CommGroup G] [LinearOrder S] [InvolutiveInv ι] [CommGroup S] [IsOrderedMonoid S] (v : ι → G) (hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹) (f : G →* S) (hf : ∀ (i : ι), f (v i) ≠ 1) : (IsMulIndecomposable.baseOf v f).Pairwise fun i j => v i / v j ∉ Set.range v
IsMulIndecomposable.image_baseOf_inv_comp_eq 📋 Mathlib.Algebra.Group.Irreducible.Indecomposable
{ι : Type u_1} {G : Type u_3} {S : Type u_4} [CommGroup G] [LinearOrder S] [InvolutiveInv ι] [CommGroup S] [IsOrderedMonoid S] (v : ι → G) (hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹) (f : G →* S) : v '' IsMulIndecomposable.baseOf v (invMonoidHom.comp f) = ⇑invMonoidHom ∘ v '' IsMulIndecomposable.baseOf v f
IsMulIndecomposable.pairwise_div_notMem_range' 📋 Mathlib.Algebra.Group.Irreducible.Indecomposable
{ι : Type u_1} {G : Type u_3} {S : Type u_4} [CommGroup G] [LinearOrder S] [InvolutiveInv ι] [CommGroup S] [IsOrderedMonoid S] (v : ι → G) (hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹) (f : G →* S) (hf : ∀ (i : ι), f (v i) ≠ 1) (s : Set ι) (hst : s ⊆ {j | IsMulIndecomposable v {i | 1 < f (v i)} j}) : s.Pairwise fun i j => v i / v j ∉ Set.range v
IsMulIndecomposable.mem_or_inv_mem_closure_baseOf 📋 Mathlib.Algebra.Group.Irreducible.Indecomposable
{ι : Type u_1} {G : Type u_3} {S : Type u_4} [CommGroup G] [LinearOrder S] [Finite ι] [InvolutiveInv ι] [CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (i : ι) (hi : f (v i) ≠ 1) (hi' : v i⁻¹ = (v i)⁻¹) : v i ∈ Submonoid.closure (v '' IsMulIndecomposable.baseOf v f) ∨ (v i)⁻¹ ∈ Submonoid.closure (v '' IsMulIndecomposable.baseOf v f)
IsMulIndecomposable.apply_ne_one_iff_mem_closure 📋 Mathlib.Algebra.Group.Irreducible.Indecomposable
{ι : Type u_1} {G : Type u_3} {S : Type u_4} [CommGroup G] [LinearOrder S] [Finite ι] [InvolutiveInv ι] [CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (i : ι) (hi : v i ≠ 1) (hi' : v i⁻¹ = (v i)⁻¹) : f (v i) ≠ 1 ↔ v i ∈ Submonoid.closure (v '' IsMulIndecomposable.baseOf v f) ∨ (v i)⁻¹ ∈ Submonoid.closure (v '' IsMulIndecomposable.baseOf v f)
Submonoid.apply_ne_one_of_mem_or_inv_mem_closure 📋 Mathlib.Algebra.Group.Irreducible.Indecomposable
{ι : Type u_1} {G : Type u_3} {S : Type u_4} [CommGroup G] [LinearOrder S] [InvolutiveInv ι] [CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (s : Set ι) (hf : ∀ i ∈ s, 1 < f (v i)) (i : ι) (hv_one : v i ≠ 1) (hv_inv : v i⁻¹ = (v i)⁻¹) (hsp : v i ∈ Submonoid.closure (v '' s) ∨ (v i)⁻¹ ∈ Submonoid.closure (v '' s)) : f (v i) ≠ 1
Finset.prod_inv_index 📋 Mathlib.Algebra.Group.Pointwise.Finset.BigOperators
{α : Type u_1} {ι : Type u_2} [CommMonoid α] [DecidableEq ι] [InvolutiveInv ι] (s : Finset ι) (f : ι → α) : ∏ i ∈ s⁻¹, f i = ∏ i ∈ s, f i⁻¹
Finset.sum_inv_index 📋 Mathlib.Algebra.Group.Pointwise.Finset.BigOperators
{α : Type u_1} {ι : Type u_2} [AddCommMonoid α] [DecidableEq ι] [InvolutiveInv ι] (s : Finset ι) (f : ι → α) : ∑ i ∈ s⁻¹, f i = ∑ i ∈ s, f i⁻¹
Finset.dens_inv 📋 Mathlib.Algebra.Group.Pointwise.Finset.Density
{α : Type u_1} [DecidableEq α] [InvolutiveInv α] [Fintype α] (s : Finset α) : s⁻¹.dens = s.dens
Set.encard_inv 📋 Mathlib.Algebra.Group.Pointwise.Set.Card
{G : Type u_1} [InvolutiveInv G] (s : Set G) : s⁻¹.encard = s.encard
Set.ncard_inv 📋 Mathlib.Algebra.Group.Pointwise.Set.Card
{G : Type u_1} [InvolutiveInv G] (s : Set G) : s⁻¹.ncard = s.ncard
Cardinal.mk_inv 📋 Mathlib.Algebra.Group.Pointwise.Set.Card
{G : Type u_1} [InvolutiveInv G] (s : Set G) : Cardinal.mk ↑s⁻¹ = Cardinal.mk ↑s
Set.natCard_inv 📋 Mathlib.Algebra.Group.Pointwise.Set.Card
{G : Type u_1} [InvolutiveInv G] (s : Set G) : Nat.card ↑s⁻¹ = Nat.card ↑s
ENNReal.instInvolutiveInv 📋 Mathlib.Basic.ENNReal.Inv
: InvolutiveInv ENNReal
SeparationQuotient.instInvolutiveInv 📋 Mathlib.Topology.Algebra.SeparationQuotient.Basic
{G : Type u_1} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] : InvolutiveInv (SeparationQuotient G)
measurableEmbedding_inv 📋 Mathlib.MeasureTheory.Group.Arithmetic
{α : Type u_3} {m : MeasurableSpace α} [InvolutiveInv α] [MeasurableInv α] : MeasurableEmbedding Inv.inv
measurable_inv_iff 📋 Mathlib.MeasureTheory.Group.Arithmetic
{α : Type u_3} {m : MeasurableSpace α} {G : Type u_4} [InvolutiveInv G] [MeasurableSpace G] [MeasurableInv G] {f : α → G} : (Measurable fun x => (f x)⁻¹) ↔ Measurable f
aemeasurable_inv_iff 📋 Mathlib.MeasureTheory.Group.Arithmetic
{α : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G : Type u_4} [InvolutiveInv G] [MeasurableSpace G] [MeasurableInv G] {f : α → G} : AEMeasurable (fun x => (f x)⁻¹) μ ↔ AEMeasurable f μ
MeasurableEquiv.inv 📋 Mathlib.MeasureTheory.Group.MeasurableEquiv
(G : Type u_4) [MeasurableSpace G] [InvolutiveInv G] [MeasurableInv G] : G ≃ᵐ G
MeasurableEquiv.inv_toEquiv 📋 Mathlib.MeasureTheory.Group.MeasurableEquiv
(G : Type u_4) [MeasurableSpace G] [InvolutiveInv G] [MeasurableInv G] : (MeasurableEquiv.inv G).toEquiv = Equiv.inv G
MeasurableEquiv.symm_inv 📋 Mathlib.MeasureTheory.Group.MeasurableEquiv
{G : Type u_4} [MeasurableSpace G] [InvolutiveInv G] [MeasurableInv G] : (MeasurableEquiv.inv G).symm = MeasurableEquiv.inv G
MeasurableEquiv.inv_apply 📋 Mathlib.MeasureTheory.Group.MeasurableEquiv
(G : Type u_4) [MeasurableSpace G] [InvolutiveInv G] [MeasurableInv G] : ⇑(MeasurableEquiv.inv G) = Inv.inv
MeasureTheory.Measure.inv.instSigmaFinite 📋 Mathlib.MeasureTheory.Group.Measure
{G : Type u_1} [MeasurableSpace G] [InvolutiveInv G] [MeasurableInv G] (μ : MeasureTheory.Measure G) [MeasureTheory.SigmaFinite μ] : MeasureTheory.SigmaFinite μ.inv
MeasureTheory.Measure.inv_inv 📋 Mathlib.MeasureTheory.Group.Measure
{G : Type u_1} [MeasurableSpace G] [InvolutiveInv G] [MeasurableInv G] (μ : MeasureTheory.Measure G) : μ.inv.inv = μ
MeasureTheory.Measure.inv_apply 📋 Mathlib.MeasureTheory.Group.Measure
{G : Type u_1} [MeasurableSpace G] [InvolutiveInv G] [MeasurableInv G] (μ : MeasureTheory.Measure G) (s : Set G) : μ.inv s = μ s⁻¹
MeasureTheory.Measure.measure_inv 📋 Mathlib.MeasureTheory.Group.Measure
{G : Type u_1} [MeasurableSpace G] [InvolutiveInv G] [MeasurableInv G] (μ : MeasureTheory.Measure G) [μ.IsInvInvariant] (A : Set G) : μ A⁻¹ = μ A
MeasureTheory.Measure.measure_preimage_inv 📋 Mathlib.MeasureTheory.Group.Measure
{G : Type u_1} [MeasurableSpace G] [InvolutiveInv G] [MeasurableInv G] (μ : MeasureTheory.Measure G) [μ.IsInvInvariant] (A : Set G) : μ (Inv.inv ⁻¹' A) = μ A
MeasureTheory.lintegral_inv_eq_self 📋 Mathlib.MeasureTheory.Group.LIntegral
{G : Type u_1} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [InvolutiveInv G] [MeasurableInv G] [μ.IsInvInvariant] (f : G → ENNReal) : ∫⁻ (x : G), f x⁻¹ ∂μ = ∫⁻ (x : G), f x ∂μ
IsPathConnected.inv 📋 Mathlib.Topology.Connected.PathConnected
{G : Type u_4} [InvolutiveInv G] [TopologicalSpace G] [ContinuousInv G] {s : Set G} (hs : IsPathConnected s) : IsPathConnected s⁻¹
JoinedIn.inv 📋 Mathlib.Topology.Connected.PathConnected
{G : Type u_4} [InvolutiveInv G] [TopologicalSpace G] [ContinuousInv G] {s : Set G} {a b : G} (hs : JoinedIn s a b) : JoinedIn s⁻¹ a⁻¹ b⁻¹
Filter.Germ.instInvolutiveInv 📋 Mathlib.Order.Filter.Germ.Basic
{α : Type u_1} {l : Filter α} {G : Type u_6} [InvolutiveInv G] : InvolutiveInv (l.Germ G)

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:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
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
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.
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 ce5dd8c