Commit 2026-01-08 06:50 98379c78

View on Github →

chore(Order/Defs/Unbundled): deprecate IsIrrefl in favor of core's Std.Irrefl (#33717)

Estimated changes

modified theorem irrefl
modified theorem irrefl_of
modified theorem ne_of_irrefl'
modified theorem ne_of_irrefl
modified theorem not_rel_of_subsingleton
deleted theorem IsIrrefl.swap
added theorem Std.Irrefl.swap
modified theorem Subsingleton.isWellOrder
modified theorem eq_empty_relation
modified theorem ne_of_ssubset
modified theorem ne_of_ssuperset
modified theorem ssubset_irrefl
modified theorem ssubset_irrfl