Commit 2021-08-03 11:55 1a8b1233

View on Github →

feat(Data/Prod) port data/prod.lean (#28)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Prod.lean

added theorem Function.injective.prod_map

added theorem Function.surjective.prod_map

added theorem Prod.eq_iff_fst_eq_snd_eq

added theorem Prod.exists'

added theorem Prod.ext'

added theorem Prod.ext_iff

added theorem Prod.forall'

added theorem Prod.fst_eq_iff

added theorem Prod.fst_injective

added theorem Prod.fst_surjective

added theorem Prod.fst_swap

added theorem Prod.id_prod

added theorem Prod.lex_def

added theorem Prod.map_comp_map

added theorem Prod.map_def

added theorem Prod.map_fst'

added theorem Prod.map_fst

added theorem Prod.map_map

added theorem Prod.map_mk

added theorem Prod.map_snd'

added theorem Prod.map_snd

added theorem Prod.mk.eta

added theorem Prod.mk.inj_iff

added theorem Prod.mk.inj_left

added theorem Prod.mk.inj_right

added theorem Prod.snd_eq_iff

added theorem Prod.snd_injective

added theorem Prod.snd_surjective

added theorem Prod.snd_swap

added def Prod.swap

added theorem Prod.swap_bijective

added theorem Prod.swap_inj

added theorem Prod.swap_injective

added theorem Prod.swap_left_inverse

added theorem Prod.swap_prod_mk

added theorem Prod.swap_right_inverse

added theorem Prod.swap_surjective

added theorem Prod.swap_swap

added theorem Prod.swap_swap_eq

added theorem Prod.«exists»

added theorem Prod.«forall»

added theorem prod_map

Modified Mathlib/Logic/Basic.lean

added def Iff.elim_left

added def Iff.elim_right

added def decidable_of_decidable_of_iff

added theorem not_iff_not_of_iff