class LO.Box (F : Type u_1) : Type u_1

• box : F → F
• box_injective : Function.Injective LO.Box.box

def LO.«term□_» : Lean.ParserDescr

Equations

• LO.«term□_» = Lean.ParserDescr.node `LO.«term□_» 76 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "□") (Lean.ParserDescr.cat `term 76))

@[reducible, match_pattern, inline]

abbrev LO.Box.boxdot {F : Type u_1} [LO.Box F] [LO.Wedge F] (φ : F) : F

Equations

• ⊡φ = φ ⋏ □φ

def LO.Box.«term⊡_» : Lean.ParserDescr

Equations

• LO.Box.«term⊡_» = Lean.ParserDescr.node `LO.Box.«term⊡_» 76 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊡") (Lean.ParserDescr.cat `term 76))

@[reducible, inline]

abbrev LO.Box.multibox {F : Type u_1} [LO.Box F] (n : ℕ) : F → F

Equations

• LO.Box.multibox n = (fun (x : F) => □x)^[n]

def LO.Box.«term□^[_]_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

class LO.Box.Subclosed {F : Type u_1} [LO.Box F] (C : F → Prop) : Prop

• box_closed : ∀ {φ : F}, C (□φ) → C φ

@[simp]

theorem LO.Box.box_injective' {F : Type u_1} [LO.Box F] {φ ψ : F} : □φ = □ψ ↔ φ = ψ

@[simp]

theorem LO.Box.multibox_succ {F : Type u_1} [LO.Box F] {φ : F} {n : ℕ} : □^[(n + 1)]φ = □□^[n]φ

@[simp]

theorem LO.Box.multibox_injective {F : Type u_1} [LO.Box F] {n : ℕ} : Function.Injective fun (x : F) => □^[n]x

@[simp]

theorem LO.Box.multimop_injective' {F : Type u_1} [LO.Box F] {φ ψ : F} {n : ℕ} : □^[n]φ = □^[n]ψ ↔ φ = ψ

class LO.Dia (F : Type u_1) : Type u_1

• dia : F → F
• dia_injective : Function.Injective LO.Dia.dia

def LO.«term◇_» : Lean.ParserDescr

Equations

• LO.«term◇_» = Lean.ParserDescr.node `LO.«term◇_» 76 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "◇") (Lean.ParserDescr.cat `term 76))

@[reducible, match_pattern, inline]

abbrev LO.Dia.diadot {F : Type u_1} [LO.Dia F] [LO.Vee F] (φ : F) : F

Equations

• ⟐φ = φ ⋎ ◇φ

def LO.Dia.«term⟐_» : Lean.ParserDescr

Equations

• LO.Dia.«term⟐_» = Lean.ParserDescr.node `LO.Dia.«term⟐_» 76 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⟐") (Lean.ParserDescr.cat `term 76))

@[reducible, inline]

abbrev LO.Dia.multidia {F : Type u_1} [LO.Dia F] (n : ℕ) : F → F

Equations

• LO.Dia.multidia n = (fun (x : F) => ◇x)^[n]

def LO.Dia.«term◇^[_]_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

class LO.Dia.Subclosed {F : Type u_1} [LO.Dia F] [LO.LogicalConnective F] (C : F → Prop) : Prop

• dia_closed : ∀ {φ : F}, C (◇φ) → C φ

@[simp]

theorem LO.Dia.dia_injective' {F : Type u_1} [LO.Dia F] {φ ψ : F} : ◇φ = ◇ψ ↔ φ = ψ

@[simp]

theorem LO.Dia.multidia_succ {F : Type u_1} [LO.Dia F] {φ : F} {n : ℕ} : ◇^[(n + 1)]φ = ◇◇^[n]φ

@[simp]

theorem LO.Dia.multidia_injective {F : Type u_1} [LO.Dia F] {n : ℕ} : Function.Injective fun (x : F) => ◇^[n]x

@[simp]

theorem LO.Dia.multidia_injective' {F : Type u_1} [LO.Dia F] {φ ψ : F} {n : ℕ} : ◇^[n]φ = ◇^[n]ψ ↔ φ = ψ

class LO.BasicModalLogicalConnective (F : Type u_1) extends LO.LogicalConnective F, LO.Box F, LO.Dia F : Type u_1

