## Stream: new members

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

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

#### Johan Commelin (Dec 14 2019 at 07:21):

What's the error you get?

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


#### Simon Hudon (Dec 14 2019 at 07:42):

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

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