Theorems · Theorem · order theory
Fin.image_cast_fun
∀ {m n : ℕ} (h : m = n), Set.image (Fin.cast h) = Set.preimage (Fin.cast ⋯)- Defined in
- Mathlib.Order.Interval.Set.Fin
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses propext, Quot.sound
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.
- Setstatement · cited by 53,352
- Set.imagestatement · cited by 5,609
- Set.preimagestatement · cited by 4,946
- Fin.image_castproof · cited by 1
Cited by18
Results whose statement or proof uses this declaration.
- Fin.map_finCongr_Iccproof · cited by 1
- Fin.map_finCongr_Iciproof · cited by 1
- Fin.map_finCongr_Icoproof · cited by 1
- Fin.map_finCongr_Iicproof · cited by 1
- Fin.map_finCongr_Iioproof · cited by 1
- Fin.map_finCongr_Iocproof · cited by 1
- Fin.map_finCongr_Ioiproof · cited by 1
- Fin.map_finCongr_Iooproof · cited by 1
- Fin.map_finCongr_uIccproof · cited by 1
- Fin.finsetImage_cast_Iccproof · cited by 0
- Fin.finsetImage_cast_Iciproof · cited by 0
- Fin.finsetImage_cast_Icoproof · cited by 0