Commit 2022-12-22 08:25 7374a9af

View on Github →

feat: port Data.Setoid.Basic (#1117)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Setoid/Basic.lean

added theorem Quot.subsingleton_iff

added theorem Quotient.eq_rel

added theorem Quotient.subsingleton_iff

added def Setoid.Rel

added theorem Setoid.bot_def

added def Setoid.comap

added theorem Setoid.comap_eq

added theorem Setoid.comap_rel

added theorem Setoid.comm'

added def Setoid.correspondence

added theorem Setoid.eq_iff_rel_eq

added theorem Setoid.eq_top_iff

added theorem Setoid.eqvGen_eq

added theorem Setoid.eqvGen_idem

added theorem Setoid.eqvGen_le

added theorem Setoid.eqvGen_mono

added theorem Setoid.eqvGen_of_setoid

added theorem Setoid.ext'

added theorem Setoid.ext_iff

added def Setoid.gi

added theorem Setoid.inf_def

added theorem Setoid.inf_iff_and

added theorem Setoid.infₛ_def

added theorem Setoid.injective_iff_ker_bot

added def Setoid.ker

added theorem Setoid.ker_apply_mk_out'

added theorem Setoid.ker_apply_mk_out

added theorem Setoid.ker_def

added theorem Setoid.ker_eq_lift_of_injective

added theorem Setoid.ker_iff_mem_preimage

added theorem Setoid.ker_lift_injective

added theorem Setoid.ker_mk_eq

added theorem Setoid.le_def

added def Setoid.liftEquiv

added theorem Setoid.lift_unique

added def Setoid.map

added def Setoid.mapOfSurjective

added theorem Setoid.mapOfSurjective_eq_map

added def Setoid.quotientKerEquivOfRightInverse

added def Setoid.quotientQuotientEquivQuotient

added theorem Setoid.refl'

added theorem Setoid.sup_def

added theorem Setoid.sup_eq_eqvGen

added theorem Setoid.supₛ_def

added theorem Setoid.supₛ_eq_eqvGen

added theorem Setoid.symm'

added theorem Setoid.top_def

added theorem Setoid.trans'