Commit 2023-01-27 10:07 c16deadd

View on Github →

feat: Port Data.Sym.Sym2 (#1805)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Sym/Sym2.lean

added theorem Sym2.IsDiag.mem_range_diag

added def Sym2.IsDiag

added def Sym2.Mem.other'

added theorem Sym2.Rel.is_equivalence

added theorem Sym2.Rel.symm

added theorem Sym2.Rel.trans

added inductive Sym2.Rel

added def Sym2.ToRel

added theorem Sym2.ball

added theorem Sym2.coe_lift_symm_apply

added theorem Sym2.coe_lift₂_symm_apply

added theorem Sym2.congr_left

added theorem Sym2.congr_right

added def Sym2.diag

added theorem Sym2.diag_injective

added theorem Sym2.diag_isDiag

added def Sym2.eqBool

added theorem Sym2.eqBool_spec

added theorem Sym2.eq_iff

added theorem Sym2.eq_of_ne_mem

added theorem Sym2.eq_swap

added def Sym2.equivMultiset

added def Sym2.equivSym

added theorem Sym2.ext

added theorem Sym2.filter_image_quotient_mk''_isDiag

added theorem Sym2.filter_image_quotient_mk''_not_isDiag

added def Sym2.fromRel

added theorem Sym2.fromRel_bot

added theorem Sym2.fromRel_irreflexive

added theorem Sym2.fromRel_proj_prop

added theorem Sym2.fromRel_prop

added theorem Sym2.fromRel_toRel

added theorem Sym2.fromRel_top

added theorem Sym2.isDiag_iff_mem_range_diag

added theorem Sym2.isDiag_iff_proj_eq

added def Sym2.lift

added theorem Sym2.lift_mk''

added def Sym2.lift₂

added theorem Sym2.lift₂_mk''

added theorem Sym2.map.injective

added def Sym2.map

added theorem Sym2.map_comp

added theorem Sym2.map_congr

added theorem Sym2.map_id'

added theorem Sym2.map_id

added theorem Sym2.map_map

added theorem Sym2.map_pair_eq

added theorem Sym2.mem_and_mem_iff

added theorem Sym2.mem_fromRel_irrefl_other_ne

added theorem Sym2.mem_iff'

added theorem Sym2.mem_iff

added theorem Sym2.mem_iff_exists

added theorem Sym2.mem_iff_mem

added theorem Sym2.mem_map

added theorem Sym2.mem_mk''_left

added theorem Sym2.mem_mk''_right

added theorem Sym2.mk''_eq_mk''_iff

added theorem Sym2.mk''_isDiag_iff

added theorem Sym2.mk''_prod_swap_eq

added theorem Sym2.other_eq_other'

added theorem Sym2.other_invol'

added theorem Sym2.other_invol

added theorem Sym2.other_mem'

added theorem Sym2.other_mem

added theorem Sym2.other_ne

added theorem Sym2.other_spec'

added theorem Sym2.other_spec

added theorem Sym2.out_fst_mem

added theorem Sym2.out_snd_mem

added def Sym2.relBool

added theorem Sym2.relBool_spec

added theorem Sym2.rel_iff

added def Sym2.sym2EquivSym'

added theorem Sym2.toRel_fromRel

added theorem Sym2.toRel_prop

added theorem Sym2.toRel_symmetric

added def Sym2