Loogle!
Result
Found 3621 declarations mentioning Function.Injective. Of these, 1596 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) - Nat.xor_left_injective 📋 Batteries.Data.Nat.Bitwise
{x : ℕ} : Function.Injective fun x_1 => x_1 ^^^ x - Nat.xor_right_injective 📋 Batteries.Data.Nat.Bitwise
{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.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.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} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β] : Function.Injective fun f => ⇑f - 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 - Function.Injective.iterate 📋 Mathlib.Logic.Function.Iterate
{α : Type u} {f : α → α} (Hinj : Function.Injective f) (n : ℕ) : Function.Injective f^[n] - 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) - 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 - 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 - 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 - Option.map_injective 📋 Mathlib.Data.Option.Basic
{α : Type u_1} {β : Type u_2} {f : α → β} (Hf : Function.Injective f) : Function.Injective (Option.map f) - 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 - 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 - 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 - injective_of_le_imp_le 📋 Mathlib.Order.Monotone.Defs
{α : Type u} {β : Type v} [PartialOrder α] [Preorder β] (f : α → β) (h : ∀ {x y : α}, f x ≤ f y → x ≤ 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.setOf_injective 📋 Mathlib.Data.Set.Basic
{α : Type u} : Function.Injective setOf - Set.singleton_injective 📋 Mathlib.Data.Set.Insert
{α : Type u} : Function.Injective singleton - GaloisCoinsertion.l_injective 📋 Mathlib.Order.GaloisConnection.Defs
{α : Type u} {β : Type v} {l : α → β} {u : β → α} [PartialOrder α] [Preorder β] (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₂) - 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.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.restrict 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 α] [i : Std.Commutative fun x1 x2 => x1 + x2] [PartialOrder α] {a : α} (ha : AddLECancellable a) : Function.Injective fun x => x + a - MulLECancellable.injective_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} [Mul α] [i : Std.Commutative fun x1 x2 => x1 * x2] [PartialOrder α] {a : α} (ha : MulLECancellable a) : Function.Injective fun x => x * a - 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 - RelIso.toEquiv_injective 📋 Mathlib.Order.RelIso.Basic
{α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : Function.Injective RelIso.toEquiv - injective_of_increasing 📋 Mathlib.Order.RelIso.Basic
{α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [IsTrichotomous α r] [IsIrrefl β s] (f : α → β) (hf : ∀ {x y : α}, r x y → s (f x) (f y)) : Function.Injective f - RelEmbedding.injective 📋 Mathlib.Order.RelIso.Basic
{α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) : Function.Injective ⇑f - RelIso.injective 📋 Mathlib.Order.RelIso.Basic
{α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) : Function.Injective ⇑e - RelEmbedding.coe_fn_injective 📋 Mathlib.Order.RelIso.Basic
{α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : Function.Injective fun f => ⇑f - RelHom.coe_fn_injective 📋 Mathlib.Order.RelIso.Basic
{α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : Function.Injective fun f => ⇑f - RelIso.coe_fn_injective 📋 Mathlib.Order.RelIso.Basic
{α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} : Function.Injective fun f => ⇑f - RelHom.injective_of_increasing 📋 Mathlib.Order.RelIso.Basic
{α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsTrichotomous α r] [IsIrrefl β s] (f : r →r s) : Function.Injective ⇑f - OrderIso.symm_injective 📋 Mathlib.Order.Hom.Basic
{α : Type u_2} {β : Type u_3} [LE α] [LE β] : Function.Injective OrderIso.symm - OrderIso.injective 📋 Mathlib.Order.Hom.Basic
{α : Type u_2} {β : Type u_3} [LE α] [LE β] (e : α ≃o β) : Function.Injective ⇑e - OrderEmbedding.subtype_injective 📋 Mathlib.Order.Hom.Basic
{α : Type u_2} [Preorder α] (p : α → Prop) : Function.Injective ⇑(OrderEmbedding.subtype p) - RelEmbedding.toOrderHom_injective 📋 Mathlib.Order.Hom.Basic
{α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] (f : (fun x1 x2 => x1 < x2) ↪r fun x1 x2 => x1 < x2) : Function.Injective ⇑f.toRelHom.toOrderHom
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:
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.
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 abad10c