Loogle!

Result

Found 658 declarations mentioning Set.MapsTo. Of these, only the first 200 are shown.

• Set.MapsTo 📋 Mathlib.Data.Set.Operations
  {α : Type u} {β : Type v} (f : α → β) (s : Set α) (t : Set β) : Prop
• Set.mapsTo_image 📋 Mathlib.Data.Set.Operations
  {α : Type u} {β : Type v} (f : α → β) (s : Set α) : Set.MapsTo f s (f '' s)
• Set.mapsTo_preimage 📋 Mathlib.Data.Set.Operations
  {α : Type u} {β : Type v} (f : α → β) (t : Set β) : Set.MapsTo f (f ⁻¹' t) t
• Set.MapsTo.restrict 📋 Mathlib.Data.Set.Operations
  {α : Type u} {β : Type v} (f : α → β) (s : Set α) (t : Set β) (h : Set.MapsTo f s t) : ↑s → ↑t
• AntitoneOn.comp 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} {t : Set β} (hg : AntitoneOn g t) (hf : AntitoneOn f s) (hs : Set.MapsTo f s t) : MonotoneOn (g ∘ f) s
• AntitoneOn.comp_MonotoneOn 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} {t : Set β} (hg : AntitoneOn g t) (hf : MonotoneOn f s) (hs : Set.MapsTo f s t) : AntitoneOn (g ∘ f) s
• MonotoneOn.comp 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} {t : Set β} (hg : MonotoneOn g t) (hf : MonotoneOn f s) (hs : Set.MapsTo f s t) : MonotoneOn (g ∘ f) s
• MonotoneOn.comp_AntitoneOn 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} {t : Set β} (hg : MonotoneOn g t) (hf : AntitoneOn f s) (hs : Set.MapsTo f s t) : AntitoneOn (g ∘ f) s
• StrictAntiOn.comp 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} {t : Set β} (hg : StrictAntiOn g t) (hf : StrictAntiOn f s) (hs : Set.MapsTo f s t) : StrictMonoOn (g ∘ f) s
• StrictAntiOn.comp_strictMonoOn 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} {t : Set β} (hg : StrictAntiOn g t) (hf : StrictMonoOn f s) (hs : Set.MapsTo f s t) : StrictAntiOn (g ∘ f) s
• StrictMonoOn.comp 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} {t : Set β} (hg : StrictMonoOn g t) (hf : StrictMonoOn f s) (hs : Set.MapsTo f s t) : StrictMonoOn (g ∘ f) s
• StrictMonoOn.comp_strictAntiOn 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} {t : Set β} (hg : StrictMonoOn g t) (hf : StrictAntiOn f s) (hs : Set.MapsTo f s t) : StrictAntiOn (g ∘ f) s
• Set.mapsTo_fst_prod 📋 Mathlib.Data.Set.Prod
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} : Set.MapsTo Prod.fst (s ×ˢ t) s
• Set.mapsTo_snd_prod 📋 Mathlib.Data.Set.Prod
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} : Set.MapsTo Prod.snd (s ×ˢ t) t
• Set.mapsTo_swap_prod 📋 Mathlib.Data.Set.Prod
  {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) : Set.MapsTo Prod.swap (s ×ˢ t) (t ×ˢ s)
• Set.piMap_mapsTo_pi 📋 Mathlib.Data.Set.Prod
  {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {I : Set ι} {f : (i : ι) → α i → β i} {s : (i : ι) → Set (α i)} {t : (i : ι) → Set (β i)} (h : ∀ i ∈ I, Set.MapsTo (f i) (s i) (t i)) : Set.MapsTo (Pi.map f) (I.pi s) (I.pi t)
• Set.MapsTo.restrict_inj 📋 Mathlib.Data.Set.Restrict
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : Set.MapsTo f s t) : Function.Injective (Set.MapsTo.restrict f s t h) ↔ Set.InjOn f s
• Set.MapsTo.restrict_surjective_iff 📋 Mathlib.Data.Set.Restrict
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : Set.MapsTo f s t) : Function.Surjective (Set.MapsTo.restrict f s t h) ↔ Set.SurjOn f s t
• Set.MapsTo.val_restrict_apply 📋 Mathlib.Data.Set.Restrict
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : Set.MapsTo f s t) (x : ↑s) : ↑(Set.MapsTo.restrict f s t h x) = f ↑x
• Set.MapsTo.coe_iterate_restrict 📋 Mathlib.Data.Set.Restrict
  {α : Type u_1} {s : Set α} {f : α → α} (h : Set.MapsTo f s s) (x : ↑s) (k : ℕ) : ↑((Set.MapsTo.restrict f s s h)^[k] x) = f^[k] ↑x
• Set.mapsTo_iff_exists_map_subtype 📋 Mathlib.Data.Set.Restrict
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} : Set.MapsTo f s t ↔ ∃ g, ∀ (x : ↑s), f ↑x = ↑(g x)
• Set.MapsTo.coe_restrict 📋 Mathlib.Data.Set.Restrict
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : Set.MapsTo f s t) : Subtype.val ∘ Set.MapsTo.restrict f s t h = s.domRestrict f
• Set.MapsTo.range_restrict 📋 Mathlib.Data.Set.Restrict
  {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) (t : Set β) (h : Set.MapsTo f s t) : Set.range (Set.MapsTo.restrict f s t h) = Subtype.val ⁻¹' f '' s
• Set.MapsTo.restrict_eq_codRestrict 📋 Mathlib.Data.Set.Restrict
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : Set.MapsTo f s t) : Set.MapsTo.restrict f s t h = Set.codRestrict (s.domRestrict f) t ⋯
• Set.MapsTo.restrict_commutes 📋 Mathlib.Data.Set.Restrict
  {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) (t : Set β) (h : Set.MapsTo f s t) : Subtype.val ∘ Set.MapsTo.restrict f s t h = f ∘ Subtype.val
• Set.mapsTo_id 📋 Mathlib.Data.Set.Function
  {α : Type u_1} (s : Set α) : Set.MapsTo id s s
• Set.mapsTo_of_subsingleton 📋 Mathlib.Data.Set.Function
  {α : Type u_1} [Subsingleton α] (f : α → α) (s : Set α) : Set.MapsTo f s s
