The unit-interval involution #
[UPSTREAM] additions to Mathlib.Algebra.Order.Interval.Set.Instances: the
involution 1 - t of Set.Icc (0 : β) 1 and its lemmas, stated at that file's
generality — generalizing unitInterval.symm beyond ℝ is its stated TODO.
Linglib uses Set.Icc (0 : ℚ) 1 as the home of gradient linguistic degrees
(at-issueness, projectivity, prior credence): mathlib's unitInterval is
real-valued and topological, while linguistic degrees are exact rationals.
The domain-facing names live with their owners (Discourse.AtIssueness).
instance
Set.Icc.instNeZeroElemOfNat_linglib
{β : Type u_1}
[Ring β]
[PartialOrder β]
[IsOrderedRing β]
[NeZero 1]
:
NeZero 1
def
Set.Icc.symm
{β : Type u_1}
[Ring β]
[PartialOrder β]
[IsOrderedRing β]
(t : ↑(Icc 0 1))
:
↑(Icc 0 1)
The involution 1 - t of the unit interval — unitInterval.symm at the
generality of this file's instances.
Equations
- Set.Icc.symm t = ⟨1 - ↑t, ⋯⟩
Instances For
@[simp]
theorem
Set.Icc.coe_symm_eq
{β : Type u_1}
[Ring β]
[PartialOrder β]
[IsOrderedRing β]
(t : ↑(Icc 0 1))
:
↑(symm t) = 1 - ↑t
@[simp]
theorem
Set.Icc.symm_symm
{β : Type u_1}
[Ring β]
[PartialOrder β]
[IsOrderedRing β]
(t : ↑(Icc 0 1))
:
theorem
Set.Icc.symm_involutive
{β : Type u_1}
[Ring β]
[PartialOrder β]
[IsOrderedRing β]
:
Function.Involutive symm
theorem
Set.Icc.symm_bijective
{β : Type u_1}
[Ring β]
[PartialOrder β]
[IsOrderedRing β]
:
Function.Bijective symm
theorem
Set.Icc.symm_inj
{β : Type u_1}
[Ring β]
[PartialOrder β]
[IsOrderedRing β]
{s t : ↑(Icc 0 1)}
:
theorem
Set.Icc.symm_eq_one
{β : Type u_1}
[Ring β]
[PartialOrder β]
[IsOrderedRing β]
{t : ↑(Icc 0 1)}
:
symm t = 1 ↔ t = 0
theorem
Set.Icc.symm_eq_zero
{β : Type u_1}
[Ring β]
[PartialOrder β]
[IsOrderedRing β]
{t : ↑(Icc 0 1)}
:
symm t = 0 ↔ t = 1
theorem
Set.Icc.symm_antitone
{β : Type u_1}
[Ring β]
[PartialOrder β]
[IsOrderedRing β]
:
Antitone symm