Loogle!
Result
Found 3855 declarations mentioning Function.Injective. Of these, 1793 match your pattern(s). Of these, only the first 200 are shown.
- Function.injective_id 📋 Init.Data.Function
{α : Sort u_1} : Function.Injective id - Function.HasLeftInverse.injective 📋 Init.Data.Function
{α : Sort u_1} {β : Sort u_2} {f : α → β} : Function.HasLeftInverse f → Function.Injective f - Function.LeftInverse.injective 📋 Init.Data.Function
{α : Sort u_1} {β : Sort u_2} {g : β → α} {f : α → β} : Function.LeftInverse g f → Function.Injective f - Function.Injective.comp 📋 Init.Data.Function
{α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {g : β → γ} {f : α → β} (hg : Function.Injective g) (hf : Function.Injective f) : Function.Injective (g ∘ f) - Char.ofOrdinal_injective 📋 Init.Data.Char.Ordinal
: Function.Injective Char.ofOrdinal - Char.ordinal_injective 📋 Init.Data.Char.Ordinal
: Function.Injective Char.ordinal - Option.map_injective 📋 Init.Data.Option.Function
{α : Type u_1} {β : Type u_2} {f : α → β} (hf : Function.Injective f) : Function.Injective (Option.map f) - Std.PRange.UpwardEnumerable.Map.injective 📋 Init.Data.Range.Polymorphic.Map
{α : Type u} {β : Type v} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] (self : Std.PRange.UpwardEnumerable.Map α β) : Function.Injective self.toFun - List.injective_sigmaCountToIdx 📋 Batteries.Data.List.Count
{α : Type u_1} [BEq α] [LawfulBEq α] {xs : List α} : Function.Injective xs.sigmaCountToIdx - List.injective_idxToSigmaCount 📋 Batteries.Data.List.Count
{α : Type u_1} [BEq α] [ReflBEq α] {xs : List α} : Function.Injective xs.idxToSigmaCount - List.Perm.idxBij_injective 📋 Batteries.Data.List.Perm
{α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} (h : xs.Perm ys) : Function.Injective h.idxBij - List.Subperm.idxInj_injective 📋 Batteries.Data.List.Perm
{α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} (h : xs.Subperm ys) : Function.Injective h.idxInj - Nat.xor_left_injective 📋 Batteries.Data.Nat.Bitwise.Lemmas
{x : ℕ} : Function.Injective fun x_1 => x_1 ^^^ x - Nat.xor_right_injective 📋 Batteries.Data.Nat.Bitwise.Lemmas
{x : ℕ} : Function.Injective fun x_1 => x ^^^ x_1 - add_left_injective 📋 Mathlib.Algebra.Group.Defs
{G : Type u_1} [Add G] [IsRightCancelAdd G] (a : G) : Function.Injective fun x => x + a - add_right_injective 📋 Mathlib.Algebra.Group.Defs
{G : Type u_1} [Add G] [IsLeftCancelAdd G] (a : G) : Function.Injective fun x => a + x - mul_left_injective 📋 Mathlib.Algebra.Group.Defs
{G : Type u_1} [Mul G] [IsRightCancelMul G] (a : G) : Function.Injective fun x => x * a - mul_right_injective 📋 Mathlib.Algebra.Group.Defs
{G : Type u_1} [Mul G] [IsLeftCancelMul G] (a : G) : Function.Injective fun x => a * x - IsAddTorsionFree.nsmul_right_injective 📋 Mathlib.Algebra.Group.Defs
{M : Type u_2} {inst✝ : AddMonoid M} [self : IsAddTorsionFree M] ⦃n : ℕ⦄ (hn : n ≠ 0) : Function.Injective fun a => n • a - IsMulTorsionFree.pow_left_injective 📋 Mathlib.Algebra.Group.Defs
{M : Type u_2} {inst✝ : Monoid M} [self : IsMulTorsionFree M] ⦃n : ℕ⦄ (hn : n ≠ 0) : Function.Injective fun a => a ^ n - Function.Injective.ite 📋 Mathlib.Logic.Basic
{α : Sort u_3} {β : Sort u_4} {p : β → Prop} [DecidablePred p] {g : β → α} (hg : Function.Injective g) {f : β → α} (hf : Function.Injective f) (h : ∀ (x y : β), g x = f y → x = y) : Function.Injective fun x => if p x then g x else f x - Function.not_injective 📋 Mathlib.Logic.Function.Basic
: Function.Injective Not - Function.injective_of_subsingleton 📋 Mathlib.Logic.Function.Basic
{α : Sort u_1} {β : Sort u_2} [Subsingleton α] (f : α → β) : Function.Injective f - Function.Involutive.injective 📋 Mathlib.Logic.Function.Basic
{α : Sort u} {f : α → α} (h : Function.Involutive f) : Function.Injective f - Function.const_injective 📋 Mathlib.Logic.Function.Basic
{α : Sort u_1} {β : Sort u_2} [Nonempty α] : Function.Injective (Function.const α) - Function.Bijective.injective 📋 Mathlib.Logic.Function.Basic
{α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Function.Bijective f) : Function.Injective f - Function.curry_injective 📋 Mathlib.Logic.Function.Basic
{α : Type u_1} {β : Type u_2} {γ : Sort u_3} : Function.Injective Function.curry - Function.uncurry_injective 📋 Mathlib.Logic.Function.Basic
{α : Type u_1} {β : Type u_2} {γ : Sort u_3} : Function.Injective Function.uncurry - Function.RightInverse.injective 📋 Mathlib.Logic.Function.Basic
{α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} (h : Function.RightInverse f g) : Function.Injective f - Function.injective_of_isPartialInv 📋 Mathlib.Logic.Function.Basic
{α : Type u_4} {β : Sort u_5} {f : α → β} {g : β → Option α} (H : Function.IsPartialInv f g) : Function.Injective f - Function.injective_surjInv 📋 Mathlib.Logic.Function.Basic
{α : Sort u} {β : Sort v} {f : α → β} (h : Function.Surjective f) : Function.Injective (Function.surjInv h) - Function.IsPartialInv.injective 📋 Mathlib.Logic.Function.Basic
{α : Type u_4} {β : Sort u_5} {f : α → β} {g : β → Option α} (H : Function.IsPartialInv f g) : Function.Injective f - Function.Injective2.right 📋 Mathlib.Logic.Function.Basic
{α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β → γ} (hf : Function.Injective2 f) (a : α) : Function.Injective (f a) - Function.Injective2.left' 📋 Mathlib.Logic.Function.Basic
{α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β → γ} (hf : Function.Injective2 f) [Nonempty β] : Function.Injective f - Function.Injective2.left 📋 Mathlib.Logic.Function.Basic
{α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β → γ} (hf : Function.Injective2 f) (b : β) : Function.Injective fun a => f a b - Function.Injective.of_comp 📋 Mathlib.Logic.Function.Basic
{α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : γ → α} (I : Function.Injective (f ∘ g)) : Function.Injective g - Function.update_injective 📋 Mathlib.Logic.Function.Basic
{α : Sort u} {β : α → Sort v} [DecidableEq α] (f : (a : α) → β a) (a' : α) : Function.Injective (Function.update f a') - Function.Injective2.uncurry 📋 Mathlib.Logic.Function.Basic
{α : Type u_4} {β : Type u_5} {γ : Type u_6} {f : α → β → γ} (hf : Function.Injective2 f) : Function.Injective (Function.uncurry f) - Function.Injective.comp_left 📋 Mathlib.Logic.Function.Basic
{α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {g : β → γ} (hg : Function.Injective g) : Function.Injective fun x => g ∘ x - Function.Injective2.right' 📋 Mathlib.Logic.Function.Basic
{α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β → γ} (hf : Function.Injective2 f) [Nonempty α] : Function.Injective fun b a => f a b - Function.Surjective.injective_comp_right 📋 Mathlib.Logic.Function.Basic
{α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : Function.Surjective f) : Function.Injective fun g => g ∘ f - Function.Injective.of_comp_right 📋 Mathlib.Logic.Function.Basic
{α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : γ → α} (I : Function.Injective (f ∘ g)) (hg : Function.Surjective g) : Function.Injective f - Function.extend_injective 📋 Mathlib.Logic.Function.Basic
{α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : Function.Injective f) (e' : β → γ) : Function.Injective fun g => Function.extend f g e' - Function.Injective.piMap 📋 Mathlib.Logic.Function.Basic
{ι : Sort u_4} {α : ι → Sort u_5} {β : ι → Sort u_6} {f : (i : ι) → α i → β i} (hf : ∀ (i : ι), Function.Injective (f i)) : Function.Injective (Pi.map f) - Function.Injective.dite 📋 Mathlib.Logic.Function.Basic
{α : Sort u_1} {β : Sort u_2} (p : α → Prop) [DecidablePred p] {f : { a // p a } → β} {f' : { a // ¬p a } → β} (hf : Function.Injective f) (hf' : Function.Injective f') (im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f ⟨x, hx⟩ ≠ f' ⟨x', hx'⟩) : Function.Injective fun x => if h : p x then f ⟨x, h⟩ else f' ⟨x, h⟩ - DFunLike.coe_injective 📋 Mathlib.Data.FunLike.Basic
{F : Sort u_1} {α : outParam (Sort u_2)} {β : outParam (α → Sort u_3)} [self : DFunLike F α β] : Function.Injective DFunLike.coe - DFunLike.coe_injective' 📋 Mathlib.Data.FunLike.Basic
{F : Sort u_1} {α : outParam (Sort u_2)} {β : outParam (α → Sort u_3)} [self : DFunLike F α β] : Function.Injective DFunLike.coe - EmbeddingLike.injective 📋 Mathlib.Data.FunLike.Embedding
{F : Sort u_1} {α : Sort u_2} {β : Sort u_3} [FunLike F α β] [i : EmbeddingLike F α β] (f : F) : Function.Injective ⇑f - EmbeddingLike.injective' 📋 Mathlib.Data.FunLike.Embedding
{F : Sort u_1} {α : outParam (Sort u_2)} {β : outParam (Sort u_3)} {inst✝ : FunLike F α β} [self : EmbeddingLike F α β] (f : F) : Function.Injective ⇑f - EquivLike.inv_injective 📋 Mathlib.Data.FunLike.Equiv
{E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [EquivLike E α β] : Function.Injective EquivLike.inv - EquivLike.injective 📋 Mathlib.Data.FunLike.Equiv
{E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [EquivLike E α β] (e : E) : Function.Injective ⇑e - Quotient.out_injective 📋 Mathlib.Data.Quot
{α : Sort u_1} {s : Setoid α} : Function.Injective Quotient.out - Subtype.val_injective 📋 Mathlib.Data.Subtype
{α : Sort u_1} {p : α → Prop} : Function.Injective Subtype.val - Subtype.coe_injective 📋 Mathlib.Data.Subtype
{α : Sort u_1} {p : α → Prop} : Function.Injective fun a => ↑a - Subtype.restrict_injective 📋 Mathlib.Data.Subtype
{α : Sort u_4} {β : Type u_5} {f : α → β} (p : α → Prop) (h : Function.Injective f) : Function.Injective (Subtype.restrict p f) - Subtype.coind_injective 📋 Mathlib.Data.Subtype
{α : Sort u_4} {β : Sort u_5} {f : α → β} {p : β → Prop} (h : ∀ (a : α), p (f a)) (hf : Function.Injective f) : Function.Injective (Subtype.coind f h) - Subtype.map_injective 📋 Mathlib.Data.Subtype
{α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} {f : α → β} (h : ∀ (a : α), p a → q (f a)) (hf : Function.Injective f) : Function.Injective (Subtype.map f h) - Equiv.injective 📋 Mathlib.Logic.Equiv.Defs
{α : Sort u} {β : Sort v} (e : α ≃ β) : Function.Injective ⇑e - Equiv.coe_fn_injective 📋 Mathlib.Logic.Equiv.Defs
{α : Sort u} {β : Sort v} : Function.Injective fun e => ⇑e - AddOpposite.op_injective 📋 Mathlib.Algebra.Opposites
{α : Type u_1} : Function.Injective AddOpposite.op - AddOpposite.unop_injective 📋 Mathlib.Algebra.Opposites
{α : Type u_1} : Function.Injective AddOpposite.unop - MulOpposite.op_injective 📋 Mathlib.Algebra.Opposites
{α : Type u_1} : Function.Injective MulOpposite.op - MulOpposite.unop_injective 📋 Mathlib.Algebra.Opposites
{α : Type u_1} : Function.Injective MulOpposite.unop - Function.Injective.iterate 📋 Mathlib.Logic.Function.Iterate
{α : Type u} {f : α → α} (Hinj : Function.Injective f) (n : ℕ) : Function.Injective f^[n] - smul_left_injective' 📋 Mathlib.Algebra.Group.Action.Faithful
{M : Type u_1} {α : Type u_3} [SMul M α] [FaithfulSMul M α] : Function.Injective fun x1 x2 => x1 • x2 - vadd_left_injective' 📋 Mathlib.Algebra.Group.Action.Faithful
{M : Type u_1} {α : Type u_3} [VAdd M α] [FaithfulVAdd M α] : Function.Injective fun x1 x2 => x1 +ᵥ x2 - Pi.mulSingle_injective 📋 Mathlib.Algebra.Notation.Pi.Basic
{ι : Type u_1} {M : ι → Type u_6} [(i : ι) → One (M i)] [DecidableEq ι] (i : ι) : Function.Injective (Pi.mulSingle i) - Pi.single_injective 📋 Mathlib.Algebra.Notation.Pi.Basic
{ι : Type u_1} {M : ι → Type u_6} [(i : ι) → Zero (M i)] [DecidableEq ι] (i : ι) : Function.Injective (Pi.single i) - PSum.inl_injective 📋 Mathlib.Data.Sum.Basic
{α : Sort u_3} {β : Sort u_4} : Function.Injective PSum.inl - PSum.inr_injective 📋 Mathlib.Data.Sum.Basic
{α : Sort u_3} {β : Sort u_4} : Function.Injective PSum.inr - Sum.inl_injective 📋 Mathlib.Data.Sum.Basic
{α : Type u} {β : Type v} : Function.Injective Sum.inl - Sum.inr_injective 📋 Mathlib.Data.Sum.Basic
{α : Type u} {β : Type v} : Function.Injective Sum.inr - Sum.elim_injective' 📋 Mathlib.Data.Sum.Basic
{α : Type u} {β : Type v} {γ : Sort u_3} {f : α → γ} : Function.Injective (Sum.elim f) - Function.Injective.sumMap 📋 Mathlib.Data.Sum.Basic
{α : Type u} {α' : Type w} {β : Type v} {β' : Type x} {f : α → β} {g : α' → β'} (hf : Function.Injective f) (hg : Function.Injective g) : Function.Injective (Sum.map f g) - Function.Injective.sumElim 📋 Mathlib.Data.Sum.Basic
{α : Type u} {β : Type v} {γ : Sort u_3} {f : α → γ} {g : β → γ} (hf : Function.Injective f) (hg : Function.Injective g) (hfg : ∀ (a : α) (b : β), f a ≠ g b) : Function.Injective (Sum.elim f g) - Option.some_injective 📋 Mathlib.Data.Option.Basic
(α : Type u_5) : Function.Injective some - Option.map_injective' 📋 Mathlib.Data.Option.Basic
{α : Type u_1} {β : Type u_2} : Function.Injective Option.map - Prod.fst_injective 📋 Mathlib.Data.Prod.Basic
{α : Type u_1} {β : Type u_2} [Subsingleton β] : Function.Injective Prod.fst - Prod.mk_right_injective 📋 Mathlib.Data.Prod.Basic
{α : Type u_5} {β : Type u_6} (a : α) : Function.Injective (Prod.mk a) - Prod.snd_injective 📋 Mathlib.Data.Prod.Basic
{α : Type u_1} {β : Type u_2} [Subsingleton α] : Function.Injective Prod.snd - Prod.swap_injective 📋 Mathlib.Data.Prod.Basic
{α : Type u_1} {β : Type u_2} : Function.Injective Prod.swap - Prod.mk_left_injective 📋 Mathlib.Data.Prod.Basic
{α : Type u_5} {β : Type u_6} (b : β) : Function.Injective fun a => (a, b) - Function.Injective.prodMap 📋 Mathlib.Data.Prod.Basic
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → γ} {g : β → δ} (hf : Function.Injective f) (hg : Function.Injective g) : Function.Injective (Prod.map f g) - LinearOrder.toPartialOrder_injective 📋 Mathlib.Order.Basic
{α : Type u_2} : Function.Injective (@LinearOrder.toPartialOrder α) - PartialOrder.toPreorder_injective 📋 Mathlib.Order.Basic
{α : Type u_2} : Function.Injective (@PartialOrder.toPreorder α) - Preorder.toLE_injective 📋 Mathlib.Order.Basic
{α : Type u_2} : Function.Injective (@Preorder.toLE α) - PLift.down_injective 📋 Mathlib.Logic.Function.ULift
{α : Sort u_1} : Function.Injective PLift.down - ULift.down_injective 📋 Mathlib.Logic.Function.ULift
{α : Type u_1} : Function.Injective ULift.down - Nat.succ_injective 📋 Mathlib.Data.Nat.Basic
: Function.Injective Nat.succ - Nat.dvd_left_injective 📋 Mathlib.Data.Nat.Basic
: Function.Injective fun x1 x2 => x1 ∣ x2 - Nat.pow_left_injective 📋 Mathlib.Data.Nat.Basic
{n : ℕ} (hn : n ≠ 0) : Function.Injective fun a => a ^ n - Nat.pow_right_injective 📋 Mathlib.Data.Nat.Basic
{a : ℕ} (ha : 2 ≤ a) : Function.Injective fun x => a ^ x - Nat.leRecOn_injective 📋 Mathlib.Data.Nat.Basic
{C : ℕ → Sort u_1} {n m : ℕ} (hnm : n ≤ m) (next : {k : ℕ} → C k → C (k + 1)) (Hnext : ∀ (n : ℕ), Function.Injective next) : Function.Injective (Nat.leRecOn hnm fun {k} => next) - Function.Injective.of_eq_imp_le 📋 Mathlib.Order.Monotone.Defs
{α : Type u} {β : Type v} [PartialOrder α] {f : α → β} (h : ∀ {x y : α}, f x = f y → x ≤ y) : Function.Injective f - Function.Injective.of_lt_imp_ne 📋 Mathlib.Order.Monotone.Defs
{α : Type u} {β : Type v} [LinearOrder α] {f : α → β} (h : ∀ (x y : α), x < y → f x ≠ f y) : Function.Injective f - StrictAnti.injective 📋 Mathlib.Order.Monotone.Basic
{α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} (hf : StrictAnti f) : Function.Injective f - StrictMono.injective 📋 Mathlib.Order.Monotone.Basic
{α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} (hf : StrictMono f) : Function.Injective f - Complementeds.coe_injective 📋 Mathlib.Order.Disjoint
{α : Type u_1} [Lattice α] [BoundedOrder α] : Function.Injective Subtype.val - Set.ofPred_injective 📋 Mathlib.Data.Set.Basic
{α : Type u} : Function.Injective Set.ofPred - Set.setOf_injective 📋 Mathlib.Data.Set.Basic
{α : Type u} : Function.Injective Set.ofPred - Set.mem_injective 📋 Mathlib.Data.Set.Basic
{α : Type u} : Function.Injective Membership.mem - Set.singleton_injective 📋 Mathlib.Data.Set.Insert
{α : Type u_1} : Function.Injective singleton - GaloisCoinsertion.l_injective 📋 Mathlib.Order.GaloisConnection.Defs
{α : Type u} {β : Type v} {u : α → β} {l : β → α} [Preorder α] [PartialOrder β] (gi : GaloisCoinsertion l u) : Function.Injective l - GaloisInsertion.u_injective 📋 Mathlib.Order.GaloisConnection.Defs
{α : Type u} {β : Type v} {l : α → β} {u : β → α} [Preorder α] [PartialOrder β] (gi : GaloisInsertion l u) : Function.Injective u - compl_injective 📋 Mathlib.Order.BooleanAlgebra.Basic
{α : Type u} [BooleanAlgebra α] : Function.Injective compl - EquivFunctor.mapEquiv.injective 📋 Mathlib.Control.EquivFunctor
(f : Type u₀ → Type u₁) [Applicative f] [LawfulApplicative f] {α β : Type u₀} (h : ∀ (γ : Type u₀), Function.Injective pure) : Function.Injective (EquivFunctor.mapEquiv f) - Equiv.optionCongr_injective 📋 Mathlib.Logic.Equiv.Option
{α : Type u_1} {β : Type u_2} : Function.Injective Equiv.optionCongr - Prod.toSigma_injective 📋 Mathlib.Data.Sigma.Basic
{α : Type u_7} {β : Type u_8} : Function.Injective Prod.toSigma - sigma_mk_injective 📋 Mathlib.Data.Sigma.Basic
{α : Type u_1} {β : α → Type u_4} {i : α} : Function.Injective (Sigma.mk i) - Sigma.fst_injective 📋 Mathlib.Data.Sigma.Basic
{α : Type u_1} {β : α → Type u_4} [h : ∀ (a : α), Subsingleton (β a)] : Function.Injective Sigma.fst - Function.Injective.of_sigma_map 📋 Mathlib.Data.Sigma.Basic
{α₁ : Type u_2} {α₂ : Type u_3} {β₁ : α₁ → Type u_5} {β₂ : α₂ → Type u_6} {f₁ : α₁ → α₂} {f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)} (h : Function.Injective (Sigma.map f₁ f₂)) (a : α₁) : Function.Injective (f₂ a) - Function.Injective.sigma_map 📋 Mathlib.Data.Sigma.Basic
{α₁ : Type u_2} {α₂ : Type u_3} {β₁ : α₁ → Type u_5} {β₂ : α₂ → Type u_6} {f₁ : α₁ → α₂} {f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)} (h₁ : Function.Injective f₁) (h₂ : ∀ (a : α₁), Function.Injective (f₂ a)) : Function.Injective (Sigma.map f₁ f₂) - Equiv.swap_injective_of_left 📋 Mathlib.Logic.Equiv.Basic
{α : Sort u_1} [DecidableEq α] (a : α) : Function.Injective fun x => Equiv.swap a x - Equiv.swap_injective_of_right 📋 Mathlib.Logic.Equiv.Basic
{α : Sort u_1} [DecidableEq α] (a : α) : Function.Injective fun x => Equiv.swap x a - symmDiff_left_injective 📋 Mathlib.Order.SymmDiff
{α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) : Function.Injective fun x => symmDiff x a - symmDiff_right_injective 📋 Mathlib.Order.SymmDiff
{α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) : Function.Injective fun x => symmDiff a x - bihimp_left_injective 📋 Mathlib.Order.SymmDiff
{α : Type u_2} [BooleanAlgebra α] (a : α) : Function.Injective fun x => bihimp x a - bihimp_right_injective 📋 Mathlib.Order.SymmDiff
{α : Type u_2} [BooleanAlgebra α] (a : α) : Function.Injective fun x => bihimp a x - Set.inclusion_injective 📋 Mathlib.Data.Set.Inclusion
{α : Type u_1} {s t : Set α} (h : s ⊆ t) : Function.Injective (Set.inclusion h) - Set.rangeSplitting_injective 📋 Mathlib.Data.Set.Image
{α : Type u_1} {β : Type u_2} (f : α → β) : Function.Injective (Set.rangeSplitting f) - Function.Injective.image_injective 📋 Mathlib.Data.Set.Image
{α : Type u_1} {β : Type u_2} {f : α → β} (hf : Function.Injective f) : Function.Injective (Set.image f) - Function.Surjective.preimage_injective 📋 Mathlib.Data.Set.Image
{α : Type u_1} {β : Type u_2} {f : α → β} (hf : Function.Surjective f) : Function.Injective (Set.preimage f) - injective_toPullbackDiag 📋 Mathlib.Data.Set.Prod
{X : Type u_1} {Y : Sort u_2} (f : X → Y) : Function.Injective (toPullbackDiag f) - Set.InjOn.injective 📋 Mathlib.Data.Set.Restrict
{α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} : Set.InjOn f s → Function.Injective (s.domRestrict f) - Set.restrictPreimage_injective 📋 Mathlib.Data.Set.Restrict
{α : Type u_1} {β : Type u_2} (t : Set β) {f : α → β} (hf : Function.Injective f) : Function.Injective (t.restrictPreimage f) - Function.Injective.restrictPreimage 📋 Mathlib.Data.Set.Restrict
{α : Type u_1} {β : Type u_2} (t : Set β) {f : α → β} (hf : Function.Injective f) : Function.Injective (t.restrictPreimage f) - Function.Injective.codRestrict 📋 Mathlib.Data.Set.Restrict
{α : Type u_1} {ι : Sort u_5} {f : ι → α} {s : Set α} (h : ∀ (x : ι), f x ∈ s) : Function.Injective f → Function.Injective (Set.codRestrict f s h) - Set.graphOn_univ_injective 📋 Mathlib.Data.Set.Function
{α : Type u_1} {β : Type u_2} : Function.Injective fun f => Set.graphOn f Set.univ - Set.InjOn.imageFactorization_injective 📋 Mathlib.Data.Set.Function
{α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} (h : Set.InjOn f s) : Function.Injective (Set.imageFactorization f s) - AddMonoidHom.toAddHom_injective 📋 Mathlib.Algebra.Group.Hom.Defs
{M : Type u_4} {N : Type u_5} [AddZero M] [AddZero N] : Function.Injective AddMonoidHom.toAddHom - AddMonoidHom.toZeroHom_injective 📋 Mathlib.Algebra.Group.Hom.Defs
{M : Type u_4} {N : Type u_5} [AddZero M] [AddZero N] : Function.Injective AddMonoidHom.toZeroHom - MonoidHom.toMulHom_injective 📋 Mathlib.Algebra.Group.Hom.Defs
{M : Type u_4} {N : Type u_5} [MulOne M] [MulOne N] : Function.Injective MonoidHom.toMulHom - MonoidHom.toOneHom_injective 📋 Mathlib.Algebra.Group.Hom.Defs
{M : Type u_4} {N : Type u_5} [MulOne M] [MulOne N] : Function.Injective MonoidHom.toOneHom - AddEquiv.toEquiv_injective 📋 Mathlib.Algebra.Group.Equiv.Defs
{α : Type u_9} {β : Type u_10} [Add α] [Add β] : Function.Injective AddEquiv.toEquiv - MulEquiv.toEquiv_injective 📋 Mathlib.Algebra.Group.Equiv.Defs
{α : Type u_9} {β : Type u_10} [Mul α] [Mul β] : Function.Injective MulEquiv.toEquiv - AddEquiv.toAddMonoidHom_injective 📋 Mathlib.Algebra.Group.Equiv.Defs
{M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] : Function.Injective AddEquiv.toAddMonoidHom - MulEquiv.toMonoidHom_injective 📋 Mathlib.Algebra.Group.Equiv.Defs
{M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] : Function.Injective MulEquiv.toMonoidHom - AddEquiv.injective 📋 Mathlib.Algebra.Group.Equiv.Defs
{M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) : Function.Injective ⇑e - MulEquiv.injective 📋 Mathlib.Algebra.Group.Equiv.Defs
{M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) : Function.Injective ⇑e - AddEquiv.comp_left_injective 📋 Mathlib.Algebra.Group.Equiv.Defs
{M : Type u_4} {N : Type u_5} {P : Type u_6} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (e : M ≃+ N) : Function.Injective fun f => f.comp ↑e - AddEquiv.comp_right_injective 📋 Mathlib.Algebra.Group.Equiv.Defs
{M : Type u_4} {N : Type u_5} {P : Type u_6} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (e : M ≃+ N) : Function.Injective fun f => (↑e).comp f - MulEquiv.comp_left_injective 📋 Mathlib.Algebra.Group.Equiv.Defs
{M : Type u_4} {N : Type u_5} {P : Type u_6} [MulOneClass M] [MulOneClass N] [MulOneClass P] (e : M ≃* N) : Function.Injective fun f => f.comp ↑e - MulEquiv.comp_right_injective 📋 Mathlib.Algebra.Group.Equiv.Defs
{M : Type u_4} {N : Type u_5} {P : Type u_6} [MulOneClass M] [MulOneClass N] [MulOneClass P] (e : M ≃* N) : Function.Injective fun f => (↑e).comp f - inv_injective 📋 Mathlib.Algebra.Group.Basic
{G : Type u_3} [InvolutiveInv G] : Function.Injective Inv.inv - neg_injective 📋 Mathlib.Algebra.Group.Basic
{G : Type u_3} [InvolutiveNeg G] : Function.Injective Neg.neg - div_left_injective 📋 Mathlib.Algebra.Group.Basic
{G : Type u_3} [Group G] {b : G} : Function.Injective fun a => a / b - div_right_injective 📋 Mathlib.Algebra.Group.Basic
{G : Type u_3} [Group G] {b : G} : Function.Injective fun a => b / a - sub_left_injective 📋 Mathlib.Algebra.Group.Basic
{G : Type u_3} [AddGroup G] {b : G} : Function.Injective fun a => a - b - sub_right_injective 📋 Mathlib.Algebra.Group.Basic
{G : Type u_3} [AddGroup G] {b : G} : Function.Injective fun a => b - a - nsmul_right_injective 📋 Mathlib.Algebra.Group.Torsion
{M : Type u_1} [AddMonoid M] [IsAddTorsionFree M] {n : ℕ} (hn : n ≠ 0) : Function.Injective fun a => n • a - pow_left_injective 📋 Mathlib.Algebra.Group.Torsion
{M : Type u_1} [Monoid M] [IsMulTorsionFree M] {n : ℕ} (hn : n ≠ 0) : Function.Injective fun a => a ^ n - zpow_left_injective 📋 Mathlib.Algebra.Group.Torsion
{G : Type u_2} [Group G] [IsMulTorsionFree G] {n : ℤ} : n ≠ 0 → Function.Injective fun a => a ^ n - zsmul_right_injective 📋 Mathlib.Algebra.Group.Torsion
{G : Type u_2} [AddGroup G] [IsAddTorsionFree G] {n : ℤ} : n ≠ 0 → Function.Injective fun a => n • a - AddUnits.val_injective 📋 Mathlib.Algebra.Group.Units.Defs
{α : Type u} [AddMonoid α] : Function.Injective AddUnits.val - Units.val_injective 📋 Mathlib.Algebra.Group.Units.Defs
{α : Type u} [Monoid α] : Function.Injective Units.val - IsAddUnit.add_left_injective 📋 Mathlib.Algebra.Group.Units.Basic
{M : Type u_1} [AddMonoid M] {b : M} (h : IsAddUnit b) : Function.Injective fun x => x + b - IsAddUnit.add_right_injective 📋 Mathlib.Algebra.Group.Units.Basic
{M : Type u_1} [AddMonoid M] {a : M} (h : IsAddUnit a) : Function.Injective fun x => a + x - IsUnit.mul_left_injective 📋 Mathlib.Algebra.Group.Units.Basic
{M : Type u_1} [Monoid M] {b : M} (h : IsUnit b) : Function.Injective fun x => x * b - IsUnit.mul_right_injective 📋 Mathlib.Algebra.Group.Units.Basic
{M : Type u_1} [Monoid M] {a : M} (h : IsUnit a) : Function.Injective fun x => a * x - AddUnits.coeHom_injective 📋 Mathlib.Algebra.Group.Units.Hom
{M : Type u} [AddMonoid M] : Function.Injective ⇑(AddUnits.coeHom M) - Units.coeHom_injective 📋 Mathlib.Algebra.Group.Units.Hom
{M : Type u} [Monoid M] : Function.Injective ⇑(Units.coeHom M) - AddUnits.map_injective 📋 Mathlib.Algebra.Group.Units.Hom
{M : Type u} {N : Type v} [AddMonoid M] [AddMonoid N] {f : M →+ N} (hf : Function.Injective ⇑f) : Function.Injective ⇑(AddUnits.map f) - Units.map_injective 📋 Mathlib.Algebra.Group.Units.Hom
{M : Type u} {N : Type v} [Monoid M] [Monoid N] {f : M →* N} (hf : Function.Injective ⇑f) : Function.Injective ⇑(Units.map f) - AddUnits.embedProduct_injective 📋 Mathlib.Algebra.Group.Prod
(α : Type u_6) [AddMonoid α] : Function.Injective ⇑(AddUnits.embedProduct α) - Units.embedProduct_injective 📋 Mathlib.Algebra.Group.Prod
(α : Type u_6) [Monoid α] : Function.Injective ⇑(Units.embedProduct α) - AddEquivClass.toAddEquiv_injective 📋 Mathlib.Algebra.Group.Equiv.Basic
{F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Add α] [Add β] [AddEquivClass F α β] : Function.Injective AddEquivClass.toAddEquiv - MulEquivClass.toMulEquiv_injective 📋 Mathlib.Algebra.Group.Equiv.Basic
{F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Mul α] [Mul β] [MulEquivClass F α β] : Function.Injective MulEquivClass.toMulEquiv - Equiv.Perm.extendDomainHom_injective 📋 Mathlib.Algebra.Group.End
{α : Type u_4} {β : Type u_5} {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p) : Function.Injective ⇑(Equiv.Perm.extendDomainHom f) - Equiv.Perm.ofSubtype_injective 📋 Mathlib.Algebra.Group.End
{α : Type u_4} {p : α → Prop} [DecidablePred p] : Function.Injective ⇑Equiv.Perm.ofSubtype - Equiv.Perm.sumCongrHom_injective 📋 Mathlib.Algebra.Group.End
{α : Type u_7} {β : Type u_8} : Function.Injective ⇑(Equiv.Perm.sumCongrHom α β) - Equiv.Perm.sigmaCongrRightHom_injective 📋 Mathlib.Algebra.Group.End
{α : Type u_7} {β : α → Type u_8} : Function.Injective ⇑(Equiv.Perm.sigmaCongrRightHom β) - Equiv.Perm.subtypeCongrHom_injective 📋 Mathlib.Algebra.Group.End
{α : Type u_4} (p : α → Prop) [DecidablePred p] : Function.Injective ⇑(Equiv.Perm.subtypeCongrHom p) - mul_left_injective₀ 📋 Mathlib.Algebra.GroupWithZero.Defs
{M₀ : Type u_1} [Mul M₀] [Zero M₀] [IsRightCancelMulZero M₀] {b : M₀} (hb : b ≠ 0) : Function.Injective fun a => a * b - mul_right_injective₀ 📋 Mathlib.Algebra.GroupWithZero.Defs
{M₀ : Type u_1} [Mul M₀] [Zero M₀] [IsLeftCancelMulZero M₀] {a : M₀} (ha : a ≠ 0) : Function.Injective fun x => a * x - GroupWithZero.mul_left_injective 📋 Mathlib.Algebra.GroupWithZero.Basic
{G₀ : Type u_2} [GroupWithZero G₀] {x : G₀} (h : x ≠ 0) : Function.Injective fun y => y * x - GroupWithZero.mul_right_injective 📋 Mathlib.Algebra.GroupWithZero.Basic
{G₀ : Type u_2} [GroupWithZero G₀] {x : G₀} (h : x ≠ 0) : Function.Injective fun y => x * y - MonoidWithZeroHom.toMonoidHom_injective 📋 Mathlib.Algebra.GroupWithZero.Hom
{α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] : Function.Injective MonoidWithZeroHom.toMonoidHom - MonoidWithZeroHom.toZeroHom_injective 📋 Mathlib.Algebra.GroupWithZero.Hom
{α : Type u_2} {β : Type u_3} [MulZeroOneClass α] [MulZeroOneClass β] : Function.Injective MonoidWithZeroHom.toZeroHom - CharZero.cast_injective 📋 Mathlib.Algebra.CharZero.Defs
{R : Type u_1} {inst✝ : AddMonoidWithOne R} [self : CharZero R] : Function.Injective Nat.cast - Nat.cast_injective 📋 Mathlib.Algebra.CharZero.Defs
{R : Type u_1} [AddMonoidWithOne R] [CharZero R] : Function.Injective Nat.cast - Int.ofNat_injective 📋 Mathlib.Data.Int.Basic
: Function.Injective Int.ofNat - Int.pow_right_injective 📋 Mathlib.Data.Int.Basic
{a : ℤ} (h : 1 < a.natAbs) : Function.Injective fun x => a ^ x - NonUnitalRingHom.coe_mulHom_injective 📋 Mathlib.Algebra.Ring.Hom.Defs
{α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] : Function.Injective fun f => ↑f - NonUnitalRingHom.coe_addMonoidHom_injective 📋 Mathlib.Algebra.Ring.Hom.Defs
{α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] : Function.Injective fun f => ↑f - RingHom.coe_addMonoidHom_injective 📋 Mathlib.Algebra.Ring.Hom.Defs
{α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} : Function.Injective fun f => ↑f - RingHom.coe_monoidHom_injective 📋 Mathlib.Algebra.Ring.Hom.Defs
{α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} : Function.Injective fun f => ↑f - Int.cast_injective 📋 Mathlib.Data.Int.Cast.Lemmas
{α : Type u_3} [AddGroupWithOne α] [CharZero α] : Function.Injective Int.cast - AddLECancellable.Injective 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} [Add α] [PartialOrder α] {a : α} (ha : AddLECancellable a) : Function.Injective fun x => a + x - MulLECancellable.Injective 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} [Mul α] [PartialOrder α] {a : α} (ha : MulLECancellable a) : Function.Injective fun x => a * x - AddLECancellable.injective_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} [Add α] [IsAddCommutative α] [PartialOrder α] {a : α} (ha : AddLECancellable a) : Function.Injective fun x => x + a - MulLECancellable.injective_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} [Mul α] [IsMulCommutative α] [PartialOrder α] {a : α} (ha : MulLECancellable a) : Function.Injective fun x => x * a - pow_right_injective₀ 📋 Mathlib.Algebra.Order.GroupWithZero.Basic
{M₀ : Type u_2} [MonoidWithZero M₀] [LinearOrder M₀] [PosMulStrictMono M₀] {a : M₀} [ZeroLEOneClass M₀] (ha₀ : 0 < a) (ha₁ : a ≠ 1) : Function.Injective fun x => a ^ x - zpow_right_injective₀ 📋 Mathlib.Algebra.Order.GroupWithZero.Basic
{G₀ : Type u_3} [GroupWithZero G₀] [LinearOrder G₀] {a : G₀} [PosMulStrictMono G₀] [ZeroLEOneClass G₀] (ha₀ : 0 < a) (ha₁ : a ≠ 1) : Function.Injective fun n => a ^ n - Function.Injective.pprod_map 📋 Mathlib.Data.Prod.PProd
{α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} {f : α → β} {g : γ → δ} (hf : Function.Injective f) (hg : Function.Injective g) : Function.Injective fun x => ⟨f x.fst, g x.snd⟩ - Equiv.toEmbedding_injective 📋 Mathlib.Logic.Embedding.Basic
{α : Sort u} {β : Sort v} : Function.Injective Equiv.toEmbedding - Function.Embedding.inj' 📋 Mathlib.Logic.Embedding.Basic
{α : Sort u_1} {β : Sort u_2} (self : α ↪ β) : Function.Injective self.toFun - Function.Embedding.injective 📋 Mathlib.Logic.Embedding.Basic
{α : Sort u_1} {β : Sort u_2} (f : α ↪ β) : Function.Injective ⇑f - Function.Embedding.coe_injective 📋 Mathlib.Logic.Embedding.Basic
{α : Sort u_1} {β : Sort u_2} : Function.Injective fun f => ⇑f - Function.Embedding.subtype_injective 📋 Mathlib.Logic.Embedding.Basic
{α : Sort u_1} (p : α → Prop) : Function.Injective ⇑(Function.Embedding.subtype p) - RelEmbedding.toEmbedding_injective 📋 Mathlib.Order.RelIso.Basic
{α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : Function.Injective RelEmbedding.toEmbedding
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 ?aIf 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 ?bBy 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 findtsum_lt_tsumeven though the hypothesisf i < g iis 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 c026161