Logic Symbols

This file defines structure that has logical connectives $\top, \bot, \land, \lor, \to, \lnot$ and their homomorphisms.

Main Definitions

• FFL.LogicalConnective is defined so that FFL.LogicalConnective F is a type that has logical connectives $\top, \bot, \land, \lor, \to, \lnot$.
• FFL.LogicalConnective.Hom is defined so that f : F →ˡᶜ G is a homomorphism from F to G, i.e., a function that preserves logical connectives.

class FFL.LogicalConnective (α : Type u_1) extends FFL.Tilde α, FFL.Arrow α, FFL.Wedge α, FFL.Vee α : Type u_1

A class for types with logical connectives $\top, \bot, \land, \lor, \to, \lnot$.

• tilde : α → α
• arrow : α → α → α
• wedge : α → α → α
• vee : α → α → α

class FFL.LogicalNeutral (α : Type u_1) extends Top α, Bot α : Type u_1

• top : α
• bot : α

class FFL.TildeInvolutive (F : Type u_1) [Tilde F] : Prop

• tilde_involutive (φ : F) : ∼∼φ = φ

class FFL.LogicalConnective.DeMorgan (F : Type u_1) [LogicalConnective F] : Prop

• imply (φ ψ : F) : φ 🡒 ψ = ∼φ ⋎ ψ
• and (φ ψ : F) : ∼(φ ⋏ ψ) = ∼φ ⋎ ∼ψ
• or (φ ψ : F) : ∼(φ ⋎ ψ) = ∼φ ⋏ ∼ψ

class FFL.LogicalNeutral.DeMorgan (F : Type u_1) [LogicalNeutral F] [Tilde F] : Prop

• verum : ∼⊤ = ⊥
• falsum : ∼⊥ = ⊤

theorem FFL.LogicalNeutral.DeMorgan.neg {F : Type u_1} {inst✝ : Tilde F} [self : TildeInvolutive F] (φ : F) : ∼∼φ = φ

Alias of FFL.TildeInvolutive.tilde_involutive.

class FFL.NegAbbrev (F : Type u_1) [Tilde F] [Arrow F] [Bot F] : Prop

Introducing ∼φ as an abbreviation of φ 🡒 ⊥.

• neg {φ : F} : ∼φ = φ 🡒 ⊥

class FFL.ŁukasiewiczAbbrev (F : Type u_1) [LogicalNeutral F] [LogicalConnective F] extends FFL.NegAbbrev F : Prop

Introducing ∼φ, φ ⋎ ψ, φ ⋏ ψ, ⊤ as abbreviation.

• neg {φ : F} : ∼φ = φ 🡒 ⊥
• top : ⊤ = ∼⊥
• or {φ ψ : F} : φ ⋎ ψ = ∼φ 🡒 ψ
• and {φ ψ : F} : φ ⋏ ψ = ∼(φ 🡒 ∼ψ)

@[simp]

theorem FFL.TildeInvolutive.tilde_injective {α : Type u_1} [Tilde α] [TildeInvolutive α] : Function.Injective fun (x : α) => ∼x

@[simp]

theorem FFL.TildeInvolutive.tilde_eq_tilde_iff_eq {α : Type u_1} [Tilde α] [TildeInvolutive α] {φ ψ : α} : ∼φ = ∼ψ ↔ φ = ψ

def FFL.Tilde.invol {α : Type u_1} [Tilde α] [TildeInvolutive α] : α ↪ α

Equations