• Set.mapsTo_univ 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) : Set.MapsTo f s Set.univ
• Set.mapsTo_range 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) : Set.MapsTo f s (Set.range f)
• Set.mapsTo_empty 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} (f : α → β) (t : Set β) : Set.MapsTo f ∅ t
• Set.BijOn.mapsTo 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : Set.BijOn f s t) : Set.MapsTo f s t
• Set.MapsTo.nonempty 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : Set.MapsTo f s t) (hs : s.Nonempty) : t.Nonempty
• Set.MapsTo.iterate 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {f : α → α} {s : Set α} (h : Set.MapsTo f s s) (n : ℕ) : Set.MapsTo f^[n] s s
• Set.mapsTo_of_subsingleton' 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} [Subsingleton β] (f : α → β) (h : s.Nonempty → t.Nonempty) : Set.MapsTo f s t
• Set.mapsTo_prodMap_diagonal 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {f : α → β} : Set.MapsTo (Prod.map f f) (Set.diagonal α) (Set.diagonal β)
• Set.mapsTo_univ_iff 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {t : Set β} {f : α → β} : Set.MapsTo f Set.univ t ↔ ∀ (x : α), f x ∈ t
• Set.mapsTo_univ_iff_range_subset 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {t : Set β} {f : α → β} : Set.MapsTo f Set.univ t ↔ Set.range f ⊆ t
• Set.InjOn.iterate 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {f : α → α} {s : Set α} (h : Set.InjOn f s) (hf : Set.MapsTo f s s) (n : ℕ) : Set.InjOn f^[n] s
• Set.MapsTo.image_subset 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : Set.MapsTo f s t) : f '' s ⊆ t
• Set.MapsTo.subset_preimage 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (hf : Set.MapsTo f s t) : s ⊆ f ⁻¹' t
• Set.mapsTo_empty_iff 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} : Set.MapsTo f s ∅ ↔ s = ∅
• Set.mapsTo_iff_image_subset 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} : Set.MapsTo f s t ↔ f '' s ⊆ t
• Set.mapsTo_iff_subset_preimage 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} : Set.MapsTo f s t ↔ s ⊆ f ⁻¹' t
• Function.Semiconj.mapsTo_range 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {fa : α → α} {fb : β → β} {f : α → β} (h : Function.Semiconj f fa fb) : Set.MapsTo fb (Set.range f) (Set.range f)
• Set.SurjOn.mapsTo_invFunOn 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} [Nonempty α] (h : Set.SurjOn f s t) : Set.MapsTo (Function.invFunOn f s) t s
• Set.LeftInvOn.mapsTo 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {f' : β → α} (h : Set.LeftInvOn f' f s) (hf : Set.SurjOn f s t) : Set.MapsTo f' t s
• Set.LeftInvOn.surjOn 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {f' : β → α} (h : Set.LeftInvOn f' f s) (hf : Set.MapsTo f s t) : Set.SurjOn f' t s
• Set.MapsTo.congr 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f₁ f₂ : α → β} (h₁ : Set.MapsTo f₁ s t) (h : Set.EqOn f₁ f₂ s) : Set.MapsTo f₂ s t
• Set.RightInvOn.mapsTo 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {f' : β → α} (h : Set.RightInvOn f' f t) (hf : Set.SurjOn f' t s) : Set.MapsTo f s t
• Set.RightInvOn.surjOn 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {f' : β → α} (hf : Set.RightInvOn f' f t) (hf' : Set.MapsTo f' t s) : Set.SurjOn f s t
• Set.mapsTo_singleton 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {t : Set β} {f : α → β} {x : α} : Set.MapsTo f {x} t ↔ f x ∈ t
• Set.EqOn.mapsTo_iff 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f₁ f₂ : α → β} (H : Set.EqOn f₁ f₂ s) : Set.MapsTo f₁ s t ↔ Set.MapsTo f₂ s t
• Set.MapsTo.mono_left 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t : Set β} {f : α → β} (hf : Set.MapsTo f s₁ t) (hs : s₂ ⊆ s₁) : Set.MapsTo f s₂ t
• Set.MapsTo.mono_right 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s : Set α} {t₁ t₂ : Set β} {f : α → β} (hf : Set.MapsTo f s t₁) (ht : t₁ ⊆ t₂) : Set.MapsTo f s t₂
• Set.SurjOn.image_eq_of_mapsTo 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h₁ : Set.SurjOn f s t) (h₂ : Set.MapsTo f s t) : f '' s = t
• Set.mapsTo_range_iff 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {t : Set β} {f : α → β} {g : ι → α} : Set.MapsTo f (Set.range g) t ↔ ∀ (i : ι), f (g i) ∈ t
• Set.image_eq_iff_surjOn_mapsTo 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} : f '' s = t ↔ Set.SurjOn f s t ∧ Set.MapsTo f s t
• Set.BijOn.mk 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h₁ : Set.MapsTo f s t) (h₂ : Set.InjOn f s) (h₃ : Set.SurjOn f s t) : Set.BijOn f s t
• Set.MapsTo.comp_left 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {f : α → β} (g : β → γ) (hf : Set.MapsTo f s t) : Set.MapsTo (g ∘ f) s (g '' t)
• Set.MapsTo.comp_right 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β → γ} {s : Set β} {t : Set γ} (hg : Set.MapsTo g s t) (f : α → β) : Set.MapsTo (g ∘ f) (f ⁻¹' s) t
• Set.mapsTo_image_iff 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : γ → α} {s : Set γ} {t : Set β} : Set.MapsTo f (g '' s) t ↔ Set.MapsTo (f ∘ g) s t
• Set.MapsTo.inter 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s : Set α} {t₁ t₂ : Set β} {f : α → β} (h₁ : Set.MapsTo f s t₁) (h₂ : Set.MapsTo f s t₂) : Set.MapsTo f s (t₁ ∩ t₂)
• Set.MapsTo.surjOn_compl 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : Set.MapsTo f s t) (h' : Function.Surjective f) : Set.SurjOn f sᶜ tᶜ
• Set.MapsTo.union 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t : Set β} {f : α → β} (h₁ : Set.MapsTo f s₁ t) (h₂ : Set.MapsTo f s₂ t) : Set.MapsTo f (s₁ ∪ s₂) t
• Set.SurjOn.mapsTo_compl 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : Set.SurjOn f s t) (h' : Function.Injective f) : Set.MapsTo f sᶜ tᶜ
• Set.InvOn.bijOn 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {f' : β → α} (h : Set.InvOn f' f s t) (hf : Set.MapsTo f s t) (hf' : Set.MapsTo f' t s) : Set.BijOn f s t
• Set.eqOn_of_leftInvOn_of_rightInvOn 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {f₁' f₂' : β → α} (h₁ : Set.LeftInvOn f₁' f s) (h₂ : Set.RightInvOn f₂' f t) (h : Set.MapsTo f₂' t s) : Set.EqOn f₁' f₂' t
• Set.mapsTo_inter 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s : Set α} {t₁ t₂ : Set β} {f : α → β} : Set.MapsTo f s (t₁ ∩ t₂) ↔ Set.MapsTo f s t₁ ∧ Set.MapsTo f s t₂
• Set.mapsTo_union 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t : Set β} {f : α → β} : Set.MapsTo f (s₁ ∪ s₂) t ↔ Set.MapsTo f s₁ t ∧ Set.MapsTo f s₂ t
• Set.LeftInvOn.congr_left 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {f₁' f₂' : β → α} (h₁ : Set.LeftInvOn f₁' f s) {t : Set β} (h₁' : Set.MapsTo f s t) (heq : Set.EqOn f₁' f₂' t) : Set.LeftInvOn f₂' f s
• Set.MapsTo.comp 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {p : Set γ} {f : α → β} {g : β → γ} (h₁ : Set.MapsTo g t p) (h₂ : Set.MapsTo f s t) : Set.MapsTo (g ∘ f) s p
• Set.MapsTo.insert 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : Set.MapsTo f s t) (x : α) : Set.MapsTo f (insert x s) (insert (f x) t)
• Set.RightInvOn.congr_right 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f₁ f₂ : α → β} {f' : β → α} (h₁ : Set.RightInvOn f' f₁ t) (hg : Set.MapsTo f' t s) (heq : Set.EqOn f₁ f₂ s) : Set.RightInvOn f' f₂ t
• Set.SurjOn.of_comp 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {p : Set γ} {f : α → β} {g : β → γ} (h : Set.SurjOn (g ∘ f) s p) (hr : Set.MapsTo f s t) : Set.SurjOn g t p
• Set.InjOn.comp 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {f : α → β} {g : β → γ} (hg : Set.InjOn g t) (hf : Set.InjOn f s) (h : Set.MapsTo f s t) : Set.InjOn (g ∘ f) s
• Function.Semiconj.mapsTo_image 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {fa : α → α} {fb : β → β} {f : α → β} {s t : Set α} (h : Function.Semiconj f fa fb) (ha : Set.MapsTo fa s t) : Set.MapsTo fb (f '' s) (f '' t)
• Function.Semiconj.mapsTo_image_right 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {fa : α → α} {fb : β → β} {f : α → β} {s : Set α} {t : Set β} (h : Function.Semiconj f fa fb) (hst : Set.MapsTo f s t) : Set.MapsTo f (fa '' s) (fb '' t)
• Function.Semiconj.mapsTo_preimage 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {fa : α → α} {fb : β → β} {f : α → β} (h : Function.Semiconj f fa fb) {s t : Set β} (hb : Set.MapsTo fb s t) : Set.MapsTo fa (f ⁻¹' s) (f ⁻¹' t)
• Set.MapsTo.mono 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β} {f : α → β} (hf : Set.MapsTo f s₁ t₁) (hs : s₂ ⊆ s₁) (ht : t₁ ⊆ t₂) : Set.MapsTo f s₂ t₂
• Set.InjOn.rightInvOn_of_leftInvOn 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {f' : β → α} (hf : Set.InjOn f s) (hf' : Set.LeftInvOn f f' t) (h₁ : Set.MapsTo f s t) (h₂ : Set.MapsTo f' t s) : Set.RightInvOn f f' s
• Set.EqOn.comp_right 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {f : α → β} {g₁ g₂ : β → γ} (hg : Set.EqOn g₁ g₂ t) (hf : Set.MapsTo f s t) : Set.EqOn (g₁ ∘ f) (g₂ ∘ f) s
• Set.MapsTo.inter_inter 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β} {f : α → β} (h₁ : Set.MapsTo f s₁ t₁) (h₂ : Set.MapsTo f s₂ t₂) : Set.MapsTo f (s₁ ∩ s₂) (t₁ ∩ t₂)
• Set.MapsTo.union_union 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β} {f : α → β} (h₁ : Set.MapsTo f s₁ t₁) (h₂ : Set.MapsTo f s₂ t₂) : Set.MapsTo f (s₁ ∪ s₂) (t₁ ∪ t₂)
• Set.MapsTo.iterate_restrict 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {f : α → α} {s : Set α} (h : Set.MapsTo f s s) (n : ℕ) : (Set.MapsTo.restrict f s s h)^[n] = Set.MapsTo.restrict f^[n] s s ⋯
• Set.SurjOn.forall 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {p : β → Prop} (hf : Set.SurjOn f s t) (hf' : Set.MapsTo f s t) : (∀ y ∈ t, p y) ↔ ∀ x ∈ s, p (f x)
• Set.SurjOn.cancel_right 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {f : α → β} {g₁ g₂ : β → γ} (hf : Set.SurjOn f s t) (hf' : Set.MapsTo f s t) : Set.EqOn (g₁ ∘ f) (g₂ ∘ f) s ↔ Set.EqOn g₁ g₂ t
• Set.LeftInvOn.comp 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {f : α → β} {g : β → γ} {f' : β → α} {g' : γ → β} (hf' : Set.LeftInvOn f' f s) (hg' : Set.LeftInvOn g' g t) (hf : Set.MapsTo f s t) : Set.LeftInvOn (f' ∘ g') (g ∘ f) s
• Set.MapsTo.mem_iff 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : Set.MapsTo f s t) (hc : Set.MapsTo f sᶜ tᶜ) {x : α} : f x ∈ t ↔ x ∈ s
• Set.RightInvOn.comp 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Set β} {p : Set γ} {f : α → β} {g : β → γ} {f' : β → α} {g' : γ → β} (hf : Set.RightInvOn f' f t) (hg : Set.RightInvOn g' g p) (g'pt : Set.MapsTo g' p t) : Set.RightInvOn (f' ∘ g') (g ∘ f) p
• Set.EqOn.cancel_left 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {f₁ f₂ : α → β} {g : β → γ} (h : Set.EqOn (g ∘ f₁) (g ∘ f₂) s) (hg : Set.InjOn g t) (hf₁ : Set.MapsTo f₁ s t) (hf₂ : Set.MapsTo f₂ s t) : Set.EqOn f₁ f₂ s
• Set.InjOn.cancel_left 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {f₁ f₂ : α → β} {g : β → γ} (hg : Set.InjOn g t) (hf₁ : Set.MapsTo f₁ s t) (hf₂ : Set.MapsTo f₂ s t) : Set.EqOn (g ∘ f₁) (g ∘ f₂) s ↔ Set.EqOn f₁ f₂ s
• Set.MapsTo.prodMk 📋 Mathlib.Data.Set.Function
  {α : Type u_6} {β₁ : Type u_7} {β₂ : Type u_8} {s : Set α} {t₁ : Set β₁} {t₂ : Set β₂} {f₁ : α → β₁} {f₂ : α → β₂} (h₁ : Set.MapsTo f₁ s t₁) (h₂ : Set.MapsTo f₂ s t₂) : Set.MapsTo (fun x => (f₁ x, f₂ x)) s (t₁ ×ˢ t₂)