• top : F
• bot : F
• tilde : F → F
• arrow : F → F → F
• wedge : F → F → F
• vee : F → F → F
• box : F → F
• box_injective : Function.Injective LO.Box.box
• dia : F → F
• dia_injective : Function.Injective LO.Dia.dia

class LO.BasicModalLogicConnective.Subclosed {F : Type u_1} [LO.BasicModalLogicalConnective F] (C : F → Prop) extends LO.LogicalConnective.Subclosed C, LO.Box.Subclosed C, LO.Dia.Subclosed C : Prop

• tilde_closed : ∀ {φ : F}, C (∼φ) → C φ
• arrow_closed : ∀ {φ ψ : F}, C (φ ➝ ψ) → C φ ∧ C ψ
• wedge_closed : ∀ {φ ψ : F}, C (φ ⋏ ψ) → C φ ∧ C ψ
• vee_closed : ∀ {φ ψ : F}, C (φ ⋎ ψ) → C φ ∧ C ψ
• box_closed : ∀ {φ : F}, C (□φ) → C φ
• dia_closed : ∀ {φ : F}, C (◇φ) → C φ

class LO.DiaAbbrev (F : Type u_1) [LO.Box F] [LO.Dia F] [LO.Tilde F] : Prop

• dia_abbrev : ∀ {φ : F}, ◇φ = ∼□(∼φ)

class LO.ModalDeMorgan (F : Type u_1) [LO.LogicalConnective F] [LO.Box F] [LO.Dia F] extends LO.DeMorgan F : Prop

• verum : ∼⊤ = ⊥
• falsum : ∼⊥ = ⊤
• imply : ∀ (φ ψ : F), φ ➝ ψ = ∼φ ⋎ ψ
• and : ∀ (φ ψ : F), ∼(φ ⋏ ψ) = ∼φ ⋎ ∼ψ
• or : ∀ (φ ψ : F), ∼(φ ⋎ ψ) = ∼φ ⋏ ∼ψ
• neg : ∀ (φ : F), ∼∼φ = φ
• dia : ∀ (φ : F), ∼◇φ = □(∼φ)
• box : ∀ (φ : F), ∼□φ = ◇(∼φ)

@[reducible, inline]

abbrev Set.multibox {F : Type u_1} [LO.Box F] (n : ℕ) : Set F → Set F

Equations

• Set.multibox n = Set.image (fun (x : F) => □x)^[n]

def «term□''^[_]_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Set.multidia {F : Type u_1} [LO.Dia F] (n : ℕ) : Set F → Set F

Equations

• Set.multidia n = Set.image (fun (x : F) => ◇x)^[n]

def «term◇''^[_]_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Set.box {F : Type u_1} [LO.Box F] : Set F → Set F

Equations

• Set.box = Set.multibox 1

def «term□''_» : Lean.ParserDescr

Equations

• «term□''_» = Lean.ParserDescr.node `«term□''_» 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "□''") (Lean.ParserDescr.cat `term 80))

@[reducible, inline]

abbrev Set.dia {F : Type u_1} [LO.Dia F] : Set F → Set F

Equations

• Set.dia = Set.multidia 1

def «term◇''_» : Lean.ParserDescr

Equations

• «term◇''_» = Lean.ParserDescr.node `«term◇''_» 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "◇''") (Lean.ParserDescr.cat `term 80))

@[reducible, inline]

abbrev Set.premultibox {F : Type u_1} [LO.Box F] (n : ℕ) : Set F → Set F

Equations

• Set.premultibox n = Set.preimage (fun (x : F) => □x)^[n]

def «term□''⁻¹^[_]_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Set.premultidia {F : Type u_1} [LO.Dia F] (n : ℕ) : Set F → Set F

Equations

• Set.premultidia n = Set.preimage (fun (x : F) => ◇x)^[n]

def «term◇''⁻¹^[_]_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Set.prebox {F : Type u_1} [LO.Box F] : Set F → Set F

Equations

• Set.prebox = Set.premultibox 1

def «term□''⁻¹_» : Lean.ParserDescr

Equations

• «term□''⁻¹_» = Lean.ParserDescr.node `«term□''⁻¹_» 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "□''⁻¹") (Lean.ParserDescr.cat `term 80))

