class LO.Modal.Neighborhood.Frame.HasPropertyK (F : Frame) : Prop

• K (X Y : Set F.World) : F.box (Xᶜ ∪ Y) ∩ F.box X ⊆ F.box Y

@[simp]

theorem LO.Modal.Neighborhood.valid_axiomK_of_hasPropertyK {F : Frame} {a b : ℕ} [F.HasPropertyK] : F ⊧ Axioms.K (Formula.atom a) (Formula.atom b)

theorem LO.Modal.Neighborhood.hasPropertyK_of_valid_axiomK {F : Frame} (h : F ⊧ Axioms.K (Formula.atom 0) (Formula.atom 1)) : F.HasPropertyK