• FFL.Tilde.invol = { toFun := fun (x : α) => ∼x, inj' := ⋯ }

@[simp]

theorem FFL.Tilde.invol_app {α : Type u_1} [Tilde α] [TildeInvolutive α] (φ : α) : invol φ = ∼φ

@[match_pattern]

def FFL.LogicalConnective.iff {α : Type u_1} [LogicalConnective α] (a b : α) : α

Equations

• a 🡘 b = (a 🡒 b) ⋏ (b 🡒 a)

def FFL.LogicalConnective.«term_🡘_» : Lean.TrailingParserDescr

A defined logical connective for "iff", defined from the logical connectives 🡒 and ⋏.

Equations

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

@[reducible]

instance FFL.LogicalConnective.PropLogicSymbols : LogicalConnective Prop

Equations

• FFL.LogicalConnective.PropLogicSymbols = { tilde := Not, arrow := fun (P Q : Prop) => P → Q, wedge := And, vee := Or }

@[instance_reducible]

instance FFL.LogicalConnective.PropLogicalNeutral : LogicalNeutral Prop

Equations

• FFL.LogicalConnective.PropLogicalNeutral = { top := True, bot := False }

@[simp]

theorem FFL.LogicalConnective.Prop.top_eq : ⊤ = True

@[simp]

theorem FFL.LogicalConnective.Prop.bot_eq : ⊥ = False

@[simp]

theorem FFL.LogicalConnective.Prop.neg_eq (φ : Prop) : ∼φ = ¬φ

@[simp]

theorem FFL.LogicalConnective.Prop.arrow_eq (φ ψ : Prop) : φ 🡒 ψ = (φ → ψ)

@[simp]

theorem FFL.LogicalConnective.Prop.and_eq (φ ψ : Prop) : φ ⋏ ψ = (φ ∧ ψ)

@[simp]

theorem FFL.LogicalConnective.Prop.or_eq (φ ψ : Prop) : φ ⋎ ψ = (φ ∨ ψ)

@[simp]

theorem FFL.LogicalConnective.Prop.iff_eq (φ ψ : Prop) : φ 🡘 ψ = (φ ↔ ψ)

instance FFL.LogicalConnective.instTildeInvolutiveProp : TildeInvolutive Prop

instance FFL.LogicalConnective.instDeMorganProp : DeMorgan Prop

instance FFL.LogicalConnective.instDeMorganProp_1 : LogicalNeutral.DeMorgan Prop

class FFL.LogicalConnective.HomClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [LogicalConnective α] [LogicalNeutral α] [LogicalConnective β] [LogicalNeutral β] [FunLike F α β] : Prop

A class for a type F which contains homomorphisms (for logical connectives) from α to β.

• map_top (f : F) : f ⊤ = ⊤
• map_bot (f : F) : f ⊥ = ⊥
• map_neg (f : F) (φ : α) : f (∼φ) = ∼f φ
• map_imply (f : F) (φ ψ : α) : f (φ 🡒 ψ) = f φ 🡒 f ψ
• map_and (f : F) (φ ψ : α) : f (φ ⋏ ψ) = f φ ⋏ f ψ
• map_or (f : F) (φ ψ : α) : f (φ ⋎ ψ) = f φ ⋎ f ψ

@[instance_reducible]

instance FFL.LogicalConnective.HomClass.instCoeFunForall (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [FunLike F α β] : CoeFun F fun (x : F) => α → β

Equations

• FFL.LogicalConnective.HomClass.instCoeFunForall F α β = { coe := DFunLike.coe }

@[simp]

theorem FFL.LogicalConnective.HomClass.map_iff (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [LogicalConnective α] [LogicalNeutral α] [LogicalConnective β] [LogicalNeutral β] [FunLike F α β] [HomClass F α β] (f : F) (a b : α) : f (a 🡘 b) = f a 🡘 f b

structure FFL.LogicalConnective.Hom (α : Type u_1) (β : Type u_2) [LogicalConnective α] [LogicalConnective β] [LogicalNeutral α] [LogicalNeutral β] : Type (max u_1 u_2)

• toTr : α → β
• map_top' : self.toTr ⊤ = ⊤
• map_bot' : self.toTr ⊥ = ⊥
• map_neg' (φ : α) : self.toTr (∼φ) = ∼self.toTr φ
• map_imply' (φ ψ : α) : self.toTr (φ 🡒 ψ) = self.toTr φ 🡒 self.toTr ψ
• map_and' (φ ψ : α) : self.toTr (φ ⋏ ψ) = self.toTr φ ⋏ self.toTr ψ
• map_or' (φ ψ : α) : self.toTr (φ ⋎ ψ) = self.toTr φ ⋎ self.toTr ψ

def FFL.LogicalConnective.«term_→ˡᶜ_» : Lean.TrailingParserDescr

A structure for homomorphisms (for logical connectives) from α to β.

Equations

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

@[instance_reducible]

instance FFL.LogicalConnective.Hom.instFunLike {α : Type u_1} {β : Type u_2} [LogicalConnective α] [LogicalConnective β] [LogicalNeutral α] [LogicalNeutral β] : FunLike (α →ˡᶜ β) α β

Equations

• FFL.LogicalConnective.Hom.instFunLike = { coe := FFL.LogicalConnective.Hom.toTr, coe_injective := ⋯ }

@[instance_reducible]

instance FFL.LogicalConnective.Hom.instCoeFunForall {α : Type u_1} {β : Type u_2} [LogicalConnective α] [LogicalConnective β] [LogicalNeutral α] [LogicalNeutral β] : CoeFun (α →ˡᶜ β) fun (x : α →ˡᶜ β) => α → β

Equations

• FFL.LogicalConnective.Hom.instCoeFunForall = DFunLike.toCoeFun

theorem FFL.LogicalConnective.Hom.ext {α : Type u_1} {β : Type u_2} [LogicalConnective α] [LogicalConnective β] [LogicalNeutral α] [LogicalNeutral β] (f g : α →ˡᶜ β) (h : ∀ (x : α), f x = g x) : f = g

theorem FFL.LogicalConnective.Hom.ext_iff {α : Type u_1} {β : Type u_2} [LogicalConnective α] [LogicalConnective β] [LogicalNeutral α] [LogicalNeutral β] {f g : α →ˡᶜ β} : f = g ↔ ∀ (x : α), f x = g x

instance FFL.LogicalConnective.Hom.instHomClass {α : Type u_1} {β : Type u_2} [LogicalConnective α] [LogicalConnective β] [LogicalNeutral α] [LogicalNeutral β] : HomClass (α →ˡᶜ β) α β

def FFL.LogicalConnective.Hom.id {α : Type u_1} [LogicalConnective α] [LogicalNeutral α] : α →ˡᶜ α

Equations

• FFL.LogicalConnective.Hom.id = { toTr := id, map_top' := ⋯, map_bot' := ⋯, map_neg' := ⋯, map_imply' := ⋯, map_and' := ⋯, map_or' := ⋯ }

@[simp]

theorem FFL.LogicalConnective.Hom.app_id {α : Type u_1} [LogicalConnective α] [LogicalNeutral α] (a : α) : Hom.id a = a

def FFL.LogicalConnective.Hom.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LogicalConnective α] [LogicalConnective β] [LogicalConnective γ] [LogicalNeutral α] [LogicalNeutral β] [LogicalNeutral γ] (g : β →ˡᶜ γ) (f : α →ˡᶜ β) : α →ˡᶜ γ

Equations

• g.comp f = { toTr := ⇑g ∘ ⇑f, map_top' := ⋯, map_bot' := ⋯, map_neg' := ⋯, map_imply' := ⋯, map_and' := ⋯, map_or' := ⋯ }

@[simp]

theorem FFL.LogicalConnective.Hom.app_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LogicalConnective α] [LogicalConnective β] [LogicalConnective γ] [LogicalNeutral α] [LogicalNeutral β] [LogicalNeutral γ] (g : β →ˡᶜ γ) (f : α →ˡᶜ β) (a : α) : (g.comp f) a = g (f a)

class FFL.LogicalConnective.AndOrClosed {F : Type u_4} [LogicalConnective F] [LogicalNeutral F] (C : F → Prop) : Prop

• verum : C ⊤
• falsum : C ⊥
• and {f g : F} : C f → C g → C (f ⋏ g)
• or {f g : F} : C f → C g → C (f ⋎ g)

class FFL.LogicalConnective.Closed {F : Type u_4} [LogicalConnective F] [LogicalNeutral F] (C : F → Prop) extends FFL.LogicalConnective.AndOrClosed C : Prop

• verum : C ⊤
• falsum : C ⊥
• and {f g : F} : C f → C g → C (f ⋏ g)
• or {f g : F} : C f → C g → C (f ⋎ g)
• not {f : F} : C f → C (∼f)
• imply {f g : F} : C f → C g → C (f 🡒 g)

def FFL.conjLt {α : Type u_1} [LogicalConnective α] [LogicalNeutral α] (φ : ℕ → α) : ℕ → α

Equations

• FFL.conjLt φ 0 = ⊤
• FFL.conjLt φ k.succ = φ k ⋏ FFL.conjLt φ k

@[simp]

theorem FFL.conjLt_zero {α : Type u_1} [LogicalConnective α] [LogicalNeutral α] (φ : ℕ → α) : conjLt φ 0 = ⊤

@[simp]

theorem FFL.conjLt_succ {α : Type u_1} [LogicalConnective α] [LogicalNeutral α] (φ : ℕ → α) (k : ℕ) : conjLt φ (k + 1) = φ k ⋏ conjLt φ k

@[simp]

theorem FFL.hom_conj_prop {α : Type u_1} [LogicalConnective α] [LogicalNeutral α] {F : Type u_3} {k : ℕ} [FunLike F α Prop] [LogicalConnective.HomClass F α Prop] (f : F) (φ : ℕ → α) : f (conjLt φ k) ↔ ∀ i < k, f (φ i)

Homomorphisms commute with k-ary conjunctions.

def FFL.disjLt {α : Type u_1} [LogicalConnective α] [LogicalNeutral α] (φ : ℕ → α) : ℕ → α

Equations

• FFL.disjLt φ 0 = ⊥
• FFL.disjLt φ k.succ = φ k ⋎ FFL.disjLt φ k

@[simp]

theorem FFL.disjLt_zero {α : Type u_1} [LogicalConnective α] [LogicalNeutral α] (φ : ℕ → α) : disjLt φ 0 = ⊥

@[simp]

theorem FFL.disjLt_succ {α : Type u_1} [LogicalConnective α] [LogicalNeutral α] (φ : ℕ → α) (k : ℕ) : disjLt φ (k + 1) = φ k ⋎ disjLt φ k

@[simp]

theorem FFL.hom_disj_prop {α : Type u_1} [LogicalConnective α] [LogicalNeutral α] {F : Type u_3} {k : ℕ} [FunLike F α Prop] [LogicalConnective.HomClass F α Prop] (f : F) (φ : ℕ → α) : f (disjLt φ k) ↔ ∃ i < k, f (φ i)

Homomorphisms commute with k-ary disjunctions.

def Matrix.conj {α : Type u_1} [Top α] [FFL.Wedge α] {n : ℕ} : (Fin n → α) → α

The conjunction of a vector of elements of type α, where α is a type with Wedge α.

Equations

• Matrix.conj x_2 = ⊤
• Matrix.conj v = v 0 ⋏ Matrix.conj (Matrix.vecTail v)

@[simp]

theorem Matrix.conj_nil {α : Type u_1} [Top α] [FFL.Wedge α] (v : Fin 0 → α) : conj v = ⊤

@[simp]

theorem Matrix.conj_cons {α : Type u_1} [Top α] [FFL.Wedge α] {n : ℕ} {a : α} {v : Fin n → α} : conj (a :> v) = a ⋏ conj v

def Matrix.disj {α : Type u_1} [Bot α] [FFL.Vee α] {n : ℕ} : (Fin n → α) → α

The disjunction of a vector of elements of type α, where α is a type with Vee α.

Equations

• Matrix.disj x_2 = ⊥
• Matrix.disj v = v 0 ⋎ Matrix.disj (Matrix.vecTail v)

@[simp]

theorem Matrix.disj_nil {α : Type u_1} [Bot α] [FFL.Vee α] (v : Fin 0 → α) : disj v = ⊥

@[simp]

theorem Matrix.disj_cons {α : Type u_1} [Bot α] [FFL.Vee α] {n : ℕ} {a : α} {v : Fin n → α} : disj (a :> v) = a ⋎ disj v

@[simp]

theorem Matrix.conj_hom_prop {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalNeutral α] {F : Type u_2} {n : ℕ} [FunLike F α Prop] [FFL.LogicalConnective.HomClass F α Prop] (f : F) (v : Fin n → α) : f (conj v) = ∀ (i : Fin n), f (v i)

Homomorphisms commute with k-ary conjunctions (vector version).

@[simp]

theorem Matrix.disj_hom_prop {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalNeutral α] {F : Type u_2} {n : ℕ} [FunLike F α Prop] [FFL.LogicalConnective.HomClass F α Prop] (f : F) (v : Fin n → α) : f (disj v) = ∃ (i : Fin n), f (v i)

Homomorphisms commute with k-ary disjunctions (vector version).

@[simp]

theorem Matrix.hom_conj {β : Type u_3} {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalConnective β] [FFL.LogicalNeutral α] [FFL.LogicalNeutral β] {F : Type u_2} {n : ℕ} [FunLike F α β] [FFL.LogicalConnective.HomClass F α β] (f : F) (v : Fin n → α) : f (conj v) = conj (⇑f ∘ v)

theorem Matrix.hom_conj₂ {β : Type u_3} {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalConnective β] [FFL.LogicalNeutral α] [FFL.LogicalNeutral β] {F : Type u_2} {n : ℕ} [FunLike F α β] [FFL.LogicalConnective.HomClass F α β] (f : F) (v : Fin n → α) : f (conj v) = conj fun (i : Fin n) => f (v i)

@[simp]

theorem Matrix.hom_disj {β : Type u_3} {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalConnective β] [FFL.LogicalNeutral α] [FFL.LogicalNeutral β] {F : Type u_2} {n : ℕ} [FunLike F α β] [FFL.LogicalConnective.HomClass F α β] (f : F) (v : Fin n → α) : f (disj v) = disj (⇑f ∘ v)

theorem Matrix.hom_disj' {β : Type u_3} {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalConnective β] [FFL.LogicalNeutral α] [FFL.LogicalNeutral β] {F : Type u_2} {n : ℕ} [FunLike F α β] [FFL.LogicalConnective.HomClass F α β] (f : F) (v : Fin n → α) : f (disj v) = disj fun (i : Fin n) => f (v i)

@[instance_reducible]

instance List.instTilde {α : Type u_1} [FFL.Tilde α] : FFL.Tilde (List α)

Equations

• List.instTilde = { tilde := fun (l : List α) => List.map (fun (x : α) => ∼x) l }

theorem List.tilde_def {α : Type u_1} [FFL.Tilde α] (l : List α) : ∼l = map (fun (x : α) => ∼x) l

@[simp]

theorem List.tilde_nil {α : Type u_1} [FFL.Tilde α] : ∼[] = []

@[simp]

theorem List.tilde_cons {α : Type u_1} [FFL.Tilde α] (a : α) (l : List α) : ∼(a :: l) = ∼a :: ∼l

@[simp]

theorem List.tilde_append {α : Type u_1} [FFL.Tilde α] (l k : List α) : ∼(l ++ k) = ∼l ++ ∼k

@[simp]

theorem List.mem_tilde_iff {α : Type u_1} [FFL.Tilde α] [FFL.TildeInvolutive α] {a : α} {l : List α} : a ∈ ∼l ↔ ∼a ∈ l

instance List.instTildeInvolutive {α : Type u_1} [FFL.Tilde α] [FFL.TildeInvolutive α] : FFL.TildeInvolutive (List α)

def List.conj {α : Type u_1} [Top α] [FFL.Wedge α] : List α → α

Equations

• [].conj = ⊤
• (a :: as).conj = a ⋏ as.conj

@[simp]

theorem List.conj_nil {α : Type u_1} [Top α] [FFL.Wedge α] : [].conj = ⊤

@[simp]

theorem List.conj_cons {α : Type u_1} [Top α] [FFL.Wedge α] {a : α} {as : List α} : (a :: as).conj = a ⋏ as.conj

def List.conj₂ {α : Type u_1} [Top α] [FFL.Wedge α] : List α → α

Remark: [φ].conj₂ = φ ≠ φ ⋏ ⊤ = [φ].conj.

Equations

• ⋀[] = ⊤
• ⋀[φ] = φ
• ⋀(φ :: ψ :: rs) = φ ⋏ ⋀(ψ :: rs)

def List.«term⋀_» : Lean.ParserDescr

The conjunction of a list of members of type α.

Equations

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

@[simp]

theorem List.conj₂_nil {α : Type u_1} [Top α] [FFL.Wedge α] : ⋀[] = ⊤

@[simp]

theorem List.conj₂_singleton {α : Type u_1} {φ : α} [Top α] [FFL.Wedge α] : ⋀[φ] = φ

@[simp]

theorem List.conj₂_doubleton {α : Type u_1} {φ ψ : α} [Top α] [FFL.Wedge α] : ⋀[φ, ψ] = φ ⋏ ψ

@[simp]

theorem List.conj₂_cons_nonempty {α : Type u_1} [Top α] [FFL.Wedge α] {a : α} {as : List α} (h : as ≠ [] := by assumption) : ⋀(a :: as) = a ⋏ ⋀as

def List.conj' {α : Type u_1} [Top α] [FFL.Wedge α] {ι : Type u_2} (f : ι → α) (l : List ι) : α

Equations

• List.conj' f l = ⋀List.map f l

@[simp]

theorem List.conj'_nil {α : Type u_1} [Top α] [FFL.Wedge α] {ι : Type u_2} (f : ι → α) : conj' f [] = ⊤

@[simp]

theorem List.conj'_singleton {α : Type u_1} [Top α] [FFL.Wedge α] {ι : Type u_2} (f : ι → α) (i : ι) : conj' f [i] = f i

@[simp]

theorem List.conj'_cons {α : Type u_1} [Top α] [FFL.Wedge α] {ι : Type u_2} (f : ι → α) (i j : ι) (is : List ι) : conj' f (i :: j :: is) = f i ⋏ conj' f (j :: is)

def List.disj {α : Type u_1} [Bot α] [FFL.Vee α] : List α → α

Equations

• [].disj = ⊥
• (a :: as).disj = a ⋎ as.disj

@[simp]

theorem List.disj_nil {α : Type u_1} [Bot α] [FFL.Vee α] : [].disj = ⊥

@[simp]

theorem List.disj_cons {α : Type u_1} [Bot α] [FFL.Vee α] {a : α} {as : List α} : (a :: as).disj = a ⋎ as.disj

def List.disj₂ {α : Type u_1} [Bot α] [FFL.Vee α] : List α → α

Remark: [φ].disj₂ = φ ≠ φ ⋎ ⊥ = [φ].disj.

Equations

• ⋁[] = ⊥
• ⋁[φ] = φ
• ⋁(φ :: ψ :: rs) = φ ⋎ ⋁(ψ :: rs)

def List.«term⋁_» : Lean.ParserDescr

The disjunction of a list of members of type α.

Equations

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

@[simp]

theorem List.disj₂_nil {α : Type u_1} [Bot α] [FFL.Vee α] : ⋁[] = ⊥

@[simp]

theorem List.disj₂_singleton {α : Type u_1} {φ : α} [Bot α] [FFL.Vee α] : ⋁[φ] = φ

@[simp]

theorem List.disj₂_doubleton {α : Type u_1} {φ ψ : α} [Bot α] [FFL.Vee α] : ⋁[φ, ψ] = φ ⋎ ψ

@[simp]

theorem List.disj₂_cons_nonempty {α : Type u_1} [Bot α] [FFL.Vee α] {a : α} {as : List α} (h : as ≠ [] := by assumption) : ⋁(a :: as) = a ⋎ ⋁as

def List.disj' {α : Type u_1} [Bot α] [FFL.Vee α] {ι : Type u_2} (f : ι → α) (l : List ι) : α

Equations

• List.disj' f l = ⋁List.map f l

@[simp]

theorem List.disj'_nil {α : Type u_1} [Bot α] [FFL.Vee α] {ι : Type u_2} (f : ι → α) : disj' f [] = ⊥

@[simp]

theorem List.disj'_singleton {α : Type u_1} [Bot α] [FFL.Vee α] {ι : Type u_2} (f : ι → α) (i : ι) : disj' f [i] = f i

@[simp]

theorem List.disj'_cons {α : Type u_1} [Bot α] [FFL.Vee α] {ι : Type u_2} (f : ι → α) (i j : ι) (is : List ι) : disj' f (i :: j :: is) = f i ⋎ disj' f (j :: is)

@[simp]

theorem List.tilde_conj {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalNeutral α] [FFL.LogicalNeutral.DeMorgan α] [FFL.LogicalConnective.DeMorgan α] (l : List α) : ∼l.disj = (∼l).conj

Variadic de Morgan's law for lists of elements of type α.

@[simp]

theorem List.tilde_disj {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalNeutral α] [FFL.LogicalNeutral.DeMorgan α] [FFL.LogicalConnective.DeMorgan α] (l : List α) : ∼l.conj = (∼l).disj

Variadic de Morgan's law for lists of elements of type α.

@[simp]

theorem List.tilde_conj₂ {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalNeutral α] [FFL.LogicalNeutral.DeMorgan α] [FFL.LogicalConnective.DeMorgan α] (l : List α) : ∼⋁l = ⋀(∼l)

Variadic de Morgan's law for lists of elements of type α.

@[simp]

theorem List.tilde_disj₂ {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalNeutral α] [FFL.LogicalNeutral.DeMorgan α] [FFL.LogicalConnective.DeMorgan α] (l : List α) : ∼⋀l = ⋁(∼l)

Variadic de Morgan's law for lists of elements of type α.

theorem List.map_tilde {β : Type u_2} {G : Type u_3} {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalNeutral α] [FFL.LogicalConnective β] [FFL.LogicalNeutral β] [FunLike G α β] [FFL.LogicalConnective.HomClass G α β] (f : G) (l : List α) : map (⇑f) (∼l) = ∼map (⇑f) l

theorem List.map_conj {β : Type u_2} {G : Type u_3} {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalNeutral α] [FFL.LogicalConnective β] [FFL.LogicalNeutral β] [FunLike G α β] [FFL.LogicalConnective.HomClass G α β] (f : G) (l : List α) : f l.conj = (map (⇑f) l).conj

theorem List.map_conj₂ {β : Type u_2} {G : Type u_3} {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalNeutral α] [FFL.LogicalConnective β] [FFL.LogicalNeutral β] [FunLike G α β] [FFL.LogicalConnective.HomClass G α β] (f : G) (l : List α) : f (⋀l) = ⋀map (⇑f) l

theorem List.map_conj' {β : Type u_3} {G : Type u_4} {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalNeutral α] [FFL.LogicalConnective β] [FFL.LogicalNeutral β] [FunLike G α β] [FFL.LogicalConnective.HomClass G α β] {ι : Type u_2} (F : G) (l : List ι) (f : ι → α) : F (conj' f l) = conj' (⇑F ∘ f) l