@[reducible, inline]

abbrev Set.predia {F : Type u_1} [LO.Dia F] : Set F → Set F

Equations

• Set.predia = Set.premultidia 1

def «term◇''⁻¹_» : Lean.ParserDescr

Equations

• «term◇''⁻¹_» = Lean.ParserDescr.node `«term◇''⁻¹_» 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "◇''⁻¹") (Lean.ParserDescr.cat `term 80))

@[simp]

theorem Set.eq_box_multibox_one {F : Type u_1} {s : Set F} [LO.Box F] : □''s = □''^[1]s

@[simp]

theorem Set.eq_prebox_premultibox_one {F : Type u_1} {s : Set F} [LO.Box F] : □''⁻¹s = □''⁻¹^[1]s

@[simp]

theorem Set.multibox_subset_mono {F : Type u_1} {s t : Set F} [LO.Box F] {n : ℕ} (h : s ⊆ t) : □''^[n]s ⊆ □''^[n]t

@[simp]

theorem Set.box_subset_mono {F : Type u_1} {s t : Set F} [LO.Box F] (h : s ⊆ t) : □''s ⊆ □''t

@[simp]

theorem Set.premultibox_subset_mono {F : Type u_1} {s t : Set F} [LO.Box F] {n : ℕ} (h : s ⊆ t) : □''⁻¹^[n]s ⊆ □''⁻¹^[n]t

@[simp]

theorem Set.prebox_subset_mono {F : Type u_1} {s t : Set F} [LO.Box F] (h : s ⊆ t) : □''⁻¹s ⊆ □''⁻¹t

@[simp]

theorem Set.iff_mem_premultibox {F : Type u_1} {s : Set F} [LO.Box F] {n : ℕ} {φ : F} : φ ∈ □''⁻¹^[n]s ↔ □^[n]φ ∈ s

@[simp]

theorem Set.iff_mem_multibox {F : Type u_1} {s : Set F} [LO.Box F] {n : ℕ} {φ : F} : □^[n]φ ∈ □''^[n]s ↔ φ ∈ s

theorem Set.subset_premulitibox_iff_multibox_subset {F : Type u_1} {s t : Set F} [LO.Box F] {n : ℕ} (h : s ⊆ □''⁻¹^[n]t) : □''^[n]s ⊆ t

theorem Set.subset_prebox_iff_box_subset {F : Type u_1} {s t : Set F} [LO.Box F] (h : s ⊆ □''⁻¹t) : □''s ⊆ t

theorem Set.subset_multibox_iff_premulitibox_subset {F : Type u_1} {s t : Set F} [LO.Box F] {n : ℕ} (h : s ⊆ □''^[n]t) : □''⁻¹^[n]s ⊆ t

theorem Set.subset_box_iff_prebox_subset {F : Type u_1} {s t : Set F} [LO.Box F] (h : s ⊆ □''t) : □''⁻¹s ⊆ t

theorem Set.forall_multibox_of_subset_multibox {F : Type u_1} {s t : Set F} [LO.Box F] {n : ℕ} (h : s ⊆ □''^[n]t) (φ : F) : φ ∈ s → ∃ ψ ∈ t, φ = □^[n]ψ

theorem Set.forall_box_of_subset_box {F : Type u_1} {s t : Set F} [LO.Box F] (h : s ⊆ □''t) (φ : F) : φ ∈ s → ∃ ψ ∈ t, φ = □ψ

theorem Set.eq_premultibox_multibox_of_subset_premultibox {F : Type u_1} {s t : Set F} [LO.Box F] {n : ℕ} (h : s ⊆ □''^[n]t) : □''^[n]□''⁻¹^[n]s = s

theorem Set.eq_prebox_box_of_subset_prebox {F : Type u_1} {s t : Set F} [LO.Box F] (h : s ⊆ □''t) : □''□''⁻¹s = s

@[simp]

theorem Set.eq_dia_multidia_one {F : Type u_1} {s : Set F} [LO.Dia F] : ◇''s = ◇''^[1]s

@[simp]

theorem Set.eq_predia_premultidia_one {F : Type u_1} {s : Set F} [LO.Dia F] : ◇''⁻¹s = ◇''⁻¹^[1]s

