Set Notation

This file defines two pieces of scoped notation related to sets and subtypes.

The first is a coercion; for each α : Type* and s : Set α, (↑) : Set s → Set α is the function coercing t : Set s into a set in the ambient type; i.e. ↑t = Subtype.val '' t.

The second, for s t : Set α, is the notation s ↓∩ t, which denotes the intersection of s and t as a set in Set s.

These notations are developed further in Data.Set.Functor and Data.Set.Subset respectively. They are defined here separately so that this file can be added as an exception to the shake linter and can thus be imported without a linting false positive when only the notation is desired.

def Set.Notation.«term_↓∩_».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

def Set.Notation.«term_↓∩_» : Lean.TrailingParserDescr

Given two sets A and B, A ↓∩ B denotes the intersection of A and B as a set in Set A.

The notation is short for ((↑) ⁻¹' B : Set A), while giving hints to the elaborator that both A and B are terms of Set α for the same α. This set is the same as {x : ↑A | ↑x ∈ B}.

Equations

• Set.Notation.«term_↓∩_» = Lean.ParserDescr.trailingNode `Set.Notation.term_↓∩_ 1022 67 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↓∩ ") (Lean.ParserDescr.cat `term 67))

instance Set.Notation.instCoeHeadElem {α : Type u_1} {s : Set α} : CoeHead (Set ↑s) (Set α)

Coercion using (Subtype.val '' ·)

Equations

• Set.Notation.instCoeHeadElem = { coe := fun (t : Set ↑s) => Subtype.val '' t }

def Set.Notation.delab_set_image_subtype : Lean.PrettyPrinter.Delaborator.Delab

If the Set.Notation namespace is open, sets of a subtype coerced to the ambient type are represented with ↑.

Equations

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