theorem List.map_disj {β : Type u_2} {G : Type u_3} {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalNeutral α] [FFL.LogicalConnective β] [FFL.LogicalNeutral β] [FunLike G α β] [FFL.LogicalConnective.HomClass G α β] (f : G) (l : List α) : f l.disj = (map (⇑f) l).disj

theorem List.map_disj₂ {β : Type u_2} {G : Type u_3} {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalNeutral α] [FFL.LogicalConnective β] [FFL.LogicalNeutral β] [FunLike G α β] [FFL.LogicalConnective.HomClass G α β] (f : G) (l : List α) : f (⋁l) = ⋁map (⇑f) l

theorem List.map_disj' {β : Type u_3} {G : Type u_4} {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalNeutral α] [FFL.LogicalConnective β] [FFL.LogicalNeutral β] [FunLike G α β] [FFL.LogicalConnective.HomClass G α β] {ι : Type u_2} (F : G) (l : List ι) (f : ι → α) : F (disj' f l) = disj' (⇑F ∘ f) l

@[simp]

theorem List.map_conj_prop {G : Type u_2} {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalNeutral α] [FunLike G α Prop] [FFL.LogicalConnective.HomClass G α Prop] {f : G} {l : List α} : f l.conj ↔ ∀ a ∈ l, f a

