Mathlib Map

Theorems · Theorem · logic and foundations

HasCardinalLT.of_le

∀ {X : Type u} {κ : Cardinal.{v}}, HasCardinalLT X κ → ∀ {κ' : Cardinal.{v}}, κ ≤ κ' → HasCardinalLT X κ'
Defined in
Mathlib.SetTheory.Cardinal.HasCardinalLT
Cited by
5 results in Mathlib
Foundations
Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

CategoryTheory.isFiltered_of_isCardinalFiltered · cited by 18CategoryTheory.isFiltered…hasCardinalLT_of_finite · cited by 5hasCardinalLT_of_finiteCategoryTheory.IsCardinalFiltered.of_le · cited by 3IsCardinalFiltered.of_leCategoryTheory.ObjectProperty.IsStrongGenerator.isDense_colimitsCardinalClosure_ι · cited by 2IsStrongGenerator.isDense…hasCardinalLT_option_iff · cited by 1hasCardinalLT_option_iffCardinal · cited by 2598Cardinallt_of_lt_of_le · cited by 438lt_of_lt_of_leHasCardinalLT · cited by 99HasCardinalLTHasCardinalLT.of_leCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by5

Results whose statement or proof uses this declaration.