Supporting results for pointwise provable equality.

inductive PointwiseComposition.FFL.Polarity : Type

Data and laws for Polarity in FFL.

• sigma : Polarity
• pi : Polarity

@[instance_reducible]

instance PointwiseComposition.FFL.Polarity.instSigmaSymbol : SigmaSymbol Polarity

Equations

• PointwiseComposition.FFL.Polarity.instSigmaSymbol = { sigma := PointwiseComposition.FFL.Polarity.sigma }

@[instance_reducible]

instance PointwiseComposition.FFL.Polarity.instPiSymbol : PiSymbol Polarity

Equations

• PointwiseComposition.FFL.Polarity.instPiSymbol = { pi := PointwiseComposition.FFL.Polarity.pi }

def PointwiseComposition.FFL.Polarity.alt : Polarity → Polarity

The alt construction in FFL.Polarity.

Equations

• PointwiseComposition.FFL.Polarity.sigma.alt = Π
• PointwiseComposition.FFL.Polarity.pi.alt = Σ

theorem PointwiseComposition.FFL.Polarity.eq_sigma : sigma = Σ

theorem PointwiseComposition.FFL.Polarity.eq_pi : pi = Π

@[simp]

theorem PointwiseComposition.FFL.Polarity.alt_sigma : Σ.alt = Π

@[simp]

theorem PointwiseComposition.FFL.Polarity.alt_pi : Π.alt = Σ

@[simp]

theorem PointwiseComposition.FFL.Polarity.alt_alt (Γ : Polarity) : Γ.alt.alt = Γ

@[reducible, inline]

abbrev PointwiseComposition.FFL.Polarity.altItr (Γ : Polarity) (k : ℕ) : Polarity

Γ with its polarity flipped k times.

Equations

• Γ.altItr k = PointwiseComposition.FFL.Polarity.alt^[k] Γ

@[simp]

theorem PointwiseComposition.FFL.Polarity.altItr_zero (Γ : Polarity) : Γ.altItr 0 = Γ

theorem PointwiseComposition.FFL.Polarity.altItr_succ (Γ : Polarity) (k : ℕ) : Γ.altItr (k + 1) = (Γ.altItr k).alt

theorem PointwiseComposition.FFL.Polarity.altItr_succ' (Γ : Polarity) (k : ℕ) : Γ.altItr (k + 1) = Γ.alt.altItr k

def PointwiseComposition.FFL.Polarity.coe {α : Type u_1} [SigmaSymbol α] [PiSymbol α] : Polarity → α

The coe construction in FFL.Polarity.

Equations

• PointwiseComposition.FFL.Polarity.sigma.coe = Σ
• PointwiseComposition.FFL.Polarity.pi.coe = Π

@[instance_reducible]

instance PointwiseComposition.FFL.Polarity.instCoe {α : Type u_1} [SigmaSymbol α] [PiSymbol α] : Coe Polarity α

Equations

• PointwiseComposition.FFL.Polarity.instCoe = { coe := PointwiseComposition.FFL.Polarity.coe }

@[simp]

theorem PointwiseComposition.FFL.Polarity.coe_sigma {α : Type u_1} [SigmaSymbol α] [PiSymbol α] : Σ.coe = Σ

@[simp]

theorem PointwiseComposition.FFL.Polarity.coe_pi {α : Type u_1} [SigmaSymbol α] [PiSymbol α] : Π.coe = Π

inductive PointwiseComposition.FFL.SigmaPiDelta : Type

Data and laws for Sigma Pi Delta in FFL.

• sigma : SigmaPiDelta
• pi : SigmaPiDelta
• delta : SigmaPiDelta

@[instance_reducible]

instance PointwiseComposition.FFL.SigmaPiDelta.instSigmaSymbol : SigmaSymbol SigmaPiDelta

Equations

• PointwiseComposition.FFL.SigmaPiDelta.instSigmaSymbol = { sigma := PointwiseComposition.FFL.SigmaPiDelta.sigma }

@[instance_reducible]

instance PointwiseComposition.FFL.SigmaPiDelta.instPiSymbol : PiSymbol SigmaPiDelta

Equations

• PointwiseComposition.FFL.SigmaPiDelta.instPiSymbol = { pi := PointwiseComposition.FFL.SigmaPiDelta.pi }

@[instance_reducible]

instance PointwiseComposition.FFL.SigmaPiDelta.instDeltaSymbol : DeltaSymbol SigmaPiDelta

Equations