@[simp]

theorem Set.multidia_subset_mono {F : Type u_1} {s t : Set F} [LO.Dia F] {n : ℕ} (h : s ⊆ t) : ◇''^[n]s ⊆ ◇''^[n]t

@[simp]

theorem Set.dia_subset_mono {F : Type u_1} {s t : Set F} [LO.Dia F] (h : s ⊆ t) : ◇''s ⊆ ◇''t

@[simp]

theorem Set.premultidia_subset_mono {F : Type u_1} {s t : Set F} [LO.Dia F] {n : ℕ} (h : s ⊆ t) : ◇''⁻¹^[n]s ⊆ ◇''⁻¹^[n]t

@[simp]

theorem Set.predia_subset_mono {F : Type u_1} {s t : Set F} [LO.Dia F] (h : s ⊆ t) : ◇''⁻¹s ⊆ ◇''⁻¹t

@[simp]

theorem Set.iff_mem_premultidia {F : Type u_1} {s : Set F} [LO.Dia F] {n : ℕ} {φ : F} : φ ∈ ◇''⁻¹^[n]s ↔ ◇^[n]φ ∈ s

@[simp]

theorem Set.iff_mem_multidia {F : Type u_1} {s : Set F} [LO.Dia F] {n : ℕ} {φ : F} : ◇^[n]φ ∈ ◇''^[n]s ↔ φ ∈ s

theorem Set.subset_premultidia_iff_multidia_subset {F : Type u_1} {s t : Set F} [LO.Dia F] {n : ℕ} (h : s ⊆ ◇''⁻¹^[n]t) : ◇''^[n]s ⊆ t

theorem Set.subset_predia_iff_dia_subset {F : Type u_1} {s t : Set F} [LO.Dia F] (h : s ⊆ ◇''⁻¹t) : ◇''s ⊆ t

theorem Set.subset_multidia_iff_premultidia_subset {F : Type u_1} {s t : Set F} [LO.Dia F] {n : ℕ} (h : s ⊆ ◇''^[n]t) : ◇''⁻¹^[n]s ⊆ t

theorem Set.subset_dia_iff_predia_subset {F : Type u_1} {s t : Set F} [LO.Dia F] (h : s ⊆ ◇''t) : ◇''⁻¹s ⊆ t

theorem Set.forall_multidia_of_subset_multidia {F : Type u_1} {s t : Set F} [LO.Dia F] {n : ℕ} (h : s ⊆ ◇''^[n]t) (φ : F) : φ ∈ s → ∃ ψ ∈ t, φ = ◇^[n]ψ

theorem Set.forall_dia_of_subset_dia {F : Type u_1} {s t : Set F} [LO.Dia F] (h : s ⊆ ◇''t) (φ : F) : φ ∈ s → ∃ ψ ∈ t, φ = ◇ψ

theorem Set.eq_premultidia_multidia_of_subset_premultidia {F : Type u_1} {s t : Set F} [LO.Dia F] {n : ℕ} (h : s ⊆ ◇''^[n]t) : ◇''^[n]◇''⁻¹^[n]s = s

theorem Set.eq_predia_dia_of_subset_predia {F : Type u_1} {s t : Set F} [LO.Dia F] (h : s ⊆ ◇''t) : ◇''◇''⁻¹s = s

@[reducible, inline]

abbrev Finset.multibox {F : Type u_1} [DecidableEq F] [LO.Box F] (n : ℕ) : Finset F → Finset F

Equations

• Finset.multibox n = Finset.image (fun (x : F) => □x)^[n]

@[reducible, inline]

abbrev Finset.multidia {F : Type u_1} [DecidableEq F] [LO.Dia F] (n : ℕ) : Finset F → Finset F

Equations

• Finset.multidia n = Finset.image (fun (x : F) => ◇x)^[n]

@[reducible, inline]

abbrev Finset.box {F : Type u_1} [DecidableEq F] [LO.Box F] : Finset F → Finset F

Equations

• Finset.box = Finset.multibox 1

@[reducible, inline]

abbrev Finset.dia {F : Type u_1} [DecidableEq F] [LO.Dia F] : Finset F → Finset F

Equations

