Theorems · Theorem · category theory

ContAction.res_map

∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] {FV : V → V → Type u_2} {CV : V → Type u_3}
  [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [inst_2 : CategoryTheory.ConcreteCategory V FV]
  [inst_3 : CategoryTheory.HasForget₂ V TopCat] {G : Type u_4} [inst_4 : Monoid G] [inst_5 : TopologicalSpace G]
  {H : Type u_5} [inst_6 : Monoid H] [inst_7 : TopologicalSpace H] (f : G →ₜ* H) {X Y : ContAction V H} (f_1 : X ⟶ Y),
  (ContAction.res V f).map f_1 = CategoryTheory.ObjectProperty.homMk ((Action.res V ↑f).map f_1.hom)

Defined in

Mathlib.CategoryTheory.Action.Continuous

Cited by

0 results in Mathlib

Foundations

Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryFunLikeCategoryTheory.ConcreteCategoryCategoryTheory.HasForget₂MonoidTopologicalSpaceMonoidTopologicalSpace