Loogle!
Result
Found 1007 definitions whose name contains "differ". Of these, only the first 200 are shown.
- CategoryTheory.DifferentialObject Mathlib.CategoryTheory.DifferentialObject
(S : Type u_1) → [inst : AddMonoidWithOne S] → (C : Type u) → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst : CategoryTheory.HasShift C S] → Type (max u v) - CategoryTheory.DifferentialObject.categoryOfDifferentialObjects Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} → [inst : AddMonoidWithOne S] → {C : Type u} → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : CategoryTheory.HasShift C S] → CategoryTheory.Category.{v, max u v} (CategoryTheory.DifferentialObject S C) - CategoryTheory.DifferentialObject.obj Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} → [inst : AddMonoidWithOne S] → {C : Type u} → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : CategoryTheory.HasShift C S] → CategoryTheory.DifferentialObject S C → C - CategoryTheory.DifferentialObject.Hom Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} → [inst : AddMonoidWithOne S] → {C : Type u} → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : CategoryTheory.HasShift C S] → CategoryTheory.DifferentialObject S C → CategoryTheory.DifferentialObject S C → Type v - CategoryTheory.DifferentialObject.Hom.id Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} → [inst : AddMonoidWithOne S] → {C : Type u} → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : CategoryTheory.HasShift C S] → (X : CategoryTheory.DifferentialObject S C) → X.Hom X - CategoryTheory.DifferentialObject.forget Mathlib.CategoryTheory.DifferentialObject
(S : Type u_1) → [inst : AddMonoidWithOne S] → (C : Type u) → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : CategoryTheory.HasShift C S] → CategoryTheory.Functor (CategoryTheory.DifferentialObject S C) C - CategoryTheory.DifferentialObject.concreteCategoryOfDifferentialObjects Mathlib.CategoryTheory.DifferentialObject
(S : Type u_1) → [inst : AddMonoidWithOne S] → (C : Type (u + 1)) → [inst_1 : CategoryTheory.LargeCategory C] → [inst_2 : CategoryTheory.ConcreteCategory C] → [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_4 : CategoryTheory.HasShift C S] → CategoryTheory.ConcreteCategory (CategoryTheory.DifferentialObject S C) - CategoryTheory.DifferentialObject.forget_faithful Mathlib.CategoryTheory.DifferentialObject
∀ (S : Type u_1) [inst : AddMonoidWithOne S] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S], (CategoryTheory.DifferentialObject.forget S C).Faithful - CategoryTheory.DifferentialObject.instHasForget₂ Mathlib.CategoryTheory.DifferentialObject
(S : Type u_1) → [inst : AddMonoidWithOne S] → (C : Type (u + 1)) → [inst_1 : CategoryTheory.LargeCategory C] → [inst_2 : CategoryTheory.ConcreteCategory C] → [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_4 : CategoryTheory.HasShift C S] → CategoryTheory.HasForget₂ (CategoryTheory.DifferentialObject S C) C - CategoryTheory.DifferentialObject.instHasShift Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} → [inst : AddCommGroupWithOne S] → (C : Type u) → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : CategoryTheory.HasShift C S] → CategoryTheory.HasShift (CategoryTheory.DifferentialObject S C) S - CategoryTheory.DifferentialObject.hasZeroMorphisms Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} → [inst : AddMonoidWithOne S] → {C : Type u} → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : CategoryTheory.HasShift C S] → [inst_4 : (CategoryTheory.shiftFunctor C 1).PreservesZeroMorphisms] → CategoryTheory.Limits.HasZeroMorphisms (CategoryTheory.DifferentialObject S C) - CategoryTheory.DifferentialObject.hasZeroObject Mathlib.CategoryTheory.DifferentialObject
∀ (S : Type u_1) [inst : AddMonoidWithOne S] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_4 : CategoryTheory.HasShift C S] [inst_5 : (CategoryTheory.shiftFunctor C 1).PreservesZeroMorphisms], CategoryTheory.Limits.HasZeroObject (CategoryTheory.DifferentialObject S C) - CategoryTheory.DifferentialObject.Hom.f Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} → [inst : AddMonoidWithOne S] → {C : Type u} → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : CategoryTheory.HasShift C S] → {X Y : CategoryTheory.DifferentialObject S C} → X.Hom Y → (X.obj ⟶ Y.obj) - CategoryTheory.DifferentialObject.Hom.comp Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} → [inst : AddMonoidWithOne S] → {C : Type u} → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : CategoryTheory.HasShift C S] → {X Y Z : CategoryTheory.DifferentialObject S C} → X.Hom Y → Y.Hom Z → X.Hom Z - CategoryTheory.DifferentialObject.isoApp Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} → [inst : AddMonoidWithOne S] → {C : Type u} → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : CategoryTheory.HasShift C S] → {X Y : CategoryTheory.DifferentialObject S C} → (X ≅ Y) → (X.obj ≅ Y.obj) - CategoryTheory.DifferentialObject.shiftFunctor Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} → [inst : AddCommGroupWithOne S] → (C : Type u) → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : CategoryTheory.HasShift C S] → S → CategoryTheory.Functor (CategoryTheory.DifferentialObject S C) (CategoryTheory.DifferentialObject S C) - CategoryTheory.DifferentialObject.Hom.id_f Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] (X : CategoryTheory.DifferentialObject S C), (CategoryTheory.DifferentialObject.Hom.id X).f = CategoryTheory.CategoryStruct.id X.obj - CategoryTheory.DifferentialObject.isoApp_refl Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] (X : CategoryTheory.DifferentialObject S C), CategoryTheory.DifferentialObject.isoApp (CategoryTheory.Iso.refl X) = CategoryTheory.Iso.refl X.obj - CategoryTheory.DifferentialObject.d Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} → [inst : AddMonoidWithOne S] → {C : Type u} → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : CategoryTheory.HasShift C S] → (self : CategoryTheory.DifferentialObject S C) → self.obj ⟶ (CategoryTheory.shiftFunctor C 1).obj self.obj - CategoryTheory.DifferentialObject.instZeroHom Mathlib.CategoryTheory.DifferentialObject
(S : Type u_1) → [inst : AddMonoidWithOne S] → (C : Type u) → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : CategoryTheory.HasShift C S] → [inst_4 : (CategoryTheory.shiftFunctor C 1).PreservesZeroMorphisms] → {X Y : CategoryTheory.DifferentialObject S C} → Zero (X ⟶ Y) - CategoryTheory.DifferentialObject.id_f Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] (X : CategoryTheory.DifferentialObject S C), (CategoryTheory.CategoryStruct.id X).f = CategoryTheory.CategoryStruct.id X.obj - CategoryTheory.DifferentialObject.Hom.ext Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} {inst : AddMonoidWithOne S} {C : Type u} {inst_1 : CategoryTheory.Category.{v, u} C} {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} {inst_3 : CategoryTheory.HasShift C S} {X Y : CategoryTheory.DifferentialObject S C} (x y : X.Hom Y), x.f = y.f → x = y - CategoryTheory.DifferentialObject.Hom.ext_iff Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} {inst : AddMonoidWithOne S} {C : Type u} {inst_1 : CategoryTheory.Category.{v, u} C} {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} {inst_3 : CategoryTheory.HasShift C S} {X Y : CategoryTheory.DifferentialObject S C} (x y : X.Hom Y), x = y ↔ x.f = y.f - CategoryTheory.DifferentialObject.isoApp_symm Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (f : X ≅ Y), CategoryTheory.DifferentialObject.isoApp f.symm = (CategoryTheory.DifferentialObject.isoApp f).symm - CategoryTheory.DifferentialObject.isoApp_hom Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (f : X ≅ Y), (CategoryTheory.DifferentialObject.isoApp f).hom = f.hom.f - CategoryTheory.DifferentialObject.isoApp_inv Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (f : X ≅ Y), (CategoryTheory.DifferentialObject.isoApp f).inv = f.inv.f - CategoryTheory.DifferentialObject.eqToHom_f Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (h : X = Y), (CategoryTheory.eqToHom h).f = CategoryTheory.eqToHom ⋯ - CategoryTheory.DifferentialObject.Hom.comp_f Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] {X Y Z : CategoryTheory.DifferentialObject S C} (f : X.Hom Y) (g : Y.Hom Z), (f.comp g).f = CategoryTheory.CategoryStruct.comp f.f g.f - CategoryTheory.DifferentialObject.shiftZero Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} → [inst : AddCommGroupWithOne S] → (C : Type u) → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : CategoryTheory.HasShift C S] → CategoryTheory.DifferentialObject.shiftFunctor C 0 ≅ CategoryTheory.Functor.id (CategoryTheory.DifferentialObject S C) - CategoryTheory.DifferentialObject.isoApp_trans Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] {X Y Z : CategoryTheory.DifferentialObject S C} (f : X ≅ Y) (g : Y ≅ Z), CategoryTheory.DifferentialObject.isoApp (f.trans g) = (CategoryTheory.DifferentialObject.isoApp f).trans (CategoryTheory.DifferentialObject.isoApp g) - CategoryTheory.DifferentialObject.ext Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] {A B : CategoryTheory.DifferentialObject S C} {f g : A ⟶ B}, autoParam (f.f = g.f) _auto✝ → f = g - CategoryTheory.DifferentialObject.comp_f Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] {X Y Z : CategoryTheory.DifferentialObject S C} (f : X ⟶ Y) (g : Y ⟶ Z), (CategoryTheory.CategoryStruct.comp f g).f = CategoryTheory.CategoryStruct.comp f.f g.f - CategoryTheory.DifferentialObject.shiftFunctorAdd Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} → [inst : AddCommGroupWithOne S] → (C : Type u) → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : CategoryTheory.HasShift C S] → (m n : S) → CategoryTheory.DifferentialObject.shiftFunctor C (m + n) ≅ (CategoryTheory.DifferentialObject.shiftFunctor C m).comp (CategoryTheory.DifferentialObject.shiftFunctor C n) - CategoryTheory.DifferentialObject.zero_f Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] [inst_4 : (CategoryTheory.shiftFunctor C 1).PreservesZeroMorphisms] (P Q : CategoryTheory.DifferentialObject S C), CategoryTheory.DifferentialObject.Hom.f 0 = 0 - CategoryTheory.DifferentialObject.shiftFunctor_obj_obj Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddCommGroupWithOne S] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] (n : S) (X : CategoryTheory.DifferentialObject S C), ((CategoryTheory.DifferentialObject.shiftFunctor C n).obj X).obj = (CategoryTheory.shiftFunctor C n).obj X.obj - CategoryTheory.DifferentialObject.Hom.comm Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (self : X.Hom Y), CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map self.f) = CategoryTheory.CategoryStruct.comp self.f Y.d - CategoryTheory.DifferentialObject.Hom.mk Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} → [inst : AddMonoidWithOne S] → {C : Type u} → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : CategoryTheory.HasShift C S] → {X Y : CategoryTheory.DifferentialObject S C} → (f : X.obj ⟶ Y.obj) → autoParam (CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f) = CategoryTheory.CategoryStruct.comp f Y.d) _auto✝ → X.Hom Y - CategoryTheory.Functor.mapDifferentialObject Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} → [inst : AddMonoidWithOne S] → {C : Type u} → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : CategoryTheory.HasShift C S] → (D : Type u') → [inst_4 : CategoryTheory.Category.{v', u'} D] → [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D] → [inst_6 : CategoryTheory.HasShift D S] → (F : CategoryTheory.Functor C D) → ((CategoryTheory.shiftFunctor C 1).comp F ⟶ F.comp (CategoryTheory.shiftFunctor D 1)) → (∀ (c c' : C), F.map 0 = 0) → CategoryTheory.Functor (CategoryTheory.DifferentialObject S C) (CategoryTheory.DifferentialObject S D) - CategoryTheory.DifferentialObject.mkIso Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} → [inst : AddMonoidWithOne S] → {C : Type u} → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : CategoryTheory.HasShift C S] → {X Y : CategoryTheory.DifferentialObject S C} → (f : X.obj ≅ Y.obj) → CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f.hom) = CategoryTheory.CategoryStruct.comp f.hom Y.d → (X ≅ Y) - CategoryTheory.DifferentialObject.Hom.comm_assoc Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (self : X.Hom Y) {Z : C} (h : (CategoryTheory.shiftFunctor C 1).obj Y.obj ⟶ Z), CategoryTheory.CategoryStruct.comp X.d (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).map self.f) h) = CategoryTheory.CategoryStruct.comp self.f (CategoryTheory.CategoryStruct.comp Y.d h) - CategoryTheory.DifferentialObject.mkIso_hom_f Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (f : X.obj ≅ Y.obj) (hf : CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f.hom) = CategoryTheory.CategoryStruct.comp f.hom Y.d), (CategoryTheory.DifferentialObject.mkIso f hf).hom.f = f.hom - CategoryTheory.DifferentialObject.mkIso_inv_f Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (f : X.obj ≅ Y.obj) (hf : CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f.hom) = CategoryTheory.CategoryStruct.comp f.hom Y.d), (CategoryTheory.DifferentialObject.mkIso f hf).inv.f = f.inv - CategoryTheory.Functor.mapDifferentialObject_obj_obj Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] (D : Type u') [inst_4 : CategoryTheory.Category.{v', u'} D] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D] [inst_6 : CategoryTheory.HasShift D S] (F : CategoryTheory.Functor C D) (η : (CategoryTheory.shiftFunctor C 1).comp F ⟶ F.comp (CategoryTheory.shiftFunctor D 1)) (hF : ∀ (c c' : C), F.map 0 = 0) (X : CategoryTheory.DifferentialObject S C), ((CategoryTheory.Functor.mapDifferentialObject D F η hF).obj X).obj = F.obj X.obj - CategoryTheory.DifferentialObject.mk Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} → [inst : AddMonoidWithOne S] → {C : Type u} → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : CategoryTheory.HasShift C S] → (obj : C) → (d : obj ⟶ (CategoryTheory.shiftFunctor C 1).obj obj) → autoParam (CategoryTheory.CategoryStruct.comp d ((CategoryTheory.shiftFunctor C 1).map d) = 0) _auto✝ → CategoryTheory.DifferentialObject S C - CategoryTheory.DifferentialObject.d_squared Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] (self : CategoryTheory.DifferentialObject S C), CategoryTheory.CategoryStruct.comp self.d ((CategoryTheory.shiftFunctor C 1).map self.d) = 0 - CategoryTheory.DifferentialObject.Hom.mk.injEq Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (f : X.obj ⟶ Y.obj) (comm : autoParam (CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f) = CategoryTheory.CategoryStruct.comp f Y.d) _auto✝) (f_1 : X.obj ⟶ Y.obj) (comm_1 : autoParam (CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f_1) = CategoryTheory.CategoryStruct.comp f_1 Y.d) _auto✝), ({ f := f, comm := comm } = { f := f_1, comm := comm_1 }) = (f = f_1) - CategoryTheory.DifferentialObject.d_squared_assoc Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] (self : CategoryTheory.DifferentialObject S C) {Z : C} (h : (CategoryTheory.shiftFunctor C 1).obj ((CategoryTheory.shiftFunctor C 1).obj self.obj) ⟶ Z), CategoryTheory.CategoryStruct.comp self.d (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).map self.d) h) = CategoryTheory.CategoryStruct.comp 0 h - CategoryTheory.Functor.mapDifferentialObject_obj_d Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] (D : Type u') [inst_4 : CategoryTheory.Category.{v', u'} D] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D] [inst_6 : CategoryTheory.HasShift D S] (F : CategoryTheory.Functor C D) (η : (CategoryTheory.shiftFunctor C 1).comp F ⟶ F.comp (CategoryTheory.shiftFunctor D 1)) (hF : ∀ (c c' : C), F.map 0 = 0) (X : CategoryTheory.DifferentialObject S C), ((CategoryTheory.Functor.mapDifferentialObject D F η hF).obj X).d = CategoryTheory.CategoryStruct.comp (F.map X.d) (η.app X.obj) - CategoryTheory.DifferentialObject.shiftFunctor_obj_d Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddCommGroupWithOne S] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] (n : S) (X : CategoryTheory.DifferentialObject S C), ((CategoryTheory.DifferentialObject.shiftFunctor C n).obj X).d = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map X.d) (CategoryTheory.shiftComm X.obj 1 n).hom - CategoryTheory.DifferentialObject.Hom.mk.sizeOf_spec Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} [inst_4 : SizeOf S] [inst_5 : SizeOf C] (f : X.obj ⟶ Y.obj) (comm : autoParam (CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f) = CategoryTheory.CategoryStruct.comp f Y.d) _auto✝), sizeOf { f := f, comm := comm } = 1 + sizeOf f + sizeOf comm - CategoryTheory.DifferentialObject.shiftZero_hom_app_f Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddCommGroupWithOne S] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] (X : CategoryTheory.DifferentialObject S C), ((CategoryTheory.DifferentialObject.shiftZero C).hom.app X).f = (CategoryTheory.shiftFunctorZero C S).hom.app X.obj - CategoryTheory.DifferentialObject.shiftZero_inv_app_f Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddCommGroupWithOne S] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] (X : CategoryTheory.DifferentialObject S C), ((CategoryTheory.DifferentialObject.shiftZero C).inv.app X).f = (CategoryTheory.shiftFunctorZero C S).inv.app X.obj - CategoryTheory.DifferentialObject.mk.injEq Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] (obj : C) (d : obj ⟶ (CategoryTheory.shiftFunctor C 1).obj obj) (d_squared : autoParam (CategoryTheory.CategoryStruct.comp d ((CategoryTheory.shiftFunctor C 1).map d) = 0) _auto✝) (obj_1 : C) (d_1 : obj_1 ⟶ (CategoryTheory.shiftFunctor C 1).obj obj_1) (d_squared_1 : autoParam (CategoryTheory.CategoryStruct.comp d_1 ((CategoryTheory.shiftFunctor C 1).map d_1) = 0) _auto✝), ({ obj := obj, d := d, d_squared := d_squared } = { obj := obj_1, d := d_1, d_squared := d_squared_1 }) = (obj = obj_1 ∧ HEq d d_1) - CategoryTheory.DifferentialObject.shiftFunctorAdd_hom_app_f Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddCommGroupWithOne S] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] (m n : S) (X : CategoryTheory.DifferentialObject S C), ((CategoryTheory.DifferentialObject.shiftFunctorAdd C m n).hom.app X).f = (CategoryTheory.shiftFunctorAdd C m n).hom.app X.obj - CategoryTheory.DifferentialObject.shiftFunctorAdd_inv_app_f Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddCommGroupWithOne S] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] (m n : S) (X : CategoryTheory.DifferentialObject S C), ((CategoryTheory.DifferentialObject.shiftFunctorAdd C m n).inv.app X).f = (CategoryTheory.shiftFunctorAdd C m n).inv.app X.obj - CategoryTheory.DifferentialObject.mk.sizeOf_spec Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] [inst_4 : SizeOf S] [inst_5 : SizeOf C] (obj : C) (d : obj ⟶ (CategoryTheory.shiftFunctor C 1).obj obj) (d_squared : autoParam (CategoryTheory.CategoryStruct.comp d ((CategoryTheory.shiftFunctor C 1).map d) = 0) _auto✝), sizeOf { obj := obj, d := d, d_squared := d_squared } = 1 + sizeOf obj + sizeOf d + sizeOf d_squared - CategoryTheory.DifferentialObject.shiftFunctor_map_f Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddCommGroupWithOne S] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] (n : S) {X Y : CategoryTheory.DifferentialObject S C} (f : X ⟶ Y), ((CategoryTheory.DifferentialObject.shiftFunctor C n).map f).f = (CategoryTheory.shiftFunctor C n).map f.f - CategoryTheory.Functor.mapDifferentialObject_map_f Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] (D : Type u') [inst_4 : CategoryTheory.Category.{v', u'} D] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D] [inst_6 : CategoryTheory.HasShift D S] (F : CategoryTheory.Functor C D) (η : (CategoryTheory.shiftFunctor C 1).comp F ⟶ F.comp (CategoryTheory.shiftFunctor D 1)) (hF : ∀ (c c' : C), F.map 0 = 0) {X Y : CategoryTheory.DifferentialObject S C} (f : X ⟶ Y), ((CategoryTheory.Functor.mapDifferentialObject D F η hF).map f).f = F.map f.f - CategoryTheory.DifferentialObject.objEqToHom Mathlib.Algebra.Homology.DifferentialObject
{β : Type u_1} → [inst : AddCommGroup β] → {b : β} → {V : Type u_2} → [inst_1 : CategoryTheory.Category.{u_3, u_2} V] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] → (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) → {i j : β} → i = j → (X.obj i ⟶ X.obj j) - CategoryTheory.DifferentialObject.objEqToHom_refl Mathlib.Algebra.Homology.DifferentialObject
∀ {β : Type u_1} [inst : AddCommGroup β] {b : β} {V : Type u_2} [inst_1 : CategoryTheory.Category.{u_3, u_2} V] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) (i : β), X.objEqToHom ⋯ = CategoryTheory.CategoryStruct.id (X.obj i) - CategoryTheory.DifferentialObject.eqToHom_f' Mathlib.Algebra.Homology.DifferentialObject
∀ {β : Type u_1} [inst : AddCommGroup β] {b : β} {V : Type u_2} [inst_1 : CategoryTheory.Category.{u_3, u_2} V] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] {X Y : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)} (f : X ⟶ Y) {x y : β} (h : x = y), CategoryTheory.CategoryStruct.comp (X.objEqToHom h) (f.f y) = CategoryTheory.CategoryStruct.comp (f.f x) (Y.objEqToHom h) - CategoryTheory.DifferentialObject.eqToHom_f'_assoc Mathlib.Algebra.Homology.DifferentialObject
∀ {β : Type u_1} [inst : AddCommGroup β] {b : β} {V : Type u_2} [inst_1 : CategoryTheory.Category.{u_3, u_2} V] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] {X Y : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)} (f : X ⟶ Y) {x y : β} (h : x = y) {Z : V} (h_1 : Y.obj y ⟶ Z), CategoryTheory.CategoryStruct.comp (X.objEqToHom h) (CategoryTheory.CategoryStruct.comp (f.f y) h_1) = CategoryTheory.CategoryStruct.comp (f.f x) (CategoryTheory.CategoryStruct.comp (Y.objEqToHom h) h_1) - CategoryTheory.DifferentialObject.objEqToHom_d Mathlib.Algebra.Homology.DifferentialObject
∀ {β : Type u_1} [inst : AddCommGroup β] {b : β} {V : Type u_2} [inst_1 : CategoryTheory.Category.{u_3, u_2} V] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) {x y : β} (h : x = y), CategoryTheory.CategoryStruct.comp (X.objEqToHom h) (X.d y) = CategoryTheory.CategoryStruct.comp (X.d x) (X.objEqToHom ⋯) - CategoryTheory.DifferentialObject.d_squared_apply Mathlib.Algebra.Homology.DifferentialObject
∀ {β : Type u_1} [inst : AddCommGroup β] {b : β} {V : Type u_2} [inst_1 : CategoryTheory.Category.{u_3, u_2} V] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) {x : β}, CategoryTheory.CategoryStruct.comp (X.d x) (X.d ((fun b_1 => b_1 + { as := 1 }.as • b) x)) = 0 - CategoryTheory.DifferentialObject.objEqToHom_d_assoc Mathlib.Algebra.Homology.DifferentialObject
∀ {β : Type u_1} [inst : AddCommGroup β] {b : β} {V : Type u_2} [inst_1 : CategoryTheory.Category.{u_3, u_2} V] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) {x y : β} (h : x = y) {Z : V} (h_1 : (CategoryTheory.shiftFunctor (CategoryTheory.GradedObjectWithShift b V) 1).obj X.obj y ⟶ Z), CategoryTheory.CategoryStruct.comp (X.objEqToHom h) (CategoryTheory.CategoryStruct.comp (X.d y) h_1) = CategoryTheory.CategoryStruct.comp (X.d x) (CategoryTheory.CategoryStruct.comp (X.objEqToHom ⋯) h_1) - CategoryTheory.DifferentialObject.d_squared_apply_assoc Mathlib.Algebra.Homology.DifferentialObject
∀ {β : Type u_1} [inst : AddCommGroup β] {b : β} {V : Type u_2} [inst_1 : CategoryTheory.Category.{u_3, u_2} V] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) {x : β} {Z : V} (h : (CategoryTheory.shiftFunctor (CategoryTheory.GradedObjectWithShift b V) 1).obj X.obj (x + 1 • b) ⟶ Z), CategoryTheory.CategoryStruct.comp (X.d x) (CategoryTheory.CategoryStruct.comp (X.d (x + 1 • b)) h) = CategoryTheory.CategoryStruct.comp 0 h - differentiable_id Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E], Differentiable 𝕜 id - differentiable_id' Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E], Differentiable 𝕜 fun x => x - differentiableAt_id Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {x : E}, DifferentiableAt 𝕜 id x - differentiableAt_id' Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {x : E}, DifferentiableAt 𝕜 (fun x => x) x - differentiableOn_id Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {s : Set E}, DifferentiableOn 𝕜 id s - Differentiable Mathlib.Analysis.Calculus.FDeriv.Basic
(𝕜 : Type u_1) → [inst : NontriviallyNormedField 𝕜] → {E : Type u_2} → [inst_1 : NormedAddCommGroup E] → [inst_2 : NormedSpace 𝕜 E] → {F : Type u_3} → [inst_3 : NormedAddCommGroup F] → [inst : NormedSpace 𝕜 F] → (E → F) → Prop - DifferentiableAt Mathlib.Analysis.Calculus.FDeriv.Basic
(𝕜 : Type u_1) → [inst : NontriviallyNormedField 𝕜] → {E : Type u_2} → [inst_1 : NormedAddCommGroup E] → [inst_2 : NormedSpace 𝕜 E] → {F : Type u_3} → [inst_3 : NormedAddCommGroup F] → [inst : NormedSpace 𝕜 F] → (E → F) → E → Prop - differentiableWithinAt_id Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E}, DifferentiableWithinAt 𝕜 id s x - DifferentiableOn Mathlib.Analysis.Calculus.FDeriv.Basic
(𝕜 : Type u_1) → [inst : NontriviallyNormedField 𝕜] → {E : Type u_2} → [inst_1 : NormedAddCommGroup E] → [inst_2 : NormedSpace 𝕜 E] → {F : Type u_3} → [inst_3 : NormedAddCommGroup F] → [inst : NormedSpace 𝕜 F] → (E → F) → Set E → Prop - DifferentiableWithinAt Mathlib.Analysis.Calculus.FDeriv.Basic
(𝕜 : Type u_1) → [inst : NontriviallyNormedField 𝕜] → {E : Type u_2} → [inst_1 : NormedAddCommGroup E] → [inst_2 : NormedSpace 𝕜 E] → {F : Type u_3} → [inst_3 : NormedAddCommGroup F] → [inst : NormedSpace 𝕜 F] → (E → F) → Set E → E → Prop - differentiable_const Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (c : F), Differentiable 𝕜 fun x => c - differentiableAt_const Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E} (c : F), DifferentiableAt 𝕜 (fun x => c) x - differentiableOn_const Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E} (c : F), DifferentiableOn 𝕜 (fun x => c) s - differentiableOn_empty Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}, DifferentiableOn 𝕜 f ∅ - differentiableWithinAt_const Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E} {s : Set E} (c : F), DifferentiableWithinAt 𝕜 (fun x => c) s x - Set.Subsingleton.differentiableOn Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E}, s.Subsingleton → DifferentiableOn 𝕜 f s - differentiableOn_singleton Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E}, DifferentiableOn 𝕜 f {x} - Differentiable.differentiableAt Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E}, Differentiable 𝕜 f → DifferentiableAt 𝕜 f x - differentiableOn_univ Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}, DifferentiableOn 𝕜 f Set.univ ↔ Differentiable 𝕜 f - Differentiable.differentiableOn Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E}, Differentiable 𝕜 f → DifferentiableOn 𝕜 f s - differentiableWithinAt_univ Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E}, DifferentiableWithinAt 𝕜 f Set.univ x ↔ DifferentiableAt 𝕜 f x - DifferentiableAt.differentiableWithinAt Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E} {s : Set E}, DifferentiableAt 𝕜 f x → DifferentiableWithinAt 𝕜 f s x - Differentiable.continuous Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}, Differentiable 𝕜 f → Continuous f - DifferentiableOn.mono Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s t : Set E}, DifferentiableOn 𝕜 f t → s ⊆ t → DifferentiableOn 𝕜 f s - DifferentiableAt.hasFDerivAt Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E}, DifferentiableAt 𝕜 f x → HasFDerivAt f (fderiv 𝕜 f x) x - DifferentiableAt.continuousAt Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E}, DifferentiableAt 𝕜 f x → ContinuousAt f x - DifferentiableOn.continuousOn Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E}, DifferentiableOn 𝕜 f s → ContinuousOn f s - DifferentiableWithinAt.mono Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E} {s t : Set E}, DifferentiableWithinAt 𝕜 f t x → s ⊆ t → DifferentiableWithinAt 𝕜 f s x - DifferentiableWithinAt.continuousWithinAt Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E} {s : Set E}, DifferentiableWithinAt 𝕜 f s x → ContinuousWithinAt f s x - DifferentiableWithinAt.hasFDerivWithinAt Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E} {s : Set E}, DifferentiableWithinAt 𝕜 f s x → HasFDerivWithinAt f (fderivWithin 𝕜 f s x) s x - DifferentiableOn.congr Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f f₁ : E → F} {s : Set E}, DifferentiableOn 𝕜 f s → (∀ x ∈ s, f₁ x = f x) → DifferentiableOn 𝕜 f₁ s - differentiableOn_congr Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f f₁ : E → F} {s : Set E}, (∀ x ∈ s, f₁ x = f x) → (DifferentiableOn 𝕜 f₁ s ↔ DifferentiableOn 𝕜 f s) - DifferentiableAt.congr_of_eventuallyEq Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f f₁ : E → F} {x : E}, DifferentiableAt 𝕜 f x → (nhds x).EventuallyEq f₁ f → DifferentiableAt 𝕜 f₁ x - Filter.EventuallyEq.differentiableAt_iff Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f₀ f₁ : E → F} {x : E}, (nhds x).EventuallyEq f₀ f₁ → (DifferentiableAt 𝕜 f₀ x ↔ DifferentiableAt 𝕜 f₁ x) - DifferentiableOn.differentiableAt Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E} {s : Set E}, DifferentiableOn 𝕜 f s → s ∈ nhds x → DifferentiableAt 𝕜 f x - DifferentiableWithinAt.differentiableAt Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E} {s : Set E}, DifferentiableWithinAt 𝕜 f s x → s ∈ nhds x → DifferentiableAt 𝕜 f x - differentiableWithinAt_congr_set Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E} {s t : Set E}, (nhds x).EventuallyEq s t → (DifferentiableWithinAt 𝕜 f s x ↔ DifferentiableWithinAt 𝕜 f t x) - DifferentiableOn.congr_mono Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f f₁ : E → F} {s t : Set E}, DifferentiableOn 𝕜 f s → (∀ x ∈ t, f₁ x = f x) → t ⊆ s → DifferentiableOn 𝕜 f₁ t - DifferentiableWithinAt.congr Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f f₁ : E → F} {x : E} {s : Set E}, DifferentiableWithinAt 𝕜 f s x → (∀ x ∈ s, f₁ x = f x) → f₁ x = f x → DifferentiableWithinAt 𝕜 f₁ s x - DifferentiableWithinAt.congr_mono Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f f₁ : E → F} {x : E} {s t : Set E}, DifferentiableWithinAt 𝕜 f s x → Set.EqOn f₁ f t → f₁ x = f x → t ⊆ s → DifferentiableWithinAt 𝕜 f₁ t x - DifferentiableWithinAt.mono_of_mem Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E} {s : Set E}, DifferentiableWithinAt 𝕜 f s x → ∀ {t : Set E}, s ∈ nhdsWithin x t → DifferentiableWithinAt 𝕜 f t x - DifferentiableWithinAt.congr_of_eventuallyEq Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f f₁ : E → F} {x : E} {s : Set E}, DifferentiableWithinAt 𝕜 f s x → (nhdsWithin x s).EventuallyEq f₁ f → f₁ x = f x → DifferentiableWithinAt 𝕜 f₁ s x - Filter.EventuallyEq.differentiableWithinAt_iff Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f₀ f₁ : E → F} {x : E} {s : Set E}, (nhdsWithin x s).EventuallyEq f₀ f₁ → f₀ x = f₁ x → (DifferentiableWithinAt 𝕜 f₀ s x ↔ DifferentiableWithinAt 𝕜 f₁ s x) - differentiableWithinAt_inter Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E} {s t : Set E}, t ∈ nhds x → (DifferentiableWithinAt 𝕜 f (s ∩ t) x ↔ DifferentiableWithinAt 𝕜 f s x) - DifferentiableOn.hasFDerivAt Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E} {s : Set E}, DifferentiableOn 𝕜 f s → s ∈ nhds x → HasFDerivAt f (fderiv 𝕜 f x) x - Filter.EventuallyEq.differentiableWithinAt_iff_of_mem Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f₀ f₁ : E → F} {x : E} {s : Set E}, (nhdsWithin x s).EventuallyEq f₀ f₁ → x ∈ s → (DifferentiableWithinAt 𝕜 f₀ s x ↔ DifferentiableWithinAt 𝕜 f₁ s x) - differentiableWithinAt_inter' Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E} {s t : Set E}, t ∈ nhdsWithin x s → (DifferentiableWithinAt 𝕜 f (s ∩ t) x ↔ DifferentiableWithinAt 𝕜 f s x) - differentiableWithinAt_congr_set' Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E} {s t : Set E} (y : E), (nhdsWithin x {y}ᶜ).EventuallyEq s t → (DifferentiableWithinAt 𝕜 f s x ↔ DifferentiableWithinAt 𝕜 f t x) - DifferentiableOn.eventually_differentiableAt Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E} {s : Set E}, DifferentiableOn 𝕜 f s → s ∈ nhds x → ∀ᶠ (y : E) in nhds x, DifferentiableAt 𝕜 f y - differentiableOn_of_locally_differentiableOn Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E}, (∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ DifferentiableOn 𝕜 f (s ∩ u)) → DifferentiableOn 𝕜 f s - DifferentiableAt.isBigO_sub Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x₀ : E}, DifferentiableAt 𝕜 f x₀ → (fun x => f x - f x₀) =O[nhds x₀] fun x => x - x₀ - DifferentiableWithinAt.isBigO_sub Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E} {x₀ : E}, DifferentiableWithinAt 𝕜 f s x₀ → (fun x => f x - f x₀) =O[nhdsWithin x₀ s] fun x => x - x₀ - HasFDerivAt.differentiableAt Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {x : E}, HasFDerivAt f f' x → DifferentiableAt 𝕜 f x - HasStrictFDerivAt.differentiableAt Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {x : E}, HasStrictFDerivAt f f' x → DifferentiableAt 𝕜 f x - HasFDerivWithinAt.differentiableWithinAt Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {s : Set E}, HasFDerivWithinAt f f' s x → DifferentiableWithinAt 𝕜 f s x - DifferentiableAt.fderivWithin Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E} {s : Set E}, DifferentiableAt 𝕜 f x → UniqueDiffWithinAt 𝕜 s x → fderivWithin 𝕜 f s x = fderiv 𝕜 f x - DifferentiableWithinAt.fderivWithin_congr_mono Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f f₁ : E → F} {x : E} {s t : Set E}, DifferentiableWithinAt 𝕜 f s x → Set.EqOn f₁ f t → f₁ x = f x → UniqueDiffWithinAt 𝕜 t x → t ⊆ s → fderivWithin 𝕜 f₁ t x = fderivWithin 𝕜 f s x - fderiv_zero_of_not_differentiableAt Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E}, ¬DifferentiableAt 𝕜 f x → fderiv 𝕜 f x = 0 - fderivWithin_zero_of_not_differentiableWithinAt Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E} {s : Set E}, ¬DifferentiableWithinAt 𝕜 f s x → fderivWithin 𝕜 f s x = 0 - IsBoundedLinearMap.differentiable Mathlib.Analysis.Calculus.FDeriv.Linear
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}, IsBoundedLinearMap 𝕜 f → Differentiable 𝕜 f - IsBoundedLinearMap.differentiableAt Mathlib.Analysis.Calculus.FDeriv.Linear
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E}, IsBoundedLinearMap 𝕜 f → DifferentiableAt 𝕜 f x - IsBoundedLinearMap.differentiableOn Mathlib.Analysis.Calculus.FDeriv.Linear
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E}, IsBoundedLinearMap 𝕜 f → DifferentiableOn 𝕜 f s - IsBoundedLinearMap.differentiableWithinAt Mathlib.Analysis.Calculus.FDeriv.Linear
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E} {s : Set E}, IsBoundedLinearMap 𝕜 f → DifferentiableWithinAt 𝕜 f s x - ContinuousLinearMap.differentiable Mathlib.Analysis.Calculus.FDeriv.Linear
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (e : E →L[𝕜] F), Differentiable 𝕜 ⇑e - ContinuousLinearMap.differentiableAt Mathlib.Analysis.Calculus.FDeriv.Linear
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (e : E →L[𝕜] F) {x : E}, DifferentiableAt 𝕜 (⇑e) x - ContinuousLinearMap.differentiableOn Mathlib.Analysis.Calculus.FDeriv.Linear
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (e : E →L[𝕜] F) {s : Set E}, DifferentiableOn 𝕜 (⇑e) s - ContinuousLinearMap.differentiableWithinAt Mathlib.Analysis.Calculus.FDeriv.Linear
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (e : E →L[𝕜] F) {x : E} {s : Set E}, DifferentiableWithinAt 𝕜 (⇑e) s x - Differentiable.iterate Mathlib.Analysis.Calculus.FDeriv.Comp
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {f : E → E}, Differentiable 𝕜 f → ∀ (n : ℕ), Differentiable 𝕜 f^[n] - DifferentiableAt.iterate Mathlib.Analysis.Calculus.FDeriv.Comp
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {x : E} {f : E → E}, DifferentiableAt 𝕜 f x → f x = x → ∀ (n : ℕ), DifferentiableAt 𝕜 f^[n] x - DifferentiableOn.iterate Mathlib.Analysis.Calculus.FDeriv.Comp
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {s : Set E} {f : E → E}, DifferentiableOn 𝕜 f s → Set.MapsTo f s s → ∀ (n : ℕ), DifferentiableOn 𝕜 f^[n] s - DifferentiableWithinAt.iterate Mathlib.Analysis.Calculus.FDeriv.Comp
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {f : E → E}, DifferentiableWithinAt 𝕜 f s x → f x = x → Set.MapsTo f s s → ∀ (n : ℕ), DifferentiableWithinAt 𝕜 f^[n] s x - Differentiable.comp Mathlib.Analysis.Calculus.FDeriv.Comp
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} {g : F → G}, Differentiable 𝕜 g → Differentiable 𝕜 f → Differentiable 𝕜 (g ∘ f) - Differentiable.comp_differentiableOn Mathlib.Analysis.Calculus.FDeriv.Comp
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} {s : Set E} {g : F → G}, Differentiable 𝕜 g → DifferentiableOn 𝕜 f s → DifferentiableOn 𝕜 (g ∘ f) s - DifferentiableAt.comp Mathlib.Analysis.Calculus.FDeriv.Comp
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} (x : E) {g : F → G}, DifferentiableAt 𝕜 g (f x) → DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 (g ∘ f) x - DifferentiableAt.comp_differentiableWithinAt Mathlib.Analysis.Calculus.FDeriv.Comp
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} (x : E) {s : Set E} {g : F → G}, DifferentiableAt 𝕜 g (f x) → DifferentiableWithinAt 𝕜 f s x → DifferentiableWithinAt 𝕜 (g ∘ f) s x - DifferentiableOn.comp Mathlib.Analysis.Calculus.FDeriv.Comp
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} {s : Set E} {g : F → G} {t : Set F}, DifferentiableOn 𝕜 g t → DifferentiableOn 𝕜 f s → Set.MapsTo f s t → DifferentiableOn 𝕜 (g ∘ f) s - DifferentiableWithinAt.comp Mathlib.Analysis.Calculus.FDeriv.Comp
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} (x : E) {s : Set E} {g : F → G} {t : Set F}, DifferentiableWithinAt 𝕜 g t (f x) → DifferentiableWithinAt 𝕜 f s x → Set.MapsTo f s t → DifferentiableWithinAt 𝕜 (g ∘ f) s x - DifferentiableWithinAt.comp' Mathlib.Analysis.Calculus.FDeriv.Comp
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} (x : E) {s : Set E} {g : F → G} {t : Set F}, DifferentiableWithinAt 𝕜 g t (f x) → DifferentiableWithinAt 𝕜 f s x → DifferentiableWithinAt 𝕜 (g ∘ f) (s ∩ f ⁻¹' t) x - differentiable_fst Mathlib.Analysis.Calculus.FDeriv.Prod
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F], Differentiable 𝕜 Prod.fst - differentiable_snd Mathlib.Analysis.Calculus.FDeriv.Prod
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F], Differentiable 𝕜 Prod.snd - differentiableAt_fst Mathlib.Analysis.Calculus.FDeriv.Prod
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {p : E × F}, DifferentiableAt 𝕜 Prod.fst p - differentiableAt_snd Mathlib.Analysis.Calculus.FDeriv.Prod
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {p : E × F}, DifferentiableAt 𝕜 Prod.snd p - differentiableOn_fst Mathlib.Analysis.Calculus.FDeriv.Prod
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set (E × F)}, DifferentiableOn 𝕜 Prod.fst s - differentiableOn_snd Mathlib.Analysis.Calculus.FDeriv.Prod
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set (E × F)}, DifferentiableOn 𝕜 Prod.snd s - differentiable_apply Mathlib.Analysis.Calculus.FDeriv.Prod
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {ι : Type u_6} [inst_1 : Fintype ι] {F' : ι → Type u_7} [inst_2 : (i : ι) → NormedAddCommGroup (F' i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (F' i)] (i : ι), Differentiable 𝕜 fun f => f i - differentiableWithinAt_fst Mathlib.Analysis.Calculus.FDeriv.Prod
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {p : E × F} {s : Set (E × F)}, DifferentiableWithinAt 𝕜 Prod.fst s p - differentiableWithinAt_snd Mathlib.Analysis.Calculus.FDeriv.Prod
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {p : E × F} {s : Set (E × F)}, DifferentiableWithinAt 𝕜 Prod.snd s p - differentiableAt_apply Mathlib.Analysis.Calculus.FDeriv.Prod
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {ι : Type u_6} [inst_1 : Fintype ι] {F' : ι → Type u_7} [inst_2 : (i : ι) → NormedAddCommGroup (F' i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (F' i)] (i : ι) (f : (i : ι) → F' i), DifferentiableAt 𝕜 (fun f => f i) f - differentiableOn_apply Mathlib.Analysis.Calculus.FDeriv.Prod
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {ι : Type u_6} [inst_1 : Fintype ι] {F' : ι → Type u_7} [inst_2 : (i : ι) → NormedAddCommGroup (F' i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (F' i)] (i : ι) (s' : Set ((i : ι) → F' i)), DifferentiableOn 𝕜 (fun f => f i) s' - differentiableWithinAt_apply Mathlib.Analysis.Calculus.FDeriv.Prod
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {ι : Type u_6} [inst_1 : Fintype ι] {F' : ι → Type u_7} [inst_2 : (i : ι) → NormedAddCommGroup (F' i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (F' i)] (i : ι) (f : (i : ι) → F' i) (s' : Set ((i : ι) → F' i)), DifferentiableWithinAt 𝕜 (fun f => f i) s' f - Differentiable.fst Mathlib.Analysis.Calculus.FDeriv.Prod
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f₂ : E → F × G}, Differentiable 𝕜 f₂ → Differentiable 𝕜 fun x => (f₂ x).1 - Differentiable.snd Mathlib.Analysis.Calculus.FDeriv.Prod
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f₂ : E → F × G}, Differentiable 𝕜 f₂ → Differentiable 𝕜 fun x => (f₂ x).2 - DifferentiableAt.fst Mathlib.Analysis.Calculus.FDeriv.Prod
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {f₂ : E → F × G}, DifferentiableAt 𝕜 f₂ x → DifferentiableAt 𝕜 (fun x => (f₂ x).1) x - DifferentiableAt.snd Mathlib.Analysis.Calculus.FDeriv.Prod
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {f₂ : E → F × G}, DifferentiableAt 𝕜 f₂ x → DifferentiableAt 𝕜 (fun x => (f₂ x).2) x - differentiable_pi'' Mathlib.Analysis.Calculus.FDeriv.Prod
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {ι : Type u_6} [inst_3 : Fintype ι] {F' : ι → Type u_7} [inst_4 : (i : ι) → NormedAddCommGroup (F' i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i}, (∀ (i : ι), Differentiable 𝕜 fun x => Φ x i) → Differentiable 𝕜 Φ - DifferentiableOn.fst Mathlib.Analysis.Calculus.FDeriv.Prod
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {f₂ : E → F × G}, DifferentiableOn 𝕜 f₂ s → DifferentiableOn 𝕜 (fun x => (f₂ x).1) s - DifferentiableOn.snd Mathlib.Analysis.Calculus.FDeriv.Prod
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {f₂ : E → F × G}, DifferentiableOn 𝕜 f₂ s → DifferentiableOn 𝕜 (fun x => (f₂ x).2) s - differentiable_pi Mathlib.Analysis.Calculus.FDeriv.Prod
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {ι : Type u_6} [inst_3 : Fintype ι] {F' : ι → Type u_7} [inst_4 : (i : ι) → NormedAddCommGroup (F' i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i}, Differentiable 𝕜 Φ ↔ ∀ (i : ι), Differentiable 𝕜 fun x => Φ x i - differentiableAt_pi'' Mathlib.Analysis.Calculus.FDeriv.Prod
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {x : E} {ι : Type u_6} [inst_3 : Fintype ι] {F' : ι → Type u_7} [inst_4 : (i : ι) → NormedAddCommGroup (F' i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i}, (∀ (i : ι), DifferentiableAt 𝕜 (fun x => Φ x i) x) → DifferentiableAt 𝕜 Φ x - DifferentiableWithinAt.fst Mathlib.Analysis.Calculus.FDeriv.Prod
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {s : Set E} {f₂ : E → F × G}, DifferentiableWithinAt 𝕜 f₂ s x → DifferentiableWithinAt 𝕜 (fun x => (f₂ x).1) s x - DifferentiableWithinAt.snd Mathlib.Analysis.Calculus.FDeriv.Prod
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {s : Set E} {f₂ : E → F × G}, DifferentiableWithinAt 𝕜 f₂ s x → DifferentiableWithinAt 𝕜 (fun x => (f₂ x).2) s x - differentiableAt_pi Mathlib.Analysis.Calculus.FDeriv.Prod
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {x : E} {ι : Type u_6} [inst_3 : Fintype ι] {F' : ι → Type u_7} [inst_4 : (i : ι) → NormedAddCommGroup (F' i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i}, DifferentiableAt 𝕜 Φ x ↔ ∀ (i : ι), DifferentiableAt 𝕜 (fun x => Φ x i) x - differentiableOn_pi'' Mathlib.Analysis.Calculus.FDeriv.Prod
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {s : Set E} {ι : Type u_6} [inst_3 : Fintype ι] {F' : ι → Type u_7} [inst_4 : (i : ι) → NormedAddCommGroup (F' i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i}, (∀ (i : ι), DifferentiableOn 𝕜 (fun x => Φ x i) s) → DifferentiableOn 𝕜 Φ s - differentiableOn_pi Mathlib.Analysis.Calculus.FDeriv.Prod
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {s : Set E} {ι : Type u_6} [inst_3 : Fintype ι] {F' : ι → Type u_7} [inst_4 : (i : ι) → NormedAddCommGroup (F' i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i}, DifferentiableOn 𝕜 Φ s ↔ ∀ (i : ι), DifferentiableOn 𝕜 (fun x => Φ x i) s - differentiableWithinAt_pi'' Mathlib.Analysis.Calculus.FDeriv.Prod
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {ι : Type u_6} [inst_3 : Fintype ι] {F' : ι → Type u_7} [inst_4 : (i : ι) → NormedAddCommGroup (F' i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i}, (∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x => Φ x i) s x) → DifferentiableWithinAt 𝕜 Φ s x - differentiableWithinAt_pi Mathlib.Analysis.Calculus.FDeriv.Prod
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {ι : Type u_6} [inst_3 : Fintype ι] {F' : ι → Type u_7} [inst_4 : (i : ι) → NormedAddCommGroup (F' i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i}, DifferentiableWithinAt 𝕜 Φ s x ↔ ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x => Φ x i) s x - Differentiable.prod Mathlib.Analysis.Calculus.FDeriv.Prod
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f₁ : E → F} {f₂ : E → G}, Differentiable 𝕜 f₁ → Differentiable 𝕜 f₂ → Differentiable 𝕜 fun x => (f₁ x, f₂ x) - DifferentiableAt.prod Mathlib.Analysis.Calculus.FDeriv.Prod
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f₁ : E → F} {x : E} {f₂ : E → G}, DifferentiableAt 𝕜 f₁ x → DifferentiableAt 𝕜 f₂ x → DifferentiableAt 𝕜 (fun x => (f₁ x, f₂ x)) x - DifferentiableOn.prod Mathlib.Analysis.Calculus.FDeriv.Prod
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f₁ : E → F} {s : Set E} {f₂ : E → G}, DifferentiableOn 𝕜 f₁ s → DifferentiableOn 𝕜 f₂ s → DifferentiableOn 𝕜 (fun x => (f₁ x, f₂ x)) s - DifferentiableWithinAt.prod Mathlib.Analysis.Calculus.FDeriv.Prod
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f₁ : E → F} {x : E} {s : Set E} {f₂ : E → G}, DifferentiableWithinAt 𝕜 f₁ s x → DifferentiableWithinAt 𝕜 f₂ s x → DifferentiableWithinAt 𝕜 (fun x => (f₁ x, f₂ x)) s x - DifferentiableAt.prod_map Mathlib.Analysis.Calculus.FDeriv.Prod
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {G' : Type u_5} [inst_7 : NormedAddCommGroup G'] [inst_8 : NormedSpace 𝕜 G'] {f : E → F} {f₂ : G → G'} (p : E × G), DifferentiableAt 𝕜 f p.1 → DifferentiableAt 𝕜 f₂ p.2 → DifferentiableAt 𝕜 (fun p => (f p.1, f₂ p.2)) p - DifferentiableAt.fderiv_prod Mathlib.Analysis.Calculus.FDeriv.Prod
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f₁ : E → F} {x : E} {f₂ : E → G}, DifferentiableAt 𝕜 f₁ x → DifferentiableAt 𝕜 f₂ x → fderiv 𝕜 (fun x => (f₁ x, f₂ x)) x = (fderiv 𝕜 f₁ x).prod (fderiv 𝕜 f₂ x) - DifferentiableWithinAt.fderivWithin_prod Mathlib.Analysis.Calculus.FDeriv.Prod
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f₁ : E → F} {x : E} {s : Set E} {f₂ : E → G}, DifferentiableWithinAt 𝕜 f₁ s x → DifferentiableWithinAt 𝕜 f₂ s x → UniqueDiffWithinAt 𝕜 s x → fderivWithin 𝕜 (fun x => (f₁ x, f₂ x)) s x = (fderivWithin 𝕜 f₁ s x).prod (fderivWithin 𝕜 f₂ s x) - HasDerivAt.differentiableAt Mathlib.Analysis.Calculus.Deriv.Basic
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜}, HasDerivAt f f' x → DifferentiableAt 𝕜 f x - HasDerivWithinAt.differentiableWithinAt Mathlib.Analysis.Calculus.Deriv.Basic
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜}, HasDerivWithinAt f f' s x → DifferentiableWithinAt 𝕜 f s x - DifferentiableAt.hasDerivAt Mathlib.Analysis.Calculus.Deriv.Basic
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜}, DifferentiableAt 𝕜 f x → HasDerivAt f (deriv f x) x - DifferentiableWithinAt.hasDerivWithinAt Mathlib.Analysis.Calculus.Deriv.Basic
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜}, DifferentiableWithinAt 𝕜 f s x → HasDerivWithinAt f (derivWithin f s x) s x - differentiableAt_of_deriv_ne_zero Mathlib.Analysis.Calculus.Deriv.Basic
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜}, deriv f x ≠ 0 → DifferentiableAt 𝕜 f x - deriv_zero_of_not_differentiableAt Mathlib.Analysis.Calculus.Deriv.Basic
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜}, ¬DifferentiableAt 𝕜 f x → deriv f x = 0 - differentiableWithinAt_of_derivWithin_ne_zero Mathlib.Analysis.Calculus.Deriv.Basic
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜}, derivWithin f s x ≠ 0 → DifferentiableWithinAt 𝕜 f s x - derivWithin_zero_of_not_differentiableWithinAt Mathlib.Analysis.Calculus.Deriv.Basic
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜}, ¬DifferentiableWithinAt 𝕜 f s x → derivWithin f s x = 0 - differentiableWithinAt_Ioi_iff_Ici Mathlib.Analysis.Calculus.Deriv.Basic
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} [inst_3 : PartialOrder 𝕜], DifferentiableWithinAt 𝕜 f (Set.Ioi x) x ↔ DifferentiableWithinAt 𝕜 f (Set.Ici x) x - DifferentiableOn.hasDerivAt Mathlib.Analysis.Calculus.Deriv.Basic
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜}, DifferentiableOn 𝕜 f s → s ∈ nhds x → HasDerivAt f (deriv f x) x - DifferentiableAt.derivWithin Mathlib.Analysis.Calculus.Deriv.Basic
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜}, DifferentiableAt 𝕜 f x → UniqueDiffWithinAt 𝕜 s x → derivWithin f s x = deriv f x - DifferentiableOn.eq_1 Mathlib.Analysis.Calculus.FDeriv.Equiv
∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E → F) (s : Set E), DifferentiableOn 𝕜 f s = ∀ x ∈ s, DifferentiableWithinAt 𝕜 f s x - LinearIsometryEquiv.differentiable Mathlib.Analysis.Calculus.FDeriv.Equiv
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (iso : E ≃ₗᵢ[𝕜] F), Differentiable 𝕜 ⇑iso - LinearIsometryEquiv.differentiableAt Mathlib.Analysis.Calculus.FDeriv.Equiv
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E} (iso : E ≃ₗᵢ[𝕜] F), DifferentiableAt 𝕜 (⇑iso) x - LinearIsometryEquiv.differentiableOn Mathlib.Analysis.Calculus.FDeriv.Equiv
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E} (iso : E ≃ₗᵢ[𝕜] F), DifferentiableOn 𝕜 (⇑iso) s - LinearIsometryEquiv.differentiableWithinAt Mathlib.Analysis.Calculus.FDeriv.Equiv
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E} {s : Set E} (iso : E ≃ₗᵢ[𝕜] F), DifferentiableWithinAt 𝕜 (⇑iso) s x - LinearIsometryEquiv.comp_differentiable_iff Mathlib.Analysis.Calculus.FDeriv.Equiv
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E}, Differentiable 𝕜 (⇑iso ∘ f) ↔ Differentiable 𝕜 f - LinearIsometryEquiv.comp_differentiableAt_iff Mathlib.Analysis.Calculus.FDeriv.Equiv
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E} {x : G}, DifferentiableAt 𝕜 (⇑iso ∘ f) x ↔ DifferentiableAt 𝕜 f x - LinearIsometryEquiv.comp_differentiableOn_iff Mathlib.Analysis.Calculus.FDeriv.Equiv
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E} {s : Set G}, DifferentiableOn 𝕜 (⇑iso ∘ f) s ↔ DifferentiableOn 𝕜 f s - LinearIsometryEquiv.comp_differentiableWithinAt_iff Mathlib.Analysis.Calculus.FDeriv.Equiv
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E} {s : Set G} {x : G}, DifferentiableWithinAt 𝕜 (⇑iso ∘ f) s x ↔ DifferentiableWithinAt 𝕜 f s x - ContinuousLinearEquiv.differentiable Mathlib.Analysis.Calculus.FDeriv.Equiv
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (iso : E ≃L[𝕜] F), Differentiable 𝕜 ⇑iso
Did you maybe mean
About
Loogle searches of Lean and Mathlib definitions and theorems.
You may also want to try the CLI version, the VS
Code extension, the lean.nvim
integration or the Zulip bot.
Usage
Loogle finds definitions and lemmas in various ways:
By constant:
🔍Real.sin
finds all lemmas whose statement somehow mentions the sine function.By lemma name substring:
🔍"differ"
finds all lemmas that have"differ"
somewhere in their lemma name.By subexpression:
🔍_ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.The pattern can also be non-linear, as in
🔍Real.sqrt ?a * Real.sqrt ?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
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 findtsum_lt_tsum
even though the hypothesisf 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, _ * _, _ ^ _, |- _ < _ → _
woould 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 currently provided by Joachim Breitner <mail@joachim-breitner.de>.
This is Loogle revision fa2ddf5
serving mathlib revision 1147162