Theorems · Definition · real analysis
OrderedFinpartition.invEmbedding
{n : ℕ} → (c : OrderedFinpartition n) → (j : Fin n) → Fin (c.partSize (c.index j))The inverse of c.emb for c : OrderedFinpartition. It maps j : Fin n to the point in
Fin (c.partSize (c.index j)) which is mapped back to j by c.emb (c.index j).
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 10 from the axioms · uses Classical.choice
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- OrderedFinpartitionstatement and proof · cited by 61
- OrderedFinpartition.partSizestatement · cited by 47
- OrderedFinpartition.indexstatement · cited by 6
- OrderedFinpartition.exists_inverseproof · cited by 1
Cited by5
Results whose statement or proof uses this declaration.
- OrderedFinpartition.emb_invEmbeddingstatement · cited by 3
- OrderedFinpartition.equivSigmaproof · cited by 2
- OrderedFinpartition.emb_zeroproof · cited by 1
- OrderedFinpartition.applyOrderedFinpartition_update_rightstatement and proof · cited by 0
- OrderedFinpartition.index_extendMiddle_zeroproof · cited by 0