Theorem FirstOrder.Language.Relations.realize_irreflexive

Modification history

2026-02-16 11:54

Mathlib/ModelTheory/Semantics.lean

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

Modified FirstOrder.Language.Relations.realize_irreflexive View on Github →

2023-05-12 15:18

Mathlib/ModelTheory/Semantics.lean

feat: port ModelTheory.Semantics (#3196)

Added FirstOrder.Language.Relations.realize_irreflexive View on Github →