Loogle!

Result

Found 138 declarations mentioning Vector.map.

• Vector.map 📋 Init.Data.Vector.Basic
  {α : Type u_1} {β : Type u_2} {n : ℕ} (f : α → β) (xs : Vector α n) : Vector β n
• Vector.map_id 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {n : ℕ} (xs : Vector α n) : Vector.map id xs = xs
• Vector.map_id' 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {n : ℕ} (xs : Vector α n) : Vector.map (fun a => a) xs = xs
• Vector.map_id_fun 📋 Init.Data.Vector.Lemmas
  {n : ℕ} {α : Type u_1} : Vector.map id = id
• Vector.map_id_fun' 📋 Init.Data.Vector.Lemmas
  {n : ℕ} {α : Type u_1} : (Vector.map fun a => a) = id
• Vector.map_const' 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {b : β} : Vector.map (fun x => b) xs = Vector.replicate n b
• Vector.map_const 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {b : β} : Vector.map (Function.const α b) xs = Vector.replicate n b
• Vector.map_id'' 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {n : ℕ} {f : α → α} (h : ∀ (x : α), f x = x) (xs : Vector α n) : Vector.map f xs = xs
• Vector.map_mkVector 📋 Init.Data.Vector.Lemmas
  {n : ℕ} {α✝ : Type u_1} {a : α✝} {α✝¹ : Type u_2} {f : α✝ → α✝¹} : Vector.map f (Vector.replicate n a) = Vector.replicate n (f a)
• Vector.map_replicate 📋 Init.Data.Vector.Lemmas
  {n : ℕ} {α✝ : Type u_1} {a : α✝} {α✝¹ : Type u_2} {f : α✝ → α✝¹} : Vector.map f (Vector.replicate n a) = Vector.replicate n (f a)
• Vector.map_const_fun 📋 Init.Data.Vector.Lemmas
  {β : Type u_1} {n : ℕ} {α : Type u_2} {x : β} : Vector.map (Function.const α x) = fun x_1 => Vector.replicate n x
• Vector.back?_map 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {xs : Vector α n} : (Vector.map f xs).back? = Option.map f xs.back?
• Vector.toArray_map 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {xs : Vector α n} : (Vector.map f xs).toArray = Array.map f xs.toArray
• Vector.map_reverse 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {xs : Vector α n} : Vector.map f xs.reverse = (Vector.map f xs).reverse
• Vector.all_map 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {n : ℕ} {β : Type u_2} {f : α → β} {xs : Vector α n} {p : β → Bool} : (Vector.map f xs).all p = xs.all (p ∘ f)
• Vector.any_map 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {n : ℕ} {β : Type u_2} {f : α → β} {xs : Vector α n} {p : β → Bool} : (Vector.map f xs).any p = xs.any (p ∘ f)
• Vector.toList_map 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {xs : Vector α n} : (Vector.map f xs).toList = List.map f xs.toList
• Vector.contains_map 📋 Init.Data.Vector.Lemmas
  {β : Type u_1} {α : Type u_2} {n : ℕ} [BEq β] {xs : Vector α n} {x : β} {f : α → β} : (Vector.map f xs).contains x = xs.any fun a => x == f a
• Vector.mem_map_of_mem 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {n✝ : ℕ} {xs : Vector α n✝} {a : α} {f : α → β} (h : a ∈ xs) : f a ∈ Vector.map f xs
• Vector.map.eq_1 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {n : ℕ} (f : α → β) (xs : Vector α n) : Vector.map f xs = { toArray := Array.map f xs.toArray, size_toArray := ⋯ }
• Vector.map_inj 📋 Init.Data.Vector.Lemmas
  {n : ℕ} {α✝ : Type u_1} {α✝¹ : Type u_2} {f g : α✝ → α✝¹} [NeZero n] : Vector.map f = Vector.map g ↔ f = g
• Vector.map_map 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} {f : α → β} {g : β → γ} {as : Vector α n} : Vector.map g (Vector.map f as) = Vector.map (g ∘ f) as
• Vector.map_setIfInBounds 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {xs : Vector α n} {i : ℕ} {a : α} : Vector.map f (xs.setIfInBounds i a) = (Vector.map f xs).setIfInBounds i (f a)
• Vector.foldl_map 📋 Init.Data.Vector.Lemmas
  {β₁ : Type u_1} {β₂ : Type u_2} {α : Type u_3} {n : ℕ} {f : β₁ → β₂} {g : α → β₂ → α} {xs : Vector β₁ n} {init : α} : Vector.foldl g init (Vector.map f xs) = Vector.foldl (fun x y => g x (f y)) init xs
