Commit 2026-03-26 23:51 69f7ea61

View on Github →

chore(Order/Defs/Unbundled): deprecate def Transitive in favor of class IsTrans (#35592)

Estimated changes

Modified Mathlib/Algebra/Group/Semiconj/Defs.lean

Modified Mathlib/CategoryTheory/Abelian/Pseudoelements.lean

modified theorem CategoryTheory.Abelian.pseudoEqual_trans

Modified Mathlib/CategoryTheory/IsConnected.lean

Modified Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean

modified def SimpleGraph.IsCompleteMultipartite

modified theorem SimpleGraph.bot_isCompleteMultipartite

Modified Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean

Modified Mathlib/Computability/Reduce.lean

added theorem isTrans_manyOneReducible

added theorem isTrans_oneOneReducible

deleted theorem transitive_manyOneReducible

deleted theorem transitive_oneOneReducible

Modified Mathlib/Data/List/MinMax.lean

modified theorem List.not_of_mem_foldl_argAux

Modified Mathlib/Data/Seq/Computation.lean

modified theorem Computation.LiftRel.equiv

modified theorem Computation.LiftRel.trans

Modified Mathlib/Data/WSeq/Relation.lean

modified theorem Stream'.WSeq.LiftRel.equiv

modified theorem Stream'.WSeq.LiftRel.trans

Modified Mathlib/GroupTheory/FreeGroup/Basic.lean

Modified Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean

Modified Mathlib/Logic/Relation.lean

added theorem IsTrans.comap

modified theorem Relation.equivalence_join

added theorem Relation.isTrans_join

added theorem Relation.isTrans_map

deleted theorem Relation.map_transitive

modified theorem Relation.reflTransGen_eq_reflGen

modified theorem Relation.reflTransGen_eq_self

added theorem Relation.reflTransGen_of_isTrans_reflexive

deleted theorem Relation.reflTransGen_of_transitive_reflexive

modified theorem Relation.transGen_eq_self

modified theorem Relation.transGen_minimal

deleted theorem Relation.transitive_join

modified theorem Relation.transitive_reflTransGen

modified theorem Relation.transitive_transGen

deleted theorem Transitive.comap

Modified Mathlib/ModelTheory/Order.lean

Modified Mathlib/ModelTheory/Semantics.lean

modified theorem FirstOrder.Language.Relations.realize_transitive

Modified Mathlib/Order/Defs/Unbundled.lean

added theorem Equivalence.isTrans

deleted theorem Equivalence.transitive

added theorem InvImage.isTrans

deleted theorem InvImage.trans

added theorem isTrans_def

Modified Mathlib/Order/Interval/Finset/Basic.lean

Modified Mathlib/Order/Quotient.lean

Modified Mathlib/Order/RelClasses.lean

added theorem isTrans_le

added theorem isTrans_lt

deleted theorem transitive_le

deleted theorem transitive_lt

Modified Mathlib/Topology/Connected/Clopen.lean

Modified Mathlib/Topology/Metrizable/Uniformity.lean