@[simp]

theorem List.map_conj₂_prop {G : Type u_2} {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalNeutral α] [FunLike G α Prop] [FFL.LogicalConnective.HomClass G α Prop] {f : G} {l : List α} : f (⋀l) ↔ ∀ a ∈ l, f a

theorem List.map_conj_append_prop {G : Type u_2} {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalNeutral α] [FunLike G α Prop] [FFL.LogicalConnective.HomClass G α Prop] (f : G) (l₁ l₂ : List α) : f (l₁ ++ l₂).conj ↔ f (l₁.conj ⋏ l₂.conj)

@[simp]

theorem List.map_conj'_prop {G : Type u_3} {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalNeutral α] [FunLike G α Prop] [FFL.LogicalConnective.HomClass G α Prop] {ι : Type u_2} {F : G} {l : List ι} {f : ι → α} : F (conj' f l) ↔ ∀ i ∈ l, F (f i)

@[simp]

theorem List.map_disj_prop {G : Type u_2} {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalNeutral α] [FunLike G α Prop] [FFL.LogicalConnective.HomClass G α Prop] {f : G} {l : List α} : f l.disj ↔ ∃ a ∈ l, f a

@[simp]

theorem List.map_disj₂_prop {G : Type u_2} {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalNeutral α] [FunLike G α Prop] [FFL.LogicalConnective.HomClass G α Prop] {f : G} {l : List α} : f (⋁l) ↔ ∃ a ∈ l, f a

