Theorems · Theorem · logic and foundations
ExistsUnique.unique
∀ {α : Sort u_1} {p : α → Prop}, (∃! x, p x) → ∀ {y₁ y₂ : α}, p y₁ → p y₂ → y₁ = y₂- Defined in
- Mathlib.Logic.ExistsUnique
- Cited by
- 42 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ExistsUniquestatement and proof · cited by 268
Cited by42
Results whose statement or proof uses this declaration.
- IsLocalRing.eq_maximalIdealproof · cited by 20
- Function.bijective_iff_existsUniqueproof · cited by 15
- IsLocalizedModule.linearMap_extproof · cited by 8
- IsBaseChange.of_lift_uniqueproof · cited by 5
- Submodule.toLinearPMap_graph_eqproof · cited by 4
- IsLocalHom.of_surjectiveproof · cited by 4
- Setoid.eq_of_mem_eqv_classproof · cited by 3
- SimpleGraph.IsTree.card_edgeFinsetproof · cited by 3
- MeasureTheory.IsAddFundamentalDomain.mk'proof · cited by 3
- SSet.S.IsUniquelyCodimOneFace.δ_eq_iffproof · cited by 3
- IsDiscreteValuationRing.TFAEproof · cited by 3