Commit 2022-11-28 16:29 0f9bf8d9

View on Github →

feat: port Logic.Equiv.Option (#674) Initial port for Logic.Equiv.Option -- syntax, naming & many proofs. Based on 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3

Estimated changes

Modified Mathlib.lean

Created Mathlib/Logic/Equiv/Option.lean

added theorem Equiv.coe_optionSubtype_apply_apply

added def Equiv.optionCongr

added theorem Equiv.optionCongr_eq_equivFunctor_mapEquiv

added theorem Equiv.optionCongr_injective

added theorem Equiv.optionCongr_refl

added theorem Equiv.optionCongr_symm

added theorem Equiv.optionCongr_trans

added def Equiv.optionSubtype

added theorem Equiv.optionSubtype_apply_apply

added theorem Equiv.optionSubtype_apply_symm_apply

added theorem Equiv.optionSubtype_symm_apply_apply_coe

added theorem Equiv.optionSubtype_symm_apply_apply_none

added theorem Equiv.optionSubtype_symm_apply_apply_some

added theorem Equiv.optionSubtype_symm_apply_symm_apply

added theorem Equiv.option_symm_apply_none_iff

added def Equiv.removeNone

added def Equiv.removeNone_aux

added theorem Equiv.removeNone_aux_inv

added theorem Equiv.removeNone_aux_none

added theorem Equiv.removeNone_aux_some

added theorem Equiv.removeNone_none

added theorem Equiv.removeNone_optionCongr

added theorem Equiv.removeNone_some

added theorem Equiv.removeNone_symm

added theorem Equiv.some_removeNone_iff