theorem List.map_disj_append_prop {G : Type u_2} {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalNeutral α] [FunLike G α Prop] [FFL.LogicalConnective.HomClass G α Prop] (f : G) (l₁ l₂ : List α) : f (l₁ ++ l₂).disj ↔ f (l₁.disj ⋎ l₂.disj)

@[simp]

theorem List.map_disj'_prop {G : Type u_3} {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalNeutral α] [FunLike G α Prop] [FFL.LogicalConnective.HomClass G α Prop] {ι : Type u_2} {F : G} {l : List ι} {f : ι → α} : F (disj' f l) ↔ ∃ i ∈ l, F (f i)

@[instance_reducible]

instance Multiset.instTilde {α : Type u_1} [FFL.Tilde α] : FFL.Tilde (Multiset α)

Equations

• Multiset.instTilde = { tilde := fun (Γ : Multiset α) => Multiset.map (fun (x : α) => ∼x) Γ }

theorem Multiset.tilde_def {α : Type u_1} [FFL.Tilde α] (Γ : Multiset α) : ∼Γ = map (fun (x : α) => ∼x) Γ

@[simp]

theorem Multiset.tilde_zero {α : Type u_1} [FFL.Tilde α] : ∼0 = 0

@[simp]

theorem Multiset.tilde_add {α : Type u_1} [FFL.Tilde α] (Γ Δ : Multiset α) : ∼(Γ + Δ) = ∼Γ + ∼Δ

