20.1. Basic language🔗

To say "Let X be a topological space", we write

variable (X : Type*) [TopologicalSpace X]

This comes with a predicate IsOpen on Set X telling us which subsets of X are open.

IsOpen.{u} {X : Type u} [TopologicalSpace X] : Set X → Prop#check IsOpen

So to state that the union of two open subsets is open, we would write

example (hs : IsOpen s) (ht : IsOpen t) : IsOpen (s ∪ t) :=
  IsOpen.union hs ht

Some other common properties of subsets are: