Zulip Chat Archive

Stream: new members

Topic: Is there a way to write dependent product of propositions?


view this post on Zulip YH (Dec 14 2019 at 07:18):

Something like
def square_root (a : ℝ) (ha : 0 ≤ a) : Σ (b : ℝ), (0 ≤ b) ∧ (b ^ 2 = a)

(I tried, won't allow me, seems like it only allows Σ over Types)

view this post on Zulip Johan Commelin (Dec 14 2019 at 07:21):

What's the error you get?

view this post on Zulip Johan Commelin (Dec 14 2019 at 07:22):

Do you want something like

def square_root (a : ) (ha : 0  a) : { (b : ) // (0  b)  (b ^ 2 = a) }

view this post on Zulip Simon Hudon (Dec 14 2019 at 07:42):

subtype (as pointed out by @Johan Commelin) and Σ' should do it

view this post on Zulip Kevin Buzzard (Dec 14 2019 at 07:45):

This { ... // ...} notation is for subtypes, which is one of the two ways Lean thinks about what mathematicians call subsets of a set. The difference between the term {x : real | x ^ 2 = 2} and the subtype {x : real // x ^ 2 = 2} is that one is a term and the other is a type, but they both express the idea of the collection of reals whose square is 2. To make a term of the subtype you need to provide a pair -- a real number, and a proof that its square is 2.


Last updated: May 17 2021 at 22:15 UTC