@[simp]

theorem Multiset.tilde_atom {α : Type u_1} [FFL.Tilde α] (φ : α) : ∼⦃φ⦄ = ⦃∼φ⦄

@[simp]

theorem Multiset.mem_tilde_iff {α : Type u_1} [FFL.Tilde α] [FFL.TildeInvolutive α] {φ : α} {Γ : Multiset α} : φ ∈ ∼Γ ↔ ∼φ ∈ Γ

instance Multiset.instTildeInvolutive {α : Type u_1} [FFL.Tilde α] [FFL.TildeInvolutive α] : FFL.TildeInvolutive (Multiset α)

theorem Multiset.map_tilde_comm {α : Type u_1} {β : Type u_2} [FFL.LogicalNeutral α] [FFL.LogicalConnective α] [FFL.LogicalNeutral β] [FFL.LogicalConnective β] {Γ : Multiset α} (f : α →ˡᶜ β) : map (⇑f) (∼Γ) = ∼map (⇑f) Γ

@[instance_reducible]

instance Finset.instTilde {α : Type u_1} [FFL.Tilde α] [FFL.TildeInvolutive α] : FFL.Tilde (Finset α)

Equations

• Finset.instTilde = { tilde := fun (l : Finset α) => Finset.map FFL.Tilde.invol l }