• PointwiseComposition.FFL.SigmaPiDelta.instDeltaSymbol = { delta := PointwiseComposition.FFL.SigmaPiDelta.delta }

def PointwiseComposition.FFL.SigmaPiDelta.alt : SigmaPiDelta → SigmaPiDelta

The alt construction in FFL.SigmaPiDelta.

Equations

• PointwiseComposition.FFL.SigmaPiDelta.sigma.alt = Π
• PointwiseComposition.FFL.SigmaPiDelta.pi.alt = Σ
• PointwiseComposition.FFL.SigmaPiDelta.delta.alt = ∆

theorem PointwiseComposition.FFL.SigmaPiDelta.eq_sigma : sigma = Σ

theorem PointwiseComposition.FFL.SigmaPiDelta.eq_pi : pi = Π

theorem PointwiseComposition.FFL.SigmaPiDelta.eq_delta : delta = ∆

@[simp]

theorem PointwiseComposition.FFL.SigmaPiDelta.alt_sigma : Σ.alt = Π

@[simp]

theorem PointwiseComposition.FFL.SigmaPiDelta.alt_pi : Π.alt = Σ

@[simp]

theorem PointwiseComposition.FFL.SigmaPiDelta.alt_delta : ∆.alt = ∆

@[simp]

theorem PointwiseComposition.FFL.SigmaPiDelta.alt_alt (Γ : SigmaPiDelta) : Γ.alt.alt = Γ

@[simp]

theorem PointwiseComposition.FFL.SigmaPiDelta.alt_coe (Γ : Polarity) : Γ.coe.alt = Γ.alt.coe

First-order quantifiers

class PointwiseComposition.FFL.FirstOrder.UnivQuantifier (α : ℕ → Type u_1) : Type u_1

Data and laws for Univ Quantifier in FFL.FirstOrder.

• all {n : ℕ} : α (n + 1) → α n

  The all construction in FFL.FirstOrder.UnivQuantifier.

def PointwiseComposition.FFL.FirstOrder.«term∀¹_» : Lean.ParserDescr

The «term∀¹ » construction in FFL.FirstOrder.

Equations

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

class PointwiseComposition.FFL.FirstOrder.ExsQuantifier (α : ℕ → Type u_1) : Type u_1

Data and laws for Exs Quantifier in FFL.FirstOrder.

• exs {n : ℕ} : α (n + 1) → α n

  The exs construction in FFL.FirstOrder.ExsQuantifier.

def PointwiseComposition.FFL.FirstOrder.«term∃¹_» : Lean.ParserDescr

The «term∃¹ » construction in FFL.FirstOrder.

Equations

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

class PointwiseComposition.FFL.FirstOrder.Quantifier (α : ℕ → Type u_1) extends PointwiseComposition.FFL.FirstOrder.UnivQuantifier α, PointwiseComposition.FFL.FirstOrder.ExsQuantifier α : Type u_1

Data and laws for Quantifier in FFL.FirstOrder.

• all {n : ℕ} : α (n + 1) → α n
• exs {n : ℕ} : α (n + 1) → α n

class PointwiseComposition.FFL.FirstOrder.LCWQ (α : ℕ → Type u_1) extends PointwiseComposition.FFL.FirstOrder.Quantifier α : Type u_1

Logical Connectives with Quantifiers.

• all {n : ℕ} : α (n + 1) → α n
• exs {n : ℕ} : α (n + 1) → α n
• connectives (n : ℕ) : LogicalConnective (α n)

  The connectives construction in FFL.FirstOrder.LCWQ.

• neutrals (n : ℕ) : LogicalNeutral (α n)

  The neutrals construction in FFL.FirstOrder.LCWQ.

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.instLogicalConnectiveOfLCWQ (α : ℕ → Type u_1) [LCWQ α] (n : ℕ) : LogicalConnective (α n)

Equations

• PointwiseComposition.FFL.FirstOrder.instLogicalConnectiveOfLCWQ α n = PointwiseComposition.FFL.FirstOrder.LCWQ.connectives n

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.instLogicalNeutralOfLCWQ (α : ℕ → Type u_1) [LCWQ α] (n : ℕ) : LogicalNeutral (α n)

Equations

• PointwiseComposition.FFL.FirstOrder.instLogicalNeutralOfLCWQ α n = PointwiseComposition.FFL.FirstOrder.LCWQ.neutrals n

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.instLCWQOfQuantifierOfLogicalConnectiveOfLogicalNeutral (α : ℕ → Type u_1) [Quantifier α] [(n : ℕ) → LogicalConnective (α n)] [(n : ℕ) → LogicalNeutral (α n)] : LCWQ α

