Notation classes for lattice operations

In this file we introduce typeclasses and definitions for lattice operations.

Main definitions

• the ⊔ notation is used for Max since November 2024
• the ⊓ notation is used for Min since November 2024
• HasCompl: type class for the ᶜ notation
• Top: type class for the ⊤ notation
• Bot: type class for the ⊥ notation

Notations

• x ⊔ y: lattice join operation;
• x ⊓ y: lattice meet operation;
• xᶜ: complement in a lattice;

class HasCompl (α : Type u_1) : Type u_1

Set / lattice complement

• compl : α → α

  Set / lattice complement

Instances

• IsIdempotentElem.instHasComplSubtype
• MeasurableSet.Subtype.instHasCompl
• Pi.hasCompl
• Prod.instHasCompl
• Prop.hasCompl
• Set.instHasCompl
• TopologicalSpace.Clopens.instHasCompl
• TopologicalSpace.CompactOpens.instHasCompl
• ULift.instHasCompl

def «term_ᶜ» : Lean.TrailingParserDescr

Set / lattice complement

Equations

• «term_ᶜ» = Lean.ParserDescr.trailingNode `«term_ᶜ» 1024 1024 (Lean.ParserDescr.symbol "ᶜ")

Sup and Inf

@[deprecated Max (since := "2024-11-06")]

class Sup (α : Type u_1) : Type u_1

Typeclass for the ⊔ (\lub) notation

• sup : α → α → α

  Least upper bound (\lub notation)

theorem Sup.ext {α : Type u_1} {x y : Sup α} (sup : sup = sup) : x = y

@[deprecated Min (since := "2024-11-06")]

class Inf (α : Type u_1) : Type u_1

Typeclass for the ⊓ (\glb) notation

• inf : α → α → α

  Greatest lower bound (\glb notation)

theorem Inf.ext {α : Type u_1} {x y : Inf α} (inf : inf = inf) : x = y

theorem Min.ext {α : Type u} {x y : Min α} (min : min = min) : x = y

theorem Max.ext {α : Type u} {x y : Max α} (max : max = max) : x = y

def «term_⊔_» : Lean.TrailingParserDescr

The maximum operation: max x y.

Equations

• «term_⊔_» = Lean.ParserDescr.trailingNode `«term_⊔_» 68 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊔ ") (Lean.ParserDescr.cat `term 69))

def «term_⊓_» : Lean.TrailingParserDescr

The minimum operation: min x y.

Equations

• «term_⊓_» = Lean.ParserDescr.trailingNode `«term_⊓_» 69 69 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊓ ") (Lean.ParserDescr.cat `term 70))

class HImp (α : Type u_1) : Type u_1

Syntax typeclass for Heyting implication ⇨.

• himp : α → α → α

  Heyting implication ⇨

Instances

• MeasurableSet.Subtype.instHImp
• Pi.instHImpForall
• Prod.instHImp
• TopologicalSpace.Clopens.instHImp
• TopologicalSpace.CompactOpens.instHImp

class HNot (α : Type u_1) : Type u_1

Syntax typeclass for Heyting negation ￢.

The difference between HasCompl and HNot is that the former belongs to Heyting algebras, while the latter belongs to co-Heyting algebras. They are both pseudo-complements, but compl underestimates while HNot overestimates. In boolean algebras, they are equal. See hnot_eq_compl.

• hnot : α → α

  Heyting negation ￢

Instances

• Pi.instHNotForall
• Prod.instHNot

def «term_⇨_» : Lean.TrailingParserDescr

Heyting implication

Equations

• «term_⇨_» = Lean.ParserDescr.trailingNode `«term_⇨_» 60 61 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇨ ") (Lean.ParserDescr.cat `term 60))

def «term￢_» : Lean.ParserDescr

Heyting negation

Equations

• «term￢_» = Lean.ParserDescr.node `«term￢_» 72 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "￢") (Lean.ParserDescr.cat `term 72))

class Top (α : Type u_1) : Type u_1

