Documentation

Linglib.Core.Algebra.Order.Interval.Set.Instances

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.

source
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
Instances For
    source
    @[simp]
    theorem Set.Icc.coe_symm_eq {β : Type u_1} [Ring β] [PartialOrder β] [IsOrderedRing β] (t : ↑(Icc 0 1)) :
    ↑(symm t) = 1 - ↑t
    source
    @[simp]
    theorem Set.Icc.symm_symm {β : Type u_1} [Ring β] [PartialOrder β] [IsOrderedRing β] (t : ↑(Icc 0 1)) :
    symm (symm t) = t
    source
    @[simp]
    theorem Set.Icc.symm_zero {β : Type u_1} [Ring β] [PartialOrder β] [IsOrderedRing β] :
    symm 0 = 1
    source
    @[simp]
    theorem Set.Icc.symm_one {β : Type u_1} [Ring β] [PartialOrder β] [IsOrderedRing β] :
    symm 1 = 0
    source
    theorem Set.Icc.symm_involutive {β : Type u_1} [Ring β] [PartialOrder β] [IsOrderedRing β] :
    Function.Involutive symm
    source
    theorem Set.Icc.symm_bijective {β : Type u_1} [Ring β] [PartialOrder β] [IsOrderedRing β] :
    Function.Bijective symm
    source
    theorem Set.Icc.symm_inj {β : Type u_1} [Ring β] [PartialOrder β] [IsOrderedRing β] {s t : ↑(Icc 0 1)} :
    symm s = symm t ↔ s = t
    source
    theorem Set.Icc.symm_eq_one {β : Type u_1} [Ring β] [PartialOrder β] [IsOrderedRing β] {t : ↑(Icc 0 1)} :
    symm t = 1 ↔ t = 0
    source
    theorem Set.Icc.symm_eq_zero {β : Type u_1} [Ring β] [PartialOrder β] [IsOrderedRing β] {t : ↑(Icc 0 1)} :
    symm t = 0 ↔ t = 1
    source
    theorem Set.Icc.symm_le_symm {β : Type u_1} [Ring β] [PartialOrder β] [IsOrderedRing β] {s t : ↑(Icc 0 1)} :
    symm s ≤ symm t ↔ t ≤ s
    source
    theorem Set.Icc.le_symm_comm {β : Type u_1} [Ring β] [PartialOrder β] [IsOrderedRing β] {s t : ↑(Icc 0 1)} :
    s ≤ symm t ↔ t ≤ symm s
    source
    theorem Set.Icc.symm_le_comm {β : Type u_1} [Ring β] [PartialOrder β] [IsOrderedRing β] {s t : ↑(Icc 0 1)} :
    symm s ≤ t ↔ symm t ≤ s
    source
    theorem Set.Icc.symm_lt_symm {β : Type u_1} [Ring β] [PartialOrder β] [IsOrderedRing β] {s t : ↑(Icc 0 1)} :
    symm s < symm t ↔ t < s
    source
    theorem Set.Icc.lt_symm_comm {β : Type u_1} [Ring β] [PartialOrder β] [IsOrderedRing β] {s t : ↑(Icc 0 1)} :
    s < symm t ↔ t < symm s
    source
    theorem Set.Icc.symm_lt_comm {β : Type u_1} [Ring β] [PartialOrder β] [IsOrderedRing β] {s t : ↑(Icc 0 1)} :
    symm s < t ↔ symm t < s
    source
    theorem Set.Icc.strictAnti_symm {β : Type u_1} [Ring β] [PartialOrder β] [IsOrderedRing β] :
    StrictAnti symm
    source
    theorem Set.Icc.antitone_symm {β : Type u_1} [Ring β] [PartialOrder β] [IsOrderedRing β] :
    Antitone symm