Theorem irreflexive_iff_subrelation_ne

Modification history

2026-02-16 11:54

Mathlib/Logic/Relation.lean

chore(Order/Defs/Unbundled): deprecate `def Irreflexive` in favor of `class Std.Irrefl` (#35191)

Deleted irreflexive_iff_subrelation_ne View on Github →

2025-11-04 21:16

Mathlib/Logic/Relation.lean

feat(Logic/Relation): a relation is reflexive iff it subsumes the equality relation (#30557) …

Added irreflexive_iff_subrelation_ne View on Github →