• Finset.dia = Finset.multidia 1

@[reducible, inline]

noncomputable abbrev Finset.premultibox {F : Type u_1} [LO.Box F] (n : ℕ) : Finset F → Finset F

Equations

• Finset.premultibox n s = s.preimage (fun (x : F) => □x)^[n] ⋯

@[reducible, inline]

noncomputable abbrev Finset.premultidia {F : Type u_1} [LO.Dia F] (n : ℕ) : Finset F → Finset F

Equations

• Finset.premultidia n s = s.preimage (fun (x : F) => ◇x)^[n] ⋯

@[reducible, inline]

noncomputable abbrev Finset.prebox {F : Type u_1} [LO.Box F] : Finset F → Finset F

Equations

• Finset.prebox = Finset.premultibox 1

@[reducible, inline]

noncomputable abbrev Finset.predia {F : Type u_1} [LO.Dia F] : Finset F → Finset F

Equations

• Finset.predia = Finset.premultidia 1

@[simp]

theorem Finset.eq_box_multibox_one {F : Type u_1} {s : Finset F} [LO.Box F] [DecidableEq F] : s.box = Finset.multibox 1 s

@[simp]

theorem Finset.eq_prebox_premultibox_one {F : Type u_1} {s : Finset F} [LO.Box F] : s.prebox = Finset.premultibox 1 s

theorem Finset.multibox_coe {F : Type u_1} {s : Finset F} {n : ℕ} [LO.Box F] [DecidableEq F] : ↑(Finset.multibox n s) = □''^[n]↑s

theorem Finset.box_coe {F : Type u_1} {s : Finset F} [LO.Box F] [DecidableEq F] : ↑s.box = □''↑s

theorem Finset.multibox_mem_coe {F : Type u_1} {s : Finset F} {n : ℕ} [LO.Box F] {φ : F} [DecidableEq F] : φ ∈ Finset.multibox n s ↔ φ ∈ □''^[n]↑s

theorem Finset.box_mem_coe {F : Type u_1} {s : Finset F} [LO.Box F] {φ : F} [DecidableEq F] : φ ∈ s.box ↔ φ ∈ □''↑s

theorem Finset.premultibox_coe {F : Type u_1} {s : Finset F} {n : ℕ} [LO.Box F] : ↑(Finset.premultibox n s) = □''⁻¹^[n]↑s

theorem Finset.prebox_coe {F : Type u_1} {s : Finset F} [LO.Box F] : ↑s.prebox = □''⁻¹↑s

theorem Finset.premultibox_multibox_eq_of_subset_multibox {F : Type u_1} {n : ℕ} [LO.Box F] [DecidableEq F] {s : Finset F} {t : Set F} (hs : ↑s ⊆ □''^[n]t) : Finset.multibox n (Finset.premultibox n s) = s

theorem Finset.prebox_box_eq_of_subset_box {F : Type u_1} [LO.Box F] [DecidableEq F] {s : Finset F} {t : Set F} (hs : ↑s ⊆ □''t) : s.prebox.box = s

@[simp]

theorem Finset.eq_dia_multidia_one {F : Type u_1} {s : Finset F} [LO.Dia F] [DecidableEq F] : s.dia = Finset.multidia 1 s

@[simp]

theorem Finset.eq_predia_premultidia_one {F : Type u_1} {s : Finset F} [LO.Dia F] : s.predia = Finset.premultidia 1 s

theorem Finset.multidia_coe {F : Type u_1} {s : Finset F} {n : ℕ} [LO.Dia F] [DecidableEq F] : ↑(Finset.multidia n s) = ◇''^[n]↑s

theorem Finset.dia_coe {F : Type u_1} {s : Finset F} [LO.Dia F] [DecidableEq F] : ↑s.dia = ◇''↑s

theorem Finset.multidia_mem_coe {F : Type u_1} {s : Finset F} {n : ℕ} [LO.Dia F] {φ : F} [DecidableEq F] : φ ∈ Finset.multidia n s ↔ φ ∈ ◇''^[n]↑s

theorem Finset.dia_mem_coe {F : Type u_1} {s : Finset F} [LO.Dia F] {φ : F} [DecidableEq F] : φ ∈ s.dia ↔ φ ∈ ◇''↑s