Equations

• PointwiseComposition.FFL.FirstOrder.instLCWQOfQuantifierOfLogicalConnectiveOfLogicalNeutral α = { toQuantifier := inst✝², connectives := inferInstance, neutrals := inferInstance }

def PointwiseComposition.FFL.FirstOrder.allClosure {α : ℕ → Type u_1} [UnivQuantifier α] {n : ℕ} : α n → α 0

The all Closure construction in FFL.FirstOrder.

Equations

• ∀¹* a = a
• ∀¹* a = ∀¹* ∀¹ a

def PointwiseComposition.FFL.FirstOrder.«term∀¹*_» : Lean.ParserDescr

The universal closure of a formula.

Equations

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

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.allClosure_zero {α : ℕ → Type u_1} [UnivQuantifier α] (a : α 0) : ∀¹* a = a

theorem PointwiseComposition.FFL.FirstOrder.allClosure_succ {α : ℕ → Type u_1} [UnivQuantifier α] {n : ℕ} (a : α (n + 1)) : ∀¹* a = ∀¹* ∀¹ a

def PointwiseComposition.FFL.FirstOrder.allItr {α : ℕ → Type u_1} [UnivQuantifier α] {n : ℕ} (k : ℕ) : α (n + k) → α n

The all Itr construction in FFL.FirstOrder.

Equations

• ∀¹^[0] a = a
• ∀¹^[k.succ] a = ∀¹^[k] ∀¹ a

def PointwiseComposition.FFL.FirstOrder.«term∀¹^[_]_» : Lean.ParserDescr

The «term∀¹^[ ] » construction in FFL.FirstOrder.

Equations

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

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.allItr_zero {α : ℕ → Type u_1} [UnivQuantifier α] {n : ℕ} (a : α n) : ∀¹^[0] a = a

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.allItr_one {α : ℕ → Type u_1} [UnivQuantifier α] {n : ℕ} (a : α (n + 1)) : ∀¹^[1] a = ∀¹ a

theorem PointwiseComposition.FFL.FirstOrder.allItr_succ {α : ℕ → Type u_1} [UnivQuantifier α] {n k : ℕ} (a : α (n + (k + 1))) : ∀¹^[k + 1] a = ∀¹^[k] ∀¹ a

def PointwiseComposition.FFL.FirstOrder.exsClosure {α : ℕ → Type u_1} [ExsQuantifier α] {n : ℕ} : α n → α 0

The exs Closure construction in FFL.FirstOrder.

Equations

• ∃¹* a = a
• ∃¹* a = ∃¹* ∃¹ a

def PointwiseComposition.FFL.FirstOrder.«term∃¹*_» : Lean.ParserDescr

The existential closure of a formula.

Equations

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

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.exsClosure_zero {α : ℕ → Type u_1} [ExsQuantifier α] (a : α 0) : ∃¹* a = a

theorem PointwiseComposition.FFL.FirstOrder.exsClosure_succ {α : ℕ → Type u_1} [ExsQuantifier α] {n : ℕ} (a : α (n + 1)) : ∃¹* a = ∃¹* ∃¹ a

def PointwiseComposition.FFL.FirstOrder.exsItr {α : ℕ → Type u_1} [ExsQuantifier α] {n : ℕ} (k : ℕ) : α (n + k) → α n

The exs Itr construction in FFL.FirstOrder.

Equations

• ∃¹^[0] a = a
• ∃¹^[k.succ] a = ∃¹^[k] ∃¹ a

def PointwiseComposition.FFL.FirstOrder.«term∃¹^[_]_» : Lean.ParserDescr

Iterated application of k existential quantifiers.

Equations

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

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.exsItr_zero {α : ℕ → Type u_1} [ExsQuantifier α] {n : ℕ} (a : α n) : ∃¹^[0] a = a

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.exsItr_one {α : ℕ → Type u_1} [ExsQuantifier α] {n : ℕ} (a : α (n + 1)) : ∃¹^[1] a = ∃¹ a

theorem PointwiseComposition.FFL.FirstOrder.exsItr_succ {α : ℕ → Type u_1} [ExsQuantifier α] {n k : ℕ} (a : α (n + (k + 1))) : ∃¹^[k + 1] a = ∃¹^[k] ∃¹ a

def PointwiseComposition.FFL.FirstOrder.ball {α : ℕ → Type u_1} {n : ℕ} [UnivQuantifier α] [Arrow (α (n + 1))] (φ ψ : α (n + 1)) : α n

