Mathlib Map

Theorems · Theorem · logic and foundations

Cardinal.toENatAux_gc

GaloisConnection Cardinal.ofENat Cardinal.toENatAux
Defined in
Mathlib.SetTheory.Cardinal.ENat
Cited by
2 results in Mathlib
Foundations
Depth 83 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.

Cardinal.enat_gc · cited by 4Cardinal.enat_gcCardinal.toENatAux_eq_nat · cited by 2Cardinal.toENatAux_eq_natENat · cited by 4985ENatLE.le.trans · cited by 3151le.transCardinal · cited by 2598CardinalCardinal.aleph0 · cited by 521Cardinal.aleph0GaloisConnection · cited by 253GaloisConnectionlt_or_ge · cited by 182lt_or_geCardinal.ofENat · cited by 66Cardinal.ofENatCardinal.toENatAux · cited by 8Cardinal.toENatAuxCardinal.toENatAux_nat · cited by 4Cardinal.toENatAux_natCardinal.ofENat_le_aleph0 · cited by 3Cardinal.ofENat_le_aleph0Cardinal.toENatAux_eq_top · cited by 3Cardinal.toENatAux_eq_topCardinal.toENatAux_gcCITED BYCITES

Cites11

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

Cited by2

Results whose statement or proof uses this declaration.