# 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.

Pretty printer defined by `notation3`

command.

## Equations

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

## Instances For

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))

## Instances For

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.