• Set.BijOn.inter_mapsTo 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β} {f : α → β} (h₁ : Set.BijOn f s₁ t₁) (h₂ : Set.MapsTo f s₂ t₂) (h₃ : s₁ ∩ f ⁻¹' t₂ ⊆ s₂) : Set.BijOn f (s₁ ∩ s₂) (t₁ ∩ t₂)
• Set.MapsTo.inter_bijOn 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β} {f : α → β} (h₁ : Set.MapsTo f s₁ t₁) (h₂ : Set.BijOn f s₂ t₂) (h₃ : s₂ ∩ f ⁻¹' t₁ ⊆ s₁) : Set.BijOn f (s₁ ∩ s₂) (t₁ ∩ t₂)
• Set.InvOn.comp 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {p : Set γ} {f : α → β} {g : β → γ} {f' : β → α} {g' : γ → β} (hf : Set.InvOn f' f s t) (hg : Set.InvOn g' g t p) (fst : Set.MapsTo f s t) (g'pt : Set.MapsTo g' p t) : Set.InvOn (f' ∘ g') (g ∘ f) s p
• Equiv.bijOn' 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} (e : α ≃ β) {s : Set α} {t : Set β} (h₁ : Set.MapsTo (⇑e) s t) (h₂ : Set.MapsTo (⇑e.symm) t s) : Set.BijOn (⇑e) s t
• Set.MapsTo.prodMap 📋 Mathlib.Data.Set.Function
  {α₁ : Type u_6} {α₂ : Type u_7} {β₁ : Type u_8} {β₂ : Type u_9} {s₁ : Set α₁} {s₂ : Set α₂} {t₁ : Set β₁} {t₂ : Set β₂} {f₁ : α₁ → β₁} {f₂ : α₂ → β₂} (h₁ : Set.MapsTo f₁ s₁ t₁) (h₂ : Set.MapsTo f₂ s₂ t₂) : Set.MapsTo (fun x => (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ t₂)
• Set.MapsTo.extendDomain 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {p : β → Prop} [DecidablePred p] {f : α ≃ Subtype p} {g : Equiv.Perm α} {s t : Set α} (h : Set.MapsTo (⇑g) s t) : Set.MapsTo (⇑(g.extendDomain f)) (Subtype.val ∘ ⇑f '' s) (Subtype.val ∘ ⇑f '' t)
• Set.MapsTo.piecewise_ite 📋 Mathlib.Data.Set.Piecewise
  {α : Type u_1} {β : Type u_2} {s s₁ s₂ : Set α} {t t₁ t₂ : Set β} {f₁ f₂ : α → β} [(i : α) → Decidable (i ∈ s)] (h₁ : Set.MapsTo f₁ (s₁ ∩ s) (t₁ ∩ t)) (h₂ : Set.MapsTo f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ)) : Set.MapsTo (s.piecewise f₁ f₂) (s.ite s₁ s₂) (t.ite t₁ t₂)
• Function.strictAntiOn_of_rightInvOn_of_mapsTo 📋 Mathlib.Data.Set.Monotone
  {α : Type u_1} {β : Type u_2} [Preorder α] [LinearOrder β] {φ : β → α} {ψ : α → β} {t : Set β} {s : Set α} (hφ : StrictAntiOn φ t) (φψs : Set.RightInvOn ψ φ s) (ψts : Set.MapsTo ψ s t) : StrictAntiOn ψ s
• Function.strictMonoOn_of_rightInvOn_of_mapsTo 📋 Mathlib.Data.Set.Monotone
  {α : Type u_1} {β : Type u_2} [Preorder α] [LinearOrder β] {φ : β → α} {ψ : α → β} {t : Set β} {s : Set α} (hφ : StrictMonoOn φ t) (φψs : Set.RightInvOn ψ φ s) (ψts : Set.MapsTo ψ s t) : StrictMonoOn ψ s
• Function.antitoneOn_of_rightInvOn_of_mapsTo 📋 Mathlib.Data.Set.Monotone
  {α : Type u_1} {β : Type u_2} [PartialOrder α] [LinearOrder β] {φ : β → α} {ψ : α → β} {t : Set β} {s : Set α} (hφ : AntitoneOn φ t) (φψs : Set.RightInvOn ψ φ s) (ψts : Set.MapsTo ψ s t) : AntitoneOn ψ s
• Function.monotoneOn_of_rightInvOn_of_mapsTo 📋 Mathlib.Data.Set.Monotone
  {α : Type u_1} {β : Type u_2} [PartialOrder α] [LinearOrder β] {φ : β → α} {ψ : α → β} {t : Set β} {s : Set α} (hφ : MonotoneOn φ t) (φψs : Set.RightInvOn ψ φ s) (ψts : Set.MapsTo ψ s t) : MonotoneOn ψ s
• Set.MapsTo.sumElim 📋 Mathlib.Order.Hom.Set
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → γ} {g : β → γ} {s : Set α × Set β} {t : Set γ} (hf : Set.MapsTo f s.1 t) (hg : Set.MapsTo g s.2 t) : Set.MapsTo (Sum.elim f g) (Set.sumEquiv.symm s) t
• Antitone.mapsTo_Ici 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a : α} (h : Antitone f) : Set.MapsTo f (Set.Ici a) (Set.Iic (f a))
• Antitone.mapsTo_Iic 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {b : α} (h : Antitone f) : Set.MapsTo f (Set.Iic b) (Set.Ici (f b))
• Monotone.mapsTo_Ici 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a : α} (h : Monotone f) : Set.MapsTo f (Set.Ici a) (Set.Ici (f a))
• Monotone.mapsTo_Iic 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {b : α} (h : Monotone f) : Set.MapsTo f (Set.Iic b) (Set.Iic (f b))
• StrictAnti.mapsTo_Iio 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {b : α} (h : StrictAnti f) : Set.MapsTo f (Set.Iio b) (Set.Ioi (f b))
• StrictAnti.mapsTo_Ioi 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a : α} (h : StrictAnti f) : Set.MapsTo f (Set.Ioi a) (Set.Iio (f a))
• StrictMono.mapsTo_Iio 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {b : α} (h : StrictMono f) : Set.MapsTo f (Set.Iio b) (Set.Iio (f b))
• StrictMono.mapsTo_Ioi 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a : α} (h : StrictMono f) : Set.MapsTo f (Set.Ioi a) (Set.Ioi (f a))
• Antitone.mapsTo_Icc 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a b : α} (h : Antitone f) : Set.MapsTo f (Set.Icc a b) (Set.Icc (f b) (f a))
• AntitoneOn.mapsTo_Ici 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a : α} (h : AntitoneOn f (Set.Ici a)) : Set.MapsTo f (Set.Ici a) (Set.Iic (f a))
• AntitoneOn.mapsTo_Iic 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {b : α} (h : AntitoneOn f (Set.Iic b)) : Set.MapsTo f (Set.Iic b) (Set.Ici (f b))
• Monotone.mapsTo_Icc 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a b : α} (h : Monotone f) : Set.MapsTo f (Set.Icc a b) (Set.Icc (f a) (f b))
• MonotoneOn.mapsTo_Ici 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a : α} (h : MonotoneOn f (Set.Ici a)) : Set.MapsTo f (Set.Ici a) (Set.Ici (f a))
• MonotoneOn.mapsTo_Iic 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {b : α} (h : MonotoneOn f (Set.Iic b)) : Set.MapsTo f (Set.Iic b) (Set.Iic (f b))
• StrictAnti.mapsTo_Ioo 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a b : α} (h : StrictAnti f) : Set.MapsTo f (Set.Ioo a b) (Set.Ioo (f b) (f a))
• StrictAntiOn.mapsTo_Iio 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {b : α} (h : StrictAntiOn f (Set.Iic b)) : Set.MapsTo f (Set.Iio b) (Set.Ioi (f b))
• StrictAntiOn.mapsTo_Ioi 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a : α} (h : StrictAntiOn f (Set.Ici a)) : Set.MapsTo f (Set.Ioi a) (Set.Iio (f a))
• StrictMono.mapsTo_Ioo 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a b : α} (h : StrictMono f) : Set.MapsTo f (Set.Ioo a b) (Set.Ioo (f a) (f b))
• StrictMonoOn.mapsTo_Iio 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {b : α} (h : StrictMonoOn f (Set.Iic b)) : Set.MapsTo f (Set.Iio b) (Set.Iio (f b))
• StrictMonoOn.mapsTo_Ioi 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a : α} (h : StrictMonoOn f (Set.Ici a)) : Set.MapsTo f (Set.Ioi a) (Set.Ioi (f a))
• StrictAnti.mapsTo_Ico 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [PartialOrder α] [Preorder β] {a b : α} (h : StrictAnti f) : Set.MapsTo f (Set.Ico a b) (Set.Ioc (f b) (f a))
• StrictAnti.mapsTo_Ioc 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [PartialOrder α] [Preorder β] {a b : α} (h : StrictAnti f) : Set.MapsTo f (Set.Ioc a b) (Set.Ico (f b) (f a))
• StrictMono.mapsTo_Ico 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [PartialOrder α] [Preorder β] {a b : α} (h : StrictMono f) : Set.MapsTo f (Set.Ico a b) (Set.Ico (f a) (f b))
• StrictMono.mapsTo_Ioc 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [PartialOrder α] [Preorder β] {a b : α} (h : StrictMono f) : Set.MapsTo f (Set.Ioc a b) (Set.Ioc (f a) (f b))
• AntitoneOn.mapsTo_Icc 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a b : α} (h : AntitoneOn f (Set.Icc a b)) : Set.MapsTo f (Set.Icc a b) (Set.Icc (f b) (f a))
• MonotoneOn.mapsTo_Icc 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a b : α} (h : MonotoneOn f (Set.Icc a b)) : Set.MapsTo f (Set.Icc a b) (Set.Icc (f a) (f b))
• StrictAntiOn.mapsTo_Ioo 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a b : α} (h : StrictAntiOn f (Set.Icc a b)) : Set.MapsTo f (Set.Ioo a b) (Set.Ioo (f b) (f a))
• StrictMonoOn.mapsTo_Ioo 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a b : α} (h : StrictMonoOn f (Set.Icc a b)) : Set.MapsTo f (Set.Ioo a b) (Set.Ioo (f a) (f b))
• StrictAntiOn.mapsTo_Ico 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [PartialOrder α] [Preorder β] {a b : α} (h : StrictAntiOn f (Set.Icc a b)) : Set.MapsTo f (Set.Ico a b) (Set.Ioc (f b) (f a))
• StrictAntiOn.mapsTo_Ioc 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [PartialOrder α] [Preorder β] {a b : α} (h : StrictAntiOn f (Set.Icc a b)) : Set.MapsTo f (Set.Ioc a b) (Set.Ico (f b) (f a))
• StrictMonoOn.mapsTo_Ico 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [PartialOrder α] [Preorder β] {a b : α} (h : StrictMonoOn f (Set.Icc a b)) : Set.MapsTo f (Set.Ico a b) (Set.Ico (f a) (f b))
• StrictMonoOn.mapsTo_Ioc 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} [PartialOrder α] [Preorder β] {a b : α} (h : StrictMonoOn f (Set.Icc a b)) : Set.MapsTo f (Set.Ioc a b) (Set.Ioc (f a) (f b))
• Antitone.mapsTo_uIcc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [Lattice β] {f : α → β} {a b : α} (hf : Antitone f) : Set.MapsTo f (Set.uIcc a b) (Set.uIcc (f a) (f b))
• Monotone.mapsTo_uIcc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [Lattice β] {f : α → β} {a b : α} (hf : Monotone f) : Set.MapsTo f (Set.uIcc a b) (Set.uIcc (f a) (f b))
• AntitoneOn.mapsTo_uIcc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [Lattice β] {f : α → β} {a b : α} (hf : AntitoneOn f (Set.uIcc a b)) : Set.MapsTo f (Set.uIcc a b) (Set.uIcc (f a) (f b))
• MonotoneOn.mapsTo_uIcc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [Lattice β] {f : α → β} {a b : α} (hf : MonotoneOn f (Set.uIcc a b)) : Set.MapsTo f (Set.uIcc a b) (Set.uIcc (f a) (f b))
• 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.MapsTo.neg 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
  {α : Type u_2} {β : Type u_3} [InvolutiveNeg β] {A : Set α} {B : Set β} {f : α → β} (h : Set.MapsTo f A B) : Set.MapsTo (-f) A (-B)