theorem Finset.tilde_def {α : Type u_1} [FFL.Tilde α] [FFL.TildeInvolutive α] (s : Finset α) : ∼s = map FFL.Tilde.invol s

@[simp]

theorem Finset.mem_tilde_iff {α : Type u_1} [FFL.Tilde α] [FFL.TildeInvolutive α] {a : α} {s : Finset α} : a ∈ ∼s ↔ ∼a ∈ s

instance Finset.instTildeInvolutive {α : Type u_1} [FFL.Tilde α] [FFL.TildeInvolutive α] : FFL.TildeInvolutive (Finset α)

@[simp]

theorem Finset.tilde_empty {α : Type u_1} [FFL.Tilde α] [FFL.TildeInvolutive α] : ∼∅ = ∅

@[simp]

theorem Finset.tilde_insert {α : Type u_1} [FFL.Tilde α] [FFL.TildeInvolutive α] (a : α) (s : Finset α) : ∼insert a s = insert (∼a) (∼s)

@[simp]

theorem Finset.tilde_union {α : Type u_1} [FFL.Tilde α] [FFL.TildeInvolutive α] (s t : Finset α) : ∼(s ∪ t) = ∼s ∪ ∼t

noncomputable def Finset.conj {α : Type u_1} [Top α] [FFL.Wedge α] (s : Finset α) : α

Equations

• s.conj = ⋀s.toList

noncomputable def Finset.conj' {α : Type u_1} {ι : Type u_2} [Top α] [FFL.Wedge α] (s : Finset ι) (f : ι → α) : α

Equations

• s.conj' f = List.conj' f s.toList

noncomputable def Finset.uconj {α : Type u_1} {ι : Type u_2} [Top α] [FFL.Wedge α] [Fintype ι] (f : ι → α) : α

Equations

• Finset.uconj f = Finset.univ.conj' f

noncomputable def Finset.disj {α : Type u_1} [Bot α] [FFL.Vee α] (s : Finset α) : α

Equations

• s.disj = ⋁s.toList

noncomputable def Finset.disj' {α : Type u_1} {ι : Type u_2} [Bot α] [FFL.Vee α] (s : Finset ι) (f : ι → α) : α

Equations

• s.disj' f = List.disj' f s.toList

noncomputable def Finset.udisj {α : Type u_1} {ι : Type u_2} [Bot α] [FFL.Vee α] [Fintype ι] (f : ι → α) : α

Equations

• Finset.udisj f = Finset.univ.disj' f

def Finset.biguconj : Lean.ParserDescr

• ⩕ i ∈ s, φ i is notation for s.conj' fun i ↦ φ i
• ⩕ i, φ i is notation for uconj fun i ↦ φ i

Equations

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

def Finset.uconjUnexpsnder : Lean.PrettyPrinter.Unexpander

Equations

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

def Finset.conj'Unexpsnder : Lean.PrettyPrinter.Unexpander

Equations

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

def Finset.bigudisj : Lean.ParserDescr

• ⩖ i ∈ s, φ i is notation for s.disj' fun i ↦ φ i
• ⩖ i, φ i is notation for udisj fun i ↦ φ i

Equations

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

def Finset.udisjUnexpsnder : Lean.PrettyPrinter.Unexpander

Equations

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

def Finset.disj'Unexpsnder : Lean.PrettyPrinter.Unexpander

Equations

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

@[simp]

theorem Finset.conj_empty {α : Type u_1} [Top α] [FFL.Wedge α] : ∅.conj = ⊤

@[simp]

theorem Finset.conj_singleton {α : Type u_1} [Top α] [FFL.Wedge α] (a : α) : {a}.conj = a

@[simp]

theorem Finset.conj'_empty {α : Type u_1} [Top α] [FFL.Wedge α] {ι : Type u_2} (f : ι → α) : ∅.conj' f = ⊤

@[simp]

theorem Finset.conj'_singleton {α : Type u_1} [Top α] [FFL.Wedge α] {ι : Type u_2} (f : ι → α) {i : ι} : {i}.conj' f = f i

@[simp]

theorem Finset.uconj_empty {α : Type u_1} [Top α] [FFL.Wedge α] {ι : Type u_2} [Fintype ι] [IsEmpty ι] (f : ι → α) : uconj f = ⊤

@[simp]

theorem Finset.uconj_singleton {α : Type u_1} [Top α] [FFL.Wedge α] {ι : Type u_2} [Fintype ι] [Unique ι] (f : ι → α) : uconj f = f default

@[simp]

theorem Finset.disj_empty {α : Type u_1} [Bot α] [FFL.Vee α] : ∅.disj = ⊥

