Theorems · Theorem · logic and foundations
Cardinal.mk_image_le_lift
∀ {α : Type u} {β : Type v} {f : α → β} {s : Set α},
Cardinal.lift.{u, v} (Cardinal.mk ↑(f '' s)) ≤ Cardinal.lift.{v, u} (Cardinal.mk ↑s)- Defined in
- Mathlib.SetTheory.Cardinal.Basic
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 24 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Set.Elemstatement · cited by 7,166
- Set.imagestatement · cited by 5,609
- Cardinalstatement · cited by 2,598
- Cardinal.mkstatement · cited by 942
- Cardinal.liftstatement · cited by 583
- Cardinal.lift_mk_leproof · cited by 10
- Function.Embedding.ofSurjectiveproof · cited by 7
- Set.imageFactorizationproof · cited by 7
- Set.imageFactorization_surjectiveproof · cited by 4
Cited by6
Results whose statement or proof uses this declaration.
- Submodule.lift_spanRank_map_leproof · cited by 3
- Cardinal.mk_preimage_of_subset_range_liftproof · cited by 3
- Ideal.lift_spanRank_map_leproof · cited by 3
- Order.lift_cof_congr_of_strictMonoproof · cited by 3
- Submodule.spanRank_baseChange_leproof · cited by 2
- GaloisConnection.cof_le_liftproof · cited by 2