The ball construction in FFL.FirstOrder.

Equations

• (∀¹[φ] ψ) = ∀¹ (φ ⇒ₗ ψ)

def PointwiseComposition.FFL.FirstOrder.bexs {α : ℕ → Type u_1} {n : ℕ} [ExsQuantifier α] [Wedge (α (n + 1))] (φ ψ : α (n + 1)) : α n

The bexs construction in FFL.FirstOrder.

Equations

• (∃¹[φ] ψ) = ∃¹ φ ⋏ ψ

def PointwiseComposition.FFL.FirstOrder.«term∀¹[_]_» : Lean.ParserDescr

A bounded universal quantifier. ∀¹[φ] ψ is defined as ∀¹ (φ ⇒ₗ ψ).

Equations

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

def PointwiseComposition.FFL.FirstOrder.«term∃¹[_]_» : Lean.ParserDescr

A bounded existential quantifier. ∃¹[φ] ψ is defined as ∃¹ (φ ⋏ ψ).

Equations

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

def PointwiseComposition.FFL.Polarity.quant {α : ℕ → Type u_1} [FirstOrder.UnivQuantifier α] [FirstOrder.ExsQuantifier α] {n : ℕ} : Polarity → α (n + 1) → α n

The quant construction in FFL.Polarity.

Equations

• PointwiseComposition.FFL.Polarity.sigma.quant = PointwiseComposition.FFL.FirstOrder.ExsQuantifier.exs
• PointwiseComposition.FFL.Polarity.pi.quant = PointwiseComposition.FFL.FirstOrder.UnivQuantifier.all

@[simp]

theorem PointwiseComposition.FFL.Polarity.quant_sigma {α : ℕ → Type u_1} [FirstOrder.UnivQuantifier α] [FirstOrder.ExsQuantifier α] {n : ℕ} (φ : α (n + 1)) : Σ.quant φ = ∃¹ φ

@[simp]

theorem PointwiseComposition.FFL.Polarity.quant_pi {α : ℕ → Type u_1} [FirstOrder.UnivQuantifier α] [FirstOrder.ExsQuantifier α] {n : ℕ} (φ : α (n + 1)) : Π.quant φ = ∀¹ φ

def PointwiseComposition.FFL.Polarity.quantItr {α : ℕ → Type u_1} [FirstOrder.UnivQuantifier α] [FirstOrder.ExsQuantifier α] (Γ : Polarity) (k : ℕ) {n : ℕ} : α (n + k) → α n

Prefixes k alternating quantifiers starting with Γ.

Equations

• Γ.quantItr 0 x✝ = x✝
• Γ.quantItr k.succ x✝ = Γ.quant (Γ.alt.quantItr k (cast ⋯ x✝))

@[simp]

theorem PointwiseComposition.FFL.Polarity.quantItr_zero {α : ℕ → Type u_1} [FirstOrder.UnivQuantifier α] [FirstOrder.ExsQuantifier α] {n : ℕ} {Γ : Polarity} (φ : α n) : Γ.quantItr 0 φ = φ

@[simp]

theorem PointwiseComposition.FFL.Polarity.quantItr_one {α : ℕ → Type u_1} [FirstOrder.UnivQuantifier α] [FirstOrder.ExsQuantifier α] {n : ℕ} {Γ : Polarity} (φ : α (n + 1)) : Γ.quantItr 1 φ = Γ.quant φ

theorem PointwiseComposition.FFL.Polarity.quantItr_succ {α : ℕ → Type u_1} [FirstOrder.UnivQuantifier α] [FirstOrder.ExsQuantifier α] {n : ℕ} {Γ : Polarity} {k : ℕ} (φ : α (n + (k + 1))) : Γ.quantItr (k + 1) φ = Γ.quant (Γ.alt.quantItr k (cast ⋯ φ))

theorem PointwiseComposition.FFL.Polarity.cast_quant {α : ℕ → Type u_1} [FirstOrder.UnivQuantifier α] [FirstOrder.ExsQuantifier α] {m₁ m₂ : ℕ} (h : m₁ = m₂) (Γ : Polarity) (φ : α (m₁ + 1)) : cast ⋯ (Γ.quant φ) = Γ.quant (cast ⋯ φ)

theorem PointwiseComposition.FFL.Polarity.quantItr_succ' {α : ℕ → Type u_1} [FirstOrder.UnivQuantifier α] [FirstOrder.ExsQuantifier α] {n : ℕ} {Γ : Polarity} {k : ℕ} (φ : α (n + (k + 1))) : Γ.quantItr (k + 1) φ = Γ.quantItr k ((Γ.altItr k).quant φ)

