Set notation for order operations

This file allows the use of ⊆ notation while the underlying constant is ≤. Similarly for ⊂/<, ⊇/≥ and ⊃/>.

A new copy of the a ⊆ b syntax is declared, which overwrites the original one. To elaborate this notation, a and b are elaborated, and if the type of a and b is tagged with @[use_set_notation_for_order], LE.le is used instead of Subset. A new delaborator for LE.le is also added so that a ≤ b prints as a ⊆ b whenever the type is tagged with @[use_set_notation_for_order].

This tag is used for Set, Finset, PSet and ZFSet. It is not used for Multiset and List, since they have both ≤ and ⊆ defined on them, with different meanings.

TODO: Unify more order operations suh as ∪/⊔ and ∩/⊓.

Delaboration

def Mathlib.Meta.SetNotationForOrder.delabLe : Lean.PrettyPrinter.Delaborator.Delab

Delaborate x ≤ y into x ⊆ y if the type is tagged with @[use_set_notation_for_order].

Equations

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

def Mathlib.Meta.SetNotationForOrder.delabLt : Lean.PrettyPrinter.Delaborator.Delab

Delaborate x < y into x ⊂ y if the type is tagged with @[use_set_notation_for_order].

Equations

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

def Mathlib.Meta.SetNotationForOrder.delabGe : Lean.PrettyPrinter.Delaborator.Delab

Delaborate x ≥ y into x ⊇ y if the type is tagged with @[use_set_notation_for_order].

Equations

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

def Mathlib.Meta.SetNotationForOrder.delabGt : Lean.PrettyPrinter.Delaborator.Delab

Delaborate x > y into x ⊃ y if the type is tagged with @[use_set_notation_for_order].

Equations

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

Elaboration

opaque Mathlib.Meta.SetNotationForOrder.SubsetElabAux {α : Type u} : α → α → Prop

This relation is an implementation detail of the ⊆ elaborator.

def Mathlib.Meta.SetNotationForOrder.subsetStx' : Lean.TrailingParserDescr

Subset relation: a ⊆ b. For types tagged with @[use_set_notation_for_order], the relation LE.le is used instead of Subset. The hover info shows which one is used.

Conventions for notations in identifiers:

• The recommended spelling of ⊆ in identifiers is subset.

Equations

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

def Mathlib.Meta.SetNotationForOrder.ssubsetStx' : Lean.TrailingParserDescr

Strict subset relation: a ⊂ b. For types tagged with @[use_set_notation_for_order], the relation LT.lt is used instead of SSubset. The hover info shows which one is used.

Conventions for notations in identifiers:

• The recommended spelling of ⊂ in identifiers is ssubset.

Equations

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

def Mathlib.Meta.SetNotationForOrder.supsetStx' : Lean.TrailingParserDescr

Superset relation: a ⊇ b. For types tagged with @[use_set_notation_for_order], the relation GE.ge is used instead of Superset. The hover info shows which one is used.

Conventions for notations in identifiers:

• The recommended spelling of ⊇ in identifiers is superset.

Equations

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

def Mathlib.Meta.SetNotationForOrder.ssupsetStx' : Lean.TrailingParserDescr

Strict superset relation: a ⊃ b. For types tagged with @[use_set_notation_for_order], the relation GT.gt is used instead of SSuperset. The hover info shows which one is used.

Conventions for notations in identifiers:

• The recommended spelling of ⊃ in identifiers is ssuperset.

Equations

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

def Mathlib.Meta.SetNotationForOrder.elabSubsetStx' : Lean.Elab.Term.TermElab

Elaborator for x ⊆ y notation.

Equations

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

def Mathlib.Meta.SetNotationForOrder.elabSSubsetStx' : Lean.Elab.Term.TermElab

Elaborator for x ⊂ y notation.

Equations

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

def Mathlib.Meta.SetNotationForOrder.elabSupsetStx' : Lean.Elab.Term.TermElab

Elaborator for x ⊇ y notation.

Equations

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

def Mathlib.Meta.SetNotationForOrder.elabSSupsetStx' : Lean.Elab.Term.TermElab

Elaborator for x ⊃ y notation.

Equations

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

def Mathlib.Meta.SetNotationForOrder.«binderPred⊆_» : Lean.ParserDescr

Declare ∀ x ⊆ y, ... as syntax for ∀ x, x ⊆ y → ... and ∃ x ⊆ y, ... as syntax for ∃ x, x ⊆ y ∧ ...

Equations

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

def Mathlib.Meta.SetNotationForOrder.«binderPred⊂_» : Lean.ParserDescr

Declare ∀ x ⊂ y, ... as syntax for ∀ x, x ⊂ y → ... and ∃ x ⊂ y, ... as syntax for ∃ x, x ⊂ y ∧ ...

Equations

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

def Mathlib.Meta.SetNotationForOrder.«binderPred⊇_» : Lean.ParserDescr

Declare ∀ x ⊇ y, ... as syntax for ∀ x, x ⊇ y → ... and ∃ x ⊇ y, ... as syntax for ∃ x, x ⊇ y ∧ ...

Equations

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

def Mathlib.Meta.SetNotationForOrder.«binderPred⊃_» : Lean.ParserDescr

Declare ∀ x ⊃ y, ... as syntax for ∀ x, x ⊃ y → ... and ∃ x ⊃ y, ... as syntax for ∃ x, x ⊃ y ∧ ...

Equations

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