@[reducible, inline]

abbrev LO.Modal.Kripke.Frame.IsIrreflexive (F : Frame) : Prop

Equations

• F.IsIrreflexive = Std.Irrefl F.Rel

@[simp]

theorem LO.Modal.Kripke.Frame.irrefl {F : Frame} [F.IsIrreflexive] (x : F.World) : ¬x ≺ x

class LO.Modal.Kripke.Frame.IsStrictPreorder (F : Frame) extends Std.Irrefl F.Rel, IsTrans F.World F.Rel : Prop

• irrefl (a : F.World) : ¬F.Rel a a
• trans (a b c : F.World) : F.Rel a b → F.Rel b c → F.Rel a c