Theorem irrefl_iff_subrelation_ne

Modification history

2026-07-01 01:31
Mathlib/Logic/Relation.lean
chore(Logic/Relation): use `≤` to spell subrelation (#30526) …
Deleted irrefl_iff_subrelation_neView on Github →
2026-02-16 11:54
Mathlib/Logic/Relation.lean
chore(Order/Defs/Unbundled): deprecate `def Irreflexive` in favor of `class Std.Irrefl` (#35191)
Added irrefl_iff_subrelation_neView on Github →