readable subquotients

Stream: general

[Johan Commelin]

So, let me return to my original question.

[Johan Commelin]

I've got

definition Spa (A : Huber_pair) : set (Spv A) :=
Spv.lift (λ v, v.is_continuous ∧ ∀ r, r ∈ A⁺ → v.val.val r ≤ 1)
(λ v₁ v₂ heq, sorry)

-- fake
definition Spa' (A : Huber_pair) : set (Spv A) :=
{v : Spv A | v.is_continuous ∧ ∀ r, r ∈ A⁺ → v.val.val r ≤ 1}
which_is_well_defined (λ v₁ v₂ heq, sorry)

[Johan Commelin]

Maybe it is really minor to people who have seen Lean for 367 days in the last year, but I think Spa' is a lot more readable than Spa.

[Johan Commelin]

Of course any mathematician who takes a first look is already brain-blocked by set (Spv A), which means "subset" instead of "set". But never mind...

[Kevin Buzzard]

Can't you put the work into the definition of v.is_continuous?

[Johan Commelin]

I'm not sure if that would help. Or do you mean that you want to define Spa as intersection of two subsets? Namely Cont and the other condition.

[Johan Commelin]

Still feels like moving the problem around...