Theorems · Theorem · category theory

CategoryTheory.ExponentialIdeal.exp_closed

∀ {C : Type u₁} {D : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.Category.{v₁, u₂} D}
  {i : CategoryTheory.Functor D C} {inst_2 : CategoryTheory.CartesianMonoidalCategory C}
  {inst_3 : CategoryTheory.MonoidalClosed C} [self : CategoryTheory.ExponentialIdeal i] {B : C},
  i.essImage B → ∀ (A : C), i.essImage (A ⟹ B)

Defined in

Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Cited by

0 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

CategoryTheory.ExponentialIdeal