Theorems · Theorem · category theory

CategoryTheory.IsCardinalFiltered.of_le

∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J] {κ : Cardinal.{w}} [hκ : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalFiltered J κ] {κ' : Cardinal.{w}} [inst_2 : Fact κ'.IsRegular],
  κ' ≤ κ → CategoryTheory.IsCardinalFiltered J κ'

Defined in

Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryFactCategoryTheory.IsCardinalFilteredFact