## Stream: general

#### Johan Commelin (Oct 01 2018 at 13:07):

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 (Oct 01 2018 at 13:08):

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 (Oct 01 2018 at 13:09):

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 (Oct 01 2018 at 14:42):

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

#### Johan Commelin (Oct 01 2018 at 14:44):

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 (Oct 01 2018 at 14:45):

Still feels like moving the problem around...

Last updated: May 08 2021 at 10:12 UTC