Commit 2022-10-25 00:37 adad5447

View on Github →

feat: port Data.Sum.Basic (#497) Changed the import from Data.Option.Basic to Logic.Function.Basic because that is enough

Estimated changes

added theorem Sum.Lex.mono
added theorem Sum.Lex.mono_left
added theorem Sum.Lex.mono_right
added inductive Sum.Lex
added theorem Sum.LiftRel.mono
added theorem Sum.LiftRel.mono_left
added theorem Sum.LiftRel.mono_right
added inductive Sum.LiftRel
added theorem Sum.comp_elim
added theorem Sum.elim_comp_inl
added theorem Sum.elim_comp_inl_inr
added theorem Sum.elim_comp_inr
added theorem Sum.elim_comp_map
added theorem Sum.elim_const_const
added theorem Sum.elim_inl
added theorem Sum.elim_inl_inr
added theorem Sum.elim_inr
added theorem Sum.elim_update_left
added theorem Sum.elim_update_right
added def Sum.getLeft
added def Sum.getRight
added theorem Sum.inl.inj_iff
added theorem Sum.inl_injective
added theorem Sum.inl_ne_inr
added theorem Sum.inr.inj_iff
added theorem Sum.inr_injective
added theorem Sum.inr_ne_inl
added def Sum.isLeft
added def Sum.isRight
added theorem Sum.lex_acc_inl
added theorem Sum.lex_acc_inr
added theorem Sum.lex_inl_inl
added theorem Sum.lex_inr_inl
added theorem Sum.lex_inr_inr
added theorem Sum.lex_wf
added theorem Sum.liftRel_inl_inl
added theorem Sum.liftRel_inr_inr
added theorem Sum.liftRel_swap_iff
added theorem Sum.map_comp_map
added theorem Sum.map_id_id
added theorem Sum.map_inl
added theorem Sum.map_inr
added theorem Sum.map_map
added def Sum.swap
added theorem Sum.swap_inl
added theorem Sum.swap_inr
added theorem Sum.swap_left_inverse
added theorem Sum.swap_right_inverse
added theorem Sum.swap_swap
added theorem Sum.swap_swap_eq
added theorem Sum.update_elim_inl
added theorem Sum.update_elim_inr
added theorem Sum.«exists»
added theorem Sum.«forall»
added def Sum3.in₀
added def Sum3.in₁
added def Sum3.in₂