Second-order quantifiers

class PointwiseComposition.FFL.SecondOrder.UnivQuantifier (α : ℕ → ℕ → Type u_1) : Type u_1

Data and laws for Univ Quantifier in FFL.SecondOrder.

• all₁ {m n : ℕ} : α (m + 1) n → α m n

  The all₁ construction in FFL.SecondOrder.UnivQuantifier.

def PointwiseComposition.FFL.SecondOrder.«term∀²_» : Lean.ParserDescr

The «term∀² » construction in FFL.SecondOrder.

Equations

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

class PointwiseComposition.FFL.SecondOrder.ExsQuantifier (α : ℕ → ℕ → Type u_1) : Type u_1

Data and laws for Exs Quantifier in FFL.SecondOrder.

• exs₁ {m n : ℕ} : α (m + 1) n → α m n

  The exs₁ construction in FFL.SecondOrder.ExsQuantifier.

def PointwiseComposition.FFL.SecondOrder.«term∃²_» : Lean.ParserDescr

The «term∃² » construction in FFL.SecondOrder.

Equations

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

class PointwiseComposition.FFL.SecondOrder.Quantifier (α : ℕ → ℕ → Type u_1) extends PointwiseComposition.FFL.SecondOrder.UnivQuantifier α, PointwiseComposition.FFL.SecondOrder.ExsQuantifier α : Type u_1

Data and laws for Quantifier in FFL.SecondOrder.

• all₁ {m n : ℕ} : α (m + 1) n → α m n
• exs₁ {m n : ℕ} : α (m + 1) n → α m n

class PointwiseComposition.FFL.SecondOrder.LCWQ (α : ℕ → ℕ → Type u_1) extends PointwiseComposition.FFL.SecondOrder.Quantifier α : Type u_1

Logical Connectives with Quantifiers.

• all₁ {m n : ℕ} : α (m + 1) n → α m n
• exs₁ {m n : ℕ} : α (m + 1) n → α m n
• firstOrder (m : ℕ) : FirstOrder.LCWQ (α m)

  The first Order construction in FFL.SecondOrder.LCWQ.

@[instance_reducible]

instance PointwiseComposition.FFL.SecondOrder.instLCWQOfLCWQ (α : ℕ → ℕ → Type u_1) [LCWQ α] (m : ℕ) : FirstOrder.LCWQ (α m)

Equations

• PointwiseComposition.FFL.SecondOrder.instLCWQOfLCWQ α m = PointwiseComposition.FFL.SecondOrder.LCWQ.firstOrder m

@[instance_reducible]

instance PointwiseComposition.FFL.SecondOrder.instLCWQOfQuantifierOfLCWQ (α : ℕ → ℕ → Type u_1) [Quantifier α] [(m : ℕ) → FirstOrder.LCWQ (α m)] : LCWQ α

Equations

• PointwiseComposition.FFL.SecondOrder.instLCWQOfQuantifierOfLCWQ α = { toQuantifier := inst✝¹, firstOrder := inferInstance }

def PointwiseComposition.FFL.SecondOrder.allClosure {α : ℕ → ℕ → Type u_1} [UnivQuantifier α] {n m : ℕ} : α m n → α 0 n

The all Closure construction in FFL.SecondOrder.

Equations

• ∀²* a = a
• ∀²* a = ∀²* ∀² a

def PointwiseComposition.FFL.SecondOrder.«term∀²*_» : Lean.ParserDescr

The «term∀²* » construction in FFL.SecondOrder.

Equations

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

@[simp]

theorem PointwiseComposition.FFL.SecondOrder.allClosure_zero {α : ℕ → ℕ → Type u_1} [UnivQuantifier α] {n : ℕ} (a : α 0 n) : ∀²* a = a

theorem PointwiseComposition.FFL.SecondOrder.allClosure_succ {α : ℕ → ℕ → Type u_1} [UnivQuantifier α] {n : ℕ} (a : α (n + 1) n) : ∀²* a = ∀²* ∀² a

def PointwiseComposition.FFL.SecondOrder.allItr {α : ℕ → ℕ → Type u_1} [UnivQuantifier α] {m n : ℕ} (k : ℕ) : α (m + k) n → α m n

The all Itr construction in FFL.SecondOrder.

Equations

• ∀²^[0] a = a
• ∀²^[k.succ] a = ∀²^[k] ∀² a