• Set.MapsTo.add 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
  {α : Type u_2} {β : Type u_3} [Add β] {A : Set α} {B₁ B₂ : Set β} {f₁ f₂ : α → β} (h₁ : Set.MapsTo f₁ A B₁) (h₂ : Set.MapsTo f₂ A B₂) : Set.MapsTo (f₁ + f₂) A (B₁ + B₂)
• Set.MapsTo.div 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
  {α : Type u_2} {β : Type u_3} [Div β] {A : Set α} {B₁ B₂ : Set β} {f₁ f₂ : α → β} (h₁ : Set.MapsTo f₁ A B₁) (h₂ : Set.MapsTo f₂ A B₂) : Set.MapsTo (f₁ / f₂) A (B₁ / B₂)
• Set.MapsTo.mul 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
  {α : Type u_2} {β : Type u_3} [Mul β] {A : Set α} {B₁ B₂ : Set β} {f₁ f₂ : α → β} (h₁ : Set.MapsTo f₁ A B₁) (h₂ : Set.MapsTo f₂ A B₂) : Set.MapsTo (f₁ * f₂) A (B₁ * B₂)
• Set.MapsTo.sub 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
  {α : Type u_2} {β : Type u_3} [Sub β] {A : Set α} {B₁ B₂ : Set β} {f₁ f₂ : α → β} (h₁ : Set.MapsTo f₁ A B₁) (h₂ : Set.MapsTo f₂ A B₂) : Set.MapsTo (f₁ - f₂) A (B₁ - B₂)
