Loogle!

Result

Found 57 declarations mentioning MvFunctor.map.

• MvFunctor.map 📋 Mathlib.Control.Functor.Multivariate
  {n : ℕ} {F : TypeVec.{u_2} n → Type u_1} [self : MvFunctor F] {α β : TypeVec.{u_2} n} : α.Arrow β → F α → F β
• LawfulMvFunctor.id_map 📋 Mathlib.Control.Functor.Multivariate
  {n : ℕ} {F : TypeVec.{u_2} n → Type u_1} {inst✝ : MvFunctor F} [self : LawfulMvFunctor F] {α : TypeVec.{u_2} n} (x : F α) : MvFunctor.map TypeVec.id x = x
• MvFunctor.id_map 📋 Mathlib.Control.Functor.Multivariate
  {n : ℕ} {α : TypeVec.{u} n} {F : TypeVec.{u} n → Type v} [MvFunctor F] [LawfulMvFunctor F] (x : F α) : MvFunctor.map TypeVec.id x = x
• MvFunctor.id_map' 📋 Mathlib.Control.Functor.Multivariate
  {n : ℕ} {α : TypeVec.{u} n} {F : TypeVec.{u} n → Type v} [MvFunctor F] [LawfulMvFunctor F] (x : F α) : MvFunctor.map (fun _i a => a) x = x
• MvFunctor.LiftP_def 📋 Mathlib.Control.Functor.Multivariate
  {n : ℕ} {α : TypeVec.{u} n} {F : TypeVec.{u} n → Type v} [MvFunctor F] (P : α.Arrow (TypeVec.repeat n Prop)) [LawfulMvFunctor F] (x : F α) : MvFunctor.LiftP' P x ↔ ∃ u, MvFunctor.map (TypeVec.subtypeVal P) u = x
• LawfulMvFunctor.comp_map 📋 Mathlib.Control.Functor.Multivariate
  {n : ℕ} {F : TypeVec.{u_2} n → Type u_1} {inst✝ : MvFunctor F} [self : LawfulMvFunctor F] {α β γ : TypeVec.{u_2} n} (g : α.Arrow β) (h : β.Arrow γ) (x : F α) : MvFunctor.map (TypeVec.comp h g) x = MvFunctor.map h (MvFunctor.map g x)
• MvFunctor.map_map 📋 Mathlib.Control.Functor.Multivariate
  {n : ℕ} {α β γ : TypeVec.{u} n} {F : TypeVec.{u} n → Type v} [MvFunctor F] [LawfulMvFunctor F] (g : α.Arrow β) (h : β.Arrow γ) (x : F α) : MvFunctor.map h (MvFunctor.map g x) = MvFunctor.map (TypeVec.comp h g) x
• MvFunctor.exists_iff_exists_of_mono 📋 Mathlib.Control.Functor.Multivariate
  {n : ℕ} {α β : TypeVec.{u} n} (F : TypeVec.{u} n → Type v) [MvFunctor F] [LawfulMvFunctor F] {P : F α → Prop} {q : F β → Prop} (f : α.Arrow β) (g : β.Arrow α) (h₀ : TypeVec.comp f g = TypeVec.id) (h₁ : ∀ (u : F α), P u ↔ q (MvFunctor.map f u)) : (∃ u, P u) ↔ ∃ u, q u
• LawfulMvFunctor.mk 📋 Mathlib.Control.Functor.Multivariate
  {n : ℕ} {F : TypeVec.{u_2} n → Type u_1} [MvFunctor F] (id_map : ∀ {α : TypeVec.{u_2} n} (x : F α), MvFunctor.map TypeVec.id x = x) (comp_map : ∀ {α β γ : TypeVec.{u_2} n} (g : α.Arrow β) (h : β.Arrow γ) (x : F α), MvFunctor.map (TypeVec.comp h g) x = MvFunctor.map h (MvFunctor.map g x)) : LawfulMvFunctor F
• MvFunctor.LiftR_def 📋 Mathlib.Control.Functor.Multivariate
  {n : ℕ} {α : TypeVec.{u} n} {F : TypeVec.{u} n → Type v} [MvFunctor F] (R : (α.prod α).Arrow (TypeVec.repeat n Prop)) [LawfulMvFunctor F] (x y : F α) : MvFunctor.LiftR' R x y ↔ ∃ u, MvFunctor.map (TypeVec.comp TypeVec.prod.fst (TypeVec.subtypeVal R)) u = x ∧ MvFunctor.map (TypeVec.comp TypeVec.prod.snd (TypeVec.subtypeVal R)) u = y
