Casting 1-p to a unit_interval real

Stream: general

[Ira Fesefeldt]

Hi! I am currently a bit lost.
I want to write a (noncomputable) function that maps to unit_interval. However, I need to use 1-p for p : unit_interval in that function. Since the unit_interval is not closed under subtraction, the expression is casted to a real. The library also does not seem to have a function for 1-p, just theorems stating that for p ∈ unit_interval we also have 1-p ∈ unit_interval.

Can I somehow cast (with a proof attached) 1-p to a unit_interval in order to use it in a function expecting a unit_interval as result?

[Siddharth Bhat]

Does this help?

https://leanprover-community.github.io/mathlib_docs/topology/unit_interval.html#unit_interval.mem_iff_one_sub_mem

[Floris van Doorn]

docs#unit_interval.symm

[Ira Fesefeldt]

Ohh... symm is exactly what I was looking for. Weird name. Thanks!

[Kevin Buzzard]

It's the obvious nontrivial symmetry!

[Eric Wieser]

Should it be has_compl.compl?

[Yaël Dillies]

Not in the current understanding of it, no.

[Yaël Dillies]

@Peter Nelson has an open PR to define lattices with involution. That would be the correct setting.