2015-09-30 23:52:56 +00:00
|
|
|
|
{x : ℕ ∈ S | x > 0} : set ℕ
|
|
|
|
|
{x : ℕ ∈ s | x > 0} : finset ℕ
|
2015-10-14 01:35:16 +00:00
|
|
|
|
@set.sep.{1} nat (λ (x : nat), @gt.{1} nat 11.source.to.has_lt x 0) S : set.{1} nat
|
|
|
|
|
@finset.sep.{1} nat (λ (a b : nat), nat.has_decidable_eq a b) (λ (x : nat), @gt.{1} nat 11.source.to.has_lt x 0)
|
|
|
|
|
(λ (a : nat), nat.decidable_lt 0 a)
|
2015-08-17 01:21:29 +00:00
|
|
|
|
s :
|
|
|
|
|
finset.{1} nat
|