Documentation

Foundation.Modal.Kripke.Filteration

def LO.Modal.Kripke.filterEquiv (M : Model) (T : Theory ) [T.SubformulaClosed] (x y : M.World) :
Equations
def LO.Modal.Kripke.FilterEqvSetoid (M : Model) (T : Theory ) [T.SubformulaClosed] :
Setoid M.World
Equations
theorem LO.Modal.Kripke.FilterEqvQuotient.finite (M : Model) (T : Theory ) [T.SubformulaClosed] (T_finite : Set.Finite T) :
class LO.Modal.Kripke.FilterOf (FM M : Model) (T : Theory ) [T.SubformulaClosed] :
Instances
theorem LO.Modal.Kripke.reflexive_filterOf_of_reflexive {M : Model} {T : Theory } [T.SubformulaClosed] {FM : Model} (h_filter : FilterOf FM M T) (hRefl : Reflexive M.Rel) :
Reflexive FM.Rel
theorem LO.Modal.Kripke.serial_filterOf_of_serial {M : Model} {T : Theory } [T.SubformulaClosed] {FM : Model} (h_filter : FilterOf FM M T) (hSerial : Serial M.Rel) :
Serial FM.Rel
@[reducible, inline]
abbrev LO.Modal.Kripke.standardFilterationValuation (M : Model) (T : Theory ) [T.SubformulaClosed] (Qx : FilterEqvQuotient M T) (a : ) :
Equations
@[reducible, inline]
abbrev LO.Modal.Kripke.coarsestFilterationFrame (M : Model) (T : Theory ) [T.SubformulaClosed] :
Equations
  • One or more equations did not get rendered due to their size.
@[reducible, inline]
abbrev LO.Modal.Kripke.finestFilterationFrame (M : Model) (T : Theory ) [T.SubformulaClosed] :
Equations
  • One or more equations did not get rendered due to their size.
theorem LO.Modal.Kripke.filteration {M : Model} {T : Theory } [T.SubformulaClosed] (FM : Model) (filterOf : FilterOf FM M T) {x : M.World} {φ : Formula } (hs : φ T) :
x φ cast x φ