class LO.ModalAlgebra (α : Type u_1) extends BooleanAlgebra α, LO.Box α, LO.Dia α : Type u_1

Algebra corresponding to Modal.K

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• sup : α → α → α
• le_sup_left (a b : α) : a ≤ sup a b
• le_sup_right (a b : α) : b ≤ sup a b
• sup_le (a b c : α) : a ≤ c → b ≤ c → sup a b ≤ c
• inf : α → α → α
• inf_le_left (a b : α) : Lattice.inf a b ≤ a
• inf_le_right (a b : α) : Lattice.inf a b ≤ b
• le_inf (a b c : α) : a ≤ b → a ≤ c → a ≤ Lattice.inf b c
• le_sup_inf (x y z : α) : (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
• compl : α → α
• sdiff : α → α → α
• himp : α → α → α
• top : α
• bot : α
• inf_compl_le_bot (x : α) : x ⊓ xᶜ ≤ ⊥
• top_le_sup_compl (x : α) : ⊤ ≤ x ⊔ xᶜ
• le_top (a : α) : a ≤ ⊤
• bot_le (a : α) : ⊥ ≤ a
• sdiff_eq (x y : α) : x \ y = x ⊓ yᶜ
• himp_eq (x y : α) : x ⇨ y = y ⊔ xᶜ
• box : α → α
• dia : α → α
• box_top : □⊤ = ⊤
• box_meet (a b : α) : □(a ⊓ b) = □a ⊓ □b
• dual_dia {a : α} : ◇a = (□aᶜ)ᶜ

theorem LO.ModalAlgebra.dual_box {α : Type u_1} [ModalAlgebra α] {a : α} : □a = (◇aᶜ)ᶜ

theorem LO.ModalAlgebra.compl_box {α : Type u_1} [ModalAlgebra α] {a : α} : (□a)ᶜ = ◇aᶜ

theorem LO.ModalAlgebra.compl_dia {α : Type u_1} [ModalAlgebra α] {a : α} : (◇a)ᶜ = □aᶜ

@[simp]

theorem LO.ModalAlgebra.dia_bot {α : Type u_1} [ModalAlgebra α] : ◇⊥ = ⊥

theorem LO.ModalAlgebra.box_imp_le_box_imp_box {α : Type u_1} [ModalAlgebra α] {a b : α} : □(a ⇨ b) ≤ □a ⇨ □b

theorem LO.ModalAlgebra.box_axiomK {α : Type u_1} [ModalAlgebra α] {a b : α} : □(a ⇨ b) ⇨ □a ⇨ □b = ⊤

theorem LO.ModalAlgebra.dia_or {α : Type u_1} [ModalAlgebra α] {a b : α} : ◇(a ⊔ b) = ◇a ⊔ ◇b

theorem LO.ModalAlgebra.dia_monotone {α : Type u_1} [ModalAlgebra α] {a b : α} (h : a ≤ b) : ◇a ≤ ◇b

theorem LO.ModalAlgebra.box_monotone {α : Type u_1} [ModalAlgebra α] {a b : α} (h : a ≤ b) : □a ≤ □b

class LO.ModalAlgebra.Transitive (α : Type u_1) extends LO.ModalAlgebra α : Type u_1

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• sup : α → α → α
• le_sup_left (a b : α) : a ≤ sup a b
• le_sup_right (a b : α) : b ≤ sup a b
• sup_le (a b c : α) : a ≤ c → b ≤ c → sup a b ≤ c
• inf : α → α → α
• inf_le_left (a b : α) : Lattice.inf a b ≤ a
• inf_le_right (a b : α) : Lattice.inf a b ≤ b
• le_inf (a b c : α) : a ≤ b → a ≤ c → a ≤ Lattice.inf b c
• le_sup_inf (x y z : α) : (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
• compl : α → α
• sdiff : α → α → α
• himp : α → α → α
• top : α
• bot : α
• inf_compl_le_bot (x : α) : x ⊓ xᶜ ≤ ⊥
• top_le_sup_compl (x : α) : ⊤ ≤ x ⊔ xᶜ
• le_top (a : α) : a ≤ ⊤
• bot_le (a : α) : ⊥ ≤ a
• sdiff_eq (x y : α) : x \ y = x ⊓ yᶜ
• himp_eq (x y : α) : x ⇨ y = y ⊔ xᶜ
• box : α → α
• dia : α → α
• box_top : □⊤ = ⊤
• box_meet (a b : α) : □(a ⊓ b) = □a ⊓ □b
• dual_dia {a : α} : ◇a = (□aᶜ)ᶜ
• box_trans {a : α} : □a ≤ □□a

class LO.ModalAlgebra.Reflexive (α : Type u_1) extends LO.ModalAlgebra α : Type u_1

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• sup : α → α → α
• le_sup_left (a b : α) : a ≤ sup a b
• le_sup_right (a b : α) : b ≤ sup a b
• sup_le (a b c : α) : a ≤ c → b ≤ c → sup a b ≤ c
• inf : α → α → α
• inf_le_left (a b : α) : Lattice.inf a b ≤ a
• inf_le_right (a b : α) : Lattice.inf a b ≤ b
• le_inf (a b c : α) : a ≤ b → a ≤ c → a ≤ Lattice.inf b c
• le_sup_inf (x y z : α) : (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
• compl : α → α
• sdiff : α → α → α
• himp : α → α → α
• top : α
• bot : α
• inf_compl_le_bot (x : α) : x ⊓ xᶜ ≤ ⊥
• top_le_sup_compl (x : α) : ⊤ ≤ x ⊔ xᶜ
• le_top (a : α) : a ≤ ⊤
• bot_le (a : α) : ⊥ ≤ a
• sdiff_eq (x y : α) : x \ y = x ⊓ yᶜ
• himp_eq (x y : α) : x ⇨ y = y ⊔ xᶜ
• box : α → α
• dia : α → α
• box_top : □⊤ = ⊤
• box_meet (a b : α) : □(a ⊓ b) = □a ⊓ □b
• dual_dia {a : α} : ◇a = (□aᶜ)ᶜ
• box_refl {a : α} : □a ≤ a