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

• regular (X Y : Set F.World) : F.box X ∩ F.box Y ⊆ F.box (X ∩ Y)

theorem LO.Modal.Neighborhood.Frame.regular {F : Frame} [F.IsRegular] {X Y : Set F.World} : F.box X ∩ F.box Y ⊆ F.box (X ∩ Y)

theorem LO.Modal.Neighborhood.Frame.regular_finset_iUnion {F : Frame} [F.IsRegular] (s : Finset (Set F.World)) (hs : s.Nonempty) : ⋂ i ∈ s, F.box i ⊆ F.box (⋂ i ∈ s, i)

theorem LO.Modal.Neighborhood.Frame.regular_finite_iUnion {F : Frame} [F.IsRegular] {ι : Type u_1} [h : Fintype ι] [Nonempty ι] {X : ι → Set F.World} : ⋂ (i : ι), F.box (X i) ⊆ F.box (⋂ (i : ι), X i)

instance LO.Modal.Neighborhood.instIsRegularSimple_blackhole : Frame.simple_blackhole.IsRegular

@[simp]

theorem LO.Modal.Neighborhood.valid_axiomC_of_isRegular {F : Frame} [F.IsRegular] : F ⊧ Axioms.C (Formula.atom 0) (Formula.atom 1)

theorem LO.Modal.Neighborhood.isRegular_of_valid_axiomC {F : Frame} (h : F ⊧ Axioms.C (Formula.atom 0) (Formula.atom 1)) : F.IsRegular

instance LO.Modal.Neighborhood.instIsRegularToModelBasicCanonicityOfHasAxiomCFormulaNat {S : Type u_1} [Entailment S (Formula ℕ)] {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.E 𝓢] [Entailment.HasAxiomC 𝓢] : (basicCanonicity 𝓢).toModel.IsRegular