Supporting results for pointwise provable equality.

Supplemental notation classes

Heterogeneous notation classes

class PointwiseComposition.FFL.HTilde (α : Type u_1) (β : outParam (Type u_2)) : Type (max u_1 u_2)

Data and laws for HTilde in FFL.

• hTilde : α → β

  The h Tilde construction in FFL.HTilde.

def PointwiseComposition.FFL.«term∼_» : Lean.ParserDescr

The «term∼ » construction in FFL.

Equations

• PointwiseComposition.FFL.«term∼_» = Lean.ParserDescr.node `PointwiseComposition.FFL.«term∼_» 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∼") (Lean.ParserDescr.cat `term 75))

class PointwiseComposition.FFL.HArrow (α : Type u_1) (β : Type u_2) (γ : outParam (Type u_3)) : Type (max (max u_1 u_2) u_3)

Data and laws for HArrow in FFL.

• hArrow : α → β → γ

  The h Arrow construction in FFL.HArrow.

def PointwiseComposition.FFL.«term_⇒ₗ_» : Lean.TrailingParserDescr

The «term ⇒ₗ » construction in FFL.

Equations

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

class PointwiseComposition.FFL.HWedge (α : Type u_1) (β : Type u_2) (γ : outParam (Type u_3)) : Type (max (max u_1 u_2) u_3)

Data and laws for HWedge in FFL.

• hWedge : α → β → γ

  The h Wedge construction in FFL.HWedge.

def PointwiseComposition.FFL.«term_⋏_» : Lean.TrailingParserDescr

The «term ⋏ » construction in FFL.

Equations

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

class PointwiseComposition.FFL.HVee (α : Type u_1) (β : Type u_2) (γ : outParam (Type u_3)) : Type (max (max u_1 u_2) u_3)

Data and laws for HVee in FFL.

• hVee : α → β → γ

  The h Vee construction in FFL.HVee.

def PointwiseComposition.FFL.«term_⋎_» : Lean.TrailingParserDescr

The «term ⋎ » construction in FFL.

Equations

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

Homogeneous notation classes

class PointwiseComposition.FFL.Tilde (α : Type u_1) : Type u_1

Data and laws for Tilde in FFL.

• tilde : α → α

  The tilde construction in FFL.Tilde.

class PointwiseComposition.FFL.Arrow (α : Type u_1) : Type u_1

Data and laws for Arrow in FFL.

• arrow : α → α → α

  The arrow construction in FFL.Arrow.

class PointwiseComposition.FFL.Wedge (α : Type u_1) : Type u_1

Data and laws for Wedge in FFL.

• wedge : α → α → α

  The wedge construction in FFL.Wedge.

class PointwiseComposition.FFL.Vee (α : Type u_1) : Type u_1

Data and laws for Vee in FFL.

• vee : α → α → α

  The vee construction in FFL.Vee.

@[instance_reducible, defaultInstance 1000]

instance PointwiseComposition.FFL.Tilde.instHTilde {α : Type u_1} [Tilde α] : HTilde α α

Equations

• PointwiseComposition.FFL.Tilde.instHTilde = { hTilde := PointwiseComposition.FFL.Tilde.tilde }

@[instance_reducible, defaultInstance 1000]

instance PointwiseComposition.FFL.Arrow.instHArrow {α : Type u_1} [Arrow α] : HArrow α α α

Equations

• PointwiseComposition.FFL.Arrow.instHArrow = { hArrow := PointwiseComposition.FFL.Arrow.arrow }

@[instance_reducible, defaultInstance 1000]

instance PointwiseComposition.FFL.Wedge.instHWedge {α : Type u_1} [Wedge α] : HWedge α α α

Equations

• PointwiseComposition.FFL.Wedge.instHWedge = { hWedge := PointwiseComposition.FFL.Wedge.wedge }

@[instance_reducible, defaultInstance 1000]

instance PointwiseComposition.FFL.Vee.instHVee {α : Type u_1} [Vee α] : HVee α α α

Equations

• PointwiseComposition.FFL.Vee.instHVee = { hVee := PointwiseComposition.FFL.Vee.vee }

class PointwiseComposition.FFL.Box (α : Type u_1) : Type u_1

Data and laws for Box in FFL.

• box : α → α

  The box construction in FFL.Box.