def PointwiseComposition.FFL.SecondOrder.«term∀²^[_]_» : Lean.ParserDescr

The «term∀²^[ ] » construction in FFL.SecondOrder.

Equations

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

@[simp]

theorem PointwiseComposition.FFL.SecondOrder.allItr_zero {α : ℕ → ℕ → Type u_1} [UnivQuantifier α] {m n : ℕ} (a : α m n) : ∀²^[0] a = a

@[simp]

theorem PointwiseComposition.FFL.SecondOrder.allItr_one {α : ℕ → ℕ → Type u_1} [UnivQuantifier α] {m n : ℕ} (a : α (m + 1) n) : ∀²^[1] a = ∀² a

theorem PointwiseComposition.FFL.SecondOrder.allItr_succ {α : ℕ → ℕ → Type u_1} [UnivQuantifier α] {m n k : ℕ} (a : α (m + (k + 1)) n) : ∀²^[k + 1] a = ∀²^[k] ∀² a

def PointwiseComposition.FFL.SecondOrder.exsClosure {α : ℕ → ℕ → Type u_1} [ExsQuantifier α] {n m : ℕ} : α m n → α 0 n

The exs Closure construction in FFL.SecondOrder.

Equations

• ∃²* a = a
• ∃²* a = ∃²* ∃² a

def PointwiseComposition.FFL.SecondOrder.«term∃²*_» : Lean.ParserDescr

The «term∃²* » construction in FFL.SecondOrder.

Equations

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

@[simp]

theorem PointwiseComposition.FFL.SecondOrder.exsClosure_zero {α : ℕ → ℕ → Type u_1} [ExsQuantifier α] {n : ℕ} (a : α 0 n) : ∃²* a = a

theorem PointwiseComposition.FFL.SecondOrder.exsClosure_succ {α : ℕ → ℕ → Type u_1} [ExsQuantifier α] {m n : ℕ} (a : α (m + 1) n) : ∃²* a = ∃²* ∃² a

def PointwiseComposition.FFL.SecondOrder.exsItr {α : ℕ → ℕ → Type u_1} [ExsQuantifier α] {m n : ℕ} (k : ℕ) : α (m + k) n → α m n

The exs Itr construction in FFL.SecondOrder.

Equations

• ∃²^[0] a = a
• ∃²^[k.succ] a = ∃²^[k] ∃² a

def PointwiseComposition.FFL.SecondOrder.«term∃²^[_]_» : Lean.ParserDescr

The «term∃²^[ ] » construction in FFL.SecondOrder.

Equations

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

@[simp]

theorem PointwiseComposition.FFL.SecondOrder.exsItr_zero {α : ℕ → ℕ → Type u_1} [ExsQuantifier α] {m n : ℕ} (a : α m n) : ∃²^[0] a = a

@[simp]

theorem PointwiseComposition.FFL.SecondOrder.exsItr_one {α : ℕ → ℕ → Type u_1} [ExsQuantifier α] {m n : ℕ} (a : α (m + 1) n) : ∃²^[1] a = ∃² a

theorem PointwiseComposition.FFL.SecondOrder.exsItr_succ {α : ℕ → ℕ → Type u_1} [ExsQuantifier α] {m n k : ℕ} (a : α (m + (k + 1)) n) : ∃²^[k + 1] a = ∃²^[k] ∃² a

def PointwiseComposition.FFL.SecondOrder.ball {α : ℕ → ℕ → Type u_1} {m n : ℕ} [UnivQuantifier α] [Arrow (α (m + 1) n)] (φ ψ : α (m + 1) n) : α m n

The ball construction in FFL.SecondOrder.

Equations

• (∀²[φ] ψ) = ∀² (φ ⇒ₗ ψ)

def PointwiseComposition.FFL.SecondOrder.bexs {α : ℕ → ℕ → Type u_1} {m n : ℕ} [ExsQuantifier α] [Wedge (α (m + 1) n)] (φ ψ : α (m + 1) n) : α m n

The bexs construction in FFL.SecondOrder.

Equations

• (∃²[φ] ψ) = ∃² φ ⋏ ψ

def PointwiseComposition.FFL.SecondOrder.«term∀²[_]_» : Lean.ParserDescr

The «term∀²[ ] » construction in FFL.SecondOrder.

Equations

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

def PointwiseComposition.FFL.SecondOrder.«term∃²[_]_» : Lean.ParserDescr

The «term∃²[ ] » construction in FFL.SecondOrder.

Equations

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