Theorem IsRefl.reflexive

Modification history

2026-01-09 08:53

Mathlib/Logic/Relation.lean

chore(Order/Defs/Unbundled): deprecate `IsRefl` in favor of core's `Std.Refl` (#33755)

Deleted IsRefl.reflexive View on Github →

2022-11-22 07:59

Mathlib/Logic/Relation.lean

feat: add `fun x ↦ t` syntax (#617)

Modified IsRefl.reflexive View on Github →

2022-11-16 23:18

Mathlib/Logic/Relation.lean

feat: port Logic.Relation (#565) …

Added IsRefl.reflexive View on Github →