• Vector.foldr_map 📋 Init.Data.Vector.Lemmas
  {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} {n : ℕ} {f : α₁ → α₂} {g : α₂ → β → β} {xs : Vector α₁ n} {init : β} : Vector.foldr g init (Vector.map f xs) = Vector.foldr (fun x y => g (f x) y) init xs
• Vector.map_eq_mkVector_iff 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : α → β} {b : β} : Vector.map f xs = Vector.replicate n b ↔ ∀ x ∈ xs, f x = b
• Vector.map_eq_replicate_iff 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : α → β} {b : β} : Vector.map f xs = Vector.replicate n b ↔ ∀ x ∈ xs, f x = b
• Vector.flatMap_def 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {n : ℕ} {β : Type u_2} {m : ℕ} {xs : Vector α n} {f : α → Vector β m} : xs.flatMap f = (Vector.map f xs).flatten
• Vector.exists_of_mem_map 📋 Init.Data.Vector.Lemmas
  {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → α✝¹} {n✝ : ℕ} {xs : Vector α✝ n✝} {b : α✝¹} (h : b ∈ Vector.map f xs) : ∃ a ∈ xs, f a = b
• Vector.forall_mem_map 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {xs : Vector α n} {P : β → Prop} : (∀ i ∈ Vector.map f xs, P i) ↔ ∀ j ∈ xs, P (f j)
• Vector.map_congr_left 📋 Init.Data.Vector.Lemmas
  {α✝ : Type u_1} {n✝ : ℕ} {xs : Vector α✝ n✝} {α✝¹ : Type u_2} {f g : α✝ → α✝¹} (h : ∀ a ∈ xs, f a = g a) : Vector.map f xs = Vector.map g xs
