Theorems · Theorem · logic and foundations
Cardinal.mk_out
∀ (c : Cardinal.{u_1}), Cardinal.mk (Quotient.out c) = c- Defined in
- Mathlib.SetTheory.Cardinal.Defs
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 20 from the axioms · uses Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Cardinalstatement and proof · cited by 2,598
- Cardinal.mkstatement · cited by 942
- Quotient.outstatement · cited by 141
- Quotient.out_eqproof · cited by 27
Cited by14
Results whose statement or proof uses this declaration.
- Cardinal.lift_sumproof · cited by 5
- Cardinal.prod_eq_of_fintypeproof · cited by 2
- Cardinal.prod_le_prodproof · cited by 2
- Cardinal.sum_lt_prodproof · cited by 1
- Cardinal.sum_nat_eq_add_sum_succproof · cited by 1
- Cardinal.sum_pow_le_max_aleph0proof · cited by 1
- Cardinal.small_iff_lift_mk_lt_univproof · cited by 1
- Cardinal.nonempty_outproof · cited by 1
- Cardinal.sum_add_distribproof · cited by 1
- FirstOrder.Language.Theory.exists_large_model_of_infinite_modelproof · cited by 1
- Cardinal.sum_pow_eq_max_aleph0proof · cited by 0
- Cardinal.out_embeddingproof · cited by 0