Theorems · Definition
List.equivSigmaTuple
{α : Type u} → List α ≃ (n : ℕ) × (Fin n → α)Lists are equivalent to the sigma type of tuples of a given length.
- Defined in
- Mathlib.Data.List.OfFn
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 49 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Equivstatement · cited by 8,337
- List.ofFn_getproof · cited by 3
Cited by7
Results whose statement or proof uses this declaration.
- List.ofFn_inj'proof · cited by 2
- List.exists_iff_exists_tupleproof · cited by 1
- List.ofFnRec_ofFnproof · cited by 0
- List.forall_iff_forall_tupleproof · cited by 0
- List.equivSigmaTuple_apply_fststatement and proof · cited by 0
- List.equivSigmaTuple_apply_sndstatement and proof · cited by 0
- List.equivSigmaTuple_symm_applystatement and proof · cited by 0