Logic.Modal.LogicSymbol

source

class LO.Box (F : Type u_1) :

Type u_1

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

Instances

source

@[simp]

theorem LO.Box.box_injective {F : Type u_1} [self : LO.Box F] :

Function.Injective LO.Box.box

source

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

source

@[reducible, match_pattern, inline]

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

Equations

⊡p = p ⋏ □p

source

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

source

@[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]

source

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

Lean.ParserDescr

Equations

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

source

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

Type

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

Instances

source

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

source

@[simp]

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

□p = □q ↔ p = q

source

@[simp]

theorem LO.Box.multibox_succ {F : Type u_1} [LO.Box F] {p : F} {n : ℕ} :

□^[(n + 1)]p = □□^[n]p

source

@[simp]

theorem LO.Box.multibox_injective {F : Type u_1} [LO.Box F] {n : ℕ} :

Function.Injective fun (x : F) => □^[n]x

source

@[simp]

theorem LO.Box.multimop_injective' {F : Type u_1} [LO.Box F] {p : F} {q : F} {n : ℕ} :

□^[n]p = □^[n]q ↔ p = q

source

class LO.Dia (F : Type u_1) :

Type u_1

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

Instances

source

@[simp]

theorem LO.Dia.dia_injective {F : Type u_1} [self : LO.Dia F] :

Function.Injective LO.Dia.dia

source

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

source

@[reducible, match_pattern, inline]

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

Equations

⟐p = p ⋎ ◇p

source

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

source

@[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]

source

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

Lean.ParserDescr

Equations

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

source

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

Instances

source

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

source

@[simp]

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

◇p = ◇q ↔ p = q

source

@[simp]

theorem LO.Dia.multidia_succ {F : Type u_1} [LO.Dia F] {p : F} {n : ℕ} :

◇^[(n + 1)]p = ◇◇^[n]p

source

@[simp]

theorem LO.Dia.multidia_injective {F : Type u_1} [LO.Dia F] {n : ℕ} :

Function.Injective fun (x : F) => ◇^[n]x

source

@[simp]

theorem LO.Dia.multidia_injective' {F : Type u_1} [LO.Dia F] {p : F} {q : F} {n : ℕ} :

◇^[n]p = ◇^[n]q ↔ p = q

source

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

Type u_1

Instances

LO.Modal.Formula.instBasicModalLogicalConnective

source

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

Instances

source

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

Type

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

Instances

LO.Modal.Formula.instDiaAbbrev

source

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)

source

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)

Instances

source

@[simp]

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

∼◇p = □(∼p)

source

@[simp]

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

∼□p = ◇(∼p)

source

@[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]

source

def «term□''^[_]_» :

Lean.ParserDescr

Equations

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

source

@[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]

source

def «term◇''^[_]_» :

Lean.ParserDescr

Equations

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

source

@[reducible, inline]

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

Set F → Set F

Equations

Set.box = Set.multibox 1

source

def «term□''_» :

Lean.ParserDescr

Equations

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

source

@[reducible, inline]

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

Set F → Set F

Equations

Set.dia = Set.multidia 1

source

def «term◇''_» :

Lean.ParserDescr

Equations

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

source

@[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]

source

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

Lean.ParserDescr

Equations

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

source

@[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]

source

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

Lean.ParserDescr

Equations

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

source

@[reducible, inline]

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

Set F → Set F

Equations

Set.prebox = Set.premultibox 1

source

def «term□''⁻¹_» :

Lean.ParserDescr

Equations

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

source

@[reducible, inline]

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

Set F → Set F

Equations

Set.predia = Set.premultidia 1

source

def «term◇''⁻¹_» :

Lean.ParserDescr

Equations

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

source

@[simp]

theorem Set.eq_box_multibox_one {F : Type u_1} [LO.Box F] {s : Set F} :

□''s = □''^[1]s

source

@[simp]

theorem Set.eq_dia_multidia_one {F : Type u_1} [LO.Dia F] {s : Set F} :

◇''s = ◇''^[1]s

source

@[simp]

theorem Set.eq_prebox_premultibox_one {F : Type u_1} [LO.Box F] {s : Set F} :

□''⁻¹s = □''⁻¹^[1]s

source

@[simp]

theorem Set.eq_predia_premultidia_one {F : Type u_1} [LO.Dia F] {s : Set F} :

◇''⁻¹s = ◇''⁻¹^[1]s

source

