# Zulip Chat Archive

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