@[simp]

theorem Finset.disj_singleton {α : Type u_1} [Bot α] [FFL.Vee α] (a : α) : {a}.disj = a

@[simp]

theorem Finset.disj'_empty {α : Type u_1} [Bot α] [FFL.Vee α] {ι : Type u_2} (f : ι → α) : ∅.disj' f = ⊥

@[simp]

theorem Finset.disj'_singleton {α : Type u_1} [Bot α] [FFL.Vee α] {ι : Type u_2} (f : ι → α) (i : ι) : {i}.disj' f = f i

@[simp]

theorem Finset.udisj_empty {α : Type u_1} [Bot α] [FFL.Vee α] {ι : Type u_2} [Fintype ι] [IsEmpty ι] (f : ι → α) : udisj f = ⊥

@[simp]

theorem Finset.udisj_singleton {α : Type u_1} [Bot α] [FFL.Vee α] {ι : Type u_2} [Fintype ι] [Unique ι] (f : ι → α) : udisj f = f default

@[simp]

theorem Finset.map_conj_prop {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalNeutral α] {F : Type u_2} [FunLike F α Prop] [FFL.LogicalConnective.HomClass F α Prop] {f : F} {s : Finset α} : f s.conj ↔ ∀ a ∈ s, f a

theorem Finset.map_conj_union {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalNeutral α] {F : Type u_2} [DecidableEq α] [FunLike F α Prop] [FFL.LogicalConnective.HomClass F α Prop] (f : F) (s₁ s₂ : Finset α) : f (s₁ ∪ s₂).conj ↔ f (s₁.conj ⋏ s₂.conj)

theorem Finset.map_conj' {β : Type u_4} {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalNeutral α] [FFL.LogicalConnective β] [FFL.LogicalNeutral β] {F : Type u_2} {ι : Type u_3} [FunLike F α β] [FFL.LogicalConnective.HomClass F α β] (Φ : F) (s : Finset ι) (f : ι → α) : Φ (⩕ (i : ι) ∈ s, f i) = ⩕ (i : ι) ∈ s, Φ (f i)

@[simp]

theorem Finset.map_conj'_prop {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalNeutral α] {F : Type u_2} {ι : Type u_3} [FunLike F α Prop] [FFL.LogicalConnective.HomClass F α Prop] {f : F} {s : Finset ι} {p : ι → α} : f (s.conj' p) ↔ ∀ i ∈ s, f (p i)

theorem Finset.map_uconj {β : Type u_4} {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalNeutral α] [FFL.LogicalConnective β] [FFL.LogicalNeutral β] {F : Type u_2} {ι : Type u_3} [FunLike F α β] [FFL.LogicalConnective.HomClass F α β] (Φ : F) [Fintype ι] (f : ι → α) : Φ (⩕ (i : ι), f i) = ⩕ (i : ι), Φ (f i)

@[simp]

theorem Finset.map_uconj_prop {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalNeutral α] {F : Type u_2} {ι : Type u_3} [FunLike F α Prop] [FFL.LogicalConnective.HomClass F α Prop] {Φ : F} [Fintype ι] {f : ι → α} : Φ (uconj f) ↔ ∀ (i : ι), Φ (f i)

@[simp]

theorem Finset.map_disj_prop {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalNeutral α] {F : Type u_2} [FunLike F α Prop] [FFL.LogicalConnective.HomClass F α Prop] (f : F) (s : Finset α) : f s.disj ↔ ∃ a ∈ s, f a

theorem Finset.map_disj_union {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalNeutral α] {F : Type u_2} [DecidableEq α] [FunLike F α Prop] [FFL.LogicalConnective.HomClass F α Prop] (f : F) (s₁ s₂ : Finset α) : f (s₁ ∪ s₂).disj ↔ f (s₁.disj ⋎ s₂.disj)

theorem Finset.map_disj' {β : Type u_4} {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalNeutral α] [FFL.LogicalConnective β] [FFL.LogicalNeutral β] {F : Type u_2} {ι : Type u_3} [FunLike F α β] [FFL.LogicalConnective.HomClass F α β] (Φ : F) (s : Finset ι) (f : ι → α) : Φ (⩖ (i : ι) ∈ s, f i) = ⩖ (i : ι) ∈ s, Φ (f i)

@[simp]

theorem Finset.map_disj'_prop {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalNeutral α] {F : Type u_2} {ι : Type u_3} [FunLike F α Prop] [FFL.LogicalConnective.HomClass F α Prop] {f : F} {s : Finset ι} {p : ι → α} : f (s.disj' p) ↔ ∃ i ∈ s, f (p i)

theorem Finset.map_udisj {β : Type u_4} {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalNeutral α] [FFL.LogicalConnective β] [FFL.LogicalNeutral β] {F : Type u_2} {ι : Type u_3} [FunLike F α β] [FFL.LogicalConnective.HomClass F α β] (Φ : F) [Fintype ι] (f : ι → α) : Φ (⩖ (i : ι), f i) = ⩖ (i : ι), Φ (f i)

@[simp]

theorem Finset.map_udisj_prop {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalNeutral α] {F : Type u_2} {ι : Type u_3} [FunLike F α Prop] [FFL.LogicalConnective.HomClass F α Prop] {Φ : F} [Fintype ι] {f : ι → α} : Φ (udisj f) ↔ ∃ (i : ι), Φ (f i)