Foundation.Modal.LogicSymbol

source

class LO.Box (F : Type u_1) :

Type u_1

box : F → F
box_injective : Function.Injective box

Instances

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} [Box F] [Wedge F] (φ : F) :

Equations

⊡φ = φ ⋏ □φ

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} [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} [Box F] (C : F → Prop) :

Prop

box_closed {φ : F} : C (□φ) → C φ

Instances

source

@[simp]

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

□φ = □ψ ↔ φ = ψ

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

□^[n]φ = □^[n]ψ ↔ φ = ψ

source

class LO.Dia (F : Type u_1) :

Type u_1

dia : F → F
dia_injective : Function.Injective dia

Instances

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} [Dia F] [Vee F] (φ : F) :

Equations

⟐φ = φ ⋎ ◇φ

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} [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} [Dia F] [LogicalConnective F] (C : F → Prop) :

Prop

dia_closed {φ : F} : C (◇φ) → C φ

Instances

source

@[simp]

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

◇φ = ◇ψ ↔ φ = ψ

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

◇^[n]φ = ◇^[n]ψ ↔ φ = ψ

source

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 box
dia : F → F
dia_injective : Function.Injective dia

Instances

source

class LO.BasicModalLogicConnective.Subclosed {F : Type u_1} [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 φ

Instances

source

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

Prop

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

Instances

LO.Modal.Formula.instDiaAbbrev

source

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

Prop

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

Instances

LO.Modal.NNFormula.instModalDeMorgan

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} {s : Set F} [LO.Box F] :

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

source

@[simp]

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

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

source

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

source

@[simp]

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

□''s ⊆ □''t

source

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

source

@[simp]

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

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

source

@[simp]

theorem Set.iff_mem_premultibox {F : Type u_1} {s : Set F} [LO.Box F] {n : ℕ} {φ : F} :

φ ∈ □''⁻¹^[n]s ↔ □^[n]φ ∈ s

source

@[simp]

theorem Set.iff_mem_multibox {F : Type u_1} {s : Set F} [LO.Box F] {n : ℕ} {φ : F} :

□^[n]φ ∈ □''^[n]s ↔ φ ∈ s

source

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

source

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

□''s ⊆ t

source

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

source

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

□''⁻¹s ⊆ t

source

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]ψ

source

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

φ ∈ s → ∃ ψ ∈ t, φ = □ψ

source

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

source

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

□''□''⁻¹s = s

source

@[simp]

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

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

source

@[simp]

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

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

source

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

source

@[simp]

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

◇''s ⊆ ◇''t

source

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

source

@[simp]

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

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

source

@[simp]

theorem Set.iff_mem_premultidia {F : Type u_1} {s : Set F} [LO.Dia F] {n : ℕ} {φ : F} :

φ ∈ ◇''⁻¹^[n]s ↔ ◇^[n]φ ∈ s

source

@[simp]

theorem Set.iff_mem_multidia {F : Type u_1} {s : Set F} [LO.Dia F] {n : ℕ} {φ : F} :

◇^[n]φ ∈ ◇''^[n]s ↔ φ ∈ s

source

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

source

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

◇''s ⊆ t

source

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

source

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

◇''⁻¹s ⊆ t

source

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]ψ

source

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

φ ∈ s → ∃ ψ ∈ t, φ = ◇ψ

source

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

source

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

s.box = Finset.multibox 1 s

source

@[simp]

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

s.prebox = Finset.premultibox 1 s

source

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

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

source

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

↑s.box = □''↑s

source

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

source

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

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

source

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

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

source

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

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

source

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

source

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

source

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

source

@[simp]

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

s.predia = Finset.premultidia 1 s

source

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

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

source

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

↑s.dia = ◇''↑s

source

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

source

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

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

source

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

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

source

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

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

source

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

source

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

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

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]ψ

source

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, φ = □ψ

source

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]ψ

source

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, φ = ◇ψ

source

@[simp]

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

□'l = □'^[1]l

source

@[simp]

theorem List.eq_prebox_premultibox_one {F : Type u_1} {l : List F} [DecidableEq F] [LO.Box 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.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.multibox_single {F : Type u_1} {φ : F} [DecidableEq F] [LO.Box F] {n : ℕ} :

□'^[n][φ] = [□^[n]φ]

source

@[simp]

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

□'[φ] = [□φ]

source

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)

source

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

(□'(φ :: l)).Perm (□φ :: □'l)

source

@[simp]

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

◇'l = ◇'^[1]l

source

@[simp]

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

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

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.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.multidia_single {F : Type u_1} {φ : F} [DecidableEq F] [LO.Dia F] {n : ℕ} :

◇'^[n][φ] = [◇^[n]φ]

source

@[simp]

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

◇'[φ] = [◇φ]

source

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)

source

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

(◇'(φ :: l)).Perm (◇φ :: ◇'l)