Loogle!

Result

Found 458 declarations mentioning Finset.map. Of these, only the first 200 are shown.

• Finset.map 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Finset α) : Finset β
• Finset.map_refl 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {s : Finset α} : Finset.map (Function.Embedding.refl α) s = s
• Finset.map_injective 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} (f : α ↪ β) : Function.Injective (Finset.map f)
• Finset.Nonempty.map 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α} : s.Nonempty → (Finset.map f s).Nonempty
• Finset.map_nonempty 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α} : (Finset.map f s).Nonempty ↔ s.Nonempty
• Finset.map_nontrivial 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α} : (Finset.map f s).Nontrivial ↔ s.Nontrivial
• Finset.map_empty 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} (f : α ↪ β) : Finset.map f ∅ = ∅
• Finset.map_cast_heq 📋 Mathlib.Data.Finset.Image
  {α β : Type u_4} (h : α = β) (s : Finset α) : HEq (Finset.map (Equiv.cast h).toEmbedding s) s
• Finset.map_inj 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s₁ s₂ : Finset α} : Finset.map f s₁ = Finset.map f s₂ ↔ s₁ = s₂
• Finset.subtype_map 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} (p : α → Prop) [DecidablePred p] {s : Finset α} : Finset.map (Function.Embedding.subtype p) (Finset.subtype p s) = Finset.filter p s
• Finset.map_eq_empty 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α} : Finset.map f s = ∅ ↔ s = ∅
• GCongr.finsetMap_ssubset 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s t : Finset α} : s ⊂ t → Finset.map f s ⊂ Finset.map f t
• GCongr.finsetMap_subset 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s₁ s₂ : Finset α} : s₁ ⊆ s₂ → Finset.map f s₁ ⊆ Finset.map f s₂
• Finset.map_ssubset_map 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s t : Finset α} : Finset.map f s ⊂ Finset.map f t ↔ s ⊂ t
• Finset.map_subset_map 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s₁ s₂ : Finset α} : Finset.map f s₁ ⊆ Finset.map f s₂ ↔ s₁ ⊆ s₂
• Finset.property_of_mem_map_subtype 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {p : α → Prop} (s : Finset { x // p x }) {a : α} (h : a ∈ Finset.map (Function.Embedding.subtype fun x => p x) s) : p a
• Finset.coe_map_subset_range 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Finset α) : ↑(Finset.map f s) ⊆ Set.range ⇑f
• Finset.map_eq_image 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : α ↪ β) (s : Finset α) : Finset.map f s = Finset.image (⇑f) s
• Finset.map_map 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α ↪ β) (g : β ↪ γ) (s : Finset α) : Finset.map g (Finset.map f s) = Finset.map (f.trans g) s
• Finset.attach_map_val 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {s : Finset α} : Finset.map (Function.Embedding.subtype fun x => x ∈ s) s.attach = s
• Finset.coe_map 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Finset α) : ↑(Finset.map f s) = ⇑f '' ↑s
• Finset.map_val 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Finset α) : (Finset.map f s).val = Multiset.map (⇑f) s.val
• Finset.not_mem_map_subtype_of_not_property 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {p : α → Prop} (s : Finset { x // p x }) {a : α} (h : ¬p a) : a ∉ Finset.map (Function.Embedding.subtype fun x => p x) s
• Finset.disjoint_map 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} {s t : Finset α} (f : α ↪ β) : Disjoint (Finset.map f s) (Finset.map f t) ↔ Disjoint s t
• Finset.subtype_map_of_mem 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Finset α} (h : ∀ x ∈ s, p x) : Finset.map (Function.Embedding.subtype p) (Finset.subtype p s) = s
• Finset.map_singleton 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} (f : α ↪ β) (a : α) : Finset.map f {a} = {f a}
• Finset.mem_map_of_mem 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} (f : α ↪ β) {a : α} {s : Finset α} : a ∈ s → f a ∈ Finset.map f s
• Equiv.finsetCongr_apply 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Finset α) : e.finsetCongr s = Finset.map e.toEmbedding s
• Finset.map_subtype_subset 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {t : Set α} (s : Finset ↑t) : ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ t) s) ⊆ t
• Finset.map_toFinset 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} {f : α ↪ β} [DecidableEq α] [DecidableEq β] {s : Multiset α} : Finset.map f s.toFinset = (Multiset.map (⇑f) s).toFinset
• Finset.mem_map' 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} (f : α ↪ β) {a : α} {s : Finset α} : f a ∈ Finset.map f s ↔ a ∈ s
• Finset.map_symm_subset 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {f : α ≃ β} : Finset.map f.symm.toEmbedding t ⊆ s ↔ t ⊆ Finset.map f.toEmbedding s
• Finset.subset_map_symm 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {f : α ≃ β} : s ⊆ Finset.map f.symm.toEmbedding t ↔ Finset.map f.toEmbedding s ⊆ t
• Finset.map_perm 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {s : Finset α} {σ : Equiv.Perm α} (hs : {a | σ a ≠ a} ⊆ ↑s) : Finset.map (Equiv.toEmbedding σ) s = s
• Function.Commute.finset_map 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {f g : α ↪ α} (h : Function.Commute ⇑f ⇑g) : Function.Commute (Finset.map f) (Finset.map g)
• Finset.map_erase 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] (f : α ↪ β) (s : Finset α) (a : α) : Finset.map f (s.erase a) = (Finset.map f s).erase (f a)
• Finset.map_inter 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {f : α ↪ β} (s₁ s₂ : Finset α) : Finset.map f (s₁ ∩ s₂) = Finset.map f s₁ ∩ Finset.map f s₂
• Finset.map_union 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {f : α ↪ β} (s₁ s₂ : Finset α) : Finset.map f (s₁ ∪ s₂) = Finset.map f s₁ ∪ Finset.map f s₂
• Finset.mem_map_equiv 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α ≃ β} {b : β} : b ∈ Finset.map f.toEmbedding s ↔ f.symm b ∈ s
• Finset.mem_map 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α} {b : β} : b ∈ Finset.map f s ↔ ∃ a ∈ s, f a = b
• Finset.apply_coe_mem_map 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Finset α) (x : { x // x ∈ s }) : f ↑x ∈ Finset.map f s
• Finset.map_insert 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (f : α ↪ β) (a : α) (s : Finset α) : Finset.map f (insert a s) = insert (f a) (Finset.map f s)
• Function.Semiconj.finset_map 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} {f : α ↪ β} {ga : α ↪ α} {gb : β ↪ β} (h : Function.Semiconj ⇑f ⇑ga ⇑gb) : Function.Semiconj (Finset.map f) (Finset.map ga) (Finset.map gb)
• Finset.filter_map 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α} {p : β → Prop} [DecidablePred p] : Finset.filter p (Finset.map f s) = Finset.map f (Finset.filter (p ∘ ⇑f) s)
• Finset.forall_mem_map 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α} {p : (a : β) → a ∈ Finset.map f s → Prop} : (∀ (y : β) (H : y ∈ Finset.map f s), p y H) ↔ ∀ (x : α) (H : x ∈ s), p (f x) ⋯
• Finset.map_filter 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α ≃ β} {p : α → Prop} [DecidablePred p] : Finset.map f.toEmbedding (Finset.filter p s) = Finset.filter (p ∘ ⇑f.symm) (Finset.map f.toEmbedding s)
• Finset.map_filter' 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} (p : α → Prop) [DecidablePred p] (f : α ↪ β) (s : Finset α) [DecidablePred fun x => ∃ a, p a ∧ f a = x] : Finset.map f (Finset.filter p s) = {b ∈ Finset.map f s | ∃ a, p a ∧ f a = b}
• Finset.mapEmbedding_apply 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α} : (Finset.mapEmbedding f) s = Finset.map f s
• Finset.map_comm 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Finset α} {β' : Type u_4} {f : β ↪ γ} {g : α ↪ β} {f' : α ↪ β'} {g' : β' ↪ γ} (h_comm : ∀ (a : α), f (g a) = g' (f' a)) : Finset.map f (Finset.map g s) = Finset.map g' (Finset.map f' s)
• Finset.map_disjUnion 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} {f : α ↪ β} (s₁ s₂ : Finset α) (h : Disjoint s₁ s₂) (h' : Disjoint (Finset.map f s₁) (Finset.map f s₂) := ⋯) : Finset.map f (s₁.disjUnion s₂ h) = (Finset.map f s₁).disjUnion (Finset.map f s₂) h'
• Finset.map_disjUnion' 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} {f : α ↪ β} (s₁ s₂ : Finset α) (h' : Disjoint (Finset.map f s₁) (Finset.map f s₂)) (h : Disjoint s₁ s₂ := ⋯) : Finset.map f (s₁.disjUnion s₂ h) = (Finset.map f s₁).disjUnion (Finset.map f s₂) h'
• Finset.subtype.eq_1 📋 Mathlib.Data.Finset.Image
  {α : Type u_4} (p : α → Prop) [DecidablePred p] (s : Finset α) : Finset.subtype p s = Finset.map { toFun := fun x => ⟨↑x, ⋯⟩, inj' := ⋯ } (Finset.filter p s).attach
• Equiv.finsetSubtypeComm_apply_coe 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} (p : α → Prop) (s : Finset { a // p a }) : ↑((Equiv.finsetSubtypeComm p) s) = Finset.map { toFun := fun a => ↑a, inj' := ⋯ } s
• Finset.filter_attach 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Finset α) : {a ∈ s.attach | p ↑a} = Finset.map ((Function.Embedding.refl α).subtypeMap ⋯) (Finset.filter p s).attach
• Finset.map_cons 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} (f : α ↪ β) (a : α) (s : Finset α) (ha : a ∉ s) : Finset.map f (Finset.cons a s ha) = Finset.cons (f a) (Finset.map f s) ⋯
• Finset.range_add_one' 📋 Mathlib.Data.Finset.Image
  (n : ℕ) : Finset.range (n + 1) = insert 0 (Finset.map { toFun := fun i => i + 1, inj' := ⋯ } (Finset.range n))
• Equiv.finsetSubtypeComm_symm_apply 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} (p : α → Prop) (s : { s // ∀ a ∈ s, p a }) : (Equiv.finsetSubtypeComm p).symm s = Finset.map (Subtype.impEmbedding (Membership.mem ↑s) p ⋯) (↑s).attach
• Finset.filter_attach' 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} [DecidableEq α] (s : Finset α) (p : { x // x ∈ s } → Prop) [DecidablePred p] : Finset.filter p s.attach = Finset.map { toFun := Subtype.map id ⋯, inj' := ⋯ } {x ∈ s | ∃ (h : x ∈ s), p ⟨x, h⟩}.attach
• Finset.map_univ_equiv 📋 Mathlib.Data.Finset.BooleanAlgebra
  {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (f : β ≃ α) : Finset.map f.toEmbedding Finset.univ = Finset.univ
• Finset.univ_map_equiv_to_embedding 📋 Mathlib.Data.Finset.BooleanAlgebra
  {α : Type u_4} {β : Type u_5} [Fintype α] [Fintype β] (e : α ≃ β) : Finset.map e.toEmbedding Finset.univ = Finset.univ
• Finset.map_univ_of_surjective 📋 Mathlib.Data.Finset.BooleanAlgebra
  {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {f : β ↪ α} (hf : Function.Surjective ⇑f) : Finset.map f Finset.univ = Finset.univ
• Finset.univ_map_subtype 📋 Mathlib.Data.Finset.BooleanAlgebra
  {α : Type u_1} [Fintype α] (p : α → Prop) [DecidablePred p] [Fintype { a // p a }] : Finset.map (Function.Embedding.subtype p) Finset.univ = Finset.filter p Finset.univ
• Set.toFinset.eq_1 📋 Mathlib.Data.Fintype.Sets
  {α : Type u_1} (s : Set α) [Fintype ↑s] : s.toFinset = Finset.map (Function.Embedding.subtype fun x => x ∈ s) Finset.univ
• Finset.prod_map 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
  {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] (s : Finset α) (e : α ↪ γ) (f : γ → β) : ∏ x ∈ Finset.map e s, f x = ∏ x ∈ s, f (e x)
• Finset.sum_map 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
  {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] (s : Finset α) (e : α ↪ γ) (f : γ → β) : ∑ x ∈ Finset.map e s, f x = ∑ x ∈ s, f (e x)
• Finset.card_map 📋 Mathlib.Data.Finset.Card
  {α : Type u_1} {β : Type u_2} {s : Finset α} (f : α ↪ β) : (Finset.map f s).card = s.card
• Finset.map_eq_of_subset 📋 Mathlib.Data.Finset.Card
  {α : Type u_1} {s : Finset α} {f : α ↪ α} (hs : Finset.map f s ⊆ s) : Finset.map f s = s
• Finset.map.eq_1 📋 Mathlib.Data.Finset.Fold
  {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Finset α) : Finset.map f s = { val := Multiset.map (⇑f) s.val, nodup := ⋯ }
• Finset.fold_map 📋 Mathlib.Data.Finset.Fold
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β} {b : β} {g : γ ↪ α} {s : Finset γ} : Finset.fold op b f (Finset.map g s) = Finset.fold op b (f ∘ ⇑g) s
• Finset.disjiUnion_map 📋 Mathlib.Data.Finset.Union
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Finset α} {t : α → Finset β} {f : β ↪ γ} {h : (↑s).PairwiseDisjoint t} : Finset.map f (s.disjiUnion t h) = s.disjiUnion (fun a => Finset.map f (t a)) ⋯
• Finset.map_disjiUnion 📋 Mathlib.Data.Finset.Union
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α ↪ β} {s : Finset α} {t : β → Finset γ} {h : (↑(Finset.map f s)).PairwiseDisjoint t} : (Finset.map f s).disjiUnion t h = s.disjiUnion (fun a => t (f a)) ⋯
• Finset.singleton_product 📋 Mathlib.Data.Finset.Prod
  {α : Type u_1} {β : Type u_2} {t : Finset β} {a : α} : {a} ×ˢ t = Finset.map { toFun := Prod.mk a, inj' := ⋯ } t
• Finset.product_singleton 📋 Mathlib.Data.Finset.Prod
  {α : Type u_1} {β : Type u_2} {s : Finset α} {b : β} : s ×ˢ {b} = Finset.map { toFun := fun i => (i, b), inj' := ⋯ } s
• Finset.map_swap_product 📋 Mathlib.Data.Finset.Prod
  {α : Type u_1} {β : Type u_2} (s : Finset α) (t : Finset β) : Finset.map { toFun := Prod.swap, inj' := ⋯ } (t ×ˢ s) = s ×ˢ t
• Finset.prodMap_map_product 📋 Mathlib.Data.Finset.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α ↪ β) (g : γ ↪ δ) (s : Finset α) (t : Finset γ) : Finset.map (f.prodMap g) (s ×ˢ t) = Finset.map f s ×ˢ Finset.map g t
• Finset.disjSum_empty 📋 Mathlib.Data.Finset.Sum
  {α : Type u_1} {β : Type u_2} (s : Finset α) : s.disjSum ∅ = Finset.map Function.Embedding.inl s
• Finset.empty_disjSum 📋 Mathlib.Data.Finset.Sum
  {α : Type u_1} {β : Type u_2} (t : Finset β) : ∅.disjSum t = Finset.map Function.Embedding.inr t
• Finset.toLeft_map_sumComm 📋 Mathlib.Data.Finset.Sum
  {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} : (Finset.map (Equiv.sumComm α β).toEmbedding u).toLeft = u.toRight
• Finset.toRight_map_sumComm 📋 Mathlib.Data.Finset.Sum
  {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} : (Finset.map (Equiv.sumComm α β).toEmbedding u).toRight = u.toLeft
• Finset.disjoint_map_inl_map_inr 📋 Mathlib.Data.Finset.Sum
  {α : Type u_1} {β : Type u_2} (s : Finset α) (t : Finset β) : Disjoint (Finset.map Function.Embedding.inl s) (Finset.map Function.Embedding.inr t)
• Finset.gc_map_inl_toLeft 📋 Mathlib.Data.Finset.Sum
  {α : Type u_1} {β : Type u_2} : GaloisConnection (fun x => Finset.map Function.Embedding.inl x) Finset.toLeft
• Finset.gc_map_inr_toRight 📋 Mathlib.Data.Finset.Sum
  {α : Type u_1} {β : Type u_2} : GaloisConnection (fun x => Finset.map Function.Embedding.inr x) Finset.toRight
• Finset.map_inl_subset_iff_subset_toLeft 📋 Mathlib.Data.Finset.Sum
  {α : Type u_1} {β : Type u_2} {s : Finset α} {u : Finset (α ⊕ β)} : Finset.map Function.Embedding.inl s ⊆ u ↔ s ⊆ u.toLeft
• Finset.map_inr_subset_iff_subset_toRight 📋 Mathlib.Data.Finset.Sum
  {α : Type u_1} {β : Type u_2} {t : Finset β} {u : Finset (α ⊕ β)} : Finset.map Function.Embedding.inr t ⊆ u ↔ t ⊆ u.toRight
• Finset.map_inl_disjUnion_map_inr 📋 Mathlib.Data.Finset.Sum
  {α : Type u_1} {β : Type u_2} (s : Finset α) (t : Finset β) : (Finset.map Function.Embedding.inl s).disjUnion (Finset.map Function.Embedding.inr t) ⋯ = s.disjSum t
• Finset.subset_map_inl 📋 Mathlib.Data.Finset.Sum
  {α : Type u_1} {β : Type u_2} {s : Finset α} {u : Finset (α ⊕ β)} : u ⊆ Finset.map Function.Embedding.inl s ↔ u.toLeft ⊆ s ∧ u.toRight = ∅
• Finset.subset_map_inr 📋 Mathlib.Data.Finset.Sum
  {α : Type u_1} {β : Type u_2} {t : Finset β} {u : Finset (α ⊕ β)} : u ⊆ Finset.map Function.Embedding.inr t ↔ u.toLeft = ∅ ∧ u.toRight ⊆ t
• Finset.map_disjSum 📋 Mathlib.Data.Finset.Sum
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Finset α} {t : Finset β} (f : α ⊕ β ↪ γ) : Finset.map f (s.disjSum t) = (Finset.map (Function.Embedding.inl.trans f) s).disjUnion (Finset.map (Function.Embedding.inr.trans f) t) ⋯
• Finset.prod_subtype_map_embedding 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
  {ι : Type u_1} {M : Type u_4} [CommMonoid M] {p : ι → Prop} {s : Finset { x // p x }} {f : { x // p x } → M} {g : ι → M} (h : ∀ x ∈ s, g ↑x = f x) : ∏ x ∈ Finset.map (Function.Embedding.subtype fun x => p x) s, g x = ∏ x ∈ s, f x
• Finset.sum_subtype_map_embedding 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
  {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] {p : ι → Prop} {s : Finset { x // p x }} {f : { x // p x } → M} {g : ι → M} (h : ∀ x ∈ s, g ↑x = f x) : ∑ x ∈ Finset.map (Function.Embedding.subtype fun x => p x) s, g x = ∑ x ∈ s, f x
• Fin.univ_map_def 📋 Mathlib.Data.Fintype.Basic
  {α : Type u_1} {n : ℕ} (f : Fin n ↪ α) : Finset.map f Finset.univ = { val := ↑(List.ofFn ⇑f), nodup := ⋯ }
• Fin.univ_succAbove 📋 Mathlib.Data.Fintype.Basic
  (n : ℕ) (p : Fin (n + 1)) : Finset.univ = Finset.cons p (Finset.map p.succAboveEmb Finset.univ) ⋯
• Fin.univ_castSuccEmb 📋 Mathlib.Data.Fintype.Basic
  (n : ℕ) : Finset.univ = Finset.cons (Fin.last n) (Finset.map Fin.castSuccEmb Finset.univ) ⋯
• Fin.univ_succ 📋 Mathlib.Data.Fintype.Basic
  (n : ℕ) : Finset.univ = Finset.cons 0 (Finset.map { toFun := Fin.succ, inj' := ⋯ } Finset.univ) ⋯
• Finset.univ_map_embedding 📋 Mathlib.Data.Fintype.EquivFin
  {α : Type u_4} [Fintype α] (e : α ↪ α) : Finset.map e Finset.univ = Finset.univ
• Finset.inf_map 📋 Mathlib.Data.Finset.Lattice.Fold
  {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] [OrderTop α] (s : Finset γ) (f : γ ↪ β) (g : β → α) : (Finset.map f s).inf g = s.inf (g ∘ ⇑f)
• Finset.sup_map 📋 Mathlib.Data.Finset.Lattice.Fold
  {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] [OrderBot α] (s : Finset γ) (f : γ ↪ β) (g : β → α) : (Finset.map f s).sup g = s.sup (g ∘ ⇑f)
• Finset.inf'_comp_eq_map 📋 Mathlib.Data.Finset.Lattice.Fold
  {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] {s : Finset γ} {f : γ ↪ β} (g : β → α) (hs : s.Nonempty) : s.inf' hs (g ∘ ⇑f) = (Finset.map f s).inf' ⋯ g
• Finset.sup'_comp_eq_map 📋 Mathlib.Data.Finset.Lattice.Fold
  {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] {s : Finset γ} {f : γ ↪ β} (g : β → α) (hs : s.Nonempty) : s.sup' hs (g ∘ ⇑f) = (Finset.map f s).sup' ⋯ g
• Finset.inf'_map 📋 Mathlib.Data.Finset.Lattice.Fold
  {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] {s : Finset γ} {f : γ ↪ β} (g : β → α) (hs : (Finset.map f s).Nonempty) : (Finset.map f s).inf' hs g = s.inf' ⋯ (g ∘ ⇑f)
• Finset.sup'_map 📋 Mathlib.Data.Finset.Lattice.Fold
  {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] {s : Finset γ} {f : γ ↪ β} (g : β → α) (hs : (Finset.map f s).Nonempty) : (Finset.map f s).sup' hs g = s.sup' ⋯ (g ∘ ⇑f)
• Finset.eraseNone_map_some 📋 Mathlib.Data.Finset.Option
  {α : Type u_1} (s : Finset α) : Finset.eraseNone (Finset.map Function.Embedding.some s) = s
• Finset.insertNone.eq_1 📋 Mathlib.Data.Finset.Option
  {α : Type u_1} : Finset.insertNone = OrderEmbedding.ofMapLEIff (fun s => Finset.cons none (Finset.map Function.Embedding.some s) ⋯) ⋯
• Finset.map_some_eraseNone 📋 Mathlib.Data.Finset.Option
  {α : Type u_1} [DecidableEq (Option α)] (s : Finset (Option α)) : Finset.map Function.Embedding.some (Finset.eraseNone s) = s.erase none
• Finset.pairwiseDisjoint_map_sigmaMk 📋 Mathlib.Data.Finset.Sigma
  {ι : Type u_1} {α : ι → Type u_2} {s : Finset ι} {t : (i : ι) → Finset (α i)} : (↑s).PairwiseDisjoint fun i => Finset.map (Function.Embedding.sigmaMk i) (t i)
• Finset.disjiUnion_map_sigma_mk 📋 Mathlib.Data.Finset.Sigma
  {ι : Type u_1} {α : ι → Type u_2} {s : Finset ι} {t : (i : ι) → Finset (α i)} : s.disjiUnion (fun i => Finset.map (Function.Embedding.sigmaMk i) (t i)) ⋯ = s.sigma t
• Finset.sigma_eq_biUnion 📋 Mathlib.Data.Finset.Sigma
  {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ((i : ι) × α i)] (s : Finset ι) (t : (i : ι) → Finset (α i)) : s.sigma t = s.biUnion fun i => Finset.map (Function.Embedding.sigmaMk i) (t i)
• Finset.sigmaLift.eq_1 📋 Mathlib.Data.Finset.Sigma
  {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {γ : ι → Type u_4} [DecidableEq ι] (f : ⦃i : ι⦄ → α i → β i → Finset (γ i)) (a : Sigma α) (b : Sigma β) : Finset.sigmaLift f a b = if h : a.fst = b.fst then Finset.map (Function.Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) else ∅
• Finset.powersetCard_one 📋 Mathlib.Data.Finset.Powerset
  {α : Type u_1} (s : Finset α) : Finset.powersetCard 1 s = Finset.map { toFun := singleton, inj' := ⋯ } s
• Finset.powersetCard_map 📋 Mathlib.Data.Finset.Powerset
  {α : Type u_1} {β : Type u_2} (f : α ↪ β) (n : ℕ) (s : Finset α) : Finset.powersetCard n (Finset.map f s) = Finset.map (Finset.mapEmbedding f).toEmbedding (Finset.powersetCard n s)
• Finset.subset_map_iff 📋 Mathlib.Data.Finset.Preimage
  {α : Type u} {β : Type v} {f : α ↪ β} {s : Finset β} {t : Finset α} : s ⊆ Finset.map f t ↔ ∃ u ⊆ t, s = Finset.map f u
• Finset.preimage_map 📋 Mathlib.Data.Finset.Preimage
  {α : Type u} {β : Type v} (f : α ↪ β) (s : Finset α) : (Finset.map f s).preimage ⇑f ⋯ = s
• Finset.preimage_subset 📋 Mathlib.Data.Finset.Preimage
  {α : Type u} {β : Type v} {f : α ↪ β} {s : Finset β} {t : Finset α} (hs : s ⊆ Finset.map f t) : s.preimage ⇑f ⋯ ⊆ t
• Finset.map_subset_iff_subset_preimage 📋 Mathlib.Data.Finset.Preimage
  {α : Type u} {β : Type v} {f : α ↪ β} {s : Finset α} {t : Finset β} : Finset.map f s ⊆ t ↔ s ⊆ t.preimage ⇑f ⋯
• Finset.Ici_toDual 📋 Mathlib.Order.Interval.Finset.Defs
  {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] (a : α) : Finset.Ici (OrderDual.toDual a) = Finset.map OrderDual.toDual.toEmbedding (Finset.Iic a)
• Finset.Iic_toDual 📋 Mathlib.Order.Interval.Finset.Defs
  {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] (a : α) : Finset.Iic (OrderDual.toDual a) = Finset.map OrderDual.toDual.toEmbedding (Finset.Ici a)
• Finset.Iio_toDual 📋 Mathlib.Order.Interval.Finset.Defs
  {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] (a : α) : Finset.Iio (OrderDual.toDual a) = Finset.map OrderDual.toDual.toEmbedding (Finset.Ioi a)
• Finset.Ioi_toDual 📋 Mathlib.Order.Interval.Finset.Defs
  {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] (a : α) : Finset.Ioi (OrderDual.toDual a) = Finset.map OrderDual.toDual.toEmbedding (Finset.Iio a)
• Finset.Ici_ofDual 📋 Mathlib.Order.Interval.Finset.Defs
  {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] (a : αᵒᵈ) : Finset.Ici (OrderDual.ofDual a) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Iic a)
• Finset.Iic_ofDual 📋 Mathlib.Order.Interval.Finset.Defs
  {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] (a : αᵒᵈ) : Finset.Iic (OrderDual.ofDual a) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Ici a)
• Finset.Iio_ofDual 📋 Mathlib.Order.Interval.Finset.Defs
  {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] (a : αᵒᵈ) : Finset.Iio (OrderDual.ofDual a) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Ioi a)
• Finset.Ioi_ofDual 📋 Mathlib.Order.Interval.Finset.Defs
  {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] (a : αᵒᵈ) : Finset.Ioi (OrderDual.ofDual a) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Iio a)
• Ici_orderDual_def 📋 Mathlib.Order.Interval.Finset.Defs
  {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] (a : αᵒᵈ) : Finset.Ici a = Finset.map OrderDual.toDual.toEmbedding (Finset.Iic (OrderDual.ofDual a))
• Iic_orderDual_def 📋 Mathlib.Order.Interval.Finset.Defs
  {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] (a : αᵒᵈ) : Finset.Iic a = Finset.map OrderDual.toDual.toEmbedding (Finset.Ici (OrderDual.ofDual a))
• Iio_orderDual_def 📋 Mathlib.Order.Interval.Finset.Defs
  {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] (a : αᵒᵈ) : Finset.Iio a = Finset.map OrderDual.toDual.toEmbedding (Finset.Ioi (OrderDual.ofDual a))
• Ioi_orderDual_def 📋 Mathlib.Order.Interval.Finset.Defs
  {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] (a : αᵒᵈ) : Finset.Ioi a = Finset.map OrderDual.toDual.toEmbedding (Finset.Iio (OrderDual.ofDual a))
• WithBot.Icc_coe_coe 📋 Mathlib.Order.Interval.Finset.Defs
  (α : Type u_1) [PartialOrder α] [OrderBot α] [LocallyFiniteOrder α] (a b : α) : Finset.Icc ↑a ↑b = Finset.map Function.Embedding.some (Finset.Icc a b)
• WithBot.Ico_coe_coe 📋 Mathlib.Order.Interval.Finset.Defs
  (α : Type u_1) [PartialOrder α] [OrderBot α] [LocallyFiniteOrder α] (a b : α) : Finset.Ico ↑a ↑b = Finset.map Function.Embedding.some (Finset.Ico a b)
• WithBot.Ioc_coe_coe 📋 Mathlib.Order.Interval.Finset.Defs
  (α : Type u_1) [PartialOrder α] [OrderBot α] [LocallyFiniteOrder α] (a b : α) : Finset.Ioc ↑a ↑b = Finset.map Function.Embedding.some (Finset.Ioc a b)
• WithBot.Ioo_coe_coe 📋 Mathlib.Order.Interval.Finset.Defs
  (α : Type u_1) [PartialOrder α] [OrderBot α] [LocallyFiniteOrder α] (a b : α) : Finset.Ioo ↑a ↑b = Finset.map Function.Embedding.some (Finset.Ioo a b)
• WithTop.Icc_coe_coe 📋 Mathlib.Order.Interval.Finset.Defs
  (α : Type u_1) [PartialOrder α] [OrderTop α] [LocallyFiniteOrder α] (a b : α) : Finset.Icc ↑a ↑b = Finset.map Function.Embedding.some (Finset.Icc a b)
• WithTop.Ico_coe_coe 📋 Mathlib.Order.Interval.Finset.Defs
  (α : Type u_1) [PartialOrder α] [OrderTop α] [LocallyFiniteOrder α] (a b : α) : Finset.Ico ↑a ↑b = Finset.map Function.Embedding.some (Finset.Ico a b)
• WithTop.Ioc_coe_coe 📋 Mathlib.Order.Interval.Finset.Defs
  (α : Type u_1) [PartialOrder α] [OrderTop α] [LocallyFiniteOrder α] (a b : α) : Finset.Ioc ↑a ↑b = Finset.map Function.Embedding.some (Finset.Ioc a b)
• WithTop.Ioo_coe_coe 📋 Mathlib.Order.Interval.Finset.Defs
  (α : Type u_1) [PartialOrder α] [OrderTop α] [LocallyFiniteOrder α] (a b : α) : Finset.Ioo ↑a ↑b = Finset.map Function.Embedding.some (Finset.Ioo a b)
• WithBot.Ioc_bot_coe 📋 Mathlib.Order.Interval.Finset.Defs
  (α : Type u_1) [PartialOrder α] [OrderBot α] [LocallyFiniteOrder α] (b : α) : Finset.Ioc ⊥ ↑b = Finset.map Function.Embedding.some (Finset.Iic b)
• WithBot.Ioo_bot_coe 📋 Mathlib.Order.Interval.Finset.Defs
  (α : Type u_1) [PartialOrder α] [OrderBot α] [LocallyFiniteOrder α] (b : α) : Finset.Ioo ⊥ ↑b = Finset.map Function.Embedding.some (Finset.Iio b)
• WithTop.Ico_coe_top 📋 Mathlib.Order.Interval.Finset.Defs
  (α : Type u_1) [PartialOrder α] [OrderTop α] [LocallyFiniteOrder α] (a : α) : Finset.Ico ↑a ⊤ = Finset.map Function.Embedding.some (Finset.Ici a)
• WithTop.Ioo_coe_top 📋 Mathlib.Order.Interval.Finset.Defs
  (α : Type u_1) [PartialOrder α] [OrderTop α] [LocallyFiniteOrder α] (a : α) : Finset.Ioo ↑a ⊤ = Finset.map Function.Embedding.some (Finset.Ioi a)
• Finset.map_subtype_embedding_Ici 📋 Mathlib.Order.Interval.Finset.Defs
  {α : Type u_1} [Preorder α] (p : α → Prop) [DecidablePred p] [LocallyFiniteOrderTop α] (a : Subtype p) (hp : ∀ ⦃a x : α⦄, a ≤ x → p a → p x) : Finset.map (Function.Embedding.subtype p) (Finset.Ici a) = Finset.Ici ↑a
• Finset.map_subtype_embedding_Iic 📋 Mathlib.Order.Interval.Finset.Defs
  {α : Type u_1} [Preorder α] (p : α → Prop) [DecidablePred p] [LocallyFiniteOrderBot α] (a : Subtype p) (hp : ∀ ⦃a x : α⦄, x ≤ a → p a → p x) : Finset.map (Function.Embedding.subtype p) (Finset.Iic a) = Finset.Iic ↑a
• Finset.map_subtype_embedding_Iio 📋 Mathlib.Order.Interval.Finset.Defs
  {α : Type u_1} [Preorder α] (p : α → Prop) [DecidablePred p] [LocallyFiniteOrderBot α] (a : Subtype p) (hp : ∀ ⦃a x : α⦄, x ≤ a → p a → p x) : Finset.map (Function.Embedding.subtype p) (Finset.Iio a) = Finset.Iio ↑a
• Finset.map_subtype_embedding_Ioi 📋 Mathlib.Order.Interval.Finset.Defs
  {α : Type u_1} [Preorder α] (p : α → Prop) [DecidablePred p] [LocallyFiniteOrderTop α] (a : Subtype p) (hp : ∀ ⦃a x : α⦄, a ≤ x → p a → p x) : Finset.map (Function.Embedding.subtype p) (Finset.Ioi a) = Finset.Ioi ↑a
• WithBot.insertBot.eq_1 📋 Mathlib.Order.Interval.Finset.Defs
  {α : Type u_1} : WithBot.insertBot = OrderEmbedding.ofMapLEIff (fun s => Finset.cons ⊥ (Finset.map Function.Embedding.coeWithBot s) ⋯) ⋯
• WithTop.insertTop.eq_1 📋 Mathlib.Order.Interval.Finset.Defs
  {α : Type u_1} : WithTop.insertTop = OrderEmbedding.ofMapLEIff (fun s => Finset.cons ⊤ (Finset.map Function.Embedding.coeWithTop s) ⋯) ⋯
• Finset.Icc_toDual 📋 Mathlib.Order.Interval.Finset.Defs
  {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : α) : Finset.Icc (OrderDual.toDual a) (OrderDual.toDual b) = Finset.map OrderDual.toDual.toEmbedding (Finset.Icc b a)
• Finset.Ico_toDual 📋 Mathlib.Order.Interval.Finset.Defs
  {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : α) : Finset.Ico (OrderDual.toDual a) (OrderDual.toDual b) = Finset.map OrderDual.toDual.toEmbedding (Finset.Ioc b a)
• Finset.Ioc_toDual 📋 Mathlib.Order.Interval.Finset.Defs
  {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : α) : Finset.Ioc (OrderDual.toDual a) (OrderDual.toDual b) = Finset.map OrderDual.toDual.toEmbedding (Finset.Ico b a)
• Finset.Ioo_toDual 📋 Mathlib.Order.Interval.Finset.Defs
  {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : α) : Finset.Ioo (OrderDual.toDual a) (OrderDual.toDual b) = Finset.map OrderDual.toDual.toEmbedding (Finset.Ioo b a)
• Finset.Icc_ofDual 📋 Mathlib.Order.Interval.Finset.Defs
  {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : αᵒᵈ) : Finset.Icc (OrderDual.ofDual a) (OrderDual.ofDual b) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Icc b a)
• Finset.Ico_ofDual 📋 Mathlib.Order.Interval.Finset.Defs
  {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : αᵒᵈ) : Finset.Ico (OrderDual.ofDual a) (OrderDual.ofDual b) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Ioc b a)
• Finset.Ioc_ofDual 📋 Mathlib.Order.Interval.Finset.Defs
  {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : αᵒᵈ) : Finset.Ioc (OrderDual.ofDual a) (OrderDual.ofDual b) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Ico b a)
• Finset.Ioo_ofDual 📋 Mathlib.Order.Interval.Finset.Defs
  {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : αᵒᵈ) : Finset.Ioo (OrderDual.ofDual a) (OrderDual.ofDual b) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Ioo b a)
• Finset.Icc_orderDual_def 📋 Mathlib.Order.Interval.Finset.Defs
  {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : αᵒᵈ) : Finset.Icc a b = Finset.map OrderDual.toDual.toEmbedding (Finset.Icc (OrderDual.ofDual b) (OrderDual.ofDual a))
• Finset.Ico_orderDual_def 📋 Mathlib.Order.Interval.Finset.Defs
  {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : αᵒᵈ) : Finset.Ico a b = Finset.map OrderDual.toDual.toEmbedding (Finset.Ioc (OrderDual.ofDual b) (OrderDual.ofDual a))
• Finset.Ioc_orderDual_def 📋 Mathlib.Order.Interval.Finset.Defs
  {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : αᵒᵈ) : Finset.Ioc a b = Finset.map OrderDual.toDual.toEmbedding (Finset.Ico (OrderDual.ofDual b) (OrderDual.ofDual a))
• Finset.Ioo_orderDual_def 📋 Mathlib.Order.Interval.Finset.Defs
  {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : αᵒᵈ) : Finset.Ioo a b = Finset.map OrderDual.toDual.toEmbedding (Finset.Ioo (OrderDual.ofDual b) (OrderDual.ofDual a))
• Finset.map_subtype_embedding_Icc 📋 Mathlib.Order.Interval.Finset.Defs
  {α : Type u_1} [Preorder α] (p : α → Prop) [DecidablePred p] [LocallyFiniteOrder α] (a b : Subtype p) (hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x) : Finset.map (Function.Embedding.subtype p) (Finset.Icc a b) = Finset.Icc ↑a ↑b
• Finset.map_subtype_embedding_Ico 📋 Mathlib.Order.Interval.Finset.Defs
  {α : Type u_1} [Preorder α] (p : α → Prop) [DecidablePred p] [LocallyFiniteOrder α] (a b : Subtype p) (hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x) : Finset.map (Function.Embedding.subtype p) (Finset.Ico a b) = Finset.Ico ↑a ↑b
• Finset.map_subtype_embedding_Ioc 📋 Mathlib.Order.Interval.Finset.Defs
  {α : Type u_1} [Preorder α] (p : α → Prop) [DecidablePred p] [LocallyFiniteOrder α] (a b : Subtype p) (hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x) : Finset.map (Function.Embedding.subtype p) (Finset.Ioc a b) = Finset.Ioc ↑a ↑b
• Finset.map_subtype_embedding_Ioo 📋 Mathlib.Order.Interval.Finset.Defs
  {α : Type u_1} [Preorder α] (p : α → Prop) [DecidablePred p] [LocallyFiniteOrder α] (a b : Subtype p) (hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x) : Finset.map (Function.Embedding.subtype p) (Finset.Ioo a b) = Finset.Ioo ↑a ↑b
• Finset.uIcc_toDual 📋 Mathlib.Order.Interval.Finset.Basic
  {α : Type u_2} [Lattice α] [LocallyFiniteOrder α] (a b : α) : Finset.uIcc (OrderDual.toDual a) (OrderDual.toDual b) = Finset.map OrderDual.toDual.toEmbedding (Finset.uIcc a b)
• Finset.Icc_map_sectL 📋 Mathlib.Order.Interval.Finset.Basic
  {α : Type u_2} {β : Type u_3} [Preorder α] [PartialOrder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableLE (α × β)] (a b : α) (c : β) : Finset.map (Function.Embedding.sectL α c) (Finset.Icc a b) = Finset.Icc (a, c) (b, c)
• Finset.Icc_map_sectR 📋 Mathlib.Order.Interval.Finset.Basic
  {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableLE (α × β)] (c : α) (a b : β) : Finset.map (Function.Embedding.sectR c β) (Finset.Icc a b) = Finset.Icc (c, a) (c, b)
• Finset.Ico_map_sectL 📋 Mathlib.Order.Interval.Finset.Basic
  {α : Type u_2} {β : Type u_3} [Preorder α] [PartialOrder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableLE (α × β)] (a b : α) (c : β) : Finset.map (Function.Embedding.sectL α c) (Finset.Ico a b) = Finset.Ico (a, c) (b, c)
• Finset.Ico_map_sectR 📋 Mathlib.Order.Interval.Finset.Basic
  {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableLE (α × β)] (c : α) (a b : β) : Finset.map (Function.Embedding.sectR c β) (Finset.Ico a b) = Finset.Ico (c, a) (c, b)
• Finset.Ioc_map_sectL 📋 Mathlib.Order.Interval.Finset.Basic
  {α : Type u_2} {β : Type u_3} [Preorder α] [PartialOrder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableLE (α × β)] (a b : α) (c : β) : Finset.map (Function.Embedding.sectL α c) (Finset.Ioc a b) = Finset.Ioc (a, c) (b, c)
• Finset.Ioc_map_sectR 📋 Mathlib.Order.Interval.Finset.Basic
  {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableLE (α × β)] (c : α) (a b : β) : Finset.map (Function.Embedding.sectR c β) (Finset.Ioc a b) = Finset.Ioc (c, a) (c, b)
• Finset.Ioo_map_sectL 📋 Mathlib.Order.Interval.Finset.Basic
  {α : Type u_2} {β : Type u_3} [Preorder α] [PartialOrder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableLE (α × β)] (a b : α) (c : β) : Finset.map (Function.Embedding.sectL α c) (Finset.Ioo a b) = Finset.Ioo (a, c) (b, c)
• Finset.Ioo_map_sectR 📋 Mathlib.Order.Interval.Finset.Basic
  {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableLE (α × β)] (c : α) (a b : β) : Finset.map (Function.Embedding.sectR c β) (Finset.Ioo a b) = Finset.Ioo (c, a) (c, b)
• Finset.uIcc_map_sectL 📋 Mathlib.Order.Interval.Finset.Basic
  {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableLE (α × β)] (a b : α) (c : β) : Finset.map (Function.Embedding.sectL α c) (Finset.uIcc a b) = Finset.uIcc (a, c) (b, c)
• Finset.uIcc_map_sectR 📋 Mathlib.Order.Interval.Finset.Basic
  {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableLE (α × β)] (c : α) (a b : β) : Finset.map (Function.Embedding.sectR c β) (Finset.uIcc a b) = Finset.uIcc (c, a) (c, b)
• Finset.range_add_eq_union 📋 Mathlib.Order.Interval.Finset.Nat
  (a b : ℕ) : Finset.range (a + b) = Finset.range a ∪ Finset.map (addLeftEmbedding a) (Finset.range b)
• Finset.supIndep_map 📋 Mathlib.Order.SupIndep
  {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [Lattice α] [OrderBot α] {f : ι → α} {s : Finset ι'} {g : ι' ↪ ι} : (Finset.map g s).SupIndep f ↔ s.SupIndep (f ∘ ⇑g)
• Fintype.piFinset.eq_1 📋 Mathlib.Data.Fintype.Pi
  {α : Type u_1} [DecidableEq α] [Fintype α] {δ : α → Type u_4} (t : (a : α) → Finset (δ a)) : Fintype.piFinset t = Finset.map { toFun := fun f a => f a ⋯, inj' := ⋯ } (Finset.univ.pi t)
• Finset.map_op_one 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
  {α : Type u_2} [One α] : Finset.map MulOpposite.opEquiv.toEmbedding 1 = 1
• Finset.map_op_zero 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
  {α : Type u_2} [Zero α] : Finset.map AddOpposite.opEquiv.toEmbedding 0 = 0
• Finset.map_one 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
  {α : Type u_2} {β : Type u_3} [One α] {f : α ↪ β} : Finset.map f 1 = {f 1}
• Finset.map_zero 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
  {α : Type u_2} {β : Type u_3} [Zero α] {f : α ↪ β} : Finset.map f 0 = {f 0}
• Finset.map_op_inv 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
  {α : Type u_2} [DecidableEq α] [Inv α] (s : Finset α) : Finset.map MulOpposite.opEquiv.toEmbedding s⁻¹ = (Finset.map MulOpposite.opEquiv.toEmbedding s)⁻¹
• Finset.map_op_neg 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
  {α : Type u_2} [DecidableEq α] [Neg α] (s : Finset α) : Finset.map AddOpposite.opEquiv.toEmbedding (-s) = -Finset.map AddOpposite.opEquiv.toEmbedding s
• Finset.map_op_add 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
  {α : Type u_2} [DecidableEq α] [Add α] (s t : Finset α) : Finset.map AddOpposite.opEquiv.toEmbedding (s + t) = Finset.map AddOpposite.opEquiv.toEmbedding t + Finset.map AddOpposite.opEquiv.toEmbedding s
• Finset.map_op_mul 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
  {α : Type u_2} [DecidableEq α] [Mul α] (s t : Finset α) : Finset.map MulOpposite.opEquiv.toEmbedding (s * t) = Finset.map MulOpposite.opEquiv.toEmbedding t * Finset.map MulOpposite.opEquiv.toEmbedding s
• Finset.map_op_nsmul 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
  {α : Type u_2} [DecidableEq α] [AddMonoid α] (s : Finset α) (n : ℕ) : Finset.map AddOpposite.opEquiv.toEmbedding (n • s) = n • Finset.map AddOpposite.opEquiv.toEmbedding s
• Finset.map_op_pow 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
  {α : Type u_2} [DecidableEq α] [Monoid α] (s : Finset α) (n : ℕ) : Finset.map MulOpposite.opEquiv.toEmbedding (s ^ n) = Finset.map MulOpposite.opEquiv.toEmbedding s ^ n
• Finsupp.support_embDomain 📋 Mathlib.Data.Finsupp.Defs
  {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α ↪ β) (v : α →₀ M) : (Finsupp.embDomain f v).support = Finset.map f v.support
• Finsupp.embDomain.eq_1 📋 Mathlib.Data.Finsupp.Defs
  {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α ↪ β) (v : α →₀ M) : Finsupp.embDomain f v = { support := Finset.map f v.support, toFun := fun a₂ => if h : a₂ ∈ Finset.map f v.support then v (Finset.choose (fun a₁ => f a₁ = a₂) v.support ⋯) else 0, mem_support_toFun := ⋯ }
• Finsupp.indicator.eq_1 📋 Mathlib.Data.Finsupp.Indicator
  {ι : Type u_1} {α : Type u_2} [Zero α] (s : Finset ι) (f : (i : ι) → i ∈ s → α) : Finsupp.indicator s f = { support := Finset.map (Function.Embedding.subtype fun x => x ∈ s) {i | f ↑i ⋯ ≠ 0}, toFun := fun i => if H : i ∈ s then f i H else 0, mem_support_toFun := ⋯ }
• Finsupp.extendDomain_support 📋 Mathlib.Data.Finsupp.Basic
  {α : Type u_1} {M : Type u_13} [Zero M] {P : α → Prop} [DecidablePred P] (f : Subtype P →₀ M) : f.extendDomain.support = Finset.map (Function.Embedding.subtype P) f.support
• Finsupp.graph.eq_1 📋 Mathlib.Data.Finsupp.Basic
  {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) : f.graph = Finset.map { toFun := fun a => (a, f a), inj' := ⋯ } f.support
• Finsupp.equivMapDomain.eq_1 📋 Mathlib.Data.Finsupp.Basic
  {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α ≃ β) (l : α →₀ M) : Finsupp.equivMapDomain f l = { support := Finset.map f.toEmbedding l.support, toFun := fun a => l (f.symm a), mem_support_toFun := ⋯ }
• Finsupp.piecewise_support 📋 Mathlib.Data.Finsupp.Basic
  {α : Type u_1} {M : Type u_13} [Zero M] {P : α → Prop} [DecidablePred P] (f : Subtype P →₀ M) (g : { a // ¬P a } →₀ M) : (f.piecewise g).support = (Finset.map (Function.Embedding.subtype P) f.support).disjUnion (Finset.map (Function.Embedding.subtype fun a => ¬P a) g.support) ⋯
• Finsupp.uncurry.eq_1 📋 Mathlib.Data.Finsupp.Basic
  {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α →₀ β →₀ M) : f.uncurry = { support := f.support.disjiUnion (fun a => Finset.map (Function.Embedding.sectR a β) (f a).support) ⋯, toFun := fun x => (f x.1) x.2, mem_support_toFun := ⋯ }
• Finset.toLeft_eq_univ 📋 Mathlib.Data.Fintype.Sum
  {α : Type u_3} {β : Type u_4} [Fintype α] {u : Finset (α ⊕ β)} : u.toLeft = Finset.univ ↔ Finset.map Function.Embedding.inl Finset.univ ⊆ u
• Finset.toRight_eq_univ 📋 Mathlib.Data.Fintype.Sum
  {α : Type u_3} {β : Type u_4} [Fintype β] {u : Finset (α ⊕ β)} : u.toRight = Finset.univ ↔ Finset.map Function.Embedding.inr Finset.univ ⊆ u
• Finset.toLeft_eq_empty 📋 Mathlib.Data.Fintype.Sum
  {α : Type u_3} {β : Type u_4} [Fintype β] {u : Finset (α ⊕ β)} : u.toLeft = ∅ ↔ u ⊆ Finset.map Function.Embedding.inr Finset.univ
• Finset.toRight_eq_empty 📋 Mathlib.Data.Fintype.Sum
  {α : Type u_3} {β : Type u_4} [Fintype α] {u : Finset (α ⊕ β)} : u.toRight = ∅ ↔ u ⊆ Finset.map Function.Embedding.inl Finset.univ
• Finset.map_add_left_Icc 📋 Mathlib.Algebra.Order.Interval.Finset.Basic
  {α : Type u_2} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a b c : α) : Finset.map (addLeftEmbedding c) (Finset.Icc a b) = Finset.Icc (c + a) (c + b)
• Finset.map_add_left_Ico 📋 Mathlib.Algebra.Order.Interval.Finset.Basic
  {α : Type u_2} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a b c : α) : Finset.map (addLeftEmbedding c) (Finset.Ico a b) = Finset.Ico (c + a) (c + b)
• Finset.map_add_left_Ioc 📋 Mathlib.Algebra.Order.Interval.Finset.Basic
  {α : Type u_2} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a b c : α) : Finset.map (addLeftEmbedding c) (Finset.Ioc a b) = Finset.Ioc (c + a) (c + b)
• Finset.map_add_left_Ioo 📋 Mathlib.Algebra.Order.Interval.Finset.Basic
  {α : Type u_2} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a b c : α) : Finset.map (addLeftEmbedding c) (Finset.Ioo a b) = Finset.Ioo (c + a) (c + b)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

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

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

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

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

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

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

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

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 19971e9 serving mathlib revision 40fea08