Supporting results for pointwise provable equality.

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 PointwiseComposition.FFL.LogicalConnective (α : Type u_1) extends PointwiseComposition.FFL.Tilde α, PointwiseComposition.FFL.Arrow α, PointwiseComposition.FFL.Wedge α, PointwiseComposition.FFL.Vee α : Type u_1

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

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

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

Truth and falsity constants for formulas.

• top : α
• bot : α

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

Data and laws for Tilde Involutive in FFL.

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

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

Data and laws for De Morgan in FFL.LogicalConnective.

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

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

Data and laws for De Morgan in FFL.LogicalNeutral.

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

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

Alias of PointwiseComposition.FFL.TildeInvolutive.tilde_involutive.

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

Introducing ∼φ as an abbreviation of φ ⇒ₗ ⊥.

• neg {φ : F} : ∼φ = φ ⇒ₗ ⊥

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

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

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

@[simp]

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

@[simp]

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

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

The invol construction in FFL.Tilde.

Equations

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

@[simp]

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

@[match_pattern]

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

The iff construction in FFL.LogicalConnective.

Equations

• a ⇔ₗ b = (a ⇒ₗ b) ⋏ (b ⇒ₗ a)

def PointwiseComposition.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 PointwiseComposition.FFL.LogicalConnective.PropLogicSymbols : LogicalConnective Prop

Equations

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

@[instance_reducible]

instance PointwiseComposition.FFL.LogicalConnective.PropLogicalNeutral : LogicalNeutral Prop

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem PointwiseComposition.FFL.LogicalConnective.Prop.arrow_eq (φ ψ : Prop) : φ ⇒ₗ ψ = (φ → ψ)

@[simp]

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

@[simp]

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

@[simp]

theorem PointwiseComposition.FFL.LogicalConnective.Prop.iff_eq (φ ψ : Prop) : φ ⇔ₗ ψ = (φ ↔ ψ)

instance PointwiseComposition.FFL.LogicalConnective.instTildeInvolutiveProp : TildeInvolutive Prop

instance PointwiseComposition.FFL.LogicalConnective.instDeMorganProp : DeMorgan Prop

instance PointwiseComposition.FFL.LogicalConnective.instDeMorganProp_1 : LogicalNeutral.DeMorgan Prop

class PointwiseComposition.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 PointwiseComposition.FFL.LogicalConnective.HomClass.instCoeFunForall (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [FunLike F α β] : CoeFun F fun (x : F) => α → β

Equations

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

@[simp]

theorem PointwiseComposition.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 PointwiseComposition.FFL.LogicalConnective.Hom (α : Type u_1) (β : Type u_2) [LogicalConnective α] [LogicalConnective β] [LogicalNeutral α] [LogicalNeutral β] : Type (max u_1 u_2)

Data and laws for Hom in FFL.LogicalConnective.

• toTr : α → β

  The to Tr construction in FFL.LogicalConnective.Hom.

• 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 PointwiseComposition.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 PointwiseComposition.FFL.LogicalConnective.Hom.instFunLike {α : Type u_1} {β : Type u_2} [LogicalConnective α] [LogicalConnective β] [LogicalNeutral α] [LogicalNeutral β] : FunLike (α →ˡᶜ β) α β

Equations

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

@[instance_reducible]

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

Equations

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

theorem PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.FFL.LogicalConnective.Hom.instHomClass {α : Type u_1} {β : Type u_2} [LogicalConnective α] [LogicalConnective β] [LogicalNeutral α] [LogicalNeutral β] : HomClass (α →ˡᶜ β) α β

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

The id construction in FFL.LogicalConnective.Hom.

Equations

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

@[simp]

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

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

The comp construction in FFL.LogicalConnective.Hom.

Equations

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

@[simp]

theorem PointwiseComposition.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 PointwiseComposition.FFL.LogicalConnective.AndOrClosed {F : Type u_4} [LogicalConnective F] [LogicalNeutral F] (C : F → Prop) : Prop

Data and laws for And Or Closed in FFL.LogicalConnective.

• 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 PointwiseComposition.FFL.LogicalConnective.Closed {F : Type u_4} [LogicalConnective F] [LogicalNeutral F] (C : F → Prop) extends PointwiseComposition.FFL.LogicalConnective.AndOrClosed C : Prop

Data and laws for Closed in FFL.LogicalConnective.

• 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 PointwiseComposition.FFL.conjLt {α : Type u_1} [LogicalConnective α] [LogicalNeutral α] (φ : ℕ → α) : ℕ → α

The conj Lt construction in FFL.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

theorem PointwiseComposition.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 PointwiseComposition.FFL.disjLt {α : Type u_1} [LogicalConnective α] [LogicalNeutral α] (φ : ℕ → α) : ℕ → α

The disj Lt construction in FFL.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

theorem PointwiseComposition.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 PointwiseComposition.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

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

@[simp]

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

@[simp]

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

def PointwiseComposition.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

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

@[simp]

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

@[simp]

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

@[simp]

theorem PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.List.instTildeList {α : Type u_1} [FFL.Tilde α] : FFL.Tilde (List α)

Equations

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

The conj construction in List.

Equations

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

@[simp]

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

@[simp]

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

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

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

Equations

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

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

The conjunction of a list of members of type α.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The conj' construction in List.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

theorem PointwiseComposition.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 PointwiseComposition.List.disj {α : Type u_1} [Bot α] [FFL.Vee α] : List α → α

The disj construction in List.

Equations

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

@[simp]

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

@[simp]

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

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

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

Equations

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

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

The disjunction of a list of members of type α.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The disj' construction in List.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

theorem PointwiseComposition.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 PointwiseComposition.List.tilde_conj {α : Type u_1} [FFL.LogicalConnective α] [FFL.LogicalNeutral α] [FFL.LogicalNeutral.DeMorgan α] [FFL.LogicalConnective.DeMorgan α] (l : List α) : ∼disj l = conj (∼l)

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

@[simp]

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

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

@[simp]

theorem PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 α) : List.map (⇑f) (∼l) = ∼List.map (⇑f) l