• List.instDecidableMapsToCoeFinsetOfDecidablePredMemSet 📋 Mathlib.Data.Finset.Defs
  {α : Type u_1} {β : Type u_2} {f : α → β} {s : Finset α} {t : Set β} [DecidablePred fun x => x ∈ t] : Decidable (Set.MapsTo f (↑s) t)
• Set.MapsTo.finsetImage_subset 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s : Finset α} {t : Finset β} : Set.MapsTo f ↑s ↑t → Finset.image f s ⊆ t
• Finset.mapsTo_iff_image_subset 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s : Finset α} {t : Finset β} : Set.MapsTo f ↑s ↑t ↔ Finset.image f s ⊆ t
• Set.SurjOn.finsetImage_eq_of_mapsTo 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s : Finset α} {t : Finset β} : Finset.image f s = t → Set.SurjOn f ↑s ↑t ∧ Set.MapsTo f ↑s ↑t
• Finset.image_eq_iff_surjOn_mapsTo 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s : Finset α} {t : Finset β} : Finset.image f s = t ↔ Set.SurjOn f ↑s ↑t ∧ Set.MapsTo f ↑s ↑t
• Finset.card_le_card_of_injOn 📋 Mathlib.Data.Finset.Card
  {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (f : α → β) (hf : Set.MapsTo f ↑s ↑t) (f_inj : Set.InjOn f ↑s) : s.card ≤ t.card
• Finset.card_nbij 📋 Mathlib.Data.Finset.Card
  {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (i : α → β) (hi : Set.MapsTo i ↑s ↑t) (i_inj : Set.InjOn i ↑s) (i_surj : Set.SurjOn i ↑s ↑t) : s.card = t.card
• Finset.image_iterate_stabilises_le_card 📋 Mathlib.Data.Finset.Card
  {α : Type u_1} [DecidableEq α] {f : α → α} {s : Finset α} (hs : Set.MapsTo f ↑s ↑s) : ∃ n ≤ s.card, ∀ (m : ℕ), n ≤ m → Finset.image f^[m] s = Finset.image f^[n] s
• Finset.injOn_of_surjOn_of_card_le 📋 Mathlib.Data.Finset.Card
  {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (f : α → β) (hf : Set.MapsTo f ↑s ↑t) (hsurj : Set.SurjOn f ↑s ↑t) (hst : s.card ≤ t.card) : Set.InjOn f ↑s
• Finset.surjOn_of_injOn_of_card_le 📋 Mathlib.Data.Finset.Card
  {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (f : α → β) (hf : Set.MapsTo f ↑s ↑t) (hinj : Set.InjOn f ↑s) (hst : t.card ≤ s.card) : Set.SurjOn f ↑s ↑t
• Finset.image_iterate_stabilises_lt_card 📋 Mathlib.Data.Finset.Card
  {α : Type u_1} [DecidableEq α] {f : α → α} {s : Finset α} (hs : Set.MapsTo f ↑s ↑s) (hs₀ : s.Nonempty) : ∃ n < s.card, ∀ (m : ℕ), n ≤ m → Finset.image f^[m] s = Finset.image f^[n] s
• Finset.card_nbij' 📋 Mathlib.Data.Finset.Card
  {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (i : α → β) (j : β → α) (hi : Set.MapsTo i ↑s ↑t) (hj : Set.MapsTo j ↑t ↑s) (left_inv : Set.LeftInvOn j i ↑s) (right_inv : Set.RightInvOn j i ↑t) : s.card = t.card
• Finset.exists_ne_map_eq_of_card_lt_of_maps_to 📋 Mathlib.Data.Finset.Card
  {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (hc : t.card < s.card) {f : α → β} (hf : Set.MapsTo f ↑s ↑t) : ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y
• Finset.existsUnique_notMem_image_of_injOn_of_card_eq_add_one 📋 Mathlib.Data.Finset.Card
  {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α → β} {t : Finset β} [DecidableEq β] (hf : Set.InjOn f ↑s) (hf' : Set.MapsTo f ↑s ↑t) (h : t.card = s.card + 1) : ∃! x, x ∈ t ∧ x ∉ Finset.image f s
• Set.infinite_of_injOn_mapsTo 📋 Mathlib.Data.Set.Finite.Basic
  {α : Type u} {β : Type v} {s : Set α} {t : Set β} {f : α → β} (hi : Set.InjOn f s) (hm : Set.MapsTo f s t) (hs : s.Infinite) : t.Infinite
• Set.Finite.of_injOn 📋 Mathlib.Data.Set.Finite.Basic
  {α : Type u} {β : Type v} {f : α → β} {s : Set α} {t : Set β} (hm : Set.MapsTo f s t) (hi : Set.InjOn f s) (ht : t.Finite) : s.Finite
• Set.Finite.injOn_iff_bijOn_of_mapsTo 📋 Mathlib.Data.Set.Finite.Basic
  {α : Type u} {s : Set α} {f : α → α} (hs : s.Finite) (hm : Set.MapsTo f s s) : Set.InjOn f s ↔ Set.BijOn f s s
• Set.Finite.surjOn_iff_bijOn_of_mapsTo 📋 Mathlib.Data.Set.Finite.Basic
  {α : Type u} {s : Set α} {f : α → α} (hs : s.Finite) (hm : Set.MapsTo f s s) : Set.SurjOn f s s ↔ Set.BijOn f s s
• Set.Infinite.exists_ne_map_eq_of_mapsTo 📋 Mathlib.Data.Set.Finite.Basic
  {α : Type u} {β : Type v} {s : Set α} {t : Set β} {f : α → β} (hs : s.Infinite) (hf : Set.MapsTo f s t) (ht : t.Finite) : ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y
• Set.mapsTo_iInter 📋 Mathlib.Data.Set.Lattice.Image
  {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {s : Set α} {t : ι → Set β} {f : α → β} : Set.MapsTo f s (⋂ i, t i) ↔ ∀ (i : ι), Set.MapsTo f s (t i)
• Set.mapsTo_iUnion 📋 Mathlib.Data.Set.Lattice.Image
  {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {s : ι → Set α} {t : Set β} {f : α → β} : Set.MapsTo f (⋃ i, s i) t ↔ ∀ (i : ι), Set.MapsTo f (s i) t
• Set.mapsTo_iInter_iInter 📋 Mathlib.Data.Set.Lattice.Image
  {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {s : ι → Set α} {t : ι → Set β} {f : α → β} (H : ∀ (i : ι), Set.MapsTo f (s i) (t i)) : Set.MapsTo f (⋂ i, s i) (⋂ i, t i)
• Set.mapsTo_iUnion_iUnion 📋 Mathlib.Data.Set.Lattice.Image
  {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {s : ι → Set α} {t : ι → Set β} {f : α → β} (H : ∀ (i : ι), Set.MapsTo f (s i) (t i)) : Set.MapsTo f (⋃ i, s i) (⋃ i, t i)
• Set.mapsTo_sInter 📋 Mathlib.Data.Set.Lattice.Image
  {α : Type u_1} {β : Type u_2} {s : Set α} {T : Set (Set β)} {f : α → β} : Set.MapsTo f s (⋂₀ T) ↔ ∀ t ∈ T, Set.MapsTo f s t
• Set.mapsTo_sUnion 📋 Mathlib.Data.Set.Lattice.Image
  {α : Type u_1} {β : Type u_2} {S : Set (Set α)} {t : Set β} {f : α → β} : Set.MapsTo f (⋃₀ S) t ↔ ∀ s ∈ S, Set.MapsTo f s t
• Set.mapsTo_iInter₂ 📋 Mathlib.Data.Set.Lattice.Image
  {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_8} {s : Set α} {t : (i : ι) → κ i → Set β} {f : α → β} : Set.MapsTo f s (⋂ i, ⋂ j, t i j) ↔ ∀ (i : ι) (j : κ i), Set.MapsTo f s (t i j)
• Set.mapsTo_iUnion₂ 📋 Mathlib.Data.Set.Lattice.Image
  {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_8} {s : (i : ι) → κ i → Set α} {t : Set β} {f : α → β} : Set.MapsTo f (⋃ i, ⋃ j, s i j) t ↔ ∀ (i : ι) (j : κ i), Set.MapsTo f (s i j) t
• Set.mapsTo_iInter₂_iInter₂ 📋 Mathlib.Data.Set.Lattice.Image
  {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_8} {s : (i : ι) → κ i → Set α} {t : (i : ι) → κ i → Set β} {f : α → β} (H : ∀ (i : ι) (j : κ i), Set.MapsTo f (s i j) (t i j)) : Set.MapsTo f (⋂ i, ⋂ j, s i j) (⋂ i, ⋂ j, t i j)
• Set.mapsTo_iUnion₂_iUnion₂ 📋 Mathlib.Data.Set.Lattice.Image
  {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_8} {s : (i : ι) → κ i → Set α} {t : (i : ι) → κ i → Set β} {f : α → β} (H : ∀ (i : ι) (j : κ i), Set.MapsTo f (s i j) (t i j)) : Set.MapsTo f (⋃ i, ⋃ j, s i j) (⋃ i, ⋃ j, t i j)
• AddMonoidHom.restrict 📋 Mathlib.Algebra.Group.Submonoid.Operations
  {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {M' : AddSubmonoid M} {N' : AddSubmonoid N} {f : M →+ N} (h : Set.MapsTo ⇑f ↑M' ↑N') : ↥M' →+ ↥N'
• MonoidHom.restrict 📋 Mathlib.Algebra.Group.Submonoid.Operations
  {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {M' : Submonoid M} {N' : Submonoid N} {f : M →* N} (h : Set.MapsTo ⇑f ↑M' ↑N') : ↥M' →* ↥N'
• AddMonoidHom.restrict_injective 📋 Mathlib.Algebra.Group.Submonoid.Operations
  {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {M' : AddSubmonoid M} {N' : AddSubmonoid N} {f : M →+ N} (h : Set.MapsTo ⇑f ↑M' ↑N') (hf' : Function.Injective ⇑f) : Function.Injective ⇑(AddMonoidHom.restrict h)
• MonoidHom.restrict_injective 📋 Mathlib.Algebra.Group.Submonoid.Operations
  {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {M' : Submonoid M} {N' : Submonoid N} {f : M →* N} (h : Set.MapsTo ⇑f ↑M' ↑N') (hf' : Function.Injective ⇑f) : Function.Injective ⇑(MonoidHom.restrict h)
• Finset.sup_preimage_self 📋 Mathlib.Data.Finset.Preimage
  {α : Type u_1} {β : Type u_2} [Nonempty α] [SemilatticeSup β] [OrderBot β] {s : Finset β} {f : α → β} (hf : Set.BijOn f (f ⁻¹' ↑s) ↑s) : (s.preimage f ⋯).sup f = s.sup id
• Set.Infinite.exists_lt_map_eq_of_mapsTo 📋 Mathlib.Order.Preorder.Finite
  {α : Type u_2} {β : Type u_3} [LinearOrder α] {s : Set α} {t : Set β} {f : α → β} (hs : s.Infinite) (hf : Set.MapsTo f s t) (ht : t.Finite) : ∃ x ∈ s, ∃ y ∈ s, x < y ∧ f x = f y
• Set.WellFoundedOn.mapsTo 📋 Mathlib.Order.WellFoundedSet
  {α : Type u_6} {β : Type u_7} {r : α → α → Prop} (f : β → α) {s : Set α} {t : Set β} (h : Set.MapsTo f t s) (hw : s.WellFoundedOn r) : t.WellFoundedOn (Function.onFun r f)
• AddAction.orbitRel.Quotient.mapsTo_vadd_orbit 📋 Mathlib.GroupTheory.GroupAction.Defs
  {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] (g : G) (x : AddAction.orbitRel.Quotient G α) : Set.MapsTo (fun x => g +ᵥ x) x.orbit x.orbit
• MulAction.orbitRel.Quotient.mapsTo_smul_orbit 📋 Mathlib.GroupTheory.GroupAction.Defs
  {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (g : G) (x : MulAction.orbitRel.Quotient G α) : Set.MapsTo (fun x => g • x) x.orbit x.orbit
• AddAction.mapsTo_vadd_orbit 📋 Mathlib.GroupTheory.GroupAction.Defs
  {M : Type u_1} {α : Type u_3} [AddMonoid M] [AddAction M α] (m : M) (a : α) : Set.MapsTo (fun x => m +ᵥ x) (AddAction.orbit M a) (AddAction.orbit M a)
• MulAction.mapsTo_smul_orbit 📋 Mathlib.GroupTheory.GroupAction.Defs
  {M : Type u_1} {α : Type u_3} [Monoid M] [MulAction M α] (m : M) (a : α) : Set.MapsTo (fun x => m • x) (MulAction.orbit M a) (MulAction.orbit M a)
• Finset.card_eq_sum_card_fiberwise 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
  {ι : Type u_1} {M : Type u_4} [DecidableEq M] {f : ι → M} {s : Finset ι} {t : Finset M} (H : Set.MapsTo f ↑s ↑t) : s.card = ∑ b ∈ t, {a ∈ s | f a = b}.card
• Finset.prod_of_injOn 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
  {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [CommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M} {g : κ → M} (e : ι → κ) (he : Set.InjOn e ↑s) (hest : Set.MapsTo e ↑s ↑t) (h' : ∀ i ∈ t, i ∉ e '' ↑s → g i = 1) (h : ∀ i ∈ s, f i = g (e i)) : ∏ i ∈ s, f i = ∏ j ∈ t, g j
• Finset.sum_of_injOn 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
  {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M} {g : κ → M} (e : ι → κ) (he : Set.InjOn e ↑s) (hest : Set.MapsTo e ↑s ↑t) (h' : ∀ i ∈ t, i ∉ e '' ↑s → g i = 0) (h : ∀ i ∈ s, f i = g (e i)) : ∑ i ∈ s, f i = ∑ j ∈ t, g j
• Set.MapsTo.exists_equiv_extend_of_card_eq 📋 Mathlib.Data.Fintype.Sum
  {α : Type u_1} {β : Type u_2} [Fintype α] {t : Finset β} (hαt : Fintype.card α = t.card) {s : Set α} {f : α → β} (hfst : Set.MapsTo f s ↑t) (hfs : Set.InjOn f s) : ∃ g, ∀ i ∈ s, ↑(g i) = f i
• Set.MapsTo.countable_of_injOn 📋 Mathlib.Data.Set.Countable
  {α : Type u} {β : Type v} {s : Set α} {t : Set β} {f : α → β} (hf : Set.MapsTo f s t) (hf' : Set.InjOn f s) (ht : t.Countable) : s.Countable
• ScottContinuousOn.fun_comp 📋 Mathlib.Order.ScottContinuity
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] {D : Set (Set α)} {f : α → β} {g : β → γ} {D' : Set (Set β)} (hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D) (hD' : Set.MapsTo (fun x => f '' x) D D') (hg : ScottContinuousOn D' g) (hf : ScottContinuousOn D f) : ScottContinuousOn D fun x => g (f x)
• ScottContinuousOn.comp 📋 Mathlib.Order.ScottContinuity
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] {D : Set (Set α)} {f : α → β} {g : β → γ} {D' : Set (Set β)} (hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D) (hD' : Set.MapsTo (fun x => f '' x) D D') (hg : ScottContinuousOn D' g) (hf : ScottContinuousOn D f) : ScottContinuousOn D (g ∘ f)
• LinearMap.restrict_commute 📋 Mathlib.Algebra.Module.Submodule.LinearMap
  {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {f g : M →ₗ[R] M} (h : Commute f g) {p : Submodule R M} (hf : Set.MapsTo ⇑f ↑p ↑p) (hg : Set.MapsTo ⇑g ↑p ↑p) : Commute (f.restrict hf) (g.restrict hg)
• LinearMap.restrict_comp 📋 Mathlib.Algebra.Module.Submodule.LinearMap
  {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {M : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} [Semiring R] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {p : Submodule R M} {p₂ : Submodule R₂ M₂} {p₃ : Submodule R₃ M₃} {f : M →ₛₗ[σ₁₂] M₂} {g : M₂ →ₛₗ[σ₂₃] M₃} (hf : Set.MapsTo ⇑f ↑p ↑p₂) (hg : Set.MapsTo ⇑g ↑p₂ ↑p₃) (hfg : Set.MapsTo ⇑(g ∘ₛₗ f) ↑p ↑p₃ := ⋯) : (g ∘ₛₗ f).restrict hfg = g.restrict hg ∘ₛₗ f.restrict hf
• LinearMap.restrict_sub 📋 Mathlib.Algebra.Module.Submodule.LinearMap
  {R : Type u_8} {R₂ : Type u_9} {M : Type u_10} {M₂ : Type u_11} [Ring R] [Ring R₂] {σ₁₂ : R →+* R₂} [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {p : Submodule R M} {q : Submodule R₂ M₂} {f g : M →ₛₗ[σ₁₂] M₂} (hf : Set.MapsTo ⇑f ↑p ↑q) (hg : Set.MapsTo ⇑g ↑p ↑q) (hfg : Set.MapsTo ⇑(f - g) ↑p ↑q := ⋯) : f.restrict hf - g.restrict hg = (f - g).restrict hfg
• Submodule.mapsTo_span 📋 Mathlib.LinearAlgebra.Span.Basic
  {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {f : M →ₛₗ[σ₁₂] M₂} {s : Set M} {t : Set M₂} (h : Set.MapsTo (⇑f) s t) : Set.MapsTo ⇑f ↑(Submodule.span R s) ↑(Submodule.span R₂ t)
• Set.MapsTo.submoduleSpan 📋 Mathlib.LinearAlgebra.Span.Basic
  {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {f : M →ₛₗ[σ₁₂] M₂} {s : Set M} {t : Set M₂} (h : Set.MapsTo (⇑f) s t) : Set.MapsTo ⇑f ↑(Submodule.span R s) ↑(Submodule.span R₂ t)
• Set.encard_le_encard_of_injOn 📋 Mathlib.Data.Set.Card
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (hf : Set.MapsTo f s t) (f_inj : Set.InjOn f s) : s.encard ≤ t.encard
• Set.exists_ne_map_eq_of_encard_lt_of_maps_to 📋 Mathlib.Data.Set.Card
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (hc : t.encard < s.encard) (hf : Set.MapsTo f s t) : ∃ a₁ ∈ s, ∃ a₂ ∈ s, a₁ ≠ a₂ ∧ f a₁ = f a₂

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:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. 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 69fae59