theorem Finset.premultidia_coe {F : Type u_1} {s : Finset F} {n : ℕ} [LO.Dia F] : ↑(Finset.premultidia n s) = ◇''⁻¹^[n]↑s

theorem Finset.predia_coe {F : Type u_1} {s : Finset F} [LO.Dia F] : ↑s.predia = ◇''⁻¹↑s

theorem Finset.premultidia_multidia_eq_of_subset_multidia {F : Type u_1} {n : ℕ} [LO.Dia F] [DecidableEq F] {s : Finset F} {t : Set F} (hs : ↑s ⊆ ◇''^[n]t) : Finset.multidia n (Finset.premultidia n s) = s

theorem Finset.predia_dia_eq_of_subset_dia {F : Type u_1} [LO.Dia F] [DecidableEq F] {s : Finset F} {t : Set F} (hs : ↑s ⊆ ◇''t) : s.predia.dia = s

@[reducible, inline]

noncomputable abbrev List.multibox {F : Type u_1} [DecidableEq F] [LO.Box F] (n : ℕ) : List F → List F

Equations

• □'^[n]l = (Finset.multibox n l.toFinset).toList

def «term□'^[_]_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev List.multidia {F : Type u_1} [DecidableEq F] [LO.Dia F] (n : ℕ) : List F → List F

Equations

• ◇'^[n]l = (Finset.multidia n l.toFinset).toList

def «term◇'^[_]_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev List.box {F : Type u_1} [DecidableEq F] [LO.Box F] : List F → List F

Equations

• List.box = List.multibox 1

def «term□'_» : Lean.ParserDescr

Equations

