Commit 2026-07-01 01:31 d52d26fc

View on Github →

chore(Logic/Relation): use ≤ to spell subrelation (#30526) Replace every ∀ x y, r x y → r' x y with r ≤ r'

Estimated changes

modified theorem Relation.EqvGen.mono
modified theorem Relation.ReflGen.mono
modified theorem Relation.ReflTransGen.lift'
modified theorem Relation.ReflTransGen.lift
modified theorem Relation.ReflTransGen.mono
modified theorem Relation.ReflTransGen.swap
modified theorem Relation.TransGen.closed
modified theorem Relation.TransGen.lift'
modified theorem Relation.TransGen.lift
modified theorem Relation.TransGen.mono
modified theorem Relation.TransGen.swap
deleted theorem Relation.join_of_single
modified theorem Relation.le_onFun_map
modified theorem Relation.map_mono
modified theorem Relation.map_onFun_le
modified theorem Relation.reflGen_minimal
modified theorem Relation.transGen_minimal
added theorem irrefl_iff_le_ne
deleted theorem irrefl_iff_subrelation_ne
added theorem refl_iff_eq_le
deleted theorem refl_iff_subrelation_eq