• Vector.map_eq_map_iff 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {n : ℕ} {f g : α → β} {xs : Vector α n} : Vector.map f xs = Vector.map g xs ↔ ∀ a ∈ xs, f a = g a
• Vector.map_inj_left 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {n✝ : ℕ} {xs : Vector α n✝} {f g : α → β} : Vector.map f xs = Vector.map g xs ↔ ∀ a ∈ xs, f a = g a
• Vector.map_set 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {xs : Vector α n} {i : ℕ} {h : i < n} {a : α} : Vector.map f (xs.set i a h) = (Vector.map f xs).set i (f a) h
• Vector.mem_map 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {n : ℕ} {b : β} {f : α → β} {xs : Vector α n} : b ∈ Vector.map f xs ↔ ∃ a ∈ xs, f a = b
• Vector.map_inj_right 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {n✝ : ℕ} {xs ys : Vector α n✝} {f : α → β} (w : ∀ (x y : α), f x = f y → x = y) : Vector.map f xs = Vector.map f ys ↔ xs = ys
• Vector.flatMap_map 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {k n : ℕ} {f : α → β} {g : β → Vector γ k} {xs : Vector α n} : (Vector.map f xs).flatMap g = xs.flatMap fun a => g (f a)
• Vector.foldl_map_hom 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {n : ℕ} {g : α → β} {f : α → α → α} {f' : β → β → β} {a : α} {xs : Vector α n} (h : ∀ (x y : α), f' (g x) (g y) = g (f x y)) : Vector.foldl f' (g a) (Vector.map g xs) = g (Vector.foldl f a xs)
• Vector.foldr_map_hom 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {n : ℕ} {g : α → β} {f : α → α → α} {f' : β → β → β} {a : α} {xs : Vector α n} (h : ∀ (x y : α), f' (g x) (g y) = g (f x y)) : Vector.foldr f' (g a) (Vector.map g xs) = g (Vector.foldr f a xs)
• Vector.map_pop 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {xs : Vector α n} : Vector.map f xs.pop = (Vector.map f xs).pop
• Vector.flatten_reverse 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {m n : ℕ} {xss : Vector (Vector α m) n} : xss.reverse.flatten = (Vector.map Vector.reverse xss).flatten.reverse
• Vector.reverse_flatten 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {m n : ℕ} {xss : Vector (Vector α m) n} : xss.flatten.reverse = (Vector.map Vector.reverse xss).reverse.flatten
• Vector.map_push 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {as : Vector α n} {x : α} : Vector.map f (as.push x) = (Vector.map f as).push (f x)
• Vector.map_empty 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} : Vector.map f { toArray := #[], size_toArray := ⋯ } = { toArray := #[], size_toArray := ⋯ }
• Vector.map_flatten 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {n m : ℕ} {f : α → β} {xss : Vector (Vector α n) m} : Vector.map f xss.flatten = (Vector.map (Vector.map f) xss).flatten
• Vector.map_flatMap 📋 Init.Data.Vector.Lemmas
  {β : Type u_1} {γ : Type u_2} {α : Type u_3} {m n : ℕ} {f : β → γ} {g : α → Vector β m} {xs : Vector α n} : Vector.map f (xs.flatMap g) = xs.flatMap fun a => Vector.map f (g a)
• Vector.getElem_map 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {n i : ℕ} (f : α → β) {xs : Vector α n} (hi : i < n) : (Vector.map f xs)[i] = f xs[i]
• Vector.map_eq_iff 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {as : Vector α n} {bs : Vector β n} : Vector.map f as = bs ↔ ∀ (i : ℕ) (h : i < n), bs[i] = f as[i]
• Vector.map_singleton 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {a : α} : Vector.map f { toArray := #[a], size_toArray := ⋯ } = { toArray := #[f a], size_toArray := ⋯ }
• Vector.map_append 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {n m : ℕ} {f : α → β} {xs : Vector α n} {ys : Vector α m} : Vector.map f (xs ++ ys) = Vector.map f xs ++ Vector.map f ys
• Vector.map_eq_singleton_iff 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Vector α 1} {b : β} : Vector.map f xs = { toArray := #[b], size_toArray := ⋯ } ↔ ∃ a, xs = { toArray := #[a], size_toArray := ⋯ } ∧ f a = b
• Vector.map_mk 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {xs : Array α} (h : xs.size = n) : Vector.map f { toArray := xs, size_toArray := h } = { toArray := Array.map f xs, size_toArray := ⋯ }
• Vector.getElem?_map 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {xs : Vector α n} {i : ℕ} : (Vector.map f xs)[i]? = Option.map f xs[i]?
• Vector.map_eq_push_iff 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {xs : Vector α (n + 1)} {ys : Vector β n} {b : β} : Vector.map f xs = ys.push b ↔ ∃ xs' a, xs = xs'.push a ∧ Vector.map f xs' = ys ∧ f a = b
• Vector.map_eq_flatMap 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {xs : Vector α n} : Vector.map f xs = Vector.cast ⋯ (xs.flatMap fun x => { toArray := #[f x], size_toArray := ⋯ })
• Vector.append_eq_map_iff 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {n✝ : ℕ} {xs : Vector β n✝} {n✝¹ : ℕ} {ys : Vector β n✝¹} {zs : Vector α (n✝ + n✝¹)} {f : α → β} : xs ++ ys = Vector.map f zs ↔ ∃ as bs, zs = as ++ bs ∧ Vector.map f as = xs ∧ Vector.map f bs = ys
• Vector.map_eq_append_iff 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {β : Type u_2} {a✝ a✝¹ : ℕ} {xs : Vector α (a✝ + a✝¹)} {ys : Vector β a✝} {zs : Vector β a✝¹} {f : α → β} : Vector.map f xs = ys ++ zs ↔ ∃ as bs, xs = as ++ bs ∧ Vector.map f as = ys ∧ Vector.map f bs = zs
• Vector.flatten_flatten 📋 Init.Data.Vector.Lemmas
  {α : Type u_1} {n m k : ℕ} {xss : Vector (Vector (Vector α n) m) k} : xss.flatten.flatten = Vector.cast ⋯ (Vector.map Vector.flatten xss).flatten
• Vector.map_lt 📋 Init.Data.Vector.Lex
  {α : Type u_1} {β : Type u_2} {n : ℕ} [LT α] [LT β] {xs ys : Vector α n} {f : α → β} (w : ∀ (x y : α), x < y → f x < f y) (h : xs < ys) : Vector.map f xs < Vector.map f ys
• Vector.map_le 📋 Init.Data.Vector.Lex
  {α : Type u_1} {β : Type u_2} {n : ℕ} [DecidableEq α] [LT α] [DecidableLT α] [DecidableEq β] [LT β] [DecidableLT β] [Std.Irrefl fun x1 x2 => x1 < x2] [Std.Asymm fun x1 x2 => x1 < x2] [Std.Antisymm fun x1 x2 => ¬x1 < x2] [Std.Irrefl fun x1 x2 => x1 < x2] [Std.Asymm fun x1 x2 => x1 < x2] [Std.Antisymm fun x1 x2 => ¬x1 < x2] {xs ys : Vector α n} {f : α → β} (w : ∀ (x y : α), x < y → f x < f y) (h : xs ≤ ys) : Vector.map f xs ≤ Vector.map f ys
• Vector.unattach.eq_1 📋 Init.Data.Vector.Attach
  {n : ℕ} {α : Type u_1} {p : α → Prop} (xs : Vector { x // p x } n) : xs.unattach = Vector.map (fun x => ↑x) xs
• Vector.attach_map_subtype_val 📋 Init.Data.Vector.Attach
  {α : Type u_1} {n : ℕ} (xs : Vector α n) : Vector.map Subtype.val xs.attach = xs
• Vector.attachWith_map_subtype_val 📋 Init.Data.Vector.Attach
  {α : Type u_1} {n : ℕ} {p : α → Prop} {xs : Vector α n} (H : ∀ a ∈ xs, p a) : Vector.map Subtype.val (xs.attachWith p H) = xs
• Vector.pmap_eq_map 📋 Init.Data.Vector.Attach
  {α : Type u_1} {β : Type u_2} {n : ℕ} {p : α → Prop} {f : α → β} {xs : Vector α n} (H : ∀ a ∈ xs, p a) : Vector.pmap (fun a x => f a) xs H = Vector.map f xs
• Vector.attachWith_map_coe 📋 Init.Data.Vector.Attach
  {α : Type u_1} {β : Type u_2} {n : ℕ} {p : α → Prop} {f : α → β} {xs : Vector α n} (H : ∀ a ∈ xs, p a) : Vector.map (fun i => f ↑i) (xs.attachWith p H) = Vector.map f xs
• Vector.attachWith_map_val 📋 Init.Data.Vector.Attach
  {α : Type u_1} {β : Type u_2} {n : ℕ} {p : α → Prop} {f : α → β} {xs : Vector α n} (H : ∀ a ∈ xs, p a) : Vector.map (fun i => f ↑i) (xs.attachWith p H) = Vector.map f xs
• Vector.map_pmap 📋 Init.Data.Vector.Attach
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} {p : α → Prop} {g : β → γ} {f : (a : α) → p a → β} {xs : Vector α n} (H : ∀ a ∈ xs, p a) : Vector.map g (Vector.pmap f xs H) = Vector.pmap (fun a h => g (f a h)) xs H
• Vector.map_subtype 📋 Init.Data.Vector.Attach
  {α : Type u_1} {n : ℕ} {β : Type u_2} {p : α → Prop} {xs : Vector { x // p x } n} {f : { x // p x } → β} {g : α → β} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) : Vector.map f xs = Vector.map g xs.unattach
• Vector.attach_map_coe 📋 Init.Data.Vector.Attach
  {α : Type u_1} {n : ℕ} {β : Type u_2} (xs : Vector α n) (f : α → β) : Vector.map (fun i => f ↑i) xs.attach = Vector.map f xs
• Vector.attach_map_val 📋 Init.Data.Vector.Attach
  {α : Type u_1} {n : ℕ} {β : Type u_2} (xs : Vector α n) (f : α → β) : Vector.map (fun i => f ↑i) xs.attach = Vector.map f xs
• Vector.unattach_flatten 📋 Init.Data.Vector.Attach
  {α : Type u_1} {n : ℕ} {p : α → Prop} {xss : Vector (Vector { x // p x } n) n} : xss.flatten.unattach = (Vector.map Vector.unattach xss).flatten
• Vector.pmap_map 📋 Init.Data.Vector.Attach
  {β : Type u_1} {γ : Type u_2} {α : Type u_3} {n : ℕ} {p : β → Prop} {g : (b : β) → p b → γ} {f : α → β} {xs : Vector α n} (H : ∀ a ∈ Vector.map f xs, p a) : Vector.pmap g (Vector.map f xs) H = Vector.pmap (fun a h => g (f a) h) xs ⋯
• Vector.map_attach 📋 Init.Data.Vector.Attach
  {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : { x // x ∈ xs } → β} : Vector.map f xs.attach = Vector.pmap (fun a h => f ⟨a, h⟩) xs ⋯
• Vector.map_attach_eq_pmap 📋 Init.Data.Vector.Attach
  {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : { x // x ∈ xs } → β} : Vector.map f xs.attach = Vector.pmap (fun a h => f ⟨a, h⟩) xs ⋯
• Vector.pmap_eq_map_attach 📋 Init.Data.Vector.Attach
  {α : Type u_1} {β : Type u_2} {n : ℕ} {p : α → Prop} {f : (a : α) → p a → β} {xs : Vector α n} (H : ∀ a ∈ xs, p a) : Vector.pmap f xs H = Vector.map (fun x => f ↑x ⋯) xs.attach
• Vector.map_attachWith 📋 Init.Data.Vector.Attach
  {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {P : α → Prop} {H : ∀ a ∈ xs, P a} {f : { x // P x } → β} : Vector.map f (xs.attachWith P H) = Vector.map (fun x => match x with | ⟨x, h⟩ => f ⟨x, ⋯⟩) xs.attach
• Vector.map_attachWith_eq_pmap 📋 Init.Data.Vector.Attach
  {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {P : α → Prop} {H : ∀ a ∈ xs, P a} {f : { x // P x } → β} : Vector.map f (xs.attachWith P H) = Vector.pmap (fun a h => f ⟨a, ⋯⟩) xs ⋯
• Vector.attachWith_map 📋 Init.Data.Vector.Attach
  {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : α → β} {P : β → Prop} (H : ∀ b ∈ Vector.map f xs, P b) : (Vector.map f xs).attachWith P H = Vector.map (fun x => match x with | ⟨x, h⟩ => ⟨f x, h⟩) (xs.attachWith (P ∘ f) ⋯)
• Vector.attach_map 📋 Init.Data.Vector.Attach
  {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : α → β} : (Vector.map f xs).attach = Vector.map (fun x => match x with | ⟨x, h⟩ => ⟨f x, ⋯⟩) xs.attach
• Vector.attach_congr 📋 Init.Data.Vector.Attach
  {α : Type u_1} {n : ℕ} {xs ys : Vector α n} (h : xs = ys) : xs.attach = Vector.map (fun x => ⟨↑x, ⋯⟩) ys.attach
• Vector.reverse_attach 📋 Init.Data.Vector.Attach
  {α : Type u_1} {n : ℕ} {xs : Vector α n} : xs.attach.reverse = Vector.map (fun x => match x with | ⟨x, h⟩ => ⟨x, ⋯⟩) xs.reverse.attach
• Vector.attach_reverse 📋 Init.Data.Vector.Attach
  {α : Type u_1} {n : ℕ} {xs : Vector α n} : xs.reverse.attach = Vector.map (fun x => match x with | ⟨x, h⟩ => ⟨x, ⋯⟩) xs.attach.reverse
• Vector.attach_push 📋 Init.Data.Vector.Attach
  {α : Type u_1} {n : ℕ} {a : α} {xs : Vector α n} : (xs.push a).attach = (Vector.map (fun x => match x with | ⟨x, h⟩ => ⟨x, ⋯⟩) xs.attach).push ⟨a, ⋯⟩
• Vector.attach_append 📋 Init.Data.Vector.Attach
  {α : Type u_1} {n m : ℕ} {xs : Vector α n} {ys : Vector α m} : (xs ++ ys).attach = Vector.map (fun x => match x with | ⟨x, h⟩ => ⟨x, ⋯⟩) xs.attach ++ Vector.map (fun x => match x with | ⟨y, h⟩ => ⟨y, ⋯⟩) ys.attach
• Vector.mapIdx_eq_zipIdx_map 📋 Init.Data.Vector.MapIdx
  {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : ℕ → α → β} : Vector.mapIdx f xs = Vector.map (fun x => match x with | (a, i) => f i a) xs.zipIdx
• Vector.mapIdx_eq_zipWithIndex_map 📋 Init.Data.Vector.MapIdx
  {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : ℕ → α → β} : Vector.mapIdx f xs = Vector.map (fun x => match x with | (a, i) => f i a) xs.zipIdx
• Vector.mapFinIdx_eq_zipIdx_map 📋 Init.Data.Vector.MapIdx
  {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : (i : ℕ) → α → i < n → β} : xs.mapFinIdx f = Vector.map (fun x => match x with | ⟨(x, i), m⟩ => f i x ⋯) xs.zipIdx.attach
• Vector.countP_map 📋 Init.Data.Vector.Count
  {α : Type u_2} {β : Type u_1} {n : ℕ} {p : β → Bool} {f : α → β} {xs : Vector α n} : Vector.countP p (Vector.map f xs) = Vector.countP (p ∘ f) xs
• Vector.count_le_count_map 📋 Init.Data.Vector.Count
  {α : Type u_2} [BEq α] [LawfulBEq α] {β : Type u_1} {n : ℕ} [BEq β] [LawfulBEq β] {xs : Vector α n} {f : α → β} {x : α} : Vector.count x xs ≤ Vector.count (f x) (Vector.map f xs)
• Vector.countP_flatten 📋 Init.Data.Vector.Count
  {α : Type u_1} {p : α → Bool} {m n : ℕ} {xss : Vector (Vector α m) n} : Vector.countP p xss.flatten = (Vector.map (Vector.countP p) xss).sum
• Vector.count_flatten 📋 Init.Data.Vector.Count
  {α : Type u_1} [BEq α] {m n : ℕ} {a : α} {xss : Vector (Vector α m) n} : Vector.count a xss.flatten = (Vector.map (Vector.count a) xss).sum
• Vector.countP_flatMap 📋 Init.Data.Vector.Count
  {α : Type u_2} {β : Type u_1} {n m : ℕ} {p : β → Bool} {xs : Vector α n} {f : α → Vector β m} : Vector.countP p (xs.flatMap f) = (Vector.map (Vector.countP p ∘ f) xs).sum
• Vector.count_flatMap 📋 Init.Data.Vector.Count
  {β : Type u_1} {n m : ℕ} {α : Type u_2} [BEq β] {xs : Vector α n} {f : α → Vector β m} {x : β} : Vector.count x (xs.flatMap f) = (Vector.map (Vector.count x ∘ f) xs).sum
• Vector.map_fst_zip 📋 Init.Data.Vector.Zip
  {α : Type u_1} {n : ℕ} {β : Type u_2} (as : Vector α n) {bs : Vector β n} : Vector.map Prod.fst (as.zip bs) = as
• Vector.map_snd_zip 📋 Init.Data.Vector.Zip
  {α : Type u_1} {n : ℕ} {β : Type u_2} {as : Vector α n} (bs : Vector β n) : Vector.map Prod.snd (as.zip bs) = bs
• Vector.zipWith_self 📋 Init.Data.Vector.Zip
  {α : Type u_1} {δ : Type u_2} {n : ℕ} {f : α → α → δ} {xs : Vector α n} : Vector.zipWith f xs xs = Vector.map (fun a => f a a) xs
• Vector.unzip_fst 📋 Init.Data.Vector.Zip
  {α✝ : Type u_1} {β✝ : Type u_2} {n✝ : ℕ} {xs : Vector (α✝ × β✝) n✝} : xs.unzip.1 = Vector.map Prod.fst xs
• Vector.unzip_snd 📋 Init.Data.Vector.Zip
  {α✝ : Type u_1} {β✝ : Type u_2} {n✝ : ℕ} {xs : Vector (α✝ × β✝) n✝} : xs.unzip.2 = Vector.map Prod.snd xs
• Vector.map_prod_left_eq_zip 📋 Init.Data.Vector.Zip
  {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : α → β} : Vector.map (fun x => (x, f x)) xs = xs.zip (Vector.map f xs)
• Vector.map_prod_right_eq_zip 📋 Init.Data.Vector.Zip
  {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : α → β} : Vector.map (fun x => (f x, x)) xs = (Vector.map f xs).zip xs
• Vector.map_uncurry_zip_eq_zipWith 📋 Init.Data.Vector.Zip
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} {f : α → β → γ} {as : Vector α n} {bs : Vector β n} : Vector.map (Function.uncurry f) (as.zip bs) = Vector.zipWith f as bs
• Vector.map_zip_eq_zipWith 📋 Init.Data.Vector.Zip
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} {f : α × β → γ} {as : Vector α n} {bs : Vector β n} : Vector.map f (as.zip bs) = Vector.zipWith (Function.curry f) as bs
• Vector.map_zipWith 📋 Init.Data.Vector.Zip
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} {δ : Type u_4} {f : α → β} {g : γ → δ → α} {as : Vector γ n} {bs : Vector δ n} : Vector.map f (Vector.zipWith g as bs) = Vector.zipWith (fun x y => f (g x y)) as bs
• Vector.zipWith_map_left 📋 Init.Data.Vector.Zip
  {α : Type u_1} {n : ℕ} {β : Type u_2} {α' : Type u_3} {γ : Type u_4} {as : Vector α n} {bs : Vector β n} {f : α → α'} {g : α' → β → γ} : Vector.zipWith g (Vector.map f as) bs = Vector.zipWith (fun a b => g (f a) b) as bs
• Vector.zipWith_map_right 📋 Init.Data.Vector.Zip
  {α : Type u_1} {n : ℕ} {β : Type u_2} {β' : Type u_3} {γ : Type u_4} {as : Vector α n} {bs : Vector β n} {f : β → β'} {g : α → β' → γ} : Vector.zipWith g as (Vector.map f bs) = Vector.zipWith (fun a b => g a (f b)) as bs
• Vector.unzip_eq_map 📋 Init.Data.Vector.Zip
  {α : Type u_1} {β : Type u_2} {n : ℕ} {xs : Vector (α × β) n} : xs.unzip = (Vector.map Prod.fst xs, Vector.map Prod.snd xs)
• Vector.zip_map' 📋 Init.Data.Vector.Zip
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} {f : α → β} {g : α → γ} {xs : Vector α n} : (Vector.map f xs).zip (Vector.map g xs) = Vector.map (fun a => (f a, g a)) xs
• Vector.zip_map_left 📋 Init.Data.Vector.Zip
  {α : Type u_1} {γ : Type u_2} {n : ℕ} {β : Type u_3} {f : α → γ} {as : Vector α n} {bs : Vector β n} : (Vector.map f as).zip bs = Vector.map (Prod.map f id) (as.zip bs)
• Vector.zip_map_right 📋 Init.Data.Vector.Zip
  {β : Type u_1} {γ : Type u_2} {α : Type u_3} {n : ℕ} {f : β → γ} {as : Vector α n} {bs : Vector β n} : as.zip (Vector.map f bs) = Vector.map (Prod.map id f) (as.zip bs)
• Vector.zipWith_map 📋 Init.Data.Vector.Zip
  {γ : Type u_1} {δ : Type u_2} {α : Type u_3} {β : Type u_4} {n : ℕ} {μ : Type u_5} {f : γ → δ → μ} {g : α → γ} {h : β → δ} {as : Vector α n} {bs : Vector β n} : Vector.zipWith f (Vector.map g as) (Vector.map h bs) = Vector.zipWith (fun a b => f (g a) (h b)) as bs
• Vector.zip_of_prod 📋 Init.Data.Vector.Zip
  {α : Type u_1} {n : ℕ} {β : Type u_2} {as : Vector α n} {bs : Vector β n} {xs : Vector (α × β) n} (hl : Vector.map Prod.fst xs = as) (hr : Vector.map Prod.snd xs = bs) : xs = as.zip bs
• Vector.zip_map 📋 Init.Data.Vector.Zip
  {α : Type u_1} {γ : Type u_2} {β : Type u_3} {δ : Type u_4} {n : ℕ} {f : α → γ} {g : β → δ} {as : Vector α n} {bs : Vector β n} : (Vector.map f as).zip (Vector.map g bs) = Vector.map (Prod.map f g) (as.zip bs)
• Vector.zipIdx_map_fst 📋 Init.Data.Vector.Range
  {α : Type u_1} {n : ℕ} (i : ℕ) (xs : Vector α n) : Vector.map Prod.fst (xs.zipIdx i) = xs
• Vector.range'_eq_map_range 📋 Init.Data.Vector.Range
  {s n : ℕ} : Vector.range' s n = Vector.map (fun x => s + x) (Vector.range n)
• Vector.zipIdx_map_snd 📋 Init.Data.Vector.Range
  {α : Type u_1} {n : ℕ} (i : ℕ) (xs : Vector α n) : Vector.map Prod.snd (xs.zipIdx i) = Vector.range' i n
• Vector.map_add_range' 📋 Init.Data.Vector.Range
  {a : ℕ} (s n step : ℕ) : Vector.map (fun x => a + x) (Vector.range' s n step) = Vector.range' (a + s) n step
• Vector.map_sub_range' 📋 Init.Data.Vector.Range
  {step a s : ℕ} (h : a ≤ s) (n : ℕ) : Vector.map (fun x => x - a) (Vector.range' s n step) = Vector.range' (s - a) n step
• Vector.range'_succ_left 📋 Init.Data.Vector.Range
  {s n step : ℕ} : Vector.range' (s + 1) n step = Vector.map (fun x => x + 1) (Vector.range' s n step)
• Vector.map_zipIdx 📋 Init.Data.Vector.Range
  {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {xs : Vector α n} {k : ℕ} : Vector.map (Prod.map f id) (xs.zipIdx k) = (Vector.map f xs).zipIdx k
• Vector.zipIdx_map 📋 Init.Data.Vector.Range
  {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {xs : Vector α n} {k : ℕ} : (Vector.map f xs).zipIdx k = Vector.map (Prod.map f id) (xs.zipIdx k)
• Vector.reverse_range' 📋 Init.Data.Vector.Range
  {s n : ℕ} : (Vector.range' s n).reverse = Vector.map (fun x => s + n - 1 - x) (Vector.range n)
• Vector.map_snd_add_zipIdx_eq_zipIdx 📋 Init.Data.Vector.Range
  {α : Type u_1} {n : ℕ} {xs : Vector α n} {m k : ℕ} : Vector.map (Prod.map id fun x => x + m) (xs.zipIdx k) = xs.zipIdx (m + k)
• Vector.zipIdx_eq_map_add 📋 Init.Data.Vector.Range
  {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} : xs.zipIdx i = Vector.map (fun x => match x with | (a, j) => (a, i + j)) xs.zipIdx
• Vector.range_add 📋 Init.Data.Vector.Range
  {n m : ℕ} : Vector.range (n + m) = Vector.range n ++ Vector.map (fun x => n + x) (Vector.range m)
• Vector.zipIdx_succ 📋 Init.Data.Vector.Range
  {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} : xs.zipIdx (i + 1) = Vector.map (fun x => match x with | (a, i) => (a, i + 1)) (xs.zipIdx i)
• Vector.range_succ_eq_map 📋 Init.Data.Vector.Range
  {n : ℕ} : Vector.range (n + 1) = Vector.cast ⋯ ({ toArray := #[0], size_toArray := ⋯ } ++ Vector.map Nat.succ (Vector.range n))
• Vector.foldlM_map 📋 Init.Data.Vector.Monadic
  {m : Type u_1 → Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {α : Type u_1} {n : ℕ} [Monad m] {f : β₁ → β₂} {g : α → β₂ → m α} {xs : Vector β₁ n} {init : α} : Vector.foldlM g init (Vector.map f xs) = Vector.foldlM (fun x y => g x (f y)) init xs
• Vector.foldrM_map 📋 Init.Data.Vector.Monadic
  {m : Type u_1 → Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {α : Type u_1} {n : ℕ} [Monad m] [LawfulMonad m] {f : β₁ → β₂} {g : β₂ → α → m α} {xs : Vector β₁ n} {init : α} : Vector.foldrM g init (Vector.map f xs) = Vector.foldrM (fun x y => g (f x) y) init xs
• Vector.mapM_pure 📋 Init.Data.Vector.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} [Monad m] [LawfulMonad m] {xs : Vector α n} (f : α → β) : Vector.mapM (fun x => pure (f x)) xs = pure (Vector.map f xs)
• Vector.forM_map 📋 Init.Data.Vector.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_4} [Monad m] [LawfulMonad m] {xs : Vector α n} {g : α → β} {f : β → m PUnit.{u_1 + 1}} : forM (Vector.map g xs) f = forM xs fun a => f (g a)
• Vector.forIn_map 📋 Init.Data.Vector.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_4} {γ : Type u_1} {init : γ} [Monad m] [LawfulMonad m] {xs : Vector α n} (g : α → β) (f : β → γ → m (ForInStep γ)) : forIn (Vector.map g xs) init f = forIn xs init fun a y => f (g a) y
• Vector.forIn'_map 📋 Init.Data.Vector.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_4} {γ : Type u_1} {init : γ} [Monad m] [LawfulMonad m] {xs : Vector α n} (g : α → β) (f : (b : β) → b ∈ Vector.map g xs → γ → m (ForInStep γ)) : forIn' (Vector.map g xs) init f = forIn' xs init fun a h y => f (g a) ⋯ y
• Vector.finRange_reverse 📋 Init.Data.Vector.FinRange
  {n : ℕ} : (Vector.finRange n).reverse = Vector.map Fin.rev (Vector.finRange n)
• Vector.finRange_succ_last 📋 Init.Data.Vector.FinRange
  {n : ℕ} : Vector.finRange (n + 1) = Vector.map Fin.castSucc (Vector.finRange n) ++ { toArray := #[Fin.last n], size_toArray := ⋯ }
• Vector.finRange_succ 📋 Init.Data.Vector.FinRange
  {n : ℕ} : Vector.finRange (n + 1) = Vector.cast ⋯ ({ toArray := #[0], size_toArray := ⋯ } ++ Vector.map Fin.succ (Vector.finRange n))
• Vector.map_extract 📋 Init.Data.Vector.Extract
  {α : Type u_1} {n : ℕ} {α✝ : Type u_2} {f : α → α✝} {xs : Vector α n} {i j : ℕ} : Vector.map f (xs.extract i j) = (Vector.map f xs).extract i j
• Vector.find?_map 📋 Init.Data.Vector.Find
  {β α : Type} {n : ℕ} {p : α → Bool} {f : β → α} {xs : Vector β n} : Vector.find? p (Vector.map f xs) = Option.map f (Vector.find? (p ∘ f) xs)
• Vector.findSome?_map 📋 Init.Data.Vector.Find
  {β : Type u_1} {γ : Type u_2} {n : ℕ} {α✝ : Type u_3} {p : γ → Option α✝} {f : β → γ} {xs : Vector β n} : Vector.findSome? p (Vector.map f xs) = Vector.findSome? (p ∘ f) xs

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 bce1d65