Mathlib Map

Theorems · Theorem

Nonempty.congr

∀ {α : Sort u_3} {β : Sort u_4} (f : α → β) (g : β → α), Nonempty α ↔ Nonempty β
Defined in
Mathlib.Logic.Nonempty
Cited by
6 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Equiv.nonempty_congr · cited by 47Equiv.nonempty_congrLinearEquiv.isotypicComponent_eq · cited by 4LinearEquiv.isotypicCompo…LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered · cited by 4LinearOrderedCommGroupWit…LinearOrderedCommGroupWithZero.wellFoundedOn_setOfPred_le_lt_iff_nonempty_discrete_of_ne_zero · cited by 2LinearOrderedCommGroupWit…CategoryTheory.CommSq.HasLift.iff_op · cited by 1HasLift.iff_opCategoryTheory.CommSq.HasLift.iff_unop · cited by 0HasLift.iff_unopNonempty.map · cited by 101Nonempty.mapNonempty.congrCITED BYCITES

Cites1

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

Cited by6

Results whose statement or proof uses this declaration.