@[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

source

@[simp]

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

□''s ⊆ □''t

source

@[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

source

@[simp]

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

◇''s ⊆ ◇''t

source

@[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

source

@[simp]

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

□''⁻¹s ⊆ □''⁻¹t

source

@[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

source

@[simp]

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

◇''⁻¹s ⊆ ◇''⁻¹t

source

@[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

source

@[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

source

@[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

source

@[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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

@[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]

source

@[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]

source

@[reducible, inline]

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

Finset F → Finset F

Equations

Finset.box = Finset.multibox 1

source

@[reducible, inline]

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

Finset F → Finset F

Equations

Finset.dia = Finset.multidia 1

source

@[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] ⋯

source

@[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] ⋯

source

@[reducible, inline]

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

Finset F → Finset F

Equations

Finset.prebox = Finset.premultibox 1

source

@[reducible, inline]

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

Finset F → Finset F

Equations

Finset.predia = Finset.premultidia 1

source

@[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

source

@[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

source

@[simp]

theorem Finset.eq_prebox_premultibox_one {F : Type u_1} [LO.Box F] {s : Finset F} :

s.prebox = Finset.premultibox 1 s

source

@[simp]

theorem Finset.eq_predia_premultidia_one {F : Type u_1} [LO.Dia F] {s : Finset F} :

s.predia = Finset.premultidia 1 s

source

theorem Finset.multibox_coe {F : Type u_1} [DecidableEq F] [LO.Box F] {s : Finset F} {n : ℕ} :

↑(Finset.multibox n s) = □''^[n]↑s

source

theorem Finset.box_coe {F : Type u_1} [DecidableEq F] [LO.Box F] {s : Finset F} :

↑s.box = □''↑s

source

theorem Finset.multidia_coe {F : Type u_1} [DecidableEq F] [LO.Dia F] {s : Finset F} {n : ℕ} :

↑(Finset.multidia n s) = ◇''^[n]↑s

source

theorem Finset.dia_coe {F : Type u_1} [DecidableEq F] [LO.Dia F] {s : Finset F} :

↑s.dia = ◇''↑s

source

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

source

theorem Finset.box_mem_coe {F : Type u_1} [DecidableEq F] [LO.Box F] {s : Finset F} {p : F} :

p ∈ s.box ↔ p ∈ □''↑s

source

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

source

theorem Finset.dia_mem_coe {F : Type u_1} [DecidableEq F] [LO.Dia F] {s : Finset F} {p : F} :

p ∈ s.dia ↔ p ∈ ◇''↑s

source

theorem Finset.premultibox_coe {F : Type u_1} [LO.Box F] {s : Finset F} {n : ℕ} :

↑(Finset.premultibox n s) = □''⁻¹^[n]↑s

source

theorem Finset.prebox_coe {F : Type u_1} [LO.Box F] {s : Finset F} :

↑s.prebox = □''⁻¹↑s

source

theorem Finset.premultidia_coe {F : Type u_1} [LO.Dia F] {s : Finset F} {n : ℕ} :

↑(Finset.premultidia n s) = ◇''⁻¹^[n]↑s

source

theorem Finset.predia_coe {F : Type u_1} [LO.Dia F] {s : Finset F} :

↑s.predia = ◇''⁻¹↑s

source

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

source

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

source

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

source

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

source

@[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

source

def «term□'^[_]_» :

Lean.ParserDescr

Equations

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

source

@[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

source

def «term◇'^[_]_» :

Lean.ParserDescr

Equations

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

source

@[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

source

def «term□'_» :

Lean.ParserDescr

Equations

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

source

@[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

source

def «term◇'_» :

Lean.ParserDescr

Equations

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

source

@[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

source

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

Lean.ParserDescr

Equations

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

source

@[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

source

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

Lean.ParserDescr

Equations

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

source

@[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

source

def «term□'⁻¹_» :

Lean.ParserDescr

Equations

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

source

@[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

source

def «term◇'⁻¹_» :

Lean.ParserDescr

Equations

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

source

@[simp]

theorem List.eq_box_multibox_one {F : Type u_1} [DecidableEq F] [LO.Box F] {l : List F} :

□'l = □'^[1]l

source

@[simp]

theorem List.eq_dia_multidia_one {F : Type u_1} [DecidableEq F] [LO.Dia F] {l : List F} :

◇'l = ◇'^[1]l

source

@[simp]

theorem List.eq_prebox_premultibox_one {F : Type u_1} [DecidableEq F] [LO.Box F] {l : List F} :

□'⁻¹l = □'⁻¹^[1]l

source

@[simp]

theorem List.eq_predia_premultidia_one {F : Type u_1} [DecidableEq F] [LO.Dia F] {l : List F} :

◇'⁻¹l = ◇'⁻¹^[1]l

source

@[simp]

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

□'^[n][] = []

source

@[simp]

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

□'[] = []

source

@[simp]

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

◇'^[n][] = []

source

@[simp]

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

◇'[] = []

source

@[simp]

theorem List.premultibox_nil {F : Type u_1} [DecidableEq F] [LO.Box F] {n : ℕ} :

□'⁻¹^[n][] = []

source

@[simp]

theorem List.prebox_nil {F : Type u_1} [DecidableEq F] [LO.Box F] :

□'⁻¹[] = []

source

@[simp]

theorem List.premultidia_nil {F : Type u_1} [DecidableEq F] [LO.Dia F] {n : ℕ} :

◇'⁻¹^[n][] = []

source

@[simp]

theorem List.predia_nil {F : Type u_1} [DecidableEq F] [LO.Dia F] :

◇'⁻¹[] = []

source

@[simp]

theorem List.multibox_single {F : Type u_1} [DecidableEq F] [LO.Box F] {p : F} {n : ℕ} :

□'^[n][p] = [□^[n]p]

source

@[simp]

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

□'[p] = [□p]

source

@[simp]

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

◇'^[n][p] = [◇^[n]p]

source

@[simp]

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

◇'[p] = [◇p]

source

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)

source

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)

source

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)

source

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)

source

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

source

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

source

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

source

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