Theorems · Theorem · order theory

Fin.image_rev_fun

∀ {n : ℕ}, Set.image Fin.rev = Set.preimage Fin.rev

Defined in: Mathlib.Order.Interval.Set.Fin
Cited by: 18 results in Mathlib
Foundations: Depth 23 from the axioms · uses propext, Quot.sound

Mathlib docs Source Loogle LeanSearch

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_revproof · cited by 1

Cited by18

Results whose statement or proof uses this declaration.

Fin.finsetImage_rev_Iccproof · cited by 0
Fin.finsetImage_rev_Iciproof · cited by 0
Fin.finsetImage_rev_Icoproof · cited by 0
Fin.finsetImage_rev_Iicproof · cited by 0
Fin.finsetImage_rev_Iioproof · cited by 0
Fin.finsetImage_rev_Iocproof · cited by 0
Fin.finsetImage_rev_Ioiproof · cited by 0
Fin.finsetImage_rev_Iooproof · cited by 0
Fin.finsetImage_rev_uIccproof · cited by 0
Fin.map_revPerm_Iccproof · cited by 0
Fin.map_revPerm_Iciproof · cited by 0
Fin.map_revPerm_Icoproof · cited by 0