• MvPFunctor.id_map 📋 Mathlib.Data.PFunctor.Multivariate.Basic
  {n : ℕ} (P : MvPFunctor.{u} n) {α : TypeVec.{u} n} (x : ↑P α) : MvFunctor.map TypeVec.id x = x
• MvPFunctor.const.get_map 📋 Mathlib.Data.PFunctor.Multivariate.Basic
  {n : ℕ} {A : Type u} {α β : TypeVec.{u} n} (f : α.Arrow β) (x : ↑(MvPFunctor.const n A) α) : MvPFunctor.const.get (MvFunctor.map f x) = MvPFunctor.const.get x
• MvPFunctor.comp_map 📋 Mathlib.Data.PFunctor.Multivariate.Basic
  {n : ℕ} (P : MvPFunctor.{u} n) {α β γ : TypeVec.{u} n} (f : α.Arrow β) (g : β.Arrow γ) (x : ↑P α) : MvFunctor.map (TypeVec.comp g f) x = MvFunctor.map g (MvFunctor.map f x)
• MvPFunctor.map_eq 📋 Mathlib.Data.PFunctor.Multivariate.Basic
  {n : ℕ} (P : MvPFunctor.{u} n) {α β : TypeVec.{u} n} (g : α.Arrow β) (a : P.A) (f : (P.B a).Arrow α) : MvFunctor.map g ⟨a, f⟩ = ⟨a, TypeVec.comp g f⟩
• MvPFunctor.comp.get_map 📋 Mathlib.Data.PFunctor.Multivariate.Basic
  {n m : ℕ} {P : MvPFunctor.{u} n} {Q : Fin2 n → MvPFunctor.{u} m} {α β : TypeVec.{u} m} (f : α.Arrow β) (x : ↑(P.comp Q) α) : MvPFunctor.comp.get (MvFunctor.map f x) = MvFunctor.map (fun i x => MvFunctor.map f x) (MvPFunctor.comp.get x)