• «term□'_» = Lean.ParserDescr.node `«term□'_» 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "□'") (Lean.ParserDescr.cat `term 80))

@[reducible, inline]

noncomputable abbrev List.dia {F : Type u_1} [DecidableEq F] [LO.Dia F] : List F → List F

Equations

• List.dia = List.multidia 1

def «term◇'_» : Lean.ParserDescr

Equations

• «term◇'_» = Lean.ParserDescr.node `«term◇'_» 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "◇'") (Lean.ParserDescr.cat `term 80))

@[reducible, inline]

noncomputable abbrev List.premultibox {F : Type u_1} [DecidableEq F] [LO.Box F] (n : ℕ) : List F → List F

Equations

• □'⁻¹^[n]l = (Finset.premultibox n l.toFinset).toList

def «term□'⁻¹^[_]_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev List.premultidia {F : Type u_1} [DecidableEq F] [LO.Dia F] (n : ℕ) : List F → List F

Equations

• ◇'⁻¹^[n]l = (Finset.premultidia n l.toFinset).toList

def «term◇'⁻¹^[_]_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev List.prebox {F : Type u_1} [DecidableEq F] [LO.Box F] : List F → List F

Equations

• List.prebox = List.premultibox 1

def «term□'⁻¹_» : Lean.ParserDescr

Equations

• «term□'⁻¹_» = Lean.ParserDescr.node `«term□'⁻¹_» 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "□'⁻¹") (Lean.ParserDescr.cat `term 80))

@[reducible, inline]

noncomputable abbrev List.predia {F : Type u_1} [DecidableEq F] [LO.Dia F] : List F → List F

Equations

• List.predia = List.premultidia 1

def «term◇'⁻¹_» : Lean.ParserDescr

Equations

• «term◇'⁻¹_» = Lean.ParserDescr.node `«term◇'⁻¹_» 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "◇'⁻¹") (Lean.ParserDescr.cat `term 80))

theorem List.forall_multibox_of_subset_multibox {F : Type u_1} {l : List F} {s : Set F} {n : ℕ} [LO.Box F] (h : ∀ φ ∈ l, φ ∈ □''^[n]s) (φ : F) : φ ∈ l → ∃ ψ ∈ s, φ = □^[n]ψ

theorem List.forall_box_of_subset_box {F : Type u_1} {l : List F} {s : Set F} [LO.Box F] (h : ∀ φ ∈ l, φ ∈ □''s) (φ : F) : φ ∈ l → ∃ ψ ∈ s, φ = □ψ

theorem List.forall_multidia_of_subset_multidia {F : Type u_1} {l : List F} {s : Set F} {n : ℕ} [LO.Dia F] (h : ∀ φ ∈ l, φ ∈ ◇''^[n]s) (φ : F) : φ ∈ l → ∃ ψ ∈ s, φ = ◇^[n]ψ

theorem List.forall_dia_of_subset_dia {F : Type u_1} {l : List F} {s : Set F} [LO.Dia F] (h : ∀ φ ∈ l, φ ∈ ◇''s) (φ : F) : φ ∈ l → ∃ ψ ∈ s, φ = ◇ψ

@[simp]

theorem List.eq_box_multibox_one {F : Type u_1} {l : List F} [DecidableEq F] [LO.Box F] : □'l = □'^[1]l

@[simp]

theorem List.eq_prebox_premultibox_one {F : Type u_1} {l : List F} [DecidableEq F] [LO.Box F] : □'⁻¹l = □'⁻¹^[1]l

@[simp]

theorem List.multibox_nil {F : Type u_1} [DecidableEq F] [LO.Box F] {n : ℕ} : □'^[n][] = []

@[simp]

theorem List.box_nil {F : Type u_1} [DecidableEq F] [LO.Box F] : □'[] = []

@[simp]

theorem List.premultibox_nil {F : Type u_1} [DecidableEq F] [LO.Box F] {n : ℕ} : □'⁻¹^[n][] = []

@[simp]

theorem List.prebox_nil {F : Type u_1} [DecidableEq F] [LO.Box F] : □'⁻¹[] = []

@[simp]

theorem List.multibox_single {F : Type u_1} {φ : F} [DecidableEq F] [LO.Box F] {n : ℕ} : □'^[n][φ] = [□^[n]φ]

@[simp]

theorem List.box_single {F : Type u_1} {φ : F} [DecidableEq F] [LO.Box F] : □'[φ] = [□φ]

theorem List.multibox_cons {F : Type u_1} {l : List F} {φ : F} [DecidableEq F] [LO.Box F] {n : ℕ} (hl : φ ∉ l) : (□'^[n](φ :: l)).Perm (□^[n]φ :: □'^[n]l)

theorem List.box_cons {F : Type u_1} {l : List F} {φ : F} [DecidableEq F] [LO.Box F] (hl : φ ∉ l) : (□'(φ :: l)).Perm (□φ :: □'l)

@[simp]

theorem List.eq_dia_multidia_one {F : Type u_1} {l : List F} [DecidableEq F] [LO.Dia F] : ◇'l = ◇'^[1]l

@[simp]

theorem List.eq_predia_premultidia_one {F : Type u_1} {l : List F} [DecidableEq F] [LO.Dia F] : ◇'⁻¹l = ◇'⁻¹^[1]l

@[simp]

theorem List.multidia_nil {F : Type u_1} [DecidableEq F] [LO.Dia F] {n : ℕ} : ◇'^[n][] = []

@[simp]

theorem List.dia_nil {F : Type u_1} [DecidableEq F] [LO.Dia F] : ◇'[] = []

@[simp]

theorem List.premultidia_nil {F : Type u_1} [DecidableEq F] [LO.Dia F] {n : ℕ} : ◇'⁻¹^[n][] = []

@[simp]

theorem List.predia_nil {F : Type u_1} [DecidableEq F] [LO.Dia F] : ◇'⁻¹[] = []

@[simp]

theorem List.multidia_single {F : Type u_1} {φ : F} [DecidableEq F] [LO.Dia F] {n : ℕ} : ◇'^[n][φ] = [◇^[n]φ]

@[simp]

theorem List.dia_single {F : Type u_1} {φ : F} [DecidableEq F] [LO.Dia F] : ◇'[φ] = [◇φ]

theorem List.multidia_cons {F : Type u_1} {l : List F} {φ : F} [DecidableEq F] [LO.Dia F] {n : ℕ} (hl : φ ∉ l) : (◇'^[n](φ :: l)).Perm (◇^[n]φ :: ◇'^[n]l)

theorem List.dia_cons {F : Type u_1} {l : List F} {φ : F} [DecidableEq F] [LO.Dia F] (hl : φ ∉ l) : (◇'(φ :: l)).Perm (◇φ :: ◇'l)