Typeclass for the ⊤ (\top) notation

• top : α

  The top (⊤, \top) element

Instances

• AddGroupTopology.instTop
• AddSubgroup.instTop
• AddSubmonoid.instTop
• AddSubsemigroup.instTop
• Associates.instTopOfZero
• ConvexCone.instTop
• EReal.instTop
• Filter.Germ.instTop
• Filter.instTop
• GroupTopology.instTop
• InfHom.instTop
• LowerSet.instTop
• MeasurableSet.Subtype.instTop
• MeasureTheory.Filtration.instTop
• NonUnitalSubring.instTop
• NonUnitalSubsemiring.instTop
• OrderDual.instTop
• OrderHom.instTopOrderHom
• Pi.instTopForall
• Prod.instTop
• Subfield.instTop
• Subgroup.instTop
• Submodule.instTop
• Submonoid.instTop
• Subring.instTop
• Subsemigroup.instTop
• Subsemiring.instTop
• SupHom.instTop
• TopologicalSpace.Clopens.instTop
• TopologicalSpace.CompactOpens.instTop
• TopologicalSpace.Compacts.instTopOfCompactSpace
• TopologicalSpace.NonemptyCompacts.instTopOfCompactSpaceOfNonempty
• TopologicalSpace.PositiveCompacts.instTopOfCompactSpaceOfNonempty
• TwoSidedIdeal.instTop
• ULift.instTop
• UpperSet.instTop
• WithBot.instTop
• WithTop.top
• instENNRealTop
• instENatTop
• instTopUniformSpace
• sInfHom.instTop

theorem Top.ext {α : Type u_1} {x y : Top α} (top : ⊤ = ⊤) : x = y

class Bot (α : Type u_1) : Type u_1

Typeclass for the ⊥ (\bot) notation

• bot : α

  The bot (⊥, \bot) element

Instances

• AddGroupTopology.instBot
• AddSubgroup.instBot
• AddSubmonoid.instBot
• AddSubsemigroup.instBot
• Associates.instBot
• ConvexCone.instBot
• Filter.Germ.instBot
• Filter.instBot
• GroupTopology.instBot
• InfHom.instBot
• LinearPMap.bot
• LowerSet.instBot
• MeasurableSet.Subtype.instBot
• MeasureTheory.Filtration.instBot
• MeasureTheory.OuterMeasure.instBot
• NonUnitalSubring.instBot
• NonUnitalSubsemiring.instBot
• OrderDual.instBot
• OrderHom.instBotOfOrderBot
• Pi.instBotForall
• Prod.instBot
• SubAddAction.instBot
• SubMulAction.instBot
• Subgroup.instBot
• Submodule.instBot
• Submonoid.instBot
• Subring.instBot
• Subsemigroup.instBot
• Subsemiring.instBot
• SupHom.instBot
• TopologicalSpace.Clopens.instBot
• TopologicalSpace.CompactOpens.instBot
• TopologicalSpace.Compacts.instBot
• TwoSidedIdeal.instBot
• ULift.instBot
• UpperSet.instBot
• WithBot.bot
• WithTop.instBot
• instBotUniformSpace
• instENatBot
• instERealBot
• sSupHom.instBot

theorem Bot.ext {α : Type u_1} {x y : Bot α} (bot : ⊥ = ⊥) : x = y

def «term⊤» : Lean.ParserDescr

The top (⊤, \top) element

Equations

• «term⊤» = Lean.ParserDescr.node `«term⊤» 1024 (Lean.ParserDescr.symbol "⊤")

def «term⊥» : Lean.ParserDescr

The bot (⊥, \bot) element

Equations

• «term⊥» = Lean.ParserDescr.node `«term⊥» 1024 (Lean.ParserDescr.symbol "⊥")

@[instance 100]

instance top_nonempty (α : Type u_1) [Top α] : Nonempty α

@[instance 100]

instance bot_nonempty (α : Type u_1) [Bot α] : Nonempty α