Theorems · Theorem · general topology

LightDiagram.mk.inj

∀ {diagram : CategoryTheory.Functor ℕᵒᵖ FintypeCat}
  {cone : CategoryTheory.Limits.Cone (diagram.comp FintypeCat.toProfinite)}
  {isLimit : CategoryTheory.Limits.IsLimit cone} {diagram_1 : CategoryTheory.Functor ℕᵒᵖ FintypeCat}
  {cone_1 : CategoryTheory.Limits.Cone (diagram_1.comp FintypeCat.toProfinite)}
  {isLimit_1 : CategoryTheory.Limits.IsLimit cone_1},
  { diagram := diagram, cone := cone, isLimit := isLimit } =
      { diagram := diagram_1, cone := cone_1, isLimit := isLimit_1 } →
    diagram = diagram_1 ∧ cone ≍ cone_1 ∧ isLimit ≍ isLimit_1

Defined in

Mathlib.Topology.Category.LightProfinite.Basic

Cited by

1 results in Mathlib

Foundations

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