theorem PointwiseComposition.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 (conj l) = conj (List.map (⇑f) l)

theorem PointwiseComposition.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) = ⋀List.map (⇑f) l

theorem PointwiseComposition.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 ((fun (x : ι → α) => conj' x l) f) = (fun (x : ι → β) => conj' x l) (⇑F ∘ f)

theorem PointwiseComposition.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 (disj l) = disj (List.map (⇑f) l)

theorem PointwiseComposition.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) = ⋁List.map (⇑f) l

theorem PointwiseComposition.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 ((fun (x : ι → α) => disj' x l) f) = (fun (x : ι → β) => disj' x l) (⇑F ∘ f)

@[simp]

theorem PointwiseComposition.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 (conj l) ↔ ∀ a ∈ l, f a

@[simp]

theorem PointwiseComposition.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 PointwiseComposition.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 (conj (l₁ ++ l₂)) ↔ f (conj l₁ ⋏ conj l₂)

@[simp]

theorem PointwiseComposition.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 ((fun (x : ι → α) => conj' x l) f) ↔ ∀ i ∈ l, F (f i)

@[simp]

theorem PointwiseComposition.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 (disj l) ↔ ∃ a ∈ l, f a

@[simp]

theorem PointwiseComposition.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 PointwiseComposition.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 (disj (l₁ ++ l₂)) ↔ f (disj l₁ ⋎ disj l₂)

@[simp]

theorem PointwiseComposition.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 ((fun (x : ι → α) => disj' x l) f) ↔ ∃ i ∈ l, F (f i)

@[instance_reducible]

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

Equations

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[instance_reducible]

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

Equations

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The conj construction in Finset.

Equations

• PointwiseComposition.Finset.conj s = ⋀s.toList

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

The conj' construction in Finset.

Equations

• PointwiseComposition.Finset.conj' s f = (fun (x : ι → α) => PointwiseComposition.List.conj' x s.toList) f

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

The uconj construction in Finset.

Equations

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

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

The disj construction in Finset.

Equations

• PointwiseComposition.Finset.disj s = ⋁s.toList

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

The disj' construction in Finset.

Equations

• PointwiseComposition.Finset.disj' s f = (fun (x : ι → α) => PointwiseComposition.List.disj' x s.toList) f

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

The udisj construction in Finset.

Equations

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

def PointwiseComposition.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 PointwiseComposition.Finset.uconjUnexpsnder : Lean.PrettyPrinter.Unexpander

The uconj Unexpsnder construction in Finset.

Equations

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

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

The conj'Unexpsnder construction in Finset.

Equations

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

def PointwiseComposition.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 PointwiseComposition.Finset.udisjUnexpsnder : Lean.PrettyPrinter.Unexpander

The udisj Unexpsnder construction in Finset.

Equations

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

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

The disj'Unexpsnder construction in Finset.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem PointwiseComposition.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 (conj s) ↔ ∀ a ∈ s, f a

theorem PointwiseComposition.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 (conj (s₁ ∪ s₂)) ↔ f (conj s₁ ⋏ conj s₂)

theorem PointwiseComposition.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 PointwiseComposition.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 (conj' s p) ↔ ∀ i ∈ s, f (p i)

theorem PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 (disj s) ↔ ∃ a ∈ s, f a

theorem PointwiseComposition.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 (disj (s₁ ∪ s₂)) ↔ f (disj s₁ ⋎ disj s₂)

theorem PointwiseComposition.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 PointwiseComposition.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 (disj' s p) ↔ ∃ i ∈ s, f (p i)

theorem PointwiseComposition.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 PointwiseComposition.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)