Mathlib Map

Theorems · Definition

Equiv.plift

{α : Sort u} → PLift α ≃ α

PLift α is equivalent to α.

Defined in
Mathlib.Logic.Equiv.Defs
Cited by
23 results in Mathlib
Foundations
Depth 10 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

finsum_eq_sum_of_support_subset · cited by 28finsum_eq_sum_of_support_…finprod_eq_prod_of_mulSupport_subset · cited by 21finprod_eq_prod_of_mulSup…AddMonoidHom.map_finsum · cited by 9AddMonoidHom.map_finsumfinsum_def · cited by 8finsum_deffinprod_def · cited by 7finprod_defPLift.up_surjective · cited by 4PLift.up_surjectiveMonoidHom.map_finprod · cited by 4MonoidHom.map_finprodPLift.down_surjective · cited by 4PLift.down_surjectiveEquiv.plift_symm_apply · cited by 3Equiv.plift_symm_applyEquiv.pprodEquivProdPLift · cited by 2Equiv.pprodEquivProdPLiftPLift.up_bijective · cited by 2PLift.up_bijectiveiInf_iSup_eq_of_finite · cited by 2iInf_iSup_eq_of_finitePLift.down_bijective · cited by 2PLift.down_bijectiveSet.Finite.biInf_iSup_eq · cited by 1Finite.biInf_iSup_eqFilter.iInf_sets_eq_finite' · cited by 1Filter.iInf_sets_eq_finit…Equiv · cited by 8337EquivEquiv.pliftCITED BYCITES

Cites1

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

  • Equivstatement · cited by 8,337

Cited by25

Results whose statement or proof uses this declaration.