Zulip Chat Archive

Stream: general

Topic: pure


view this post on Zulip Kenny Lau (Oct 02 2018 at 19:56):

what is pure?

view this post on Zulip Patrick Massot (Oct 02 2018 at 19:56):

It means non-constructive

view this post on Zulip Kenny Lau (Oct 02 2018 at 19:58):

eh, more details?

view this post on Zulip 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.

view this post on Zulip Bryan Gin-ge Chen (Oct 02 2018 at 20:05):

deleted

view this post on Zulip Kenny Lau (Oct 02 2018 at 20:17):

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

view this post on Zulip Patrick Massot (Oct 02 2018 at 20:17):

the pure filter?

view this post on Zulip Patrick Massot (Oct 02 2018 at 20:17):

does it have type filter a?

view this post on Zulip Kenny Lau (Oct 02 2018 at 20:18):

yes

view this post on Zulip 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₁

view this post on Zulip Kenny Lau (Oct 02 2018 at 20:19):

maybe it doesn't

view this post on Zulip Kenny Lau (Oct 02 2018 at 20:19):

it has type α → filter α

view this post on Zulip Patrick Massot (Oct 02 2018 at 20:19):

Ok, pure x is the filter of all sets containing x

view this post on Zulip Kenny Lau (Oct 02 2018 at 20:20):

so it's just the principal filter?

view this post on Zulip Patrick Massot (Oct 02 2018 at 20:20):

yes

view this post on Zulip Patrick Massot (Oct 02 2018 at 20:20):

of the singleton x

view this post on Zulip Patrick Massot (Oct 02 2018 at 20:21):

it's more specialized than principal

view this post on Zulip Patrick Massot (Oct 02 2018 at 20:21):

Let me google this for you

view this post on Zulip Patrick Massot (Oct 02 2018 at 20:22):

https://github.com/leanprover/mathlib/blob/9a7a611c426c90f3894addba8a38cf4f9f3d8775/order/filter.lean#L632

view this post on Zulip Kevin Buzzard (Oct 03 2018 at 07:18):

Kenny did you read the stuff about monads in Programming In Lean? It is very accessible.


Last updated: May 08 2021 at 10:12 UTC