Mathlib Map

Theorems · Definition · logic and foundations

uniqueElim

{ι : Sort u_2} → {α : ι → Sort u_3} → [inst : Unique ι] → α default → (i : ι) → α i

Given one value over a unique, we get a dependent function.

Defined in
Mathlib.Logic.Unique
Cited by
29 results in Mathlib
Foundations
Depth 5 from the axioms · uses no axioms
Assumes
Unique
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

groupCohomology.comp_d₀₁_eq · cited by 6groupCohomology.comp_d₀₁_…Equiv.piUnique · cited by 4Equiv.piUniqueEquiv.funUnique_symm_apply · cited by 4Equiv.funUnique_symm_applyFunction.update_eq_updateFinset · cited by 3Function.update_eq_update…uniqueElim_default · cited by 1uniqueElim_defaultEquiv.piUnique_symm_apply · cited by 1Equiv.piUnique_symm_applyMeasurableEquiv.funUnique_symm_apply · cited by 1MeasurableEquiv.funUnique…ContinuousLinearEquiv.piUnique_symm_apply · cited by 0ContinuousLinearEquiv.piU…MeasureTheory.measurable_uniqueElim_cylinderEvents · cited by 0MeasureTheory.measurable_…AddEquiv.piUnique_symm_apply · cited by 0AddEquiv.piUnique_symm_ap…RingEquiv.piUnique_symm_apply · cited by 0RingEquiv.piUnique_symm_a…Set.uniqueElim_preimage · cited by 0Set.uniqueElim_preimageSet.termDefinable₁_iff_exists_term · cited by 0Set.termDefinable₁_iff_ex…PiLp.equivOfUnique_symm_apply · cited by 0PiLp.equivOfUnique_symm_a…measurable_uniqueElim · cited by 0measurable_uniqueElimUnique · cited by 400UniqueuniqueElimCITED BYCITES

Cites1

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

  • Uniquestatement and proof · cited by 400

Cited by30

Results whose statement or proof uses this declaration.