• MvPFunctor.M.dest_corec 📋 Mathlib.Data.PFunctor.Multivariate.M
  {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {β : Type u} (g : β → ↑P (α ::: β)) (x : β) : MvPFunctor.M.dest P (MvPFunctor.M.corec P g x) = MvFunctor.map (TypeVec.id ::: MvPFunctor.M.corec P g) (g x)
• MvPFunctor.M.dest_map 📋 Mathlib.Data.PFunctor.Multivariate.M
  {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α β : TypeVec.{u} n} (g : α.Arrow β) (x : P.M α) : MvPFunctor.M.dest P (MvFunctor.map g x) = MvFunctor.map (g ::: fun x => MvFunctor.map g x) (MvPFunctor.M.dest P x)
• MvPFunctor.M.bisim' 📋 Mathlib.Data.PFunctor.Multivariate.M
  {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} (R : P.M α → P.M α → Prop) (h : ∀ (x y : P.M α), R x y → MvFunctor.map (TypeVec.id ::: Quot.mk R) (MvPFunctor.M.dest P x) = MvFunctor.map (TypeVec.id ::: Quot.mk R) (MvPFunctor.M.dest P y)) (x y : P.M α) (r : R x y) : x = y
• MvPFunctor.M.bisim₀ 📋 Mathlib.Data.PFunctor.Multivariate.M
  {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} (R : P.M α → P.M α → Prop) (h₀ : Equivalence R) (h : ∀ (x y : P.M α), R x y → MvFunctor.map (TypeVec.id ::: Quot.mk R) (MvPFunctor.M.dest P x) = MvFunctor.map (TypeVec.id ::: Quot.mk R) (MvPFunctor.M.dest P y)) (x y : P.M α) (r : R x y) : x = y
• MvPFunctor.M.map_dest 📋 Mathlib.Data.PFunctor.Multivariate.M
  {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α β : TypeVec.{u} n} (g : (α ::: P.M α).Arrow (β ::: P.M β)) (x : P.M α) (h : ∀ (x : P.M α), TypeVec.lastFun g x = MvFunctor.map (TypeVec.dropFun g) x) : MvFunctor.map g (MvPFunctor.M.dest P x) = MvPFunctor.M.dest P (MvFunctor.map (TypeVec.dropFun g) x)
• MvPFunctor.w_map_wMk 📋 Mathlib.Data.PFunctor.Multivariate.W
  {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α β : TypeVec.{u} n} (g : α.Arrow β) (a : P.A) (f' : (P.drop.B a).Arrow α) (f : P.last.B a → P.W α) : MvFunctor.map g (P.wMk a f' f) = P.wMk a (TypeVec.comp g f') fun i => MvFunctor.map g (f i)
• MvPFunctor.map_objAppend1 📋 Mathlib.Data.PFunctor.Multivariate.W
  {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α γ : TypeVec.{u} n} (g : α.Arrow γ) (a : P.A) (f' : (P.drop.B a).Arrow α) (f : P.last.B a → P.W α) : MvFunctor.map (g ::: P.wMap g) (P.objAppend1 a f' f) = P.objAppend1 a (TypeVec.comp g f') fun x => P.wMap g (f x)
• MvQPF.id_map 📋 Mathlib.Data.QPF.Multivariate.Basic
  {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F] {α : TypeVec.{u} n} (x : F α) : MvFunctor.map TypeVec.id x = x
• MvQPF.abs_map 📋 Mathlib.Data.QPF.Multivariate.Basic
  {n : ℕ} {F : TypeVec.{u} n → Type u_1} [self : MvQPF F] {α β : TypeVec.{u} n} (f : α.Arrow β) (p : ↑(MvQPF.P F) α) : MvQPF.abs (MvFunctor.map f p) = MvFunctor.map f (MvQPF.abs p)
• MvQPF.comp_map 📋 Mathlib.Data.QPF.Multivariate.Basic
  {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F] {α β γ : TypeVec.{u} n} (f : α.Arrow β) (g : β.Arrow γ) (x : F α) : MvFunctor.map (TypeVec.comp g f) x = MvFunctor.map g (MvFunctor.map f x)
• MvQPF.supp_map 📋 Mathlib.Data.QPF.Multivariate.Basic
  {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F] (h : MvQPF.IsUniform) {α β : TypeVec.{u} n} (g : α.Arrow β) (x : F α) (i : Fin2 n) : MvFunctor.supp (MvFunctor.map g x) i = g i '' MvFunctor.supp x i
• MvQPF.mk 📋 Mathlib.Data.QPF.Multivariate.Basic
  {n : ℕ} {F : TypeVec.{u} n → Type u_1} [toMvFunctor : MvFunctor F] (P : MvPFunctor.{u} n) (abs : {α : TypeVec.{u} n} → ↑P α → F α) (repr : {α : TypeVec.{u} n} → F α → ↑P α) (abs_repr : ∀ {α : TypeVec.{u} n} (x : F α), abs (repr x) = x) (abs_map : ∀ {α β : TypeVec.{u} n} (f : α.Arrow β) (p : ↑P α), abs (MvFunctor.map f p) = MvFunctor.map f (abs p)) : MvQPF F
• MvQPF.ofEquiv 📋 Mathlib.Data.QPF.Multivariate.Basic
  {n : ℕ} {F : TypeVec.{u} n → Type u_2} {F' : TypeVec.{u} n → Type u_3} [q : MvQPF F'] [MvFunctor F] (eqv : (α : TypeVec.{u} n) → F α ≃ F' α) (map_eq : ∀ (α β : TypeVec.{u} n) (f : α.Arrow β) (a : F α), MvFunctor.map f a = (eqv β).symm (MvFunctor.map f ((eqv α) a)) := by intros; rfl) : MvQPF F
• MvQPF.liftR_map 📋 Mathlib.Data.QPF.Multivariate.Constructions.Cofix
  {n : ℕ} {α β : TypeVec.{u_1} n} {F' : TypeVec.{u_1} n → Type u} [MvFunctor F'] [LawfulMvFunctor F'] (R : (β.prod β).Arrow (TypeVec.repeat n Prop)) (x : F' α) (f g : α.Arrow β) (h : α.Arrow (TypeVec.Subtype_ R)) (hh : TypeVec.comp (TypeVec.subtypeVal R) h = TypeVec.comp (TypeVec.prod.map f g) TypeVec.prod.diag) : MvFunctor.LiftR' R (MvFunctor.map f x) (MvFunctor.map g x)
• MvQPF.Cofix.dest_corec 📋 Mathlib.Data.QPF.Multivariate.Constructions.Cofix
  {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : β → F (α ::: β)) (x : β) : (MvQPF.Cofix.corec g x).dest = MvFunctor.map (TypeVec.id ::: MvQPF.Cofix.corec g) (g x)
• MvQPF.corec_roll 📋 Mathlib.Data.QPF.Multivariate.Constructions.Cofix
  {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {X Y : Type u} {x₀ : X} (f : X → Y) (g : Y → F (α ::: X)) : MvQPF.Cofix.corec (g ∘ f) x₀ = MvQPF.Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x₀)
• MvQPF.Cofix.mk.eq_1 📋 Mathlib.Data.QPF.Multivariate.Constructions.Cofix
  {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} : MvQPF.Cofix.mk = MvQPF.Cofix.corec fun x => MvFunctor.map (TypeVec.id ::: fun i => i.dest) x
• MvQPF.Cofix.dest_corec' 📋 Mathlib.Data.QPF.Multivariate.Constructions.Cofix
  {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : β → F (α ::: (MvQPF.Cofix F α ⊕ β))) (x : β) : (MvQPF.Cofix.corec' g x).dest = MvFunctor.map (TypeVec.id ::: Sum.elim id (MvQPF.Cofix.corec' g)) (g x)
• MvQPF.liftR_map_last' 📋 Mathlib.Data.QPF.Multivariate.Constructions.Cofix
  {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] [LawfulMvFunctor F] {α : TypeVec.{u} n} {ι : Type u} (R : ι → ι → Prop) (x : F (α ::: ι)) (f : ι → ι) (hh : ∀ (x : ι), R (f x) x) : MvFunctor.LiftR' (α.RelLast' R) (MvFunctor.map (TypeVec.id ::: f) x) x
• MvQPF.Cofix.dest_corec₁ 📋 Mathlib.Data.QPF.Multivariate.Constructions.Cofix
  {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : {X : Type u} → (MvQPF.Cofix F α → X) → (β → X) → β → F (α ::: X)) (x : β) (h : ∀ (X Y : Type u) (f : MvQPF.Cofix F α → X) (f' : β → X) (k : X → Y), g (k ∘ f) (k ∘ f') x = MvFunctor.map (TypeVec.id ::: k) (g f f' x)) : (MvQPF.Cofix.corec₁ g x).dest = g id (MvQPF.Cofix.corec₁ g) x
• MvQPF.Cofix.corec'.eq_1 📋 Mathlib.Data.QPF.Multivariate.Constructions.Cofix
  {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : β → F (α ::: (MvQPF.Cofix F α ⊕ β))) (x : β) : MvQPF.Cofix.corec' g x = MvQPF.Cofix.corec (Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ MvQPF.Cofix.dest) g) (Sum.inr x)
• MvQPF.liftR_map_last 📋 Mathlib.Data.QPF.Multivariate.Constructions.Cofix
  {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] [lawful : LawfulMvFunctor F] {α : TypeVec.{u} n} {ι ι' : Type u} (R : ι' → ι' → Prop) (x : F (α ::: ι)) (f g : ι → ι') (hh : ∀ (x : ι), R (f x) (g x)) : MvFunctor.LiftR' (α.RelLast' R) (MvFunctor.map (TypeVec.id ::: f) x) (MvFunctor.map (TypeVec.id ::: g) x)
• MvQPF.Cofix.bisim_rel 📋 Mathlib.Data.QPF.Multivariate.Constructions.Cofix
  {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (r : MvQPF.Cofix F α → MvQPF.Cofix F α → Prop) (h : ∀ (x y : MvQPF.Cofix F α), r x y → MvFunctor.map (TypeVec.id ::: Quot.mk r) x.dest = MvFunctor.map (TypeVec.id ::: Quot.mk r) y.dest) (x y : MvQPF.Cofix F α) : r x y → x = y
• MvQPF.corecF_eq 📋 Mathlib.Data.QPF.Multivariate.Constructions.Cofix
  {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : β → F (α ::: β)) (x : β) : MvPFunctor.M.dest (MvQPF.P F) (MvQPF.corecF g x) = MvFunctor.map (TypeVec.id ::: MvQPF.corecF g) (MvQPF.repr (g x))
• MvQPF.Cofix.dest.eq_1 📋 Mathlib.Data.QPF.Multivariate.Constructions.Cofix
  {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} : MvQPF.Cofix.dest = Quot.lift (fun x => MvFunctor.map (TypeVec.id ::: Quot.mk MvQPF.Mcongr) (MvQPF.abs (MvPFunctor.M.dest (MvQPF.P F) x))) ⋯
• MvQPF.Comp.get_map 📋 Mathlib.Data.QPF.Multivariate.Constructions.Comp
  {n m : ℕ} {F : TypeVec.{u} n → Type u_1} {G : Fin2 n → TypeVec.{u} m → Type u} {α β : TypeVec.{u} m} (f : α.Arrow β) [MvFunctor F] [(i : Fin2 n) → MvFunctor (G i)] (x : MvQPF.Comp F G α) : (MvFunctor.map f x).get = MvFunctor.map (fun i x => MvFunctor.map f x) x.get
• MvQPF.Comp.map_mk 📋 Mathlib.Data.QPF.Multivariate.Constructions.Comp
  {n m : ℕ} {F : TypeVec.{u} n → Type u_1} {G : Fin2 n → TypeVec.{u} m → Type u} {α β : TypeVec.{u} m} (f : α.Arrow β) [MvFunctor F] [(i : Fin2 n) → MvFunctor (G i)] (x : F fun i => G i α) : MvFunctor.map f (MvQPF.Comp.mk x) = MvQPF.Comp.mk (MvFunctor.map (fun i x => MvFunctor.map f x) x)
• MvQPF.Const.get_map 📋 Mathlib.Data.QPF.Multivariate.Constructions.Const
  {n : ℕ} {A : Type u} {α β : TypeVec.{u} n} (f : α.Arrow β) (x : MvQPF.Const n A α) : (MvFunctor.map f x).get = x.get
• MvQPF.Const.map_mk 📋 Mathlib.Data.QPF.Multivariate.Constructions.Const
  {n : ℕ} {A : Type u} {α β : TypeVec.{u} n} (f : α.Arrow β) (x : A) : MvFunctor.map f (MvQPF.Const.mk x) = MvQPF.Const.mk x
• MvQPF.Fix.rec_eq 📋 Mathlib.Data.QPF.Multivariate.Constructions.Fix
  {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : F (α ::: β) → β) (x : F (α ::: MvQPF.Fix F α)) : MvQPF.Fix.rec g (MvQPF.Fix.mk x) = g (MvFunctor.map (TypeVec.id ::: MvQPF.Fix.rec g) x)
• MvQPF.Fix.rec_unique 📋 Mathlib.Data.QPF.Multivariate.Constructions.Fix
  {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : F (α ::: β) → β) (h : MvQPF.Fix F α → β) (hyp : ∀ (x : F (α ::: MvQPF.Fix F α)), h (MvQPF.Fix.mk x) = g (MvFunctor.map (TypeVec.id ::: h) x)) : MvQPF.Fix.rec g = h
• MvQPF.Fix.drec 📋 Mathlib.Data.QPF.Multivariate.Constructions.Fix
  {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : MvQPF.Fix F α → Type u} (g : (x : F (α ::: Sigma β)) → β (MvQPF.Fix.mk (MvFunctor.map (TypeVec.id ::: Sigma.fst) x))) (x : MvQPF.Fix F α) : β x
• MvQPF.Fix.dest.eq_1 📋 Mathlib.Data.QPF.Multivariate.Constructions.Fix
  {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} : MvQPF.Fix.dest = MvQPF.Fix.rec (MvFunctor.map (TypeVec.id ::: MvQPF.Fix.mk))
• MvQPF.wEquiv_map 📋 Mathlib.Data.QPF.Multivariate.Constructions.Fix
  {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α β : TypeVec.{u} n} (g : α.Arrow β) (x y : (MvQPF.P F).W α) : MvQPF.WEquiv x y → MvQPF.WEquiv (MvFunctor.map g x) (MvFunctor.map g y)
• MvQPF.Fix.ind_rec 📋 Mathlib.Data.QPF.Multivariate.Constructions.Fix
  {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g₁ g₂ : MvQPF.Fix F α → β) (h : ∀ (x : F (α ::: MvQPF.Fix F α)), MvFunctor.map (TypeVec.id ::: g₁) x = MvFunctor.map (TypeVec.id ::: g₂) x → g₁ (MvQPF.Fix.mk x) = g₂ (MvQPF.Fix.mk x)) (x : MvQPF.Fix F α) : g₁ x = g₂ x
• MvQPF.recF_eq' 📋 Mathlib.Data.QPF.Multivariate.Constructions.Fix
  {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : F (α ::: β) → β) (x : (MvQPF.P F).W α) : MvQPF.recF g x = g (MvQPF.abs (MvFunctor.map (TypeVec.id ::: MvQPF.recF g) ((MvQPF.P F).wDest' x)))
• MvQPF.Fix.mk.eq_1 📋 Mathlib.Data.QPF.Multivariate.Constructions.Fix
  {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x : F (α ::: MvQPF.Fix F α)) : MvQPF.Fix.mk x = Quot.mk (⇑(MvQPF.wSetoid α)) ((MvQPF.P F).wMk' (MvFunctor.map (TypeVec.id ::: MvQPF.fixToW) (MvQPF.repr x)))
• MvQPF.wrepr_wMk 📋 Mathlib.Data.QPF.Multivariate.Constructions.Fix
  {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (a : (MvQPF.P F).A) (f' : ((MvQPF.P F).drop.B a).Arrow α) (f : (MvQPF.P F).last.B a → (MvQPF.P F).W α) : MvQPF.wrepr ((MvQPF.P F).wMk a f' f) = (MvQPF.P F).wMk' (MvQPF.repr (MvQPF.abs (MvFunctor.map (TypeVec.id ::: MvQPF.wrepr) ⟨a, (MvQPF.P F).appendContents f' f⟩)))
• MvQPF.Quot1.mvFunctor 📋 Mathlib.Data.QPF.Multivariate.Constructions.Quot
  {n : ℕ} {F : TypeVec.{u} n → Type u} (R : ⦃α : TypeVec.{u} n⦄ → F α → F α → Prop) [MvFunctor F] (Hfunc : ∀ ⦃α β : TypeVec.{u} n⦄ (a b : F α) (f : α.Arrow β), R a b → R (MvFunctor.map f a) (MvFunctor.map f b)) : MvFunctor (MvQPF.Quot1 R)
• MvQPF.relQuot 📋 Mathlib.Data.QPF.Multivariate.Constructions.Quot
  {n : ℕ} {F : TypeVec.{u} n → Type u} (R : ⦃α : TypeVec.{u} n⦄ → F α → F α → Prop) [q : MvQPF F] (Hfunc : ∀ ⦃α β : TypeVec.{u} n⦄ (a b : F α) (f : α.Arrow β), R a b → R (MvFunctor.map f a) (MvFunctor.map f b)) : MvQPF (MvQPF.Quot1 R)
• MvQPF.Quot1.map 📋 Mathlib.Data.QPF.Multivariate.Constructions.Quot
  {n : ℕ} {F : TypeVec.{u} n → Type u} (R : ⦃α : TypeVec.{u} n⦄ → F α → F α → Prop) [MvFunctor F] (Hfunc : ∀ ⦃α β : TypeVec.{u} n⦄ (a b : F α) (f : α.Arrow β), R a b → R (MvFunctor.map f a) (MvFunctor.map f b)) ⦃α β : TypeVec.{u} n⦄ (f : α.Arrow β) : MvQPF.Quot1 R α → MvQPF.Quot1 R β
• MvQPF.quotientQPF 📋 Mathlib.Data.QPF.Multivariate.Constructions.Quot
  {n : ℕ} {F : TypeVec.{u} n → Type u} [q : MvQPF F] {G : TypeVec.{u} n → Type u} [MvFunctor G] {FG_abs : {α : TypeVec.{u} n} → F α → G α} {FG_repr : {α : TypeVec.{u} n} → G α → F α} (FG_abs_repr : ∀ {α : TypeVec.{u} n} (x : G α), FG_abs (FG_repr x) = x) (FG_abs_map : ∀ {α β : TypeVec.{u} n} (f : α.Arrow β) (x : F α), FG_abs (MvFunctor.map f x) = MvFunctor.map f (FG_abs x)) : MvQPF G

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