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

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

@[simp]

theorem LO.Box.box_injective {F : Type u_1} [self : LO.Box F] : 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] (p : F) : F

Equations

• ⊡p = p ⋏ □p

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) : Type

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

theorem LO.Box.Subclosed.box_closed {F : Type u_1} [LO.Box F] {C : F → Prop} [self : LO.Box.Subclosed C] {p : F} : C (□p) → C p

@[simp]

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

@[simp]

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

@[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] {p : F} {q : F} {n : ℕ} : □^[n]p = □^[n]q ↔ p = q

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

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

@[simp]

theorem LO.Dia.dia_injective {F : Type u_1} [self : LO.Dia F] : 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] (p : F) : F

Equations

• ⟐p = p ⋎ ◇p

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) : Type

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

theorem LO.Dia.Subclosed.dia_closed {F : Type u_1} [LO.Dia F] [LO.LogicalConnective F] {C : F → Prop} [self : LO.Dia.Subclosed C] {p : F} : C (◇p) → C p

@[simp]

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

@[simp]

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

@[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] {p : F} {q : F} {n : ℕ} : ◇^[n]p = ◇^[n]q ↔ p = q

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

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

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

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

theorem LO.DiaAbbrev.dia_abbrev {F : Type u_1} [LO.Box F] [LO.Dia F] [LO.Tilde F] [self : LO.DiaAbbrev F] {p : F} : ◇p = ∼□(∼p)

class LO.ModalDeMorgan (F : Type u_1) [LO.BasicModalLogicalConnective F] extends LO.DeMorgan : Type

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

@[simp]

theorem LO.ModalDeMorgan.dia {F : Type u_1} [LO.BasicModalLogicalConnective F] [self : LO.ModalDeMorgan F] (p : F) : ∼◇p = □(∼p)

@[simp]

theorem LO.ModalDeMorgan.box {F : Type u_1} [LO.BasicModalLogicalConnective F] [self : LO.ModalDeMorgan F] (p : F) : ∼□p = ◇(∼p)

@[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} [LO.Box F] {s : Set F} : □''s = □''^[1]s

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Set.eq_predia_dia_of_subset_predia {F : Type u_1} [LO.Dia F] {s : Set F} {t : Set 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} [DecidableEq F] [LO.Box F] {s : Finset F} : s.box = Finset.multibox 1 s

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Finset.premultibox_multibox_eq_of_subset_multibox {F : Type u_1} [DecidableEq F] [LO.Box F] {n : ℕ} {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} [DecidableEq F] [LO.Box F] {s : Finset F} {t : Set F} (hs : ↑s ⊆ □''t) : s.prebox.box = s

theorem Finset.premultidia_multidia_eq_of_subset_multidia {F : Type u_1} [DecidableEq F] [LO.Dia F] {n : ℕ} {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} [DecidableEq F] [LO.Dia 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))

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem List.eq_predia_premultidia_one {F : Type u_1} [DecidableEq F] [LO.Dia F] {l : List 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.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.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.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.multibox_single {F : Type u_1} [DecidableEq F] [LO.Box F] {p : F} {n : ℕ} : □'^[n][p] = [□^[n]p]

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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