Commit 2026-04-14 12:34 aff21abb

View on Github →

chore(Order/Defs/Unbundled): deprecate def Reflexive in favor of class Std.Refl (#37278) Also adds definitional lemmas std*_def for the relation classes, and cleans up things nearby, especially in Logic/Relation.lean.

Estimated changes

deleted theorem isTrans_manyOneReducible
deleted theorem isTrans_oneOneReducible
deleted theorem reflexive_oneOneReducible
modified theorem Computation.LiftRel.equiv
deleted theorem Computation.LiftRel.refl
deleted theorem Computation.LiftRel.trans
modified theorem Sym2.diagSet_subset_fromRel
modified theorem Stream'.WSeq.LiftRel.equiv
deleted theorem Stream'.WSeq.LiftRel.refl
modified theorem FreeGroup.join_red_of_step
deleted theorem IsTrans.comap
added theorem IsTrans.map
deleted theorem Reflexive.comap
deleted theorem Reflexive.ne_imp_iff
deleted theorem Reflexive.rel_of_ne_imp
modified theorem Relation.equivalence_join
modified theorem Relation.isTrans_join
deleted theorem Relation.isTrans_map
modified theorem Relation.join_of_single
deleted theorem Relation.map_reflexive
modified theorem Relation.reflGen_eq_self
modified theorem Relation.reflGen_minimal
deleted theorem Relation.reflexive_join
modified theorem Relation.reflexive_reflGen
modified theorem Relation.transGen_eq_self
modified theorem Relation.transGen_minimal
added theorem Std.Refl.map
added theorem Std.Refl.ne_imp_iff
deleted theorem Std.Refl.reflexive
added theorem Std.Refl.rel_of_ne_imp
deleted theorem reflexive_ne_imp_iff
deleted theorem Equivalence.reflexive
added theorem Equivalence.stdRefl
deleted theorem InvImage.irrefl
deleted theorem InvImage.isTrans
added theorem antisymm_def
added theorem asymm_def
added theorem irrefl_def
added theorem refl_def
added theorem symm_def
added theorem total_def
added theorem trichotomous_def
modified theorem directedOn_pair'
modified theorem directedOn_pair
modified theorem directedOn_singleton