Theorem irrefl_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)

Added irrefl_iff_subrelation_ne View on Github →