Theorem irreflexive_iff_subrelation_ne

Modification history

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_neView on Github →