def PointwiseComposition.FFL.«term□_» : Lean.ParserDescr

The «term□ » construction in FFL.

Equations

• PointwiseComposition.FFL.«term□_» = Lean.ParserDescr.node `PointwiseComposition.FFL.«term□_» 76 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "□") (Lean.ParserDescr.cat `term 76))

class PointwiseComposition.FFL.Dia (α : Type u_1) : Type u_1

Data and laws for Dia in FFL.

• dia : α → α

  The dia construction in FFL.Dia.

def PointwiseComposition.FFL.«term◇_» : Lean.ParserDescr

The «term◇ » construction in FFL.

Equations

• PointwiseComposition.FFL.«term◇_» = Lean.ParserDescr.node `PointwiseComposition.FFL.«term◇_» 76 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "◇") (Lean.ParserDescr.cat `term 76))

class PointwiseComposition.FFL.Rhd (α : Type u_1) : Type u_1

Data and laws for Rhd in FFL.

• rhd : α → α → α

  The rhd construction in FFL.Rhd.

def PointwiseComposition.FFL.«term_▷_» : Lean.TrailingParserDescr

The «term ▷ » construction in FFL.

Equations

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

class PointwiseComposition.FFL.Exp (α : Type u_1) : Type u_1

Data and laws for Exp in FFL.

• exp : α → α

  The exp construction in FFL.Exp.

class PointwiseComposition.FFL.Superexp (α : Type u_1) : Type u_1

Data and laws for Superexp in FFL.

• superexp : α → α

  The superexp construction in FFL.Superexp.

class PointwiseComposition.FFL.Smash (α : Type u_1) : Type u_1

Data and laws for Smash in FFL.

• smash : α → α → α

  The smash construction in FFL.Smash.

def PointwiseComposition.FFL.«term_⊛_» : Lean.TrailingParserDescr

The «term ⊛ » construction in FFL.

Equations

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

class PointwiseComposition.FFL.Length (α : Type u_1) : Type u_1

Data and laws for Length in FFL.

• length : α → α

  The length construction in FFL.Length.

def PointwiseComposition.FFL.«term‖_‖» : Lean.ParserDescr

The «term‖ ‖» construction in FFL.

Equations

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

class PointwiseComposition.FFL.GödelQuote (α : Sort u_1) (β : Sort u_2) : Sort (max (max 1 u_1) u_2)

Coding objects into syntactic objects (e.g. natural numbers, first-order terms)

• quote : α → β

  The quote construction in FFL.GödelQuote.

def PointwiseComposition.FFL.«term⌜_⌝» : Lean.ParserDescr

The «term⌜ ⌝» construction in FFL.

Equations

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

class PointwiseComposition.FFL.SigmaSymbol (α : Type u_1) : Type u_1

Data and laws for Sigma Symbol in FFL.

• sigma : α

  The sigma construction in FFL.SigmaSymbol.

class PointwiseComposition.FFL.PiSymbol (α : Type u_1) : Type u_1

Data and laws for Pi Symbol in FFL.

• pi : α

  The pi construction in FFL.PiSymbol.

class PointwiseComposition.FFL.DeltaSymbol (α : Type u_1) : Type u_1

Data and laws for Delta Symbol in FFL.

• delta : α

  The delta construction in FFL.DeltaSymbol.

def PointwiseComposition.FFL.«termΣ» : Lean.ParserDescr

The «termΣ» construction in FFL.

Equations

• PointwiseComposition.FFL.«termΣ» = Lean.ParserDescr.node `PointwiseComposition.FFL.«termΣ» 1024 (Lean.ParserDescr.symbol "Σ")

def PointwiseComposition.FFL.«termΠ» : Lean.ParserDescr

The «termΠ» construction in FFL.

Equations

• PointwiseComposition.FFL.«termΠ» = Lean.ParserDescr.node `PointwiseComposition.FFL.«termΠ» 1024 (Lean.ParserDescr.symbol "Π")

def PointwiseComposition.FFL.«term∆» : Lean.ParserDescr

The «term∆» construction in FFL.

Equations

• PointwiseComposition.FFL.«term∆» = Lean.ParserDescr.node `PointwiseComposition.FFL.«term∆» 1024 (Lean.ParserDescr.symbol "∆")