Mathlib v3 is deprecated. Go to Mathlib v4

Theorem order_iso.to_equiv_to_fun

Modification history

2020-06-01 03:45
src/order/order_iso.lean
feat(order/order_iso): group structure on order automorphisms (#2875) …
Deleted order_iso.to_equiv_to_funView on Github →
2019-05-10 00:53
src/order/order_iso.lean
feat(set_theory): add to cardinal, ordinal, cofinality (#963) …
Added order_iso.to_equiv_to_funView on Github →