exists data

Stream: general

[Johan Commelin]

Is there a clean way to avoid the , true in this condition?

def generate_sieve (c : covering_family U) : covering_family U :=
{ V : over U | ∃ (Ui : over U) (hUi : Ui ∈ c) (f : V ⟶ Ui), true }

I guess I should use nonempty? Somehow, that doesn't feel clean to me, and in the past I found it harder to use.

[Mario Carneiro]

that's nonempty

[Mario Carneiro]

{ V : over U | ∃ Ui ∈ c, nonempty (V ⟶ Ui) }

[Johan Commelin]

Ok, I'll try using it again.