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.

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.