Zulip Chat Archive

Stream: general

Topic: pure

Kenny Lau (Oct 02 2018 at 19:56):

what is pure?

Patrick Massot (Oct 02 2018 at 19:56):

It means non-constructive

Kenny Lau (Oct 02 2018 at 19:58):

eh, more details?

Johannes Hölzl (Oct 02 2018 at 19:59):

pure : A -> F A is usually the unit in a monad F. Sometimes its called return. Instances are the singleton list, finset, multiset, set. Or for tactics its the tactic returning a value.

Bryan Gin-ge Chen (Oct 02 2018 at 20:05):

deleted

Kenny Lau (Oct 02 2018 at 20:17):

So what would it be, in the context of topology?

Patrick Massot (Oct 02 2018 at 20:17):

the pure filter?

Patrick Massot (Oct 02 2018 at 20:17):

does it have type filter a?

Kenny Lau (Oct 02 2018 at 20:18):

yes

Kenny Lau (Oct 02 2018 at 20:19):

lemma pure_le_nhds : pure ≤ (nhds : α → filter α) :=
assume a, le_infi $ assume s, le_infi $ assume ⟨h₁, _⟩, principal_mono.mpr $
  singleton_subset_iff.2 h₁