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 such as iUnion/iSup and sUnion and sSup

class UsesSetNotationForOrder (α : Type u_1) : Type

UsesSetNotationForOrder is used to track whether a type is tagged with @[use_set_notation_for_order].

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.

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

Delaborate max 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.delabMin : Lean.PrettyPrinter.Delaborator.Delab

Delaborate min 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.

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

This operation 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.unionStx' : Lean.TrailingParserDescr

a ∪ b is the union of a and b. For types tagged with @[use_set_notation_for_order], the function Max.max is used instead of Union.union. The hover info shows which one is used.

Conventions for notations in identifiers:

• The recommended spelling of ∪ in identifiers is union.

Equations

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

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

a ∩ b is the intersection of a and b. For types tagged with @[use_set_notation_for_order], the function Min.min is used instead of Inter.inter. The hover info shows which one is used.

Conventions for notations in identifiers:

• The recommended spelling of ∩ in identifiers is inter.

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.elabUnionStx' : 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.elabInterStx' : 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.

Dot-notation namespace linter

def Mathlib.Meta.SetNotationForOrder.subsetDotNotationLinter : Batteries.Tactic.Lint.Linter

A temporary linter to help adapt to @[set_notation_for_order]. It gives a warning when a lemma is in the wrong namespace for